Require Import Bool Arith List.

Variables P Q R : Prop.

Lemma example1 : P -> P.
Proof.
intros P_is_true.
exact P_is_true.
Qed.

Lemma example4 : (P -> Q) -> P -> Q.
Proof.
intros Q_if_P.
intros P_is_true.
apply Q_if_P.
exact P_is_true.
Qed.

Lemma example5 : (P -> R) -> P -> P /\ R.
Proof.
intros R_if_P.
intros P_is_true.
split.
  exact P_is_true.
apply R_if_P.
exact P_is_true.
Qed.

Lemma example6 : (P -> R -> Q) -> P /\ R -> Q.
Proof.
intros Q_if_PR.
intros PR_are_true.
apply Q_if_PR.
  destruct PR_are_true as [P_is_true R_is_true].
  exact P_is_true.
destruct PR_are_true as [P_is_true R_is_true].
exact R_is_true.
Qed.

Lemma example6bis : (P -> R -> Q) -> P /\ R -> Q.
Proof.
intros Q_if_PR.
intros PR_are_true.
destruct PR_are_true as [P_is_true R_is_true].
apply Q_if_PR.
  exact P_is_true.
exact R_is_true.
Qed.

Lemma example7 : P \/ Q -> Q \/ P.
Proof.
intros PQ_is_true.
destruct PQ_is_true as [P_is_true | Q_is_true].
  right.
  exact P_is_true.
left.
exact Q_is_true.
Qed.

Lemma example_not : P -> ~ P -> Q.
Proof.
intros P_is_true.
intros notP_is_true.
case notP_is_true.
exact P_is_true.
Qed.







(* STOP *)








Lemma example2 : forall n : nat, n = n.
Proof.
intros n.
reflexivity.
Qed.

Lemma example3 : 7 = 3 + 4.
Proof.
reflexivity.
Qed.

Lemma example10 : forall n, n = 3 -> n + 7 = 10.
Proof.
intros n.
intros n_is_3.
rewrite -> n_is_3.
reflexivity.
Qed.

Lemma example11 : forall n, 3 = n -> n + 7 = 10.
Proof.
intros n.
intros n_is_3.
rewrite <- n_is_3.
reflexivity.
Qed.

Lemma example13 : forall (i : nat), i = 3 -> 2 * i = 6.
Proof.
intros i.
intros i_is_3.
rewrite i_is_3.
reflexivity.
Qed.

Lemma example14 :
  forall (V W : nat -> Prop), 
  (forall (i : nat), V i -> W i) -> V 3 -> W 3.
Proof.
intros V W.
intros Vi_to_Wi.
intros V3.
apply Vi_to_Wi.
exact V3.
Qed.

Lemma example15 :
  forall (V : nat -> Prop),
  (forall (i : nat), V i -> P) -> V 3 -> P.
Proof.
intros V.
intros Vi_to_P.
intros V3.
apply Vi_to_P with ( i := 3 ).
exact V3.
Qed.

Lemma example8 : exists (n : nat), n = 4.
Proof.
exists (2 + 2).
reflexivity.
Qed.

Lemma example12 :
  forall (V W : nat -> Prop),
  (exists (i : nat), W i) ->
  (forall j, W j -> V j) ->
   exists (j : nat), V j.  
Proof.
intros V W.
intros exiW.
intros Wj_to_Vj.
destruct exiW as [k Wk].
exists k.
apply Wj_to_Vj.
exact Wk.
Qed.

Lemma example_arith : forall a b, a + (b + b) = (b + a) + b.
Proof.
intros a b.
SearchAbout (_ + _ + _).
rewrite -> plus_assoc.
SearchAbout (_ + _ = _ + _).
rewrite -> (plus_comm a b).
reflexivity.
Qed.