(*
   Using the command Goal we enter the proof mode and set the
   proposition that we will try to prove.
*)

Goal forall A B C: Prop, (A -> B -> C) -> (A -> B) -> (A -> C).
intros.
apply H.
assumption.
apply H0.
assumption.
(**  
  The proof is now complete. It can be saved for future use 
 with the command Save, followed by a name for the new
 theorem. This also ends the proof mode.
*)
Save Tautology1.

(**  
  To prove and save the result above, we could also have 
 stated it as a Theorem or Lemma, as follows: 
*)

Lemma Tautology1': 
forall A B C:Prop, (A -> B -> C) -> (A -> B) -> (A -> C).
Proof.
intros.
apply H.
assumption.
apply H0.
assumption.
Qed.

Section Implication_Logic.
Variable A B C : Prop.

Lemma ex_1b : (A -> B) -> (B -> C) -> (A -> C).
Admitted.

Lemma ex_1c : (A -> A -> B) -> (A -> B).
Admitted.

Lemma ex_1d : (A -> B) -> (A -> A -> B).
Admitted.

Lemma ex_2a : (A -> B) -> ~B -> ~A.
Admitted.

End Implication_Logic.

Section And_Or.

Variable A B C : Prop.

Lemma prop_001 : (A /\ B) -> (B /\A).
intro H.
elim H.
intros H1 H2.
split.
assumption. 
assumption.
Qed.

Lemma prop_001a : (A \/ B) -> (B \/ A).
intro H.
elim H.
intro H1.
right.
assumption. 
left. 
assumption.
Qed.

Lemma prop_001b : (A \/ B)/\C -> (A \/ B)/\(A\/C).
Admitted.
(* use just intros apply assumption elim split left right *)

Lemma prop_001c : (A \/ B -> C) -> (A -> C)/\(B -> C).
Admitted.

(* This one is found tricky *)
Lemma prop_037 : ((A /\ B) -> C) -> ((A -> C) \/ (B -> C)).
Admitted.

Lemma prop_035 : (A -> (B -> C)) /\ (A -> B) -> (A -> C).
Admitted.

End And_Or.

Section Negation.

Variable A B C : Prop.

(* ~A is defined as A -> False, where from False we can derive anything *)

Theorem prop_026 : (~A /\ ~B) -> ~(A \/ (~A /\ B)).
intro H.
intro H1. (* Here we exploit that ~(A \/ (~A /\ B)) is just (A \/ (~A /\ B)) -> False *)
elim H1.
intro H2.
elim H.
intros H3 H4.
apply H3. (* remember that ~A is just A -> False *)
assumption.
intro H2.
elim H.
intros H3 H4.
elim H2.
intros H5 H6.
contradiction. 
(* This simplifies things a bit; it checks if a False is derivable
   from the context and then closes *) 
Qed.

Lemma ex_2c : ~~~A -> ~A.
Admitted.

Lemma ex_2d : (A -> ~A) -> ~A.
Admitted.

Lemma prop_014 : (~(A /\ A) -> (~A \/ ~A)).
Admitted.

Lemma ex_2e : (A -> B) -> (A -> ~B) -> A -> C.
intros H1 H2 H3.
absurd B. 
(* This says that B and ~B is derivable, and so we have False, from which anything follows *) 
apply H2.
assumption.
exact (H1 H3).
Qed.

End Negation.

(* Tired of constantly doing disjunction/conjunction elimination,
   followed by arrow introduction? You may consider to try the
   'destruct' tactic next time. 
*)

Section Classical.

Require Import Classical.

(* It provides the axiom of excluded middle (amoung other things) *)
Check classic.
(* One way of using it in the proofs is by means of the elimination
   rule for disjunction:
    elim (classic A)
*)

Variable A B C : Prop.

Theorem dn_law : ~~A -> A.
elim (classic A).
intros; assumption.
intros; contradiction.
Qed.
(* Here we start "chaining tactics" ; is sequential composition 
   t1 ; t2 means that t2 is applied to _all_ goals generated by t1 *)   

Lemma prop_002 : (~A -> A) -> A.
Admitted.

Lemma prop_003 : (~A -> A) \/ ~A.
Admitted.

Lemma prop_025 : A -> (~B \/ (A /\ B)).
Admitted.

Lemma prop_021 : ~A \/ (B -> A).
Admitted.

Lemma prop_065 : (A /\ B) \/ ~B -> B -> (A /\ B).
Admitted.

Lemma prop_104 : (A \/ B) -> ~(~A /\ ~B).
Admitted.

End Classical.

Section Assorted.
Variable A B C D: Prop.

(* We do a bit of chaining and tactic combination in the next proof Try for ytourself *)
Lemma prop_085 : ~((A -> (B \/ ~C)) /\ (B -> ~A) /\ (A -> C) /\ A).
Proof.
intro H.
destruct H as [H [H1 H2]].
(* Does the same as destruct H. destruct H1. destruct H2. *)
destruct H.
destruct H2; assumption.
apply H1. 
assumption.
destruct H2.
assumption.
apply H.
destruct H2.
apply (H0 H2).
Qed.

(* tricky; can be done without classical logic *)
Lemma prop_063 : ~~((~A -> B) /\ (~A -> ~B) -> A).
Admitted.

Lemma prop_082 : (A -> B) /\ (C -> D) -> (~B \/ ~D) -> (~A \/ ~C).
Admitted.

(* A variant of De Morgan; use classical logic here *)
Lemma prop_106 : ~(~A /\ ~B) -> (A \/ B).
Admitted.

End Assorted.