Variables P, Q, R, S : Prop.

Theorem absurd : S /\ ~S -> Q.

Intro H.
Elim H.
Intros H0 H1.
Unfold not in H1.
Elim H1.
Undo 2.
Elim H1.
Assumption.
Save.




Theorem conj_disj : P/\Q -> P\/Q.

Intro H.
Elim H.
Clear H.
Intros H H0.
Left.
Assumption.
Save.

Print Proof  conj_disj.



Theorem pc : (P->Q) /\ (R->S) -> (P/\R -> Q/\S).

Intros H H0.
Elim H; Clear H; Elim H0; Clear H0.
Intros H H0 H1 H2.
Split.
Apply H1; Assumption.
Apply H2; Assumption.
Save.

Check pc.

(*---------- Questao 6A --------- *)

Theorem q6A : P /\ (Q \/ R) -> (P /\ Q) \/ (P /\ R).

Intros.
Elim H.
Intros.
Elim H1.
Intros.
Left.
Split.
Assumption.
Assumption.
Intros.
Right.
Split.
Assumption.
Assumption.
Qed.


(*---------- Questao 6B --------- *)

Theorem q6B : (P /\ Q) \/ R -> (P \/ R) /\ (Q \/ R).

Intros.
Split.
Elim H.
Intros.
Left; Elim H0; Intros; Assumption.
Intros; Right; Assumption.
Elim H.
Intros.
Left; Elim H0; Intros; Assumption.
Intro; Right; Assumption.
Qed.



(*---------- Questao 6C --------- *)

Theorem q6C : (P /\ Q) \/ (P /\ R) -> P /\ (Q \/ R).

Intros.
Split.
Elim H.
Intro.
Elim H0.
Intros.
Assumption.
Intros.
Elim H0.
Intros.
Assumption.
Elim H.
Intro.
Left.
Elim H0; Intros; Assumption.
Intro.
Right.
Elim H0; Intros; Assumption.
Qed.

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


Check ex.

Variable U : Set.
Variable C : U -> Prop.
Check (ex U [x:U](C x)).

Check (Ex [x:U](C x)).


Variable D : Set.
Variables A, B : D -> Prop.

Goal (Ex [x:D]((A x) -> (B x))) -> ((x:D)(A x)) -> (Ex [x:D](B x)).
Intros H H0.
Elim H; Clear H.
Intros y H.
Exists y.
Apply H.
Apply H0.
Abort.




(* ----------------- Questao 7A ------------------ *)

Lemma q7A : (Ex [x:D] (A x)\/(B x)) -> (Ex [x:D] (A x)) \/ (Ex [x:D] (B x)).

Intros.
Elim H.
Intros.
Elim H0.
Intros; Left; Exists x; Assumption.
Intros; Right; Exists x; Assumption.
Qed.


 (* ----------------- Questao 7B ------------------ *)

 Lemma q7B : (Ex [x:D] (A x)/\(B x)) -> (Ex [x:D] (A x)) /\ (Ex [x:D] (B x)).

Intros.
Split.
Elim H.
Intros.
Exists x.
Elim H0.
Intros; Assumption.
Elim H.
Intros.
Exists x.
Elim H0.
Intros; Assumption.


Restart.
Intros; Split; Elim H; Intros; Exists x; Elim H0; Intros; Assumption.

Qed.






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


Section tmp.

Variable P : D -> D -> Prop.

Goal ((x:D)(Ex [y:D] (P x y))) -> (Ex [y:D] (x:D) (P x y)).

Intros.
(* ??????????? *)
Abort. 


(* -----  Extra ------ *)

Goal  (Ex [y:D] (x:D) (P x y)) -> ((x:D)(Ex [y:D] (P x y))).

Intros.
Elim H.
Intros.
Exists x0.
Apply H0.
Qed.


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


Section Classical.

Hypothesis raa  : (A:Prop) ~~A -> A.
Theorem tnd : (A:Prop) A \/ ~A.
Intro A0.
Apply raa.
Red.
Intro.
Elim H.
Left.
Apply raa.
Red.
Intro.
Elim H.
Right.
Assumption.

Restart.
Intro A0.
Apply raa.
Red.
Intro.
Cut ~A0.
Intro H0.
Elim H.
Right; Assumption.
Red.
Intro H0.
Elim H.
Left; Assumption.

Restart.
Intro A0.
Apply raa.
Red.
Intro.
Cut ~A0.
Auto.
Red.
Auto.

Restart.
Intro A0; Apply raa; Red; Intro; Cut ~A0; [Auto | Red; Auto].

Restart.
Unfold not; Unfold not in raa; Intro; Apply raa; Auto.
Save.

Check tnd.

End Classical.

Check tnd.



Section Classical2.

Hypothesis te : (X:Prop) X \/ ~X.

Theorem raa : (Y:Prop) ~~Y -> Y.

Intros Y H.
(* Elim te. *)
Elim te with Y.
Auto.
Intro H0.
Elim H.
Assumption.


Restart.
Intros Y H; Elim te with Y; [Auto | Intro H0; Elim H; Assumption].

Save.


Theorem dq : ((x:D) ~(A x)) \/ (Ex [x:D] (A x)).

Elim (te (Ex [x:D] (A x))).
Auto.
Intro H.
Left.
Intro x.
Red; Intro. Elim H.
Exists x.
Exact H0.

Restart.
Elim (te (Ex [x:D] (A x))); 
    [Auto | Intro H; Left; Intro x; Red; Intro; Elim H; Exists x; Exact H0].
Save.

End Classical2.
  
Section Exercicio.

Variable A, B : Prop.
Variable D : Set.
Variable M : D -> Prop.

Hypothesis raa : (A:Prop) ~~A -> A.

Goal (A -> B) -> (~A \/ B).

Intros.
Apply raa.
Unfold not.
Intros.
Elim H0.
Left.
Intro.
Apply H0.
Right.
Apply H; Assumption.

Save e1.


Goal ~(Ex [x:D] ~(M x)) -> (x:D)(M x).

Intros.
Apply raa.
Red.
Unfold not in H.
Intros.
Apply H.
Exists x.
Assumption.

Save e2.


 
End Exercicio.