Require Import ProofWeb.
(* Exemplos na lógica proposicional *)
Variables A B C : Prop.
(*Primeiro uma demonstração usando apenas regras "Backward"
(para trás - seguindo da conclusão às premissas) *)
Theorem example_01 : A /\ B -> B /\ A.
Proof.
imp_i H.
con_i.
con_e2 (A).
(* Insere um "A" numa conjunção com B *)
ass H.
con_e1 (B).
ass H.
Qed.
(* mesma demonstração usando o máximo de regras "Forward" possíveis
(para frente - seguindo das premissas à conclusão) *)
Theorem example_02 : A /\ B -> B /\ A.
Proof.
imp_i H.
insert H1 (A).
(* insere a hipótese A para que ela possa ser usada na introdução da conjunção para frente *)
f_con_e1 H.
insert H2 (B).
f_con_e2 H.
f_con_i H2 H1.
Qed.
(* Utilizando táticas mistas "Forward" e "Backward" (para frente e para trás) *)
Theorem example_03 : A /\ B -> B /\ A.
Proof.
imp_i H.
con_i.
f_con_e2 H.
f_con_e1 H.
Qed.
(* Um exemplo com a eliminação da disjunção usando apenas táticas "Backward" *)
Theorem example_04 : A \/ B -> B \/ A.
Proof.
imp_i H.
dis_e (A \/ B) H1 H2.
ass H.
dis_i2.
ass H1.
dis_i1.
ass H2.
Qed.
(* ... e uma solução bem menor usando apenas táticas "Forward" *)
Theorem example_05 : A \/ B -> B \/ A.
Proof.
imp_i H.
f_dis_e H H1 H2.
(* Para reduzir o tamanho da derivação, a eliminação da disjunção
deve ser aplicada antes de outras regras... *)
f_dis_i2 H1.
(* Nesta caso, se a eliminação da disjunção fosse utilizada depois de outras regras,
não se conseguiria demonstrar *)
f_dis_i1 H2.
Qed.
(* Exemplo de uma demonstração intuicionista com várias negações *)
Theorem example_06 : ~~(~~A -> A).
Proof.
neg_i H.
insert H1 (~~A -> A).
imp_i H2.
insert H3 (~A).
neg_i H4.
neg_e (~~A -> A).
(* Aplicada regra "Backward" em que surgem as duas fórmulas eliminadas pela negação *)
ass H.
imp_i H5.
ass H4.
fls_e.
f_neg_e H2 H3.
f_neg_e H H1.
Qed.
(* Demonstrando a Lei do terceiro excluido *)
Theorem example_07 : A \/ ~A.
Proof.
PBC H0.
(*... assim como a Eliminação da Disjunção, deve-se usar o Absurdo Clássico antes
de outras regras... *)
(* a idéia é ter o máximo de hipóteses para se trabalhar na demonstração,
e as regras PBC e dis_e fazem isso... *)
neg_e (A \/ ~ A).
ass H0.
(* Observe que estamos com a mesma fórmula, mas agora temos uma hipótese H0 adicional *)
dis_i2.
neg_i H1.
neg_e (A \/ ~ A).
ass H0.
(* mais uma vez estamos com a mesma fórmula, mas agora temos duas hipóteses H0 e H1 *)
dis_i1.
ass H1.
(* Pronto!!! *)
Qed.