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

【问题标题】：Contradictory hypothesis using coq inversion tactic使用 coq 反转策略的矛盾假设
【发布时间】：2018-05-22 16:55:43
【问题描述】：

从这个例子：

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 不可能同时为真。

有人可以解释一下发生了什么吗？只是这个例子是“糟糕的设计”（两个假设都是矛盾的）并且 Coq 倒置策略只是吞下了它们？它是基于一起考虑的两个假设的爆炸原理吗？如果是这样，那么是否有可能仅通过从虚假中推导出任何东西来证明这个例子？怎么样？

【问题讨论】：

标签： coq proof coq-tactic

【解决方案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 通过考虑通过案例分析获得的一些子目标来证明结论。如果某些子目标恰好是矛盾的，那就更好了：那里没有任何工作要做。

【讨论】：