「SF-PLF」17 UseTactics
Pin Young Lv9
  2021-03-28 00:00:00 2021-03-28 00:00   2023-02-02 13:37:47   238 字  1 分钟  
1
From PLF Require Import LibTactics.

LibTactics vs. SSReflect (another tactics package)

  • for PL vs. for math
  • traditional vs. rethinks..so harder

Tactics for Naming and Performing Inversion

introv

1
2
3
4
5
6
Theorem ceval_deterministic: ∀c st st1 st2,
  st =[ c ]⇒ st1 →
  st =[ c ]⇒ st2 →
  st1 = st2.
intros c st st1 st2 E1 E2. (* 以往如果想给 Hypo 命名必须说全 *)
introv E1 E2.              (* 现在可以忽略 forall 的部分 *)

inverts

1
2
3
4
5
6
7
8
(* was... 需要 subst, clear *)
- inversion H. subst. inversion H2. subst. 
(* now... *)
- inverts H. inverts H2. 


(* 可以把 invert 出来的东西放在 goal 的位置让你自己用 intro 命名！*)
inverts E2 as.

Tactics for N-ary Connectives

Because Coq encodes conjunctions and disjunctions using binary constructors ∧ and ∨…
to work with a N-ary logical connectives…

splits

n-ary conjunction

n-ary split

branch

n-ary disjunction

faster destruct?

Tactics for Working with Equality

asserts_rewrite and cuts_rewrite

substs

better subst - not fail on circular eq

fequals

vs f_equal?

applys_eq

variant of eapply

Some Convenient Shorthands

unfolds

better unfold

false and tryfalse

better exfalso

gen

shorthand for generalize dependent, multiple arg.

1
2
3
4
5
6
(* old *)
intros Gamma x U v t S Htypt Htypv.
generalize dependent S. generalize dependent Gamma.
 
(* new...so nice!!! *)
introv Htypt Htypv. gen S Gamma.

admits, admit_rewrite and admit_goal

wrappers around admit

sort

proof context more readable

vars -> top
hypotheses -> bottom

Tactics for Advanced Lemma Instantiation

Working on lets

Working on applys, forwards and specializes

  • 本文标题：「SF-PLF」17 UseTactics
  • 本文作者：Pin Young
  • 创建时间：2021-03-28 00:00:00
  • 本文链接：posts/5700.html
  • 版权声明：本博客所有文章除特别声明外，均采用 BY-NC-SA 许可协议。转载请注明出处！
  1. 1. Tactics for Naming and Performing Inversion
    1. 1.1. introv
    2. 1.2. inverts
  2. 2. Tactics for N-ary Connectives
    1. 2.1. splits
    2. 2.2. branch
  3. 3. Tactics for Working with Equality
    1. 3.1. asserts_rewrite and cuts_rewrite
    2. 3.2. substs
    3. 3.3. fequals
    4. 3.4. applys_eq
  4. 4. Some Convenient Shorthands
    1. 4.1. unfolds
    2. 4.2. false and tryfalse
    3. 4.3. gen
    4. 4.4. admits, admit_rewrite and admit_goal
    5. 4.5. sort
  5. 5. Tactics for Advanced Lemma Instantiation
    1. 5.1. Working on lets
    2. 5.2. Working on applys, forwards and specializes