coq
1.函数作为返回值。
使用场合
Definition constfun {X: Type} (x: X) : nat->X :=
fun (k:nat) => x.
因为constfun的返回值是nat->X.所以需要一个函数作为其返回值。
例子：
Definition override {X: Type} (f: nat->X) (k:nat) (x:X) : nat->X:=
fun (k':nat) => if beq_nat k k' then x else f k'.
2.apply
1.当要求的目标和已知条件或者已经证明的引理一样时，可以使用apply。
2.当apply的是一个蕴含式，则这个式子的前提会被纳入要证明的子目标中。使用apply，coq会进行自动匹配。
注意:使用apply时，如果等式左右交换的，此时apply不起作用。要使用symmetry来交换左右。
3.inversion.
coq中不同的构造因子是不想交的。
如：
Inductive nat : Type :=
| O : nat
| S : nat -> nat.
中O永远都不会等于任何S n或者n。
假设H是一个前文的假设或者一个已经证明的引理。
c a1 a2 a3……am = d b1 b2 b3……bm
对于某个构造因子和参数[a1 a2 a3 ……am],[b1 b2 b3……bm]。
inversion H指导coq去颠倒这个等式，从而获取信息。
（1） 如果c = d。。那么有事实：a1 = b1……
（2）如果c不等于d。那么说明这个假设或者前文引理是矛盾的。coq会把当前要证的目标标记为已证（证明它是错误的）。
4.在假设中使用apply和对目标使用apply是不同的。
如果L是：L1->L2。那么使用apply L。在L2与目标匹配的时候，让L1成为子目标。（后退）
使用apply L in H。是匹配H和L1，如果匹配，那么使用L2作为H.（前进）
5.destruct 可以用来分析一些变量的值，也可以用来分析一些表达式的结果。
Theorem sillyfun_false : forall (n : nat),
sillyfun n = false.
Proof.
intros n. unfold sillyfun.
destruct (beq_nat n 3).
Case "beq_nat n 3 = true". reflexivity.
Case "beq_nat n 3 = false". destruct (beq_nat n 5).
SCase "beq_nat n 5 = true". reflexivity.
SCase "beq_nat n 5 = false". reflexivity. Qed.
6.remember
因为destruct 表达式时会把所有匹配的地方都进行替换。这样会损失表达式中的信息。
remember (beq_nat n 5) as e5.
destruct e5.
之后可以从e5中获得beq_nat n 5这个信息。
7.apply with
Theorem trans_eq : forall {X:Type} (n m o : X),
n = m -> m = o -> n = o.
m作为一个中间变量。实现了传递性。
要证：
Example trans_eq_example' : forall (a b c d e f : nat),
[a,b] = [c,d] ->
[c,d] = [e,f] ->
[a,b] = [e,f].
时，把[c,d]看做m即可得证。
apply trans_eq with (m:=[c,d]). apply eq1. apply eq2. Qed.
其中m可以省略不写。写成 apply trans_eq with [c,d]即可。
已经学到的：
Here are the ones we've seen:
- [intros]:
move hypotheses/variables from goal to context
- [reflexivity]:
finish the proof (when the goal looks like [e = e])
- [apply]:
prove goal using a hypothesis, lemma, or constructor
- [apply... in H]:
apply a hypothesis, lemma, or constructor to a hypothesis in
the context (forward reasoning)
- [apply... with...]:
explicitly specify values for variables that cannot be
determined by pattern matching
明确指定值的变量，可以不通过模式匹配确定
- [simpl]:
simplify computations in the goal
- [simpl in H]:
... or a hypothesis
- [rewrite]:
use an equality hypothesis (or lemma) to rewrite the goal
- [rewrite ... in H]:
... or a hypothesis
- [symmetry]:
changes a goal of the form [t=u] into [u=t]
- [symmetry in H]:
changes a hypothesis of the form [t=u] into [u=t]
- [unfold]:
replace a defined constant by its right-hand side in the goal
- [unfold... in H]:
... or a hypothesis
- [destruct... as...]:
case analysis on values of inductively defined types
- [induction... as...]:
induction on values of inductively defined types
- [inversion]:
reason by injectivity and distinctness of constructors
- [remember (e) as x]:
give a name ([x]) to an expression ([e]) so that we can
destruct [x] without "losing" [e]
- [assert (e) as H]:
introduce a "local lemma" [e] and call it [H]
*)