Coq 的数学证明语言：在 if 条件下重写

Question

我正在尝试学习 Coq 的数学证明语言，但我运行在试图证明我简化为以下愚蠢陈述的东西时遇到了一些麻烦：

Lemma foo: forall b: bool, b = true -> (if b then 0 else 1) = 0.

这是我的尝试：

proof.
  let b: bool.
  let H: (b = true).

此时证明状态为：

  b : bool
  H : b = true
  ============================
  thesis := 
   (if b then 0 else 1) = 0

现在我想将 if 条件 b 重写为 true 以便能够证明论文。但是，"small step" 和

  have ((if b then 0 else 1) = (if true then 0 else 1)) by H.

和 "bigger step" 的

  have ((if b then 0 else 1) = 0) by H.

失败 Warning: Insufficient justification. 我不认为重写条件有什么问题，因为正常的 rewrite -> H 策略会做同样的事情。

我也可以通过将 if 包装在一个函数中来让它正常工作：

Definition ite (cond: bool) (a b: nat) := if cond then a else b.
Lemma bar: forall b: bool, b = true -> (ite b 0 1) = 0.
proof.
  let b: bool. let H: (b = true).
  have (ite b 0 1 = ite true 0 1) by H. thus ~= 0.
end proof.

当然，这不是很好。我做错了什么吗？有没有办法挽救我的原始证明？这只是数学证明语言实现的一个缺点吗？

我注意到手册的第 11.3.3 节中有一个可能相关的示例（在 https://coq.inria.fr/doc/Reference-Manual013.html）：

  a := false : bool
  b := true : bool
  H : False
  ============================
  thesis :=
  if b then True else False

Coq <  reconsider thesis as True.

但我不知道如何将 b := true 部分放入上下文中。

Answer 1

关键字proof似乎进入了声明式证明模式。相比之下，关键字 Proof 进入命令式证明模式。在第二种情况下，我们可以很容易地证明如下。

Lemma foo: forall b: bool, b = true -> (if b then 0 else 1) = 0.                                     
Proof.                                                                                              
  intros b H.                                                                                       
  rewrite H.                                                                                        
  reflexivity.                                                                                      
Qed.

第一种情况我没有答案。我尝试了多种与您类似的方法，但一次又一次地发现了同样的问题。也许对声明性证明比较熟悉的人可以给出完整的答案。如果您找到解决方案，请告诉我们！

Answer 2

一种可能的解决方案是在 b 上使用 per cases（参见 sect. 11.3.12）：

Lemma foo:
  forall b: bool, b = true -> (if b then 0 else 1) = 0.
proof.
  let b : bool.
  per cases on b.
    suppose it is true. thus thesis.
    suppose it is false. thus thesis.
  end cases.
end proof.
Qed.

我还尝试重新创建您的参考手册示例的证明状态，您可以使用 define：

Lemma manual_11_3_3 :
  if false then True else False ->
  if true then True else False.
proof.
  define a as false.
  define b as true.
  assume H : (if a then True else False).
  reconsider H as False.
  reconsider thesis as True.
Abort.

Coq 的数学证明语言：在 if 条件下重写

Coq's mathematical proof language: Rewriting in if condition

coq