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

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为了能够证明论点.但是,两者都是"小步"

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

和"更大的一步"

  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

一种可能的解决方案是使用per cases（b参见第 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.