(* Logica Proposicional e Logica Proposicional de Segunda Ordem *)

Variable A : Prop.

Theorem trivial : A -> A.
Intro hip1.
Exact hip1.
Save.
Print Proof trivial.



Section Hilbert1.
Variables A, B : Prop.

Theorem K : A->B->A.
Intros.
Assumption.
Save.
Print Proof K.

End Hilbert1.
Check K.


Section Hilbert2.

Theorem S : (A,B,C:Prop)(A->B->C)->(A->B)->(A->C).
Intro.
Intro.
Intro.
Intros H H0 H1.
Apply H.
Assumption.
Apply H0.
Assumption.
Save.

End Hilbert2.


(* -------------- Questao ? --------------------------- *)


Print not.

Section s1.

Variables A, B : Prop.
Theorem t1 : (A->B) -> (~B -> ~A).
Intros H H0.
Unfold not.
Unfold not in H0.
Intro H1.
Apply H0 ; Apply H ; Exact H1.
Save.

End s1.
Print Proof t1.

(* Exercicio *)

Lemma ex : (A:Prop) A -> ~~A.
Intros.
Unfold not.
Intro.
Apply H0 ; Assumption.
Qed.

Print ex.

(* Logica de Predicados de Primeira Ordem *)

Section Pred.

Variable D : Set.
Variable P : D -> Prop.
Variable Q : D -> D -> Prop.


Section Pred1.
Theorem pred1 : (y:D)((x:D)(P x)) -> (P y).
Intros y H.
Apply H.
Save.
End Pred1.
Print Proof pred1.

Section Pred2.
Theorem pred2 : ((x,y:D)(Q x y)) -> (x,y:D)(Q y x).
Intros H x y ; Apply H.
Save.
End Pred2.

End Pred.

(* ----- Questoes ---- *)


(* Logica Proposicional: as conectivas que faltam I *)

Section E.

Definition e := [P,Q:Prop](A:Prop)(P->Q->A)->A.
Check e.

Theorem conj_e1 : (U,V:Prop)(e U V)->U.
Intros U V H.
Unfold e in H.
Apply H.
Intros ; Assumption.
Save.

Print conj_e1.

(* ----------- Exercicio ------- *)

Theorem conj_i : (U,V:Prop) U->V->(e U V).
Intros.
Unfold e.
Intros.
Apply H1.
Assumption.
Exact H0.
Qed.

(* ------ *)

Variable E : Prop -> Prop -> Prop.
Hypothesis Iconj : (A,B:Prop) A -> B -> (E A B). 
Hypothesis Econj1 : (A,B:Prop) (E A B) -> A.
Hypothesis Econj2 : (A,B:Prop) (E A B) -> B.

Theorem def_conj : (P,Q:Prop)(E P Q) -> (e P Q).
Red.
Intros P Q H A0 H0.
Apply H0.
Apply Econj1 with Q.
Assumption.
Apply Econj2 with P.
Assumption.
Save.

End E.

Check def_conj.