Coq学习——《Software-Foundation》Volume1.5-Tactics

Tactics

More tactics and more properties of functional programs.

  • how to use auxiliary lemmas in both “forward-“ and “backward-style” proofs; “正推”“逆推”中使用辅助引理;
  • how to reason about data constructors — in particular, how to use the fact that they are injective and disjoint; 如何对数据构造子进行论证,特别是,如何利用它们单射且不交的事实;
  • how to strengthen an induction hypothesis, and when such strengthening is required; 如何增强归纳假设,以及何时需要增强;
  • more details on how to reason by case analysis. 还有通过分类讨论进行论证的更多细节。

The [apply] Tactic

The goal to be proved is the same as some hypothesis in the context or some proved lemma, so we can apply them to finish the proof.

Finish with [apply H.] instead of [rewrite H. reflexivity.]

直接应用某条定理,而非重写后用 reflexivity.

1
2
3
4
5
6
7
Theorem silly2 : forall (n m o p : nat),
n = m ->
(n = m -> [n;o] = [m;p]) ->
[n;o] = [m;p].
Proof.
intros n m o p eq1 eq2.
apply eq2. apply eq1. Qed.

When we [apply] some statements with $\forall$, Coq will try to find appropriate values.

当我们应用 apply 定理的时候,Coq 会自动找寻符合定理的值,以下面为例:

1
2
3
4
5
6
7
8
9
10
11
12
Theorem silly_ex :
(forall n, evenb n = true -> oddb (S n) = true) ->
evenb 2 = true ->
oddb 3 = true.
Proof.
intros.
(* If we don't use apply tactic *)
(* rewrite -> H. reflexivity. *)
(* rewrite -> H0. reflexivity. *)
apply H.
apply H0.
Qed.

这里我们使用 [apply H.] Coq 找到 [n=2]的实例,符合[H]定理要求,所以我们将结论转换为前提。

The [apply with] Tactic

Proof the theorem trans_eq first, and proof by using [apply trans_eq with (m:=[c;d])] (gives an instantiation of [X]). Trans_eq use abstract type so we can “with” the actual type.

Coq also has a tactic [transitivity] that accomplishes the same purpose as applying [trans_eq]. The tactic requires us to state the instantiation we want, just like [apply with] does.

Like:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
Example trans_eq_example' : forall (a b c d e f : nat),
[a;b] = [c;d] ->
[c;d] = [e;f] ->
[a;b] = [e;f].
Proof.
intros a b c d e f eq1 eq2.

(** If we simply tell Coq [apply trans_eq] at this point, it can
tell (by matching the goal against the conclusion of the lemma)
that it should instantiate [X] with [[nat]], [n] with [[a,b]], and
[o] with [[e,f]]. However, the matching process doesn't determine
an instantiation for [m]: we have to supply one explicitly by
adding "[with (m:=[c,d])]" to the invocation of [apply]. *)

apply trans_eq with (m:=[c;d]).
apply eq1. apply eq2. Qed.

Example trans_eq_example'' : forall (a b c d e f : nat),
[a;b] = [c;d] ->
[c;d] = [e;f] ->
[a;b] = [e;f].
Proof.
intros a b c d e f eq1 eq2.
transitivity [c;d].
apply eq1. apply eq2. Qed.

The [injection] and [discriminate] Tactics

举自然数定义,性质:

  • 构造子$S$是单射(Injective) 或“一一对应”的。即,如果$S n = S m$,那么$n=m$必定成立。
  • 构造子$O$和$S$是不相交(Disjoint)的。即,对于任何$n$,$O$都不等于$S n$

可以用pred 推广到任意构造子上,编写撤销一次构造子调用的函数。为此,Coq 提供了更加简便的[injection] 策略,它能让我们利用构造子的单射性。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
Theorem S_injective' : forall (n m : nat),
S n = S m ->
n = m.
Proof.
intros n m H.

(** By writing [injection H as Hmn] at this point, we are asking Coq
to generate all equations that it can infer from [H] using the
injectivity of constructors (in the present example, the equation
[n = m]). Each such equation is added as a hypothesis (with the
name [Hmn] in this case) into the context. *)

injection H as Hnm. apply Hnm.
Qed.

If you jest say [injection XX] with no [as] clause, then all the equations will be turned into hypotheses at the beginning of the goal. (We can follow with [intros] tactics).

one exercise

1
2
3
4
5
6
7
8
9
10
11
12
13
Example injection_ex3 : forall (X : Type) (x y z : X) (l j : list X),
x :: y :: l = z :: j ->
j = z :: l ->
x = y.
Proof.
intros.
(* Yes, you can write a graph yourself and you will find the head ele will be the same (x = z) and the rest of list, due to the constructor of the list *)
injection H.
intros.
assert (H': z::l = y::l). { rewrite H1. symmetry. apply H0. }
- injection H' as Hinj.
rewrite H2. apply Hinj.
Qed.

About disjointnesses.

Two terms beginning with different constructors (like [0] ans [S], or [true] and [false]) can never be equal.

Nonsensial to anything: Beginning with different constructors, any time we find ourselves in a context where we’ve _assumed_ that two such terms are equal, we are justified in concluding anything we want.

The [discriminate] tactic embodies this principle: It is used on a hypothesis involving an equality between different constructors.

逻辑学原理“爆炸原理”,断言矛盾的前提会推出任何东西,甚至是假命题。

Example

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
Theorem eqb_0_l : forall n,
0 =? n = true -> n = 0.
Proof.
intros n.

(** We can proceed by case analysis on [n]. The first case is
trivial. *)

destruct n as [| n'] eqn:E.
- (* n = 0 *)
intros H. reflexivity.

(** However, the second one doesn't look so simple: assuming [0
=? (S n') = true], we must show [S n' = 0]! The way forward is to
observe that the assumption itself is nonsensical: *)

- (* n = S n' *)
simpl.

(** If we use [discriminate] on this hypothesis, Coq confirms
that the subgoal we are working on is impossible and removes it
from further consideration. *)

intros H. discriminate H.
Qed.

The injectivity (one to one) allows us to use [f_equal] tactic to reason form like [n = m -> f x = f y].

Given a goal of the form [f a1 … an = g b1 … bn], the tactic [f_equal] will produce subgoals of the form [f = g], [a1 = b1], …, [an = bn]. At the same time, any of these subgoals that are simple enough (e.g., immediately provable by [reflexivity]) will be automatically discharged by [f_equal].

Using Tactics on Hypotheses

Change the goal -> change the context.

For example, [simple in H], [apply L in H].

! [apply L in H]会针对 $X$ 匹配 $H$,如果成功,就将其替换为 $Y$ 。换言之,

  • [apply L in H] 给了我们一种“正向推理(forward reasoning)” :
    • 根据 $X \rightarrow Y$ 和一个匹配 $X$ 的假设, 它会产生一个匹配 $Y$ 的假设。
    • Forward reasoning starts from what is _given_ (premises, previously proven theorems) and iteratively draws conclusions from them until the goal is reached
  • [apply L]是一种“反向推理”:
    • 如果我们指导 $X \rightarrow Y$ 并且试图证明 $Y$, 那么证明 $X$ 就足够了。
    • Backward reasoning starts from
      the _goal_ and iteratively reasons about what would imply the goal, until premises or previously proven theorems are reached.

数学或计算机科学课上见过的非形式化证明(informal proofs)可能倾向于正向推理。通常,Coq 习惯上倾向于使用反向推理,但在某些情况下,正向推理更易于思考。

Varying the Induction Hypothesis

变换归纳假设

[intros m] in the wrong places.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
(* Failed Proof *)
Theorem double_injective_FAILED : forall n m,
double n = double m ->
n = m.
Proof.
intros n m. induction n as [| n' IHn'].
- (* n = O *) simpl. intros eq. destruct m as [| m'] eqn:E.
+ (* m = O *) reflexivity.
+ (* m = S m' *) discriminate eq.
- (* n = S n' *) intros eq. destruct m as [| m'] eqn:E.
+ (* m = O *) discriminate eq.
+ (* m = S m' *) apply f_equal.

(** At this point, the induction hypothesis ([IHn']) does _not_ give us
[n' = m'] -- there is an extra [S] in the way -- so the goal is
not provable. *)

Abort.

分析问题,由于我们已经通过[intros] 将 [m] 引入到上下文中。直观上我们告诉 Coq“现在开始考虑具体的[n]和[m]”,而在对[n]归纳证明时,[P n -> P ( S n )],对于具体[m]来说是没有意义的(useless)。

我们需求证明更一般的事情,(在后面才具体化[m])。

1
2
3
4
5
6
7
8
1 subgoal (ID 282)

n', m, m' : nat
E : m = S m'
IHn' : double n' = double (S m') -> n' = S m'
eq : double (S n') = double (S m')
============================
S n' = S m'

What’s wrong in the second-second case.

Trying to carry out this proof by induction on [n] when [m] is already in the context doesn’t work because we are then trying to prove a statement involving _every_ [n] but just a _single_ [m].

如果我们试着根据 Q 证明 R,就会以“假设 double (S n) = 10..”这样的句子开始, 不过之后我们就会卡住:知道 double (S n) 为 10 并不能告诉我们 double n 是否为 10。(实际上,它强烈地表示 double n ‘不是’ 10!) 因此 Q 是没有用的。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
(* Successful Proof *)
Theorem double_injective : forall n m,
double n = double m ->
n = m.
Proof.
intros n. induction n as [| n' IHn'].
- (* n = O *) simpl. intros m eq. destruct m as [| m'] eqn:E.
+ (* m = O *) reflexivity.
+ (* m = S m' *) discriminate eq.

- (* n = S n' *) simpl.

(** Notice that both the goal and the induction hypothesis are
different this time: the goal asks us to prove something more
general (i.e., to prove the statement for _every_ [m]), but the IH
is correspondingly more flexible, allowing us to choose whichever
[m] we like when we apply the IH. *)

intros m eq.

(** Now we've chosen a particular [m] and introduced the assumption
that [double n = double m]. Since we are doing a case analysis on
[n], we also need a case analysis on [m] to keep the two "in sync." *)

destruct m as [| m'] eqn:E.
+ (* m = O *)

(** The 0 case is trivial: *)

discriminate eq.
+ (* m = S m' *)
apply f_equal.

(** At this point, since we are in the second branch of the [destruct
m], the [m'] mentioned in the context is the predecessor of the
branch of the induction, this is perfect: if we instantiate the
[m] we started out talking about. Since we are also in the [S]
generic [m] in the IH with the current [m'] (this instantiation is
performed automatically by the [apply] in the next step), then
[IHn'] gives us exactly what we need to finish the proof. *)

apply IHn'. simpl in eq. injection eq as goal. apply goal. Qed.

We get a more general context.

1
2
3
4
5
6
7
8
9
1 subgoal (ID 286)

n' : nat
IHn' : forall m : nat, double n' = double m -> n' = m
m, m' : nat
E : m = S m'
eq : S (S (double n')) = double (S m')
============================
S n' = S m'

What you should take away from all this is that we need to be careful, when using induction, that we are not trying to prove something too specific: When proving a property involving two variables [n] and [m] by induction on [n], it is sometimes crucial to leave [m] generic.

One of my exercises.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
Theorem eqb_true : forall n m,
n =? m = true -> n = m.
Proof.
intros n.
induction n as [| n' IHn'].
- intros. destruct m as [| m'].
+ reflexivity.
+ simpl in H. discriminate H.
- intros. destruct m as [| m'].
+ simpl in H. discriminate H.
+ simpl in H.
(* We apply IHn' in H. Forward reasonning. *)
apply IHn' in H.
rewrite H.
reflexivity.
Qed.

Another

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
Theorem plus_n_n_injective : forall n m,
n + n = m + m ->
n = m.
Proof.
(* Hint: use [plus_n_Sm] *)
intros n.
induction n as [| n' IHn'].
- intros. destruct m as [| m'].
+ reflexivity.
+ simpl in H. discriminate H.
- destruct m as [| m'].
+ intros. discriminate H.
+ intros. simpl in H.
Check plus_n_Sm.
Search (S ( _ + _ ) ).
rewrite <- plus_n_Sm in H.
rewrite <- plus_n_Sm in H.
(* Use injection property *)
injection H as IHinj.
(* Now we can apply IHn' in IHinj with specific m ( that is m') *)
apply IHn' in IHinj.
Search ( ?a = ?b -> S ?a = S ?b).
(* As a backward reasoning, we could rewrite the goal with IHinj and *)
rewrite IHinj.
reflexivity.
(* As a forward reasoning, I search the existing therom and make S n' = S m' *)
(* apply eq_S in IHinj. *)
(* apply IHinj. *)
Qed.
(** [] *)

Rearrangement of quantified variables

有时候需要对量化的变量做一下“重排”。

比如之前的double_injective的证明,如果我们不引入任何东西就执行[induction m], Coq 就会自动帮我们引入 n。

What can we do?

  • works but not nice: rewrite the statement of the lemma so that [m] is quantified before [n].
  • work and nice: first intro duce all and then _re-generalize_ one or more with tactic [generalize dependent].

An exercise

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
Theorem nth_error_after_last: forall (n : nat) (X : Type) (l : list X),
length l = n ->
nth_error l n = None.
Proof.
(* Prove by induction on [l] *)
intros n X l.
generalize dependent n.
generalize dependent X.
induction l as [| hd' l' IHl'].
- simpl. reflexivity.
- destruct n.
+ simpl. intros. discriminate H.
+ simpl. intros. injection H as IHinj.
apply IHl' in IHinj. apply IHinj.
Qed.

Unfolding Definitions

Manually unfold a name that has been introduced by a [Definition].

As for automatic unfolding (with tactic [simpl]), Coq is not smart enough…

Use [unfold] to explicitly tell Coq what to do.

1
2
3
4
5
6
7
8
9
10
11
12
13
Fact silly_fact_2' : forall m, bar m + 1 = bar (m + 1) + 1.
Proof.
intros m.
unfold bar.

(** Now it is apparent that we are stuck on the [match] expressions on
both sides of the [=], and we can use [destruct] to finish the
proof without thinking too hard. *)

destruct m eqn:E.
- reflexivity.
- reflexivity.
Qed.

As for automatic unfolding the definition, if [simpl] meet a function involving a pattern match with an application of an variable. It is not smart enough to notice whether the two branches of are identical or not.

Two ways to make progress

  • Destruct the variable (depends on recognizing the dependencis)
  • Tell Coq to unfold the function and show directly, and then …

Using [destruct] on Compound Expressions

We have used this for the case analysis before.

About the [eqn:]!

When [destruct]ing compound expressions, the information recorded by the [eqn:] can actually be critical: if we leave it out, then [destruct] can erase information we need to complete a proof.

So becareful to add [eqn:] when destructing compound expressions.

exercise

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
Theorem bool_fn_applied_thrice :
forall (f : bool -> bool) (b : bool),
f (f (f b)) = f b.
Proof.
intros f b.
destruct (b) eqn:Heq1.
- destruct (f true) eqn:Heq2.
+ rewrite Heq2. rewrite Heq2. reflexivity.
+ destruct (f false) eqn:Heq3.
* apply Heq2.
* apply Heq3.
- destruct (f false) eqn:Heq2.
+ destruct (f true) eqn:Heq3.
* apply Heq3.
* apply Heq2.
+ rewrite Heq2. apply Heq2.
Qed.

Review

Review 部分摘录翻译版。

  • intros:将前提/变量从证明目标移到上下文中
  • reflexivity:(当目标形如 e = e 时)结束证明
  • apply:用前提、引理或构造子证明目标
  • apply... in H:将前提、引理或构造子应用到上下文中的假设上(正向推理)
  • apply... with...:为无法被模式匹配确定的变量显式指定值
  • simpl:化简目标中的计算
  • simpl in H:化简前提中的计算
  • rewrite:使用相等关系假设(或引理)来改写目标
  • rewrite ... in H:使用相等关系假设(或引理)来改写前提
  • symmetry:将形如 t=u 的目标改为 u=t
  • symmetry in H:将形如 t=u 的前提改为 u=t
  • unfold:用目标中的右式替换定义的常量
  • unfold... in H:用前提中的右式替换定义的常量
  • destruct... as...:对归纳定义类型的值进行情况分析
  • destruct... eqn:...:为添加到上下文中的等式指定名字, 记录情况分析的结果
  • induction... as...: 对归纳定义类型的值进行归纳
  • injection: reason by injectivity on equalities between values of inductively defined types
  • discriminate: reason by disjointness of constructors on equalities between values of inductively defined types
  • assert (H: e)(或 assert (e) as H):引入“局部引理”e 并称之为 H
  • generalize dependent x:将变量 x(以及任何依赖它的东西) 从上下文中移回目标公式内的前提中