(* 
All exercises are theorems to be proved using basic tactics,
such as :
- intro 
- intros
- exact
- apply
- left
- right
- destruct

Notice: an exercise is successfully finished
when "Admitted" is replaced by "Qed"

The effect of the keyword "Admitted" is to stop the exercise:
the formula to be proved is then admitted as an axiom.
*)


Section sec_ex1.

Variables A B C : Prop.

(* Prove the following formulas. *)

Theorem t1 : A -> B -> A.
Proof.

Admitted.

Theorem t2 : A -> B -> A /\ B.
Proof.

Admitted.

Theorem t3 : A /\ B -> A.
Proof.

Admitted.

Theorem t4 : A -> A \/ B.
Proof.

Admitted.

Theorem t5 : B /\ C -> A \/ B.
Proof.

Admitted.

Theorem t6 : A -> not (not A).
Proof.

Admitted.

Theorem t7 : (not A \/ B) -> A -> B.
Proof.

Admitted.

(* Prove the following De Morgan's laws. *)

Lemma not_and :
  not A \/ not B -> not (A /\ B).
Proof.

Admitted.

Lemma not_or :
 not A /\ not B -> not (A \/ B).
Proof.

Admitted.

Lemma and_not :
  not (A \/ B) -> not A /\ not B.
Proof.

Admitted.

(* Prove the following implication. *)

Theorem t8 : ((A /\ B) \/ (not A /\ not B)) -> (A <-> B).
Proof.

Admitted.

(* Prove the associativity of logical connectives "/\" and "\/". *)

Lemma and_assoc :
  (A /\ (B /\ C)) <-> ((A /\ B) /\ C).
Proof.

Admitted.

Lemma or_assoc :
  (A \/ (B \/ C)) <-> ((A \/ B) \/ C).
Proof.

Admitted.

(* Prove the distributivity of each connective "/\" and "\/" with respect to the other. *)

Lemma and_or :
  (A /\ C) \/ (B /\ C) <-> (A \/ B) /\ C.
Proof.

Admitted.

Lemma or_and :
  (A \/ C) /\ (B \/ C) <-> (A /\ B) \/ C.
Proof.

Admitted.

(* State and prove a lemma "elim_and" such that "apply elim_and" behaves almost
  like "destruct c as [a1 a2]" when c proves a conjunction. *)
(* Once the lemma is proved, show how to use it so that it behaves exactly the same? *)

Lemma elim_and :
  forall H1 H2 G : Prop,
  to_be_filled -> (H1 /\ H2 -> G).
Proof.

Admitted.

Theorem t9 : A /\ B -> B /\ A.
Proof.
intros H.
(* ... by using "apply elim_and" instead of "destruct" *)

Admitted.

(* Same question with "destruct d as [c1 | c2]" when d proves a disjunction. *)

Lemma elim_or :
  forall H1 H2 G : Prop,
  to_be_filled -> (H1 \/ H2 -> G).
Proof.

Admitted.

Theorem t10 : A \/ B -> B \/ A.
Proof.

Admitted.

(* Prove the following formula. Suggestion: first prove "not (not A /\ not (not A))". *)

Theorem t11 : not (not (not (not A) -> A)).
Proof.

Admitted.

End sec_ex1.