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
