Блог

Извините за слишком сложный пример. У меня есть

 Lemma test : forall x y z : Prop,
 (
     (((x → (y ∨ z)) → (x ∨ y)) ↔ (x ∨ y))
   ∧ (((y → (x ∨ z)) → (x ∨ y)) ↔ (x ∨ y))
   ∧  ((y → (x ∨ z)) → (x ∨ (x → (y ∨ z))))
   ∧  ((x → (y ∨ z)) → (y ∨ (y → (x ∨ z))))
  )  → ((x → (y ∨ z)) → (y ∨ z)).
 

Выполнение

 Proof.
  intros.
  destruct H.
  destruct H1.
  destruct H2.
  pose proof (H3 H0).
 

дает

 1 goal
x, y, z : Prop
H : ((x → y ∨ z) → x ∨ y) ↔ x ∨ y
H1 : ((y → x ∨ z) → x ∨ y) ↔ x ∨ y
H2 : (y → x ∨ z) → x ∨ (x → y ∨ z)
H3 : (x → y ∨ z) → y ∨ (y → x ∨ z)
H0 : x → y ∨ z
H4 : y ∨ (y → x ∨ z)
______________________________________(1/1)
y ∨ z
 

Затем я делаю destruct H4. , и это дает

 2 goals
x, y, z : Prop
H : ((x → y ∨ z) → x ∨ y) ↔ x ∨ y
H1 : ((y → x ∨ z) → x ∨ y) ↔ x ∨ y
H2 : (y → x ∨ z) → x ∨ (x → y ∨ z)
H3 : (x → y ∨ z) → y ∨ (y → x ∨ z)
H0 : x → y ∨ z
H4 : y
______________________________________(1/2)
y ∨ z
______________________________________(2/2)
y ∨ z
 

чего я уже не понимаю: почему две одинаковые цели??
Затем я делаю left. и получаю

 2 goals
x, y, z : Prop
H : ((x → y ∨ z) → x ∨ y) ↔ x ∨ y
H1 : ((y → x ∨ z) → x ∨ y) ↔ x ∨ y
H2 : (y → x ∨ z) → x ∨ (x → y ∨ z)
H3 : (x → y ∨ z) → y ∨ (y → x ∨ z)
H0 : x → y ∨ z
H4 : y
______________________________________(1/2)
y
______________________________________(2/2)
y ∨ z
 

и затем assumption. дает

 1 goal
x, y, z : Prop
H : ((x → y ∨ z) → x ∨ y) ↔ x ∨ y
H1 : ((y → x ∨ z) → x ∨ y) ↔ x ∨ y
H2 : (y → x ∨ z) → x ∨ (x → y ∨ z)
H3 : (x → y ∨ z) → y ∨ (y → x ∨ z)
H0 : x → y ∨ z
H4 : y → x ∨ z
______________________________________(1/1)
y ∨ z
 

Затем делаем

 pose proof (H3 H0).
destruct H5.
left.
assumption.
 

снова вводит две идентичные цели и подводит меня к

 1 goal
x, y, z : Prop
H : ((x → y ∨ z) → x ∨ y) ↔ x ∨ y
H1 : ((y → x ∨ z) → x ∨ y) ↔ x ∨ y
H2 : (y → x ∨ z) → x ∨ (x → y ∨ z)
H3 : (x → y ∨ z) → y ∨ (y → x ∨ z)
H0 : x → y ∨ z
H4, H5 : y → x ∨ z
______________________________________(1/1)
y ∨ z
 

который идентичен предыдущему состоянию, за исключением того, что теперь у меня есть два идентичных помещения y → x ∨ z .

Я застрял. Очевидно, я делаю что-то не так, но что?

Давайте начнем с вашего первого вопроса. На самом деле, две цели, которые были сгенерированы после destruct , не совпадают. Их выводы действительно являются обоими y / z , но их предпосылки различаются: у первого есть H4 : y , а у второго есть H4 : y -> x / z . В более общем плане, если у вас есть цель вида

 (* ... *)
H : A / B
------------
 C
 

и вы это делаете destruct H as [H1 | H2]. , вы генерируете подцели

 (* ... *)
H1 : A
-----------
  C
 

и

 (* ... *)
H2 : B
------------
  C
 

с одинаковыми выводами.

Что касается вашего второго вопроса, проблема, вероятно, в том, что вы звоните pose proof (H3 H0) дважды. Если вы пройдетесь по своему сценарию, вы заметите, что гипотезы, выдвигаемые этой тактикой, одинаковы для обоих вызовов : y / (y -> x / z) . Я подозреваю, что вы должны иметь H2 H4 при втором вызове вместо H3 H0 , хотя я не проверял.

Заключительный комментарий: вы должны позволить Coq подбирать названия гипотез для вас, поскольку это приводит к недостижимым сценариям доказательства (см. Здесь ). По возможности следует использовать такие формы, как destruct H as [H1 | H2] вместо destruct H .

Это не только проблема тактики или понимания того, как работает Coq: ваша цель ложна, как показано ниже.

 Lemma test : ~ forall x y z : Prop,
 (
     (((x -> (y / z)) -> (x / y)) <-> (x / y))
   / (((y -> (x / z)) -> (x / y)) <-> (x / y))
   /  ((y -> (x / z)) -> (x / (x -> (y / z))))
   /  ((x -> (y / z)) -> (y / (y -> (x / z))))
  )  -> ((x -> (y / z)) -> (y / z)).
Proof.
  intros H.
  specialize (H False False False).
  firstorder.
Qed.
 

Другими словами, если x y и z принимаются равными False , то все предпосылки вашей леммы верны, но ее вывод — нет.

[Редактировать: как я это обнаружил] Сначала я попробовал firstorder тактику (процедуру принятия решения для таких целей первого порядка) и обнаружил, что она не завершается, что вызвало у меня подозрения. Затем я обратился к соответствующему логическому значению цели (используя ssreflect / ssrbool packages ), где я мог бы использовать разбиение на регистры x y и z вычисление, чтобы проверить, выполняется ли лемма. Выяснив, что, когда false цель сводилась к трем из них false , у меня был свой контрпример, а затем я просто превратил его обратно в пропозициональный контрпример.