Закон Деморгана для квантификаторов в Coq - PullRequest
Новая
       73

Закон Деморгана для квантификаторов в Coq

0 голосов
/ 04 июля 2019

Я пытаюсь доказать некоторые эквиваленты FOL. У меня проблемы с использованием законов Деморгана для квантификаторов, в частности

~ (exists x. P(x)) <-> forall x. ~P(x)

Я пытался применить not_ex_all_not из Coq.Logic.Classical_Pred_Type. И очистил StackOverflow ( Преобразование Coq не существует в выражение оператора , Преобразовать ~ существует в поиск в гипотезе ), но не пришло близко к решению вопроса. 

Theorem t3: forall (T: Type), forall p q: T -> Prop, forall r: T -> T -> Prop, 
~(exists (x: T), ((p x) /\ (exists (y: T), ((q y) /\ ~(r x y)))))
<-> forall (x y: T), ((p x) -> (((q y) -> (r x y)))).
Proof.
intros T p q r.
split.
- intros H.
apply not_ex_all_not.

Я получаю эту ошибку: 

In environment
T : Type
p, q : T → Prop
r : T → T → Prop
H : ¬ (∃ x : T, p x ∧ (∃ y : T, q y ∧ ¬ r x y))
Unable to unify
 "∀ (U : Type) (P : U → Prop), ¬ (∃ n : U, P n) → ∀ n : U, ¬ P n"
with "∀ x y : T, p x → q y → r x y".

Я ожидал, что закон Деморгана будет применен к цели, что приведет к отрицанию экзистенциальности.

1 Ответ

3 голосов
/ 05 июля 2019

Давайте посмотрим, что мы можем извлечь из H: 

~ (exists x : T, p x /\ (exists y : T, q y /\ ~ r x y))
=> (not exists <-> forall not)
forall x : T, ~ (p x /\ (exists y : T, q y /\ ~ r x y))
=> (not (A and B) <-> A implies not B)
forall x : T, p x -> ~ (exists y : T, q y /\ ~ r x y)
=>
forall x : T, p x -> forall y : T, ~ (q y /\ ~ r x y)
=>
forall x : T, p x -> forall y : T, q y -> ~ (~ r x y)

В результате мы получим двойное отрицание в заключении.Если вы не возражаете против использования классической аксиомы, мы можем применить NNPP, чтобы убрать ее, и все готово.

Вот эквивалентное доказательство Coq: 

Require Import Classical.

(* I couldn't find this lemma in the stdlib, so here is a quick proof. *)
Lemma not_and_impl_not : forall P Q : Prop, ~ (P /\ Q) <-> (P -> ~ Q).
Proof. tauto. Qed.

Theorem t3: forall (T: Type), forall p q: T -> Prop, forall r: T -> T -> Prop, 
~(exists (x: T), ((p x) /\ (exists (y: T), ((q y) /\ ~(r x y)))))
<-> forall (x y: T), ((p x) -> (((q y) -> (r x y)))).
Proof.
intros T p q r.
split.
- intros H x y Hp Hq.
  apply not_ex_all_not with (n := x) in H.
  apply (not_and_impl_not (p x)) in H; try assumption.
  apply not_ex_all_not with (n := y) in H.
  apply (not_and_impl_not (q y)) in H; try assumption.
  apply NNPP in H. assumption.

Вышесказанное было прямым рассуждением.Если вы хотите задом наперед (применяя леммы к цели вместо гипотез), все становится немного сложнее, потому что вам нужно построить точные формы, прежде чем применять леммы к цели .Это также, почему ваш apply терпит неудачу.Coq автоматически не находит, где и как применить лемму из коробки.

(И apply - это тактика относительно низкого уровня. Там - это продвинутыйФункция Coq , которая позволяет применять пропозициональную лемму к подтермам.) 

Require Import Classical.

Lemma not_and_impl_not : forall P Q : Prop, ~ (P /\ Q) <-> (P -> ~ Q).
Proof. tauto. Qed.

Theorem t3: forall (T: Type), forall p q: T -> Prop, forall r: T -> T -> Prop, 
~(exists (x: T), ((p x) /\ (exists (y: T), ((q y) /\ ~(r x y)))))
<-> forall (x y: T), ((p x) -> (((q y) -> (r x y)))).
Proof.
intros T p q r.
split.
- intros H x y Hp Hq.
  apply NNPP. revert dependent Hq. apply not_and_impl_not.
  revert dependent y. apply not_ex_all_not.
  revert dependent Hp. apply not_and_impl_not.
  revert dependent x. apply not_ex_all_not. apply H.

На самом деле, существует тактика автоматизации под названием firstorder, которая (как вы уже догадались) решает интуиционистскую логику первого порядка.Обратите внимание, что NNPP все еще требуется, поскольку firstorder не поддерживает классическую логику. 

Theorem t3: forall (T: Type), forall p q: T -> Prop, forall r: T -> T -> Prop, 
~(exists (x: T), ((p x) /\ (exists (y: T), ((q y) /\ ~(r x y)))))
<-> forall (x y: T), ((p x) -> (((q y) -> (r x y)))).
Proof.
intros T p q r.
split.
- intros H x y Hp Hq. apply NNPP. firstorder.
- firstorder. Qed.
...