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（以及任何依赖它的东西） 从上下文中移回目标公式内的前提中