Coq 的数学证明语言 : Rewriting in if condition

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 (见 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.