Тактика дизъюнктивного силлогизма в Coq? - PullRequest
Новая
       50

Тактика дизъюнктивного силлогизма в Coq?

0 голосов
/ 21 октября 2018

Я изучаю логику высказываний и правила вывода.Правило дизъюнктивного силлогизма гласит, что если мы имеем в наших помещениях (P или Q), а также (не P);тогда мы можем достичь Q.

Я не могу на всю жизнь понять, как это сделать в Coq.Допустим, у меня есть: 

H : A \/ B
H0 : ~ A
______________________________________(1/1)

Какую тактику я должен использовать для достижения 

H1 : B.

В качестве дополнения, я был бы рад, если бы кто-то мог поделиться со мной тактическими эквивалентами Coq основныхправила вывода, такие как modus tollens, дизъюнктивное введение и т. д. Есть ли плагин, который я могу использовать?

Ответы [ 3 ]

0 голосов
/ 21 октября 2018

Coq не имеет этой встроенной тактики, но, к счастью, вы можете определить свою собственную тактику.Обратите внимание, что 

destruct H as [H1 | H1]; [contradiction |].

помещает H1 : B в контекст, как вы и просили.Таким образом, вы можете создать псевдоним для этой комбинированной тактики: 

Ltac disj_syllogism AorB notA B :=
  destruct AorB as [? | B]; [contradiction |].

Теперь мы можем легко имитировать правило дизъюнктивного силлогизма, например: 

Section Foo.
Context (A B : Prop) (H : A \/ B) (H0 : ~ A).
Goal True.
  disj_syllogism H H0 H1.
End Foo.

Позвольте мне показать пару менее автоматизированных подходов:

Ltac disj_syllogism AorB notA B :=
  let A := fresh "A" in
  destruct AorB as [A | B]; [contradiction (notA A) |].

Этот подход не просит Coq найти противоречие, он предоставляет его непосредственно к тактике contradiction (термин notA A).Или мы могли бы использовать явный термин с тактикой pose proof: 

Ltac disj_syllogism AorB notA B :=
  pose proof (match AorB with
              | or_introl a => False_ind _ (notA a)
              | or_intror b => b
              end) as B.

Надеюсь, это поможет.Я не уверен, что нужно какое-то дополнительное объяснение - не стесняйтесь просить разъяснения, и я обновлю свой ответ.

0 голосов
/ 22 октября 2018

Основываясь на ответе Антона Трунова, более простая версия для дизъюнктивного силлогизма выглядит следующим образом:

(* Helper tactics. *) Ltac oe1 P_or_Q not_P := destruct P_or_Q ; [ contradiction | ]. Ltac oe2 P_or_Q not_Q := destruct P_or_Q ; [ | contradiction ].

(* Main tactic *) Ltac oE AorB H := oe1 AorB H || oe2 AorB H.

Такт помощника каждыйРаботайте над одним случаем, основываясь на том, находится ли ложный дизъюнкт справа или слева, основная тактика пробует оба варианта и возвращает результат в зависимости от того, какой из них успешен.

0 голосов
/ 21 октября 2018

Я думаю, что у вас могут быть неправильные ожидания относительно того, как работает Coq?Общий способ доказать это, по сути, представляет собой таблицу истинности о различных возможностях: 

Lemma it: forall a b, (a \/ b) /\ ~a -> b.
Proof.
  intuition.
  Show Proof.
Qed.

(fun (a b : Prop) (H : (a \/ b) /\ ~ a) =>
 and_ind
   (fun (H0 : a \/ b) (H1 : ~ a) =>
    or_ind (fun H2 : a => let H3 : False := H1 H2 in False_ind b H3)
      (fun H2 : b => H2) H0) H)

Если вы посмотрите на полученное доказательство, вы увидите, что Coq по сути разбирает логические конструкторы.Мы можем сделать это вручную и получить тот же проверочный термин: 

Lemma it: forall a b, (a \/ b) /\ ~a -> b.
Proof.
  intros a b H.
  induction H.
  induction H.
  contradict H. exact H0.
  exact H.
Qed.

В то время как, например, modus ponens соответствует apply в Coq, я не думаю, что это «встроено» каким-либо прямым способом.

Впоследствии вы можете использовать эту лемму (и я уверен, что где-то в стандартной библиотеке есть соответствующая версия), чтобы вывести свою дополнительную гипотезу через apply.

...