coq - 破坏不动点时，添加假设而不简化

Question

假设我必须证明以下引理:

Require Import Coq.Arith.EqNat.

Lemma myLemma: forall m,
  if beq_nat m 0
  then m = 0
  else m <> 0.

我这样做:

Proof.
  intro.
  destruct (beq_nat m 0).  (* [1] *)
  - (* [2] *)
  - (* ???? Can't do anything *)
Qed.

然后，在点 [1] 处，destruct首先通过案例分析进行beq_nat m 0替换为 true在 if简化为目标 m = 0 ，没有额外的假设(在点[2])。

我的问题是:有没有办法分割目标，并添加相应的案例作为假设，而不是分割目标，替换和简化？

也就是说，在点 [2] 处，而不是具有以下内容:

m : nat
______________________________________(1/1)
m = 0

我想要:

m : nat
true = PeanoNat.Nat.eqb m 0
______________________________________(1/1)
if PeanoNat.Nat.eqb m 0 then m = 0 else m <> 0

并继续进行以下证明。

(注意:这是一个非常虚拟的mwe，我知道还有其他方法可以完成这里，我的观点不是完成这个特定的证明，而是有一种方法从析构中获得假设)。

Answer 1

而不是 destruct (beq_nat m 0)你可以使用

destruct (beq_nat m 0) eqn:Equation_name.

或

case_eq (beq_nat m 0).

destruct ... eqn:E就像 case_eq ...; intros E 。您可以详细了解 destruct 之间的差异和case读过这篇文章entry .

前两个选项简化了事情，但我们可以这样做来避免简化:

remember (beq_nat m 0) as b eqn:E; rewrite E; destruct b.

第三个选项将为您提供这样的证明状态

m : nat
E : true = PeanoNat.Nat.eqb m 0
============================
if PeanoNat.Nat.eqb m 0 then m = 0 else m <> 0

第一个子目标。