Противоречивая гипотеза с использованием тактики инверсии кока

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 быть правдой в то же время.

Может кто-нибудь объяснить мне, что происходит? Это просто, что пример "плохо спроектирован" (обе гипотезы противоречивы) и что тактика инверсии 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 доказать заключение, рассмотрев несколько подзадач, полученных в результате анализа случаев. Если некоторые из подзадач окажутся противоречивыми, даже лучше: там не будет никакой работы.