使用 coq 反转策略的矛盾假设

Question

来自这个例子：

Example foo : forall (X : Type) (x y z : X) (l j : list X),
  x :: y :: l = z :: j ->
  y :: l = x :: j ->
  x = y.

只需要对第二个假设做inversion就可以解决：

Proof.
  intros X x y z l j eq1 eq2. inversion eq2. reflexivity. Qed.

然而，在第一个假设中也做 inversion，会产生明显矛盾的假设：

Proof.
  intros X x y z l j eq1 eq2. inversion eq2. inversion eq1. reflexivity. Qed.

因为，在最后一个证明中，生成的假设是：

H0 : y = x
H1 : l = j
H2 : x = z
H3 : y :: l = j

但是，如果我没有遗漏一些明显的东西，H1 和 H3 不可能同时成立。

谁能给我解释一下这是怎么回事？只是这个例子是 "bad designed" （两个假设都是矛盾的）并且 Coq 反转策略只是吞没了它们？它是基于两个假设一起考虑的爆炸原理吗？如果是这样，是否有可能仅仅通过从错误中推导出任何东西来证明这个例子？怎么样？

Answer 1

您的示例假设了相互矛盾的假设：它们暗示 length l + 2 等于 length l + 1。

Require Import Coq.Lists.List.
Require Import Omega.

Example foo : forall (X : Type) (x y z : X) (l j : list X),
  x :: y :: l = z :: j ->
  y :: l = x :: j ->
  x = y.
Proof.
  intros X x y z l j eq1 eq2.
  apply (f_equal (@length _)) in eq1.
  apply (f_equal (@length _)) in eq2.
  simpl in *.
  omega.
Qed.

根据爆炸原理，Coq能够推导出矛盾的上下文也就不足为奇了。

除了这个小怪异之外，生成的假设是矛盾的这一事实并没有错：即使原始假设是一致的，也会出现这样的上下文。考虑以下（公认的人为的）证明：

Goal forall b c : bool, b = c -> c = b.
Proof.
intros b c e.
destruct b, c.
- reflexivity.
- discriminate.
- discriminate.
- reflexivity.
Qed.

第二个和第三个分支有相互矛盾的假设（true = false和false = true），即使最初的假设b = c是无害的。这个例子和原来的有点不同，因为矛盾不是通过组合假设得到的。相反，当我们调用 destruct 时，我们承诺 Coq 会通过考虑案例分析获得的一些子目标来证明结论。如果一些子目标碰巧是矛盾的，那就更好了：那里不会有任何工作要做。

使用 coq 反转策略的矛盾假设

Contradictory hypothesis using coq inversion tactic

coq

proof

coq-tactic