代码之家 › 专栏 › 技术社区 › Waiting for Dev...

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

coq-tactic proof coq

Waiting for Dev... · 技术社区 · 6 年前

从这个例子中:

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.

但是,做 反转 同样在第一个假设中,产生了明显矛盾的假设:

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反转策略只是吞下了它们?这是基于两个假设的爆炸原理吗?如果是这样,那么是否可以通过从虚假中得到任何东西来证明这个例子?怎么用?

1 回复 | 直到 6 年前

Arthur Azevedo De Amorim 6 年前

你的例子假设了相互矛盾的假设:它们意味着 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 通过对案例分析得到的几个子目标的考虑,我们保证质量成本能够证明这一结论。如果一些子目标恰好是矛盾的,甚至更好:在那里没有任何工作要做。