(* REALIZAR Y COMPLETAR. NO ESTA PERMITIDO EL USO DE AUTO NI TAUTO *)

Section EjemplosCalculoProposicional1.

Variables A,B,C:Prop.

Lemma distr_impl : (A->(B->C))->(A->B)->(A->C).
Intros hip1 hip2 hip3.
Generalize (hip2 hip3); Intro prop4.
Generalize (hip1 hip3); Intro prop5.
Generalize (prop5 prop4); Intro H.
Exact H.
Save.

Lemma and_commutative : (A /\ B) -> (B /\ A).
Intro hip1.
Elim hip1; Intros prop2 prop3.
Split.
Exact prop3.
Exact prop2.
Save.

Lemma or_commutative : (A \/ B) -> (B \/ A).
Intro hip1.
Elim hip1; [Intro hip2 | Intro hip51].
Right.
Exact hip2.
Left.
Exact hip51.
Save.

End  EjemplosCalculoProposicional1.

(*EXPLICA LOS TIPOS QUE TIENEN AHORA LAS CONSTANTES QUE SE HAN INTRODUCIDO
HASTA AHORA.*)




Section EjemploSecuentes.

Variables p,q:Prop.
Hypothesis premisa1: ~p \/ q.

Lemma ejemplo1 : p -> q.
Elim premisa1; [Intro hip2 | Intro hip51].
Intro hip3.
Absurd p; Try Assumption.
Intro hip52.
Assumption.
Save.

End EjemploSecuentes.


Section Regla_MT.

Variables A,B:Prop.
Hypothesis premisa1 : A->B.
Hypothesis premisa2 : ~B.

Theorem MT : ~A.
Intro hip3.
Generalize (premisa1 hip3); Intro prop4.
Absurd B; Try Assumption.
Save.

End Regla_MT.


Section IntDN.

Variable x:Prop.
Lemma dn:~~(x\/~x).
Proof.
Intro hip1.
Apply hip1.
xxxxxxxxxxxxxxxx.
xxxxxxxxxxxxxxxx.
xxxxxxxxxxxxxxxx.
xxxxxxxxxxxxxxxx.
Qed.

End IntDN.

Section DN_TE.

Hypothesis dni:(x:Prop)~~x->x.

Variable P:Prop.

Theorem te: P\/~P.
Proof.
Generalize (dni P\/~P).
xxxxxxxxxxxxxxx.
xxxxxxxxxxxxxxx.
xxxxxxxxxxxxxxx.
Qed.

End DN_TE.

Theorem te_dn: ((P:Prop)P\/~P) -> ((x:Prop)~~x->x).
Proof.
Intros H x H0.
Elim (H x).
xxxxxxxxxxxxxxxxxxxx.
xxxxxxxxxxxxxxxxxxxx.
xxxxxxxxxxxxxxxxxxxx.
Qed.


Section Pierce.

Variables p,q:Prop.

Theorem Pierce : ((p -> q) -> p) -> p.
Intro hip1.
Require Classical.
Apply NNPP.
Intro hip2.
Generalize (MT (p->q) p hip1 hip2); Intro hip3.
xxxxxxxxxxxxxxxxxxxxx.
xxxxxxxxxxxxxxxxxxxxx.
xxxxxxxxxxxxxxxxxxxxx.
Save.

End Pierce.


Section Quantificador1.

Variable tm:Set.
Variables P,Q:tm->Prop.

Hypothesis premisa1: (x:tm)(P x)->(Q x).
Hypothesis premisa2: (x:tm)(P x).

Lemma Q1 : (x:tm)(Q x).
Intro x0.
Generalize (premisa1 x0); Intro prop3.
xxxxxxxxxxxxxxxxxxx.
xxxxxxxxxxxxxxxxxxx.
xxxxxxxxxxxxxxxxxxx.
Save.

End Quantificador1.

Section Quantificador2.

Variable tm:Set.
Variables P,Q:tm->Prop.

Hypothesis premisa1: (x:tm)(P x)->(Q x).
Hypothesis premisa2: (EX x:tm | (P x)).

Lemma Q2 : (EX x:tm | (Q x)).
Elim premisa2; Intros x0 assump3.
xxxxxxxxxxxxxxxxxx.
xxxxxxxxxxxxxxxxxx.
Exists x0.
Assumption.
Save.

End Quantificador2.


Section Ejemplo_eq.

Variables x,y:nat.

Hypothesis premisa1 : y=x.
Hypothesis premisa2 : O=y.


Lemma simple : x=O.
Rewrite <- premisa1.
xxxxxxxxxxxxxxxxx.
xxxxxxxxxxxxxxxxx.
Save.

End Ejemplo_eq.