ProofWeb

Oficial Site - ProofWeb
Oficial Site - ©ProofWeb
RU SURF VU LoLITA - DIMAp/UFRN
LoLITA - DIMAp/UFRN

Working with ProofWeb

Tips on First Ordem Logic


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.