Require Import ProofWeb.
(* Ilustração de teoremas em Lógica de Primeira Ordem. *)
Variable P : D -> Prop.
Variable Q : D * D -> Prop.
Variable R : D * D * D -> Prop.
(* Estratégia para trás *)
Theorem exemplo_01 : all x, P(x) -> all y, P(y).
Proof.
imp_i H.
all_i z.
all_e (all x, P(x)).
ass H.
Qed.
(* Estratégia para frente *)
Theorem exemplo_02 : all x, P(x) -> all y, P(y).
Proof.
imp_i H.
all_i z.
f_all_e H.
Qed.
(* O próximo caso pode ser resolvido sem eliminar ou introduzir os *)
(* quantificadores, uma vez que os nomes das variáveis ligadas não importam. *)
Theorem exemplo_03 : all x, P(x) -> all y, P(y).
Proof.
imp_i H.
ass H.
Qed.
(* O próximo caso só é demonstrável se houver um termo conhecido na linguagem. *)
Variable i : D.
Theorem exemplo_04 : all x, P(x) -> exi x, P(x).
Proof.
imp_i H.
exi_i i.
all_e (all x, P(x)).
ass H.
Qed.
(* Estratégia "Para frente". *)
Theorem exemplo_05 : all x, P(x) -> exi x, P(x).
Proof.
imp_i H.
insert H1 (P(i)).
f_all_e H.
f_exi_i H1.
Qed.
(* Utilizando a Eliminação do Existencial: Para frente *)
Theorem exemplo_06 : exi x, ~P(x) -> ~all x, P(x).
Proof.
imp_i H.
neg_i H1.
exi_e (exi x, ~P(x)) y H2.
ass H.
neg_e (P(y)).
ass H2.
all_e (all x, P(x)).
ass H1.
Qed.
(* Para trás *)
Theorem exemplo_07 : exi x, ~P(x) -> ~all x, P(x).
Proof.
imp_i H.
neg_i H1.
f_exi_e H y H2.
insert H3 (P(y)).
f_all_e H1.
f_neg_e H2 H3.
Qed.
(* Ilustração de estratégia heurística útil. *)
Variable S : D -> Prop.
Hypothesis P1: (all x, P(x)/\exi y, S(y)).
Theorem exemplo_08 : all x, exi y, ( P(x)/\S(y)).
Proof.
(* Sempre tente utilizar primeiro as regras de Introdução do Universal... *)
all_i j.
(* ...e de Eliminação do Existencial. *)
exi_e (exi y, S(y)) k H0.
(* Motivo: Essas regras no ProofWeb introduzem termos que poderão ser *)
(* utilizados pela Introdução do Existencial e pela Eliminação do Universal *)
f_con_e2 P1.
exi_i k.
con_i.
all_e (all x, P(x)).
f_con_e1 P1.
ass H0.
Qed.