coq - 如何使用不等式来简化 Coq 中的 if-then-else？

Question

我正在做一个证明，在那里我生成了两个案例

destruct (eq_id_dec Y X)

（eq_id_dec本质上类似于eq_nat_dec）。

e: Y = X这给出了两种情况，分别增加了平等和不平等的假设n: Y <> X。

在第一种情况下，我可以轻松使用rewrite eor rewrite <- e。

但是我怎样才能有效地利用第二种情况下的不等式呢？例如，考虑一个目标，例如

(if eq_id_dec X Y then AAA else BBB) = BBB

?

我尝试unfold eq_id_dec了一些rewriteS 但卡住了。

Answer 1

理想情况下，你想说的话

forall (P : Prop)
       (b : {P} + {~ P})
       (H : ~ P), b = right H.

不幸的是，如果不假设函数可扩展性，就不可能显示这个结果，因为没有有用的原则可以让你证明两个否定证明是相等的。

您可以为您的案例证明此引理的一般结果，如下所示：

Require Import Coq.Arith.Peano_dec.

Lemma sumboolF T P (b : {P} + {~ P}) x y : ~ P -> (if b then x else y) = y :> T.
Proof.
intros; destruct b; tauto.
Qed.

Lemma test n m : n <> m -> (if eq_nat_dec n m then 1 else 0) = 0.
Proof.
intros H; rewrite sumboolF; auto.
Qed.

这有助于解决您的问题，但可能需要为该类型的其他用途显示类似的结果sumbool。

这是让我们考虑sumbool从 Software Foundations 书中删除的问题之一，而只使用普通的布尔值。