Software Foundations Vol.I : 更多基本策略(Tactics)
本章主要内容包括:
- 如何在“向前证明”和“向后证明”两种风格中使用辅助引理;
- 如何对数据构造子进行论证,特别是,如何利用它们单射且不交的事实;
- 如何增强归纳假设,以及何时需要增强;
- 还有通过分类讨论进行论证的更多细节。
Apply策略
通常,经常会遇到待证目标与上下文中的前提或已证引理'刚好相同'的情况。
Theorem silly1 : ∀ (n m o p : nat),n = m →[n;o] = [n;p] →[n;o] = [m;p].
Proof.intros n m o p eq1 eq2.rewrite <- eq1.
此时可以像之前那样用“rewrite → eq2. reflexivity.”来完成。
apply: 从结论出发,对待证明结论q通过apply模式p->q结合,转化待证明命题为p.这是一种结论上移的操作.
不过如果使用 apply 策略,只需一步就能完成此证明:
apply eq2. Qed.
apply 策略也可以配合'条件(Conditional)'假设和引理来使用: 如果被应用的语句是一个蕴含式,那么该蕴含式的前提就会被添加到待证子目标列表中。
Theorem silly2 : ∀ (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.
通常,当使用 apply H 时,语句 H 会以一个引入了某些 '通用变量(Universal Variables)' 的 ∀ 开始。在 Coq 针对 H 的结论匹配当前目标时,它会尝试为这些变量查找适当的值。
例如, 当我们在以下证明中执行 apply eq2 时,eq2 中的通用变量 q 会以 n 实例化,而 r 会以 m 实例化。
Theorem silly2a : ∀ (n m : nat),(n,n) = (m,m) →(∀ (q r : nat), (q,q) = (r,r) → [q] = [r]) →[n] = [m].
Proof.intros n m eq1 eq2.apply eq2. apply eq1.
Qed.
要使用 apply 策略,被应用的事实(的结论)必须精确地匹配证明目标:若当等式的左右两边互换后,apply 就无法起效了。
Theorem silly3_firsttry : ∀ (n : nat),true = (n =? 5) →(S (S n)) =? 7 = true.
Proof.intros n H.
在这里,无法直接使用 apply,若试图apply H,则会出现如下的报错:
In environment
n : nat
H : true = (n =? 5)
Unable to unify "true = (n =? 5)" with "(S (S n) =? 7) = true".
不过可以用 symmetry 策略 它会交换证明目标中等式的左右两边。
symmetry.simpl.apply H.
Qed.
symmetry: 将待证明等式左右两侧互换.
Apply with策略
以下愚蠢的例子在一行中使用了两次改写来将 [a;b] 变成 [e;f]。
Example trans_eq_example : ∀ (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.rewrite → eq1. rewrite → eq2. reflexivity.
Qed.
由于这种模式十分常见,因此一劳永逸地把它作为一条引理记录下来,即等式具有传递性。
Theorem trans_eq : ∀ (X:Type) (n m o : X),n = m → m = o → n = o.
Proof.intros X n m o eq1 eq2. rewrite → eq1. rewrite → eq2.reflexivity.
Qed.
现在,按理说应该可以用 trans_eq 来证明前面的例子了。 然而,实际上为此还需要稍微改进一下 apply 策略。
Example trans_eq_example' : ∀ (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.apply trans_eq with (m:=[c;d]).apply eq1. apply eq2.
Qed.
这是因为,匹配过程并没有为 m 确定实例:我们必须在 apply 的调用后面加上 "with (m:=[c,d])" 来显式地提供一个实例。
apply with: 对于未确定实例的apply模式,指定其中部分变量实例.
(实际上,通常不必在 with 从句中包含名字 m,Coq 一般足够聪明来确定实例化的变量。因此也可以写成: apply trans_eq with [c;d]。)
Injection与Discriminate策略
回想自然数的定义:
Inductive nat : Type :=| O| S (n : nat).
可从该定义中观察到,所有的数都是两种形式之一:
- 要么是构造子 O,
- 要么就是将构造子 S 应用到另一个数上。
不过这里还有无法直接看到的:自然数的定义中还蕴含了两个事实:
- 构造子 S 是'单射(Injective)'或'一一对应'的。 即,如果 S n = S m,那么 n = m 必定成立。
- 构造子 O 和 S 是'不相交(Disjoint)'的。 即,对于任何 n,O 都不等于 S n。
类似的原理同样适用于所有归纳定义的类型:所有构造子都是单射的, 而不同构造子构造出的值绝不可能相等。
对于列表来说,cons 构造子是单射的,而 nil 不同于任何非空列表。
对于布尔值来说,true 和 false 是不同的。 因为 true 和 false 二者都不接受任何参数,它们既不在这边也不在那边。
其它归纳类型亦是如此。
例如,可以使用定义在 Basics.v 中的 pred 函数来证明 S 的单射性。
Theorem S_injective : ∀ (n m : nat),S n = S m →n = m.
Proof.intros n m H1.assert (H2: n = pred (S n)). {reflexivity. }rewrite H2. rewrite H1. reflexivity.
Qed.
这个技巧可以通过编写等价的 pred 来推广到任意的构造子上 —— 即编写一个“撤销”一次构造子调用的函数。
为此,Coq 提供了更加简便的 injection 策略,它能让我们利用任意构造子的单射性。
下面是使用 injection 对上面定理的另一种证法:
Theorem S_injective' : ∀ (n m : nat),S n = S m →n = m.
Proof.intros n m H.injection H as Hnm. apply Hnm.
Qed.
通过在此处编写 injection H as Hmn,让 Coq 利用构造子的单射性来产生所有它能从 H 所推出的等式(本例中为等式 n = m)。
每一个这样的等式都作为假设(本例中为 Hmn)被添加到上下文中。
injection: 利用构造子单射性来产生推演.
以下例子展示了一个 injection 如何直接得出多个等式。
Theorem injection_ex1 : ∀ (n m o : nat),[n; m] = [o; o] →[n] = [m].
Proof.intros n m o H.injection H as H1 H2.rewrite H1. rewrite H2. reflexivity.
Qed.
另一方面,如果只使用 injection H 而不带 as 从句,那么所有的等式都会在目标的开头被转变为假设。
Theorem injection_ex1 : ∀ (n m o : nat),[n; m] = [o; o] →[n] = [m].
Proof.intros n m o H.injection H.intros H1 H2.rewrite H1. rewrite H2. reflexivity.
Qed.
关于构造子的injectivity就这么多吧, 来看到其disjointness.
disjointness原则指出,以不同构造子开始的项(如O 与 S,或者true 和 false)永远不可能相等.
这意味着,当在某个情境中假定两个这样的项相等时,都有充分的理由得出任何想要的结论,因为这种假设是毫无意义的(trivial).
discriminate策略体现了这一原则: 其适用于涉及不同构造子之间相等关系的假设(例如 S n=O),并且能够立即解决当前的目标.
下面是一个例子:
Theorem eqb_0_l : ∀ n,0 =? n = true → n = 0.
Proof.intros n.destruct n as [| n'] eqn:E.- (* n = 0 *)intros H. reflexivity.- (* n = S n' *)simpl. intros H. discriminate H.
Qed.
其中,第二个分支中,假设O=?(S n')=true,那么必须证明 S n'=O.接下来观察到这个假设本身是无意义的.
如果我们对这个假设使用 discriminate , Coq 便会确认我们当前正在证明的目标不可行,并同时移除它,不再考虑。
本例是逻辑学原理'爆炸原理'的一个实例,它断言矛盾的前提会推出任何东西, 甚至是假命题!
discriminate: 利用爆炸原理,通过矛盾的前提直接切除分支.
Theorem discriminate_ex1 : ∀ (n : nat),S n = O →2 + 2 = 5.
Proof.intros n contra. discriminate contra.
Qed.Theorem discriminate_ex2 : ∀ (n m : nat),false = true →[n] = [m].
Proof.intros n m contra. discriminate contra.
Qed.
爆炸原理可能令人费解,那么请记住上述证明'并不'肯定其后件,而是说明:'如果'荒谬的前件成立,'那么'就会得出荒谬的结论, 如此一来我们将生活在一个不一致的宇宙中,这里每个陈述都是正确的。
构造子的单射性能让我们论证 ∀ (n m : nat), S n = S m → n = m。 此蕴含式的逆形式是一个构造子和函数的更一般的实例, 在后面我们会发现它用起来很方便:
Theorem f_equal : ∀ (A B : Type) (f: A → B) (x y: A),x = y → f x = f y.
Proof. intros A B f x y eq. rewrite eq. reflexivity.
Qed.Theorem eq_implies_succ_equal : ∀ (n m : nat),n = m → S n = S m.
Proof. intros n m H. apply f_equal. apply H.
Qed.
此外,还有一种名为"f_equal"的策略可以用来证明此类定理.
对于形如 f a1 ... an=g b1 ... bn的目标,策略"f_equal"会生成形如f=g, a1=b1, ... , an=bn的子目标.同时,任意这些子目标中只要足够简单,"f_equal"都会将其自动消去.
Theorem eq_implies_succ_equal' : ∀ (n m : nat),n = m → S n = S m.
Proof. intros n m H. f_equal. apply H.
Qed.
f_equal: 对于形如 f a1 ... an=g b1 ... bn的目标进行自动检查的策略.
针对假设的策略
默认情况下,大部分策略会作用于目标公式并保持上下文不变。然而, 大部分策略还有对应的变体来对上下文中的语句执行类似的操作。
例如,策略 simpl in H 会对上下文中的假设 H 执行化简。
Theorem S_inj : ∀ (n m : nat) (b : bool),(S n) =? (S m) = b →n =? m = b.
Proof.intros n m b H. simpl in H. apply H.
Qed.
simpl in: 对局部的前提进行简化.
symmetry in: 对局部的前提进行翻转.
类似地,apply L in H 会针对上下文中的假设 H 匹配某些 (形如 X → Y 中的)条件语句 L。
然而,与一般的 apply 不同 (它将匹配 Y 的目标改写为子目标 X),apply L in H 会针对 X 匹配 H,如果成功,就将其替换为 Y。
换言之,apply L in H 给了我们一种“正向推理”的方式:
根据 X → Y 和一个匹配 X 的假设,它会产生一个匹配 Y 的假设。
作为对比,apply L 是一种“反向推理”:它表示如果我们知道 X → Y 并且试图证明 Y,那么证明 X 就足够了。
apply in: 通过X->Y,X的模式,类似于mp方式代入.
下面是前面证明的一种变体,它始终使用正向推理而非反向推理。
Theorem silly3' : ∀ (n : nat),(n =? 5 = true → (S (S n)) =? 7 = true) →true = (n =? 5) →true = ((S (S n)) =? 7).
Proof.intros n eq H.symmetry in H. apply eq in H. symmetry in H.apply H.
Qed.
正向推理从'给定'的东西开始(即前提、已证明的定理), 根据它们迭代地刻画结论直到抵达目标。
反向推理从'目标'开始, 迭代地推理蕴含目标的东西,直到抵达前提或已证明的定理。
你在数学或计算机科学课上见过的非形式化证明可能倾向于正向推理。
通常,Coq 习惯上倾向于使用反向推理,但在某些情况下,正向推理更易于思考
变换Induction假设
在 Coq 中进行归纳证明时,有时控制归纳假设的确切形式是十分重要的。
特别是,在调用 induction 策略前,需要用 intros 将假设从目标移到上下文中时要十分小心。
例如,假设我们要证明 double 函数是单射的,即将不同的参数映射到不同的结果:
Theorem double_injective: ∀ n m,double n = double m → n = m.intros n. induction n.
(*...*)
此证明的开始方式有点微妙:如果我们以intros n. induction n.开头开始,那么一切都好。
然而假如以intros n m. induction n.开始,就会卡在归纳情况中...
Theorem double_injective_FAILED : ∀ 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.
Abort.
此时,归纳假设 IHn' '不会'给出 n' = m',会有个额外的 S 阻碍,因此该目标无法证明。
哪里出了问题?
问题在于,在调用归纳假设的地方已经将 m 引入了上下文中--直观上,我们已经告诉了 Coq “我们来考虑具体的 n 和 m...”,
而现在必须为那些'具体的' n 和 m 证明 double n = double m, 然后才有 n = m。
下一个策略 induction n 告诉 Coq:我们要对 n 归纳来证明该目标。
也就是说,我们要证明对于'所有的' n,命题 P n = "if double n = double m, then n = m"成立,需通过证明
- P O (即,若“double O = double m 则 O = m”)和
- P n → P (S n) (即,若“double n = double m 则 n = m”蕴含“若 double (S n) = double m 则 S n = m”)
来得出。
如果我们仔细观察第二个语句,就会发现它说了奇怪的事情:
对于一个'具体的' m,如果我们知道 “若 double n = double m 则 n = m” 那么我们就能证明 “若 double (S n) = double m 则 S n = m”。
但是知道 Q 对于证明 R 来说并没有任何帮助!
(如果我们试着根据 Q 证明 R,就会以“假设 double (S n) = 10..”这样的句子开始, 不过之后我们就会卡住:知道 double (S n) 为 10 并不能告诉我们 double n 是否为 10。(实际上,它强烈地表示 double n '不是' 10!) 因此 Q 是没有用的。)
当 m 已经在上下文中时,试图对 n 进行归纳来进行此证明是行不通的, 因为我们之后要尝试证明涉及'每一个' n 的命题,而不只是'单个' m。
对 double_injective 的成功证明将 m 留在了目标语句中 induction 作用于 n 的地方:
注意,此时的证明目标和归纳假设是不同的:证明目标要求我们证明更一般的事情 (即,为'每一个' m 证明该语句),而归纳假设 IH 相应地更加灵活, 允许我们在应用归纳假设时选择任何想要的 m。
Theorem double_injective : ∀ 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.intros m eq.destruct m as [| m'] eqn:E.+ (* m = O *) simpl.discriminate eq.+ (* m = S m' *)apply f_equal.apply IHn'. injection eq as goal. apply goal.
Qed.
到这里,由于我们在 destruct m 的第二个分支中,因此上下文中涉及到的 m' 就是我们开始讨论的 m 的前趋。
由于我们也在归纳的 S 分支中,这就很完美了: 如果我们在归纳假设中用当前的 m'(此实例由下一步的 apply 自动产生) 实例化一般的 m,那么 IHn' 就刚好能给出我们需要的来结束此证明。
从上面的一切中,应当领悟到的是: 在运用induction时,必须谨慎行事,切不可试图证明过于具体的内容: 在通过关于变量n与m的命题进行归纳证明时,有时必须将变量m设为通用形式,这一点至关重要.
在 induction 之前做一些 intros 来获得更一般归纳假设并不总是奏效。
有时需要对量化的变量做一下'重排'。例如,假设我们想要通过对 m 而非 n 进行归纳来证明 double_injective。
Theorem double_injective_take2_FAILED : ∀ n m,double n = double m →n = m.
Proof.intros n m. induction m as [| m' IHm'].- (* m = O *) simpl. intros eq. destruct n as [| n'] eqn:E.+ (* n = O *) reflexivity.+ (* n = S n' *) discriminate eq.- (* m = S m' *) intros eq. destruct n as [| n'] eqn:E.+ (* n = O *) discriminate eq.+ (* n = S n' *) apply f_equal.(* 和前面一样,又卡在这儿了。 *)
Abort.
问题在于,要对 m 进行归纳,我们首先必须对 n 归纳。(而如果我们不引入任何东西就执行 induction m,Coq 就会自动为我们引入 n)
我们可以对它做什么?
一种可能就是改写该引理的陈述使得 m 在 n 之前量化。
这样是可行的,不过它不够好:我们不想调整该引理的陈述来适应具体的证明策略!我们更想以最清晰自然的方式陈述它。
我们可以先引入所有量化的变量,然后'重新一般化(re-generalize)' 其中的一个或几个,选择性地从上下文中挑出几个变量并将它们放回证明目标的开始处。
用 generalize dependent 策略就能做到。
Theorem double_injective_take2 : ∀ n m,double n = double m →n = m.
Proof.intros n m.(* n and m are both in the context *)generalize dependent n.(* 现在 n 回到了目标中,我们可以对 m 进行归纳并得到足够一般的归纳假设了。 *)induction m as [| m' IHm'].- (* m = O *) simpl. intros n eq. destruct n as [| n'] eqn:E.+ (* n = O *) reflexivity.+ (* n = S n' *) discriminate eq.- (* m = S m' *) intros n eq. destruct n as [| n'] eqn:E.+ (* n = O *) discriminate eq.+ (* n = S n' *) apply f_equal.apply IHm'. injection eq as goal. apply goal.
Qed.
generalize dependent: 将某个intros的符号变量提取出来一般化,避免实例化带来的不便.
来看一下此定理的非形式化证明。注意保持 n 的量化状态并通过归纳证明的命题,对应于形式化证明中依赖的一般化。
'定理':对于任何自然数 n 和 m,若 double n = double m,则 n = m。
'证明':令 m 为一个 nat。通过对 m 进行归纳来证明,对于任何 n, 若 double n = double m,则 n = m。
首先,设 m = 0,而 n 是一个数使得 double n = double m。 我们必须证明 n = 0。
由于 m = 0,根据 double 的定义,有 double n = 0。此时对于 n 需要考虑两种情况。
- 若 n = 0,则得证,因为 m = 0 = n,正如所需。
- 否则,若对于某个 n' 有 n = S n',我们就会导出矛盾:根据 double 的定义,我们可得出 double n = S (S (double n')),但它与 double n = 0 相矛盾。
其次,设 m = S m',而 n 同样是一个数使得 double n = double m。
必须证明 n = S m',根据归纳假设,对于任何数 s,若 double s = double m',则 s = m'。
根据 m = S m' 的事实以及 double 的定义我们有 double n = S (S (double m'))。
此时对于 n 需要考虑两种情况。
- 若 n = 0,则根据 double n = 0 的定义会得出矛盾。
- 故存在 n' 使得 n = S n'。
再次根据 double 之定义,可得 S (S (double n')) = S (S (double m'))。
再由构造子单射可知 double n' = double m'。以n' 代入归纳假设,推得 n' = m',故显然 S n' = S m', 其中 S n' = n,S m' = m,所以原命题得证。 ☐
展开Definition
有时候我们会需要手动展开一个Definition引入的名称,以便能够对它所表示的表达式进行操作.例如:我们试图定义:
Definition square n := n × n.
...并试图证明一个关于 square 的简单事实...
Lemma square_mult : ∀ n m, square (n × m) = square n × square m.
Proof.intros n m.simpl.unfold square.rewrite mult_assoc.assert (H : n × m × n = n × n × m). { rewrite mult_comm. apply mult_assoc. }rewrite H. rewrite mult_assoc. reflexivity.
Qed.
...那么就会卡住:simpl 无法化简任何东西,而由于我们尚未证明任何关于 square 的事实,也就没有任何可以用来 apply 或 rewrite 的东西。为此,可以手动用 unfold 展开 square 的定义.
等式两边都是涉及乘法的表达式,有很多可用的关于乘法的事实。特别是它满足交换性和结合性,该引理据此不难证明。
现在,是时候讨论下展开和化简了。
已经观察到,像 simpl、reflexivity 和 apply 这样的策略, 通常总会在需要时自动展开函数的定义。
例如,若我们将 foo m 定义为常量 5...
Definition foo (x: nat) := 5.
那么在以下证明中 simpl(或 reflexivity,如果我们忽略 simpl) 就会将 foo m 展开为 (fun x ⇒ 5) m 并进一步将其化简为 5。
Fact silly_fact_1 : ∀ m, foo m + 1 = foo (m + 1) + 1.
Proof.intros m.simpl.reflexivity.
Qed.
然而,这种自动展开有些保守。例如,若用模式匹配定义稍微复杂点的函数,那么类似的证明就会被卡住:
Definition bar x :=match x with| O ⇒ 5| S _ ⇒ 5end.
simpl 没有进展的原因在于,它注意到在试着展开 bar m 之后会留下被匹配的 m,它是一个变量,因此 match 无法被进一步化简。
它还没有聪明到发现 match 的两个分支是完全相同的。因此它会放弃展开 bar m 并留在那。
类似地,在试着展开 bar (m+1) 时会留下一个 match,被匹配者是一个函数应用 (即它本身,即便在展开 + 的定义后也无法被化简),因此 simpl 会留下它。
此时有两种方法可以继续。
- 一种是用 destruct m 将证明分为两种情况, 每一种都关注于更具体的 m(O vs S _)。在这两种情况下, bar 中的 match 可以继续了,证明则很容易完成。
Fact silly_fact_2 : ∀ m, bar m + 1 = bar (m + 1) + 1.
Proof.intros m.destruct m eqn:E.- simpl. reflexivity.- simpl. reflexivity.
Qed.
- 这种方法是可行的,不过它依赖于我们能发现隐藏在 bar 中的 match 阻碍了证明的进展。一种更直白的方式就是明确地告诉 Coq 去展开 bar。
Fact silly_fact_2' : ∀ m, bar m + 1 = bar (m + 1) + 1.
Proof.intros m.unfold bar.destruct m eqn:E.- reflexivity.- reflexivity.
Qed.
对复合表达式使用Destruct
我们已经见过许多通过 destruct 进行情况分析来处理一些变量的值了。
有时需要根据某些'表达式'的结果的情况来进行推理。也可以用 destruct 来做这件事。
下面是一些例子:
Definition sillyfun (n : nat) : bool :=if n =? 3 then falseelse if n =? 5 then falseelse false.
Theorem sillyfun_false : ∀ (n : nat),sillyfun n = false.
Proof.intros n. unfold sillyfun.destruct (n =? 3) eqn:E1.- (* n =? 3 = true *) reflexivity.- (* n =? 3 = false *) destruct (n =? 5) eqn:E2.+ (* n =? 5 = true *) reflexivity.+ (* n =? 5 = false *) reflexivity.
Qed.
在前面的证明中展开 sillyfun 后,我们发现卡在 if (n =? 3) then ... else ... 上了。
但由于 n 要么等于 3 要么不等于,因此我们可以用 destruct (eqb n 3) 来对这两种情况进行推理。
通常,destruct 策略可用于对任何计算结果进行情况分析。
如果 e 是某个表达式,其类型为归纳定义的类型 T,那么对于 T 的每个构造子 c,destruct e 都会生成一个子目标,其中(即目标和上下文中)所有的 e 都会被替换成 c。
destruct 策略的 eqn: 部分是可选的:目前,大部分时间都会包含它, 只是为了文档的目的。
然而在用 destruct 结构复合表达式时,eqn: 记录的信息是十分关键的:如果我们丢弃它,那么 destruct 会擦除我们完成证明时所需的信息。
例如,假设函数 sillyfun1 定义如下:
Definition sillyfun1 (n : nat) : bool :=if n =? 3 then trueelse if n =? 5 then trueelse false.
现在假设我们想让coq相信,对于sillyfun1 n来说,只有当n为奇数时其结果才为真值.
如果在证明过程中这样开始(destruct操作不加上eqn:)就会陷入困境.因为当前的上下文中没有足够的信息来证明这一目标!
Theorem sillyfun1_odd_FAILED : ∀ (n : nat),sillyfun1 n = true →oddb n = true.
Proof.intros n eq. unfold sillyfun1 in eq.destruct (n =? 3).(* 卡住了... *)
Abort.
问题在于,destruct操作的方式极其粗暴--在这种情况下,它会丢弃所有出现"n=?3"的情况,但我们需要保留对这个表达式以及它是如何被destruct的记忆,因为需要能够推断出"n=?3=true"导致必然有"n=3"--据此可以得出n为奇数的结论.
在此的目标是完全替代掉现有的"n=3"这样的表述,同时在上下文中添加一个方程,用于记录所处的情况.这是"eqn:"限定符所起到的作用.
Theorem sillyfun1_odd : ∀ (n : nat),sillyfun1 n = true →oddb n = true.
Proof.intros n eq. unfold sillyfun1 in eq.destruct (n =? 3) eqn:Heqe3.(* 现在我们的状态和前面卡住的地方一样了,除了上下文中包含了额外的相等关系假设,它就是我们继续推进所需要的。 *)- (* e3 = true *) apply eqb_true in Heqe3.rewrite → Heqe3. reflexivity.- (* e3 = false *)(* 当我们到达正在推理的函数体中第二个相等关系测试时,我们可以再次使用eqn:,以便结束此证明。 *)destruct (n =? 5) eqn:Heqe5.+ (* e5 = true *)apply eqb_true in Heqe5.rewrite → Heqe5. reflexivity.+ (* e5 = false *) discriminate eq.
Qed.
复习
现在我们已经见过 Coq 中最基础的策略了。
未来的章节中我们还会介绍更多, 之后我们会看到一些更加强大的'自动化'策略,它能让 Coq 帮我们处理底层的细节。
下面是我们已经见过的:
- 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: 通过injectivity来分析由归纳定义所对应值之间的相等关系的原理
- discriminate: 依据constructors之间的disjointness来对由归纳定义的类型所表示的值之间相等关系进行推理
- assert (H: e)(或 assert (e) as H):引入“局部引理”e 并称之为 H
- generalize dependent x:将变量 x(以及任何依赖它的东西) 从上下文中移回目标公式内的前提中