Software Foundation 做题的 Notes

发表于 |

https://github.com/CalvinNeo/SF-zh 做题笔记。

Basic

intro 和 intros 会按顺序将命题中的 forall 里面的，和 -> 左边的按照顺序移动下来作为假设。

reflexivity 相当于是化简等号两边，看是否相等。

rewrite -> H 是用 H 改写 goal 右边的部分，可以被简写为 rewrite H。rewrite <- H 则是从右到左改写。

有个证明 andb b c = true -> c = true 的看起来挺奇怪的，但实际上后面可以用 discriminate 来证明。

Induction

Coq 中 induction 的归纳，不是数学归纳，而是根据构造函数归纳。比如皮亚诺自然数就有两个构造函数 S 和 O。

Lists

Poly

一般证明一些结论，用到 induction 的时候，会用某个操作符对某个操作符的分配率。

1
2
plus_n_Sm: forall n m : nat, S (n + m) = n + S m
plus_Sn_m: forall n m : nat, S n + m = S (n + m)

其目的是用分配率，把“递推”条件里面的部分给拆掉，一部分用 IHl' 直接 apply 过去，剩下来一部分是比较简单处理的。
对 list 而言，就是证明各种函数，如 length、rev 和 ++ 之间的关系。

Tactic

这里 apply eq2. apply eq1 好像三段论一样，eq2 是大前提，eq1 是小前提。

apply 类似于反过来推。apply H，如果 H 是 x = y，则可以进行代入的改写，这不是很直观。但如果 H 是 x -> y 这样，就可以将 y 这样的 goal 改写成 x，这就类似于是倒推了。
要使用 apply 策略，被应用的事实（的结论）必须精确地匹配证明目标。甚至等号反一下都不行，需要 symmetry 倒过来。
apply x in H 类似于正过来推。它是把 x 应用到假设 H 而不是 goal 上。具体来说，[apply L in H] 会针对上下文中的假设 [H] 匹配某些形如 [X -> Y] 的条件语句 [L]。[apply L in H] 会针对 [X] 匹配 [H]，如果成功，就将其替换为 [Y]。简而言之，就还是用 L 改写，但是改写 H 了。

同理，simpl in H 也是简化假设 H 而不是 goal。同理，也有 rewrite ... in H 来改写前提。

apply x with (m:=xxx)，也就是帮助 apply 选择把 m 代成是什么。这里我不太清楚如果有多个 forall 如何逐个指定。但另外有一种方式是 pose proof。

injection 是利用单射的性质。能方便的证明 S n = S m -> n = m 这样的命题。在 evSS_ev_remember 中也能看到有使用处理 S (S n') = S (S n)。主要目的还是用来去掉包在外面的上下文。
通过编写 injection H as Hmn1 Hmn2 这样，我们让 Coq 利用构造子的单射性来产生所有它能从 H 所推出的等式。 每一个这样的等式都作为假设被添加到上下文中。

discriminate 用来处理 False -> P 这样的问题。也就是后面提到的 ex_falso_quodlibet，爆炸原理。

plus_n_n_injective 的证明很 tricky，我有几种方式都不太证得了，不知道为啥。

eqb_true 里面 intros [] eq 和 intros m eq 是有区别的。

intros 有个问题是，它始终是按照顺序引入的。如果我 intros n m，但我只想对 m 归纳，继续 forall n，那就需要 generalize dependent n 这样把 n 再还回去。
intros 另一个问题是，如果多引入了假设，或者少引入了假设，会导致后面处理会比较奇怪。所以一般直接 intros，看自己要用哪些。

用 unfold 展开定义。同理也有 unfold... in H。类似的展开方法还有 destruct。如 silly_fact_2 中举的例子一样，可以用 destruct 把用 match 讨论的 bar 函数的各个构造函数 destruct 出来讨论。

可以使用 destruct (n =? 3) eqn:E1 这样对表达式的结果进行讨论。

本文中最后总结了已有的一些策略。

一些 case

split 可以使用 match 做一个单 arm 的 destruct。

1
2
3
4
5
6
7
8
9
10
Theorem combine_split : forall X Y (l : list (X * Y)) l1 l2,
  split l = (l1, l2) ->
  combine l1 l2 = l.
Proof.
  intros tx ty l.
  induction l as [| h t IH].
  - simpl. intros l1 l2 H. simpl in H. inversion H. reflexivity.
  - intros r1 r2 H.
    destruct h.
    destruct (split t) eqn: E.

下面就引入了多余的 n'

1
2
3
4
5
6
7
8
9
10
Theorem mult_assoc : forall n m p : nat,
  n * (m * p) = (n * m) * p.
Proof.
  intros n.
  induction n as [| n' IHn] eqn: eq1.
  - reflexivity.
  - simpl. intros m p.
    assert (H3: (m + n' * m) * p = m * p + n' * m * p).
    apply mult_plus_distr_r.
    rewrite H3.

Logic

本章开始提到了之前证明了很多 a = b、a -> b 和 forall x, P x 的命题。
表达式 n = m 只是 eq n m 的语法糖（它使用 Notation 机制定义在 Coq 标准库中）。由于 eq 可被用于任何类型的元素，因此它也是多态的。

遇到 \/ 作为条件，可以 destruct H as [H1 | H2]，产生两个 subgoal。然后用 bullet 去讨论。也可以直接 intros [H1 | H2] 甚至 intros [H | H]。
遇到 \/ 作为 goal，可以用 left 或者 right 选择要证明哪一边。
遇到 /\ 作为条件，可以用 destruct 分离成两个条件。
遇到 /\ 作为 goal，需要用 split 将它分开成两个 subgoal，用 bullet 组织。

在 ex_falso_quodlibet 的证明中，会发现有的时候 False 出现在条件中，这个时候只需要 destruct 这个条件就可以了。如 destruct contra。

1
2
3
4
5
1 goal
P : Prop
contra : False
______________________________________(1/1)
P

如果在条件中出现 P -> False，但 goal 是 P，则可以使用 exfalso。我感觉好像他的作用是把 goal 变成 False。

一个诸如 H : exists x : A, f x = y /\ In x t 这样的条件，可以被 destruct 为 [w [h1 h2]] 这样。此时 w 就是这个 x。可以直接假设 exists w。

对于后面的排中律系列，在 (P \/ P -> False) 时，建议选择 right，因为 right 会得到一个 P 的假设。

注意
1.P : Prop means “let P be an arbitrary proposition”. It could be true, it could be false.
2.p : P means “let p be a proof of P”. That’s what means that P is true.

对映

我们可以通过以下两种方式来断言 n 为偶数：
evenb n 求值为 true

1
Example even_42_bool : evenb 42 = true.

或者存在某个 k 使得 n = double k

1
Example even_42_prop : even 42.

解释了之前为什么要证明一个很奇怪的什么 eqb_true 的东西。

1
2
3
4
5
6
7
8
9
10
11
Theorem eqb_true : forall n m,
    n =? m = true -> n = m.
Proof.
intro n. induction n as [| n' IHn'].
  - intro m. induction m as [| m' IHm'].
    + reflexivity.
    + discriminate.
  - intros m eq. induction m as [| m' IHm'].
    + simpl. discriminate.
    + apply f_equal. apply IHn'. apply eq.
Qed.

一些 case

In_map_iff 的思路是考虑 H 的话，如果 y = x 则是另外的情况，否则 y 在 l 里面。就可以 destruct 出来，一部分匹配 IHl。
另外，下面的 intros [H | H] 的意思是把 f h = y \/ In y (map f t) -> 引入，但生成两个 subgoal。第一个 goal 是对 f h = y 证明成立，第二个是对 In y (map f t) 成立。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
Lemma In_map_iff :
  forall (A B : Type) (f : A -> B) (l : list A) (y : B),
    In y (map f l) <->
    exists x, f x = y /\ In x l.
Proof.
  intros A B f l y. split.
  induction l as [| h t IHl].
  - simpl. intros. destruct H.
  (* In y (map f (h :: t)) -> exists x : A, f x = y /\ In x (h :: t) *)
  - simpl. intros [H | H].
    + exists h. simpl. split.
      * apply H.
      * left. reflexivity.
    (* f x != y *)
    + apply IHl in H. destruct H as [w [h1 h2]].
      (* now H is useable *)
      exists w. split.
      * apply h1.
      * right. apply h2.
  (* (exists x : A, f x = y /\ In x l) -> In y (map f l) *)
  - intros [w [h1 h2]].
    rewrite <- h1. apply In_map. exact h2.
Qed.

另外，下面这个目标中的 x = x 如何被 simpl 掉？似乎没办法执行。

1
2
3
4
5
6
7
8
9
10
11
12
Lemma In_map_iff2 :
  forall (A B : Type) (f : A -> B) (l : list A) (y : B),
    In y (map f l) <->
    exists x, f x = y /\ In x l.
Proof.
  intros A B f l y. split.
    induction l.
    - simpl. intros. destruct H.
    - intros. simpl. exists x. split.
      destruct H. apply H. apply IHl in H.
      + admit.
      + simpl.

对应的 goal 如下

1
2
3
4
5
6
7
8
9
10
11
1 goal
A : Type
B : Type
f : A -> B
x : A
l : list A
y : B
IHl : In y (map f l) -> exists x : A, f x = y /\ In x l
H : In y (map f (x :: l))
______________________________________(1/1)
f x = y /\ (x = x \/ In x l)

下面这里的 apply H 我觉得比较有意思。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
Theorem excluded_middle_2_double_negation_elimination :
  excluded_middle <-> double_negation_elimination.
Proof.
  split.
  - unfold excluded_middle.
    unfold double_negation_elimination.
    unfold not.
    intros.
    destruct (H P).
    + apply H1.
    + exfalso. apply H1. apply H0 in H1. destruct H1.
  - unfold excluded_middle.
    unfold double_negation_elimination.
    unfold not.
    intros.
    (* Get rid of forall *)
    apply H.
    intros.
    apply H0.
    right. intros. apply H0. left. apply H1.
Qed.

当时的 goal 是

1
2
3
4
5
1 goal
H : forall P : Prop, ((P -> False) -> False) -> P
P : Prop
______________________________________(1/1)
P \/ (P -> False)

容易想到的是 left 或者 right 这样。但会陷入循环。比如我 left. apply H. apply H. apply H0. apply H.，最终是回到了最初的起点了。但是 apply H 完了之后，就得到

1
(P \/ (P -> False) -> False) -> False

如果我 right. apply H. intros. apply H0. intros. apply H in H1. 就会得到如下的形式。我们不能 apply H in H1，因为这会得到什么呢？注意，这里是前向 apply 了，我们用 P 代换得不到sm东西。

1
2
3
4
5
6
7
1 goal
H : forall P : Prop, ((P -> False) -> False) -> P
P : Prop
H0 : (P -> False) -> False
H1 : P
______________________________________(1/1)
False

这个应该是用 ((P -> False) -> False) 代换了原来 goal 中的两处 P，然后再利用各种结合率啥的重新组合得到的。所以我觉得如果有 forall P : Prop, … -> P 这样的东西，右边很简单的，不如大胆做个代换。

我们会遇到如 andb_true_iff 或者 ev5_nonsense 这样的，给一堆条件，证明 false = true 或者 ev 5 -> 2 + 2 = 9 这样奇怪的命题。我们要做的并不是去 discriminate 掉 goal，而是要在条件中构造出一个 False，然后通过爆炸原理来证明。这里我觉得主要是，如果假设中能退出 True，那实际上是要证明 True -> False，这个命题实际上是错误的。

另外，在 andb_true_iff 中需要注意 False 和 false 的区别。False 的定义是

1
Inductive False : Prop :=  .

而 false 只是我们定义的 bool 类型的一个构造函数。而 False 是一个 type，或者一个 proposition。所以无法证明 (false = true) = false。相应的，我们应该证明 false = true <-> False。

另一个回答说，他说 falsehood 通常的构造办法：
1.假设从一个空集中去一个值，这个值就不能被创造出来
2.两个值从不同的构造函数中构造出来的值是相同的，而凑早函数被认为是 injective 的。
比如，如果假设中有 H: False 我们可以 destruct H。如果假设中有 false = true，那么就可以 inversion。

承认排中律

不需要排中律即可证明 double_neg 即 P -> ~~P。但是反过来的 ~~P -> P 则需要排中律来证明。其实 ~~P -> P 感觉就是反证法。

~~(P \/ ~P) 可以被证明，但 P \/ ~P 排中律则依赖选择公理。为什么前者可以被证明呢？因为我们不能同时证明 P \/ ~P 和证伪 P \/ ~P。这样 (P \/ ~P) 和 ~(P \/ ~P) 不能同时为真。因为 forall P: Prop, P -> ~~P，所以 ~~(P \/ ~P) 和 ~(P \/ ~P) 不能同时为真。

~~(P \/ ~P) 的证明流程。unfold 去掉 not，得到的 goal 是 forall P : Prop, (P \/ (P -> False) -> False) -> False。好像是证明 “P \/ (P -> False) 是不可能的”是不可能的。intros 把 P \/ (P -> False) -> False 作为假设，goal 变成 False。这里发现可以进一步 apply 这个假设，替换到如下的形式

1
2
3
4
5
1 goal
P : Prop
H : P \/ (P -> False) -> False
______________________________________(1/1)
P \/ (P -> False)

看起来好像是承认 Q -> False 的情况下，反过来证明 Q 成立？继续证明。现在是给定 H : P \/ (P -> False) -> False 要证明 P \/ (P -> False)。假设 P -> False 成立，用 intros，假设 P 成立，证明 False。而已知条件是 P \/ (P -> False) -> False，不如再假设 P 成立，然后证明 P \/ (P -> False)。

排中律本身和其他一些定理可以串起来形成一个证明的圈。这个和实数那几个的定理一样。

InductionProp

之前，我们定义偶数一般是使用 nat。但现在介绍用 nat -> Prop 这样的形式来定义偶数 ev。

1
2
3
Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS (n : nat) (H : ev n) : ev (S (S n)).

注意，另一种方式会出错，也就是将 nat 放到 : 的左侧。

1
2
3
Fail Inductive wrong_ev (n : nat) : Prop :=
| wrong_ev_0 : wrong_ev 0
| wrong_ev_SS (H: wrong_ev n) : wrong_ev (S (S n)).
  • We already know how to perform case analysis on n using destruct or induction
  • But for some proofs we may instead want to analyze the evidence that ev n directly
    这是因为如果某人展示了对于 [ev n] 的 evidence [E]，那么我们知道 [E] 要么从 ev_0 来的，要么从 ev_SS 来的。
    一个反演命题。这个命题是对 ev 这个判断奇偶性的命题而言的。对这个命题直接使用 induction 是搞不定的，因为
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    Theorem ev_inversion :
      forall (n : nat), ev n ->
        (n = 0) \/ (exists n', n = S (S n') /\ ev n').
    Proof.
      intros n E.
      destruct E as [ | n' E'].
      - (* E = ev_0 : ev 0 *)
        left. reflexivity.
      - (* E = ev_SS n' E' : ev (S (S n')) *)
        right. exists n'. split. reflexivity. apply E'.
    Qed.

The [inversion] tactic can detect that:
1.the first case ([n =0]) does not apply
2.the [n’] that appears in the [ev_SS] case must be the same as [n].

It has an “[as]” variant similar to [destruct], allowing us to assign names rather than have Coq choose them.

1
2
3
4
5
6
7
8
Theorem evSS_ev' : forall n,
  ev (S (S n)) -> ev n.
Proof.
  intros n E.
  inversion E as [| n' E' EQ].
  (* We are in the [E = ev_SS n' E'] case now. *)
  apply E'.
Qed.

inversion 策略会做很多东西，比如如果对一个等式使用，就相当于 discriminate 加上 injection。另外，它还会带上使用 injection 可能必须的 intros 和 rewrite。它还可以被 apply，去 analyze evident for inductively defined 命题。下面会用 inversion 来尝试证明 Tactics 章节中涉及的一些定理。

[inversion] 的工作原理大致如下：假设 [H] 指代上下文中的假设 [P]，且 [P] 由 [Inductive] 归纳定义，则对于 [P] 每一种可能的构造，[inversion H] 各为其生成子目标。子目标中自相矛盾者被忽略，证明其余子命题即可得证原命题。
在证明子目标时，上下文中的 [H] 会替换为 [P] 的构造条件，即其构造子所需参数以及必要的等式关系。例如：倘若 [ev n] 由 [ev_SS] 构造，上下文中会引入参数 [n’]、[ev n’]，以及等式 [S (S n’) = n]。

下面，是另一个问题。为了证明 [n] 的性质对于 [ev n] 成立的所有数字都成立。我们需要在 [ev n] 上 induction。证明分为两块，和 [ev n] 的两个构造函数对应。如果他通过 [ev_0] 构造，则 n = 0，那么性质肯定对 [0] 成立。如果他通过 [ev_SS] 构造，那么 [ev n] 的证据就具有形式 [en_SS n’ E’]，其中 [n = S (S n’)] ，[E’] 是 [eb n’] 的证据。这样，the inductive hypothesis says that the property we are trying to prove holds for [n’]。

注意，这里的 exists (S k'). 来自于 ev 的定义，我们这里没有展开 ev。

从 le 的定义来看，可以总结出 destruct、inversion 和 induction 三种策略在 H: le e1 e2 上的作用。destruct H 能够产生两个 case。第一个 case 中 destruct H 产生两个情况，第一个是 e1 = e2，此时 e2 被 e1 替换掉。在第二个 case 中，e2 = S n’，并且对于某个 n’ 有 le e1 n’ 成立，并且用 S n’ 替换 e2。inversion H 会移除不可能的 case，并且将生成的新的等式添加到上下文中。执行 induction H，在第二种情况下，会将 induction hypothesis 的 e2 用 n’ 替换。

具体 case

1
2
3
4
5
6
7
8
Theorem ev'_ev_try1 : forall n, ev' n <-> ev n.

Proof.
  intros.
  split.
  - induction n.
    + intros. apply ev_0.
    + simpl. Abort.

对应的 goal 如下，S n 肯定对 ev’ 啥的不成立了啊。

1
2
3
4
5
1 goal
n : nat
IHn : ev' n -> ev n
______________________________________(1/1)
ev' (S n) -> ev (S n)

这里和 le_trans 相关的命题都是放缩法。遇到 S n，就通过 le_S 去掉 S。但是放缩法要符合情理。比如 n_le_m__Sn_le_Sm 里面就不能从 S n <= S m 放缩到 S n <= m。
要从 H : S n <= 1 推导 n <= 0，可以 inversion H。从 H1 : S n <= 0 推 n <= 0，也可以 inversion。感觉总的来说，inversion 是将一个更强的条件去分解为多个较弱的条件。
这里一个问题是不能用 injection 解决S n <= S (S m) 推导 n <= S m。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
Theorem le_S_ab2_try : forall a b,
  S a <= b -> a <= b.
Proof.
  intros a b. 
  induction a.
  - intros. inversion H.
    apply le_S. apply le_n. apply O_le_n.
  - intros. inversion H.

2 goals
a, b : nat
IHa : S a <= b -> a <= b
H : S (S a) <= b
H0 : S (S a) = b
______________________________________(1/2)
S a <= S (S a)
______________________________________(2/2)
S a <= S m
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
Theorem le_S_ab2 : forall a b,
  S a <= b -> a <= b.
Proof.
  intros a b. 
  generalize dependent a.
  induction b.
  - intros. inversion H.
  - intros. inversion H. apply le_S. apply le_n.
    apply le_S. apply IHb. apply H1.
Qed.

2 goals
b : nat
IHb : forall a : nat, S a <= b -> a <= b
a : nat
H : S a <= S b
H1 : a = b
______________________________________(1/2)
b <= S b
______________________________________(2/2)
a <= S b

比较有意思的是这里又找到一个必须要 apply with 的结构

1
2
3
4
5
6
7
8
9
10
11
Theorem add_le_cases : forall n m p q,
    n + m <= p + q -> n <= p \/ m <= q.
Proof.
    intros.
    generalize dependent p.
    induction n. left. apply O_le_n.
    intros. destruct p.
    * right. rewrite plus_O_n in H. apply le_S_ab2.
      apply add_le_cases_helper.

Unable to find an instance for the variable n.

另一个启发是不要过早地使用 left 或者 right 策略。会出现如下所示的问题，我们的条件和 goal 是不相关的。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
Theorem add_le_cases : forall n m p q,
    n + m <= p + q -> n <= p \/ m <= q.
Proof.
    intros.
    generalize dependent p.
    induction n. left. apply O_le_n.
    intros. destruct p.
    * right. rewrite plus_O_n in H. apply le_S_ab2.
      apply add_le_cases_helper with (n:=n). exact H.
    * left. simpl in H. apply add_le_helper2 in H. apply IHn in H.
      destruct H.
      - apply n_le_m__Sn_le_Sm. exact H.
      - 
1 goal
n, m, q : nat
IHn : forall p : nat, n + m <= p + q -> n <= p \/ m <= q
p : nat
H : m <= q
______________________________________(1/1)
S n <= S p

其实在第二个目标中，不要那么早使用 left 策略，而是先想办法 destruct H，根据 destruct 得到的条件选择是 left 还是 right 就能解决问题了。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
Theorem add_le_cases : forall n m p q,
    n + m <= p + q -> n <= p \/ m <= q.
Proof.
    intros.
    generalize dependent p.
    induction n. left. apply O_le_n.
    intros. destruct p.
    * right. rewrite plus_O_n in H. apply le_S_ab2.
      apply add_le_cases_helper with (n:=n). exact H.
    * simpl in H. apply add_le_helper2 in H. apply IHn in H.
      destruct H.
      - left. apply n_le_m__Sn_le_Sm. exact H.
      - right. exact H.
Qed.

Reference

  1. https://coq.inria.fr/doc/V8.13+beta1/refman/proofs/writing-proofs/rewriting.html
    介绍 rewrite