# 「软件基础 - PLF」 17. Tactic Library For Coq: A Gentle Introduction

Posted by Hux on March 17, 2019
1
From PLF Require Import LibTactics.


LibTactics vs. SSReflect (another tactics package)

• for PL vs. for math

## 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

### 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