(** * Introduction to Rocq

 To prove a result, we announce it as a Theorem or Lemma, 
 with a name, as follows. *)

Lemma Tautology: 
forall A B C:Prop, (A -> B -> C) -> (A -> B) -> (A -> C).
(** Then we give the proof using tactics; we are now in "proof mode" 
   We start with [Proof], which is not mandatory but clarifies the structure *)
Proof.
intros.
(** moves as many hypotheses as possible to the context *) 
apply H.
(** applies hypothesis [H] to prove [C] *) 
assumption.
(** searches for a variable of type [A] in the context *)
apply H0. 
assumption.
(**  The proof is now complete. It is saved for future use 
  with the command [Qed.] We can refer to this proof by the name we have given: [Tautology]
  This ends the proof mode.
*)
Qed.

(** Here is the same proof with bulleting to improve the structure and make subgoals explicit *)
Lemma Tautology': 
forall A B C:Prop, (A -> B -> C) -> (A -> B) -> (A -> C).
Proof.
intros.
apply H.
- assumption.
- apply H0. assumption.
(** See the files by Jules Jacobs on the webpage for further explanation on 
    the bulleting and indentation *)
Qed.

(** * Implication_Logic *)
Section Implication_Logic.
Variable A B C : Prop.
(** It is nicer to not quantify over [A B C : Prop] all the time but to keep
   these global within a Section *)

(** TODO: use just [intros] [apply] [assumption] to prove the following. 
 So you have to replace each [Admitted] by a proof script ending in [Qed.]
*)

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.

End Implication_Logic.

(** * Conjunction and disjunction *)
Section And_Or.

Variable A B C : Prop.

Lemma prop_001 : (A /\ B) -> (B /\ A).
Proof.
intro H.
destruct H as [H1 H2].
(** Also try#<br># 
      [destruct H.]#<br>#
   or #<br>#
      [elim H.
      intros H1 H2.]#<br>#
   or #<br>#
      [case H.]#<br>#
   The primitive tactic is [elim].#<br># 
   [destruct] basically does an [intros] immediately after the [elim].#<br>#
   [destruct H as [H1 H2]] does the intros with the given names; here [[H1 H2]]
   describes the "intro pattern" for [/\]: we get two pieces of data, 
   [H1:A] and [H2:B]
*)
split.
- assumption. (** or: [exact H2.] in case you want to name the assumption *) 
- assumption.
Qed.

Lemma prop_001a : (A \/ B) -> (B \/ A).
Proof.
intro H.
destruct H as [H1 | H2].
(** Also try #<br>#
      [destruct H.]#<br>#
   or #<br>#
      [elim H.
      intros H1.]#<br>#
   or #<br>#
      [case H.]#<br>#
  Here [[H1 | H2]] describes the "intro pattern" for [\/]: we get a case split, 
  as we get two cases, one with [H1:A] and one with [H2:B].
*)
- right. assumption. 
- left; assumption. 
(** The ; is for "chaining" tactics. The second tactic is applied to _all_ goals
   generated by the first tactic *)
Qed.

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

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

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

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

End And_Or.

(** * Negation *)

Section Negation.

Variable A B C : Prop.

(** The negation of [A], [not A], with notation [~A], is defined as [A -> False], 
   where from [False] we can derive anything. #<br>#
   Type [unfold not] to unfold the definition of [~A] into [A -> False]
   and then you can apply your usual tactics *)

Lemma ex_2a : (A -> B) -> ~B -> ~A.
Proof.
intros H H0.
intro H1. (** or [unfold not. intro H1] *)
apply H0.
apply H.
assumption.
Qed.


Theorem prop_026 : (~A /\ ~B) -> ~(A \/ (~A /\ B)).
(** NB Theorem does the same as Lemma, it is just for you if you want to
   distinguish between main results and auxiliary results*)
Proof.
intros.
intro H1. 
(** Here we exploit that [~(A \/ (~A /\ B))] is just [(A \/ (~A /\ B)) -> False] #<br># 
   Rocq does not automatically unfold this definition, 
   but when we say [intro H1] it does. #<br>#
   Try: [unfold not] to unfold the definition of [~] *)
destruct H1 as [H2|H3]. (** Note that [A \/ ~ A /\ B] means [A \/ (~ A /\ B)] *)
- destruct H as [H4 H5].
  apply H4. (** remember that [~A] is just [A -> False] *)
  assumption.
- destruct H as [H4 H5].
  destruct H3 as [H6  H7].
  contradiction. 
(** This simplifies things a bit; Rocq tries to derive [False] in the present context and if
   it succeeds, the proof is finished, as everything is provable from [False] *) 
Qed.

Lemma ex_2c : ~~~A -> ~A.
Proof.
intros.
unfold not.
intros.
apply H. (** [~~~A] is just [(~~A) -> False] *)
intro H1. (** forces Rocq to consider [~~A] as [(~A) -> False]; just [intros] does not do this *)
contradiction. (** or [apply H1] etc *) 
Qed.

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

Lemma prop_065 : (A /\ B) \/ ~B -> B -> (A /\ B).
Proof.
intros.
destruct H as [H1|H2].
- exact H1.
- contradiction.
Qed.

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

Lemma ex_2e : (A -> B) -> (A -> ~B) -> A -> C.
Proof.
intros H1 H2 H3.
absurd B. 
(** This says that [B] and [~B] are derivable, and so we have [False], from which anything follows *) 
- apply H2. 
  assumption.
- exact (H1 H3). 
(** Note that you can also destruct/apply/elim larger terms, like [H1 H3] here,
    you don't just have to refer to variables *) 

(** Also try typing [intuition] immediately after [intros H1 H2 H3] #<br>#
   [intuition] does some simple proposition logic steps automatically *)
Qed.

End Negation.

(** * Classical Logic *)
Section Classical.

Require Import Classical.

(** It provides "excluded middle" as an axiom *)
Check classic.
(** One way of using it in the proofs is by means of the elimination
   rule for disjunction:
    [destruct (classic A)]
*)

Variable A B C : Prop.

Theorem dn_law : ~~A -> A.
Proof.
destruct (classic A).
- intros. assumption.
- intros. contradiction.
Qed.
(** Again, we "chain tactics". The ; 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.
Proof.
destruct (classic A) as [Ha | Hna]. 
- left. intro H. assumption.
- right. assumption.  
Qed.

Lemma prop_025 : A -> (~B \/ (A /\ B)).
Proof.
intros H. destruct (classic B) as [Hb | Hnb].
- right; split; assumption.
- left. assumption.
Qed. 

Lemma prop_021 : ~A \/ (B -> A).
Proof.
destruct (classic A) as [Ha | Hna].
- right; intros; assumption.
- left; assumption.
Qed.

(** This one can also be done without classical logic *)
Lemma prop_065b : (A /\ B) \/ ~B -> B -> (A /\ B).
Proof.
intros H H1.
split.
- destruct H as [Hl | Hr].
  * destruct Hl; assumption.
  * contradiction.
- assumption.
Qed.

(** The following one can be done without classical logic *)
Lemma prop_104 : (A \/ B) -> ~(~A /\ ~B).
Proof.
intros H H1.
destruct H as [Ha | Hb].
- destruct H1 as [Hna Hnb].
  contradiction.
- destruct H1 as [Hna Hnb].
  contradiction.
(** or just #<br>#
 [intros H H1.] #<br>#
 [destruct H as [Ha | Hb]; destruct H1 as [Hna Hnb]; contradiction.] *)
Qed.

(** This one is found tricky and can only be doen using classical logic *)
Lemma prop_037 : ((A /\ B) -> C) -> ((A -> C) \/ (B -> C)).
Proof.
intro H.
destruct (classic B); destruct (classic A).
- left. (** or [right.] also works *)
  intros Ha. apply H. split; assumption.
- left. 
  intro Ha. contradiction.
- right. 
  intro Hb. contradiction.
- left. (** or [right.] also works *)
  intro Ha. contradiction.
Qed.


End Classical.

(** * Assorted examples *)

Section Assorted.
Variable A B C D: Prop.

(** We do a bit of chaining and tactic combination in the next proof 
   Try for yourself *)
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.

(** The following is tricky, but can be done without classical logic; 
   for now you may use classical logic by typing #<br>#
   [Require Import Classical.]
 *)
Lemma prop_063 : ~~((~A -> B) /\ (~A -> ~B) -> A).
Proof.
(** We do the proof without classical *)
intro H.
(** Note that the only we we can prove [False] is by applying [H].
   This looks weird because then we have to prove the "stronger"
   result, the one without the [~~]. The point is that one can prove it from
   its negation, which is now in the context as [H] *)
apply H.
intro H0.
destruct H0.
(** Here is a proof using the [assert] tactic, but I try to avoid [assert], as Rocq is a goal directed prover #<br>#
[assert (~A).
- intros H4. apply H. intros. assumption.
- assert False.
  + apply H1.
    * assumption.
    * apply H0. assumption.
  + contradiction.]
*)
destruct H1. (** !! This says: we will derive the goal from the [False] at the end of
 [~A -> ~ B].  This leaves us with the goals to prove [~A] and [B]  *)
- intro H2. apply H.
  intros;assumption.
- apply H0.
  intro H2; apply H; intros; assumption.
Qed.

(** You don't need Classical here *)
Lemma prop_082 : (A -> B) /\ (C -> D) -> (~B \/ ~D) -> (~A \/ ~C).
Proof.
intros H H0.
destruct H as [Hl Hr]. (* you need to split the /\ in all cases *)
destruct H0 as [H1 | H2].
(* Now, ~ A follows from ~B and A-> B so we can choose *)
- left. intro Ha; apply H1. apply Hl; assumption.
- right. intro Hc; apply H2. apply Hr; assumption.
Qed.

(** A variant of De Morgan; you need classical logic here:
   [Require Import Classical.]
 *)
Require Import Classical.
Lemma prop_106 : ~(~A /\ ~B) -> (A \/ B).
Proof.
destruct (classic A).
- left; assumption.
- intros. 
  destruct (classic B).
  * right; assumption.
  * destruct H0.
    split; assumption.
Qed.

End Assorted.