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

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

0 голосов
/ 22 мая 2018

Из этого примера: 

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 просто проглатывает их?Это принцип взрыва, основанный на двух гипотезах, рассматриваемых вместе?Если да, то можно ли доказать пример, просто извлекая что-то из лжи?Как?

1 Ответ

0 голосов
/ 22 мая 2018

Ваш пример предполагает противоречивые гипотезы: они подразумевают, что 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 способен вывести противоречивыеcontext.

Помимо этой небольшой странности, нет ничего плохого в том, что сгенерированные гипотезы противоречивы: такие контексты могут возникать, даже если исходные гипотезы непротиворечивы.Рассмотрим следующее (заведомо надуманное) доказательство: 

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

...