(* ================================================================== *)
Section EX.

Variables (A:Set) (P : A->Prop).
Variable Q:Prop.

(* Check the type of an expression. *)
Check P.  

Lemma trivial : forall x:A, P x -> P x.
Proof.
intros.
assumption.
Qed.


(* Prints the definition of an identifier. *)
Print trivial.


Lemma example : forall x:A, (Q -> Q -> P x) -> Q -> P x.
Proof.
intros x H H0.
apply H.
assumption.
assumption.
Qed.

Print example.

End EX.

Print trivial.
Print example.
(* ================================================================== *)


Require Import ZArith.


(* ================================================================== *)
(* ================ Coq as a Programming Language =================== *)

(* prints the definition of an identifier *)
Print nat.

(* check the type of an expression *)
Check S (S O).


(* defining new constants *)
Definition double (x:nat) : nat := 2 * x.

Check double.
Print double.

Definition triple := fun x : nat => x + (double x).

Check triple.

(* performs evaluation of an expression
   strategy: call-by-value;  reductions: delta*)
Eval cbv delta [double] in (double 22).

(* "Eval compute" is equivalent to "Eval cbv delta beta iota zeta" *) 
Eval compute in (double 22).

Eval compute in triple (double 10).


(* ================================================================== *)
(* ================== Interpretation Scopes ========================= *)


(* some notations are overloaded *)

(* to find the function hidden behind a notation *)
Locate "+".
Locate "*".

Print Scope nat_scope.
Print Scope Z_scope.

Locate "*".

Check 3.
Eval compute in 4+5.

Check (3*5)%Z.  (* "term%key" bounds the interpretation of "term" to the scope "key" *)
Eval compute in (3 + 5)%Z.


(* When a given notation has several interpretations, 
   the most recently opened scope takes precedence. *)
Open Scope Z_scope.


Check 3.
Check (S (S (S O))).
Eval compute in 7*3.

Close Scope Z_scope.

Check 3.



(* ================================================================== *)
(* ===================== Implicit Arguments ========================= *)


Definition comp : forall A B C:Set, (A->B) -> (B->C) -> A -> C
  := fun A B C f g x => g (f x).

Definition example0 (A:Set) (f:nat->A) := comp _ _ _ S f.

Print example0.

Set Implicit Arguments.

Definition comp1 : forall A B C:Set, (A->B) -> (B->C) -> A -> C
  := fun A B C f g x => g (f x).

Definition example1 (A:Set) (f:nat->A) := comp1 S f.

Check (comp1 (C:=nat) S).

Check (@comp1 nat nat nat S S).

Unset Implicit Arguments.

Definition comp2 : forall A B C:Set, (A->B) -> (B->C) -> A -> C
  := fun A B C f g x => g (f x).

Implicit Arguments comp2 [A C].

Definition example2 (A:Set) (f:nat->A) := comp2 nat S f.

Print Implicit example2.
Print Implicit comp2.


Set Implicit Arguments.





(* ================================================================== *)
(* ====================== Propositional Logic ======================= *)
(* ================================================================== *)

Section ExamplesPL.

Variables Q P :Prop.

Lemma ex1 : (P -> Q) -> ~Q -> ~P.
Proof.
tauto.
Qed.

Print ex1.

Lemma ex1' : (P -> Q) -> ~Q -> ~P.
Proof.
intros.
intro.
apply H0.
apply H.
assumption.
Qed.

Print ex1'.


Lemma ex2 : P /\ Q -> Q /\ P.
Proof.
intro H.
split.
destruct H as [H1 H2].
exact H2.
destruct H; assumption.
Qed.


Lemma ex3 : P \/ Q -> Q \/ P.
Proof.
intros.
destruct H as [h1 | h2].
right.
assumption.
left; assumption.
Qed.



Theorem ex4 : forall A:Prop, A -> ~~A.
Proof.
intros.
intro.
apply H0. 
exact H.
Qed.

Lemma ex4' : forall A:Prop, A -> ~~A.
Proof.
intros.
red.     (* does only the unfolding of the head of the goal *)
intro.
unfold not in H0.   (* unfold – applies the delta rule for a transparent constant. *)
apply H0; assumption.
Save.




Axiom double_neg_law : forall A:Prop, ~~A -> A.  (* classical *)

(* CAUTION: Axiom is a global declaration. Even after the section is closed double_neg_law is assume in the enviroment, and can be used. If we want to avoid this we should decalre double_neg_law using the command Hypothesis *) 


Lemma ex5 : (~Q -> ~P) -> P -> Q.   (* this result is only valid classically *)
Proof.
intros.
apply double_neg_law.
intro.
(* apply H; assumption. *)
apply H.
assumption.
assumption.
Qed.


Lemma ex6 : (P\/Q)/\~P -> Q.   
Proof.
intros.
destruct H.
destruct H.

assert False.
apply H0; assumption.
elim H1.  (* contradiction. *)
assumption.

(* **** or simply...
contradiction.
assumption.
*)

Qed.


Lemma ex7 : ~(P \/ Q) <-> ~P /\ ~Q.   
Proof.
red.
split.
intros.
split.
unfold not in H.
intro H1.
apply H.
left; assumption.
intro H1; apply H; right; assumption.

intros H H1.
destruct H.
destruct H1.
contradiction.
contradiction.
Qed.


Lemma ex7' : ~(P \/ Q) <-> ~P /\ ~Q.
Proof.
tauto.
Qed.



Variable B :Prop.
Variable C :Prop.


(* exercise *)
Lemma ex8 : (P->Q) /\ (B->C) /\ P /\ B -> Q/\C. 
Admitted.
 
(* exercise *)
Lemma ex9 : ~ (P /\ ~P).   
Admitted.


End ExamplesPL.

(* ================================================================== *)
(* =======================  First-Order Logic ======================= *)
(* ================================================================== *)

Section ExamplesFOL.

Variable X :Set.
Variable t :X. 
Variables R W : X -> Prop.

Lemma ex10 : R(t) -> (forall x, R(x)->~W(x)) -> ~W(t).
Proof.
intros.
apply H0.
exact H.
Qed.


Lemma ex11 : forall x, R x -> exists x, R x.
Proof.
intros.
exists x.
assumption.
Qed.


Lemma ex11' : forall x, R x -> exists x, R x.
Proof.
firstorder.
Qed.



Lemma ex12 : (exists x, ~(R x)) -> ~ (forall x, R x).
Proof.
intros H H1.
destruct H as [x0 H0].
apply H0.
apply H1.
Qed.


(* Exercise *)
Lemma ex13 : (forall x, R x) \/ (forall x, W x) -> forall x, (R x) \/ (W x).
Admitted.

Variable G : X->X->Prop.

(* Exercise *)
Lemma ex14 : (exists x, exists y, (G x y)) -> exists y, exists x, (G x y).
Admitted.


(* Exercise *)
Proposition ex15: (forall x, W x)/\(forall x, R x) -> (forall x, W x /\ R x).
Admitted.


(* ------- Note that we can have nested sections ----------- *)
Section Relations.       

Variable D : Set.
Variable Rel : D->D->Prop.

Hypothesis R_symmetric : forall x y:D, Rel x y -> Rel y x.
Hypothesis R_transitive : forall x y z:D, Rel x y -> Rel y z -> Rel x z.


Lemma refl_if : forall x:D, (exists y, Rel x y) -> Rel x x.
intros.
destruct H.
(* try "apply R_transitive" to see de error message *)
apply R_transitive with x0. 
assumption.
apply R_symmetric.
assumption.
Qed.

Check refl_if.

End Relations.

Check refl_if. (* Note the difference after the end of the section Relations. *)



(* ====== OTHER USES OF AXIOMS ====== *)

(* --- A stack abstract data type --- *)
Section Stack.

Variable U:Type.

Parameter stack : Type -> Type.
Parameter emptyS : stack U. 
Parameter push : U -> stack U -> stack U.
Parameter pop : stack U -> stack U.
Parameter top : stack U -> U.
Parameter isEmpty : stack U -> Prop.

Axiom emptyS_isEmpty : isEmpty emptyS.
Axiom push_notEmpty : forall x s, ~isEmpty (push x s).
Axiom pop_push : forall x s, pop (push x s) = s.
Axiom top_push : forall x s, top (push x s) = x.

End Stack.

Check pop_push.

(* Now we can make use of stacks in our formalisation!!! *)

(* A NOTE OF CAUTION!!! *)
(* The capability to extend the underlying theory with arbitary axiom is a powerful but dangerous mechanism. We must avoid inconsistency. *)
Section Caution.

Check False_ind.

Hypothesis ABSURD : False.

Theorem oops : forall (P:Prop), P /\ ~P.
elim ABSURD.
Qed.

End Caution. (* We have declared ABSURD as an hypothesis to avoid its use outside this section. *)



(* ==================== Dealing with the equality ==================== *)
 
Print nat.

Check  (S (S (S O))).


(* Performs evaluation of an expression. 
   "Eval compute" is equivalent to "Eval cbv delta beta iota zeta"
*) 
Eval compute in 3+5*2. 


(* ====== Finding existing proofs ====== *)

Search le.

SearchPattern (_ + _ <= _ + _).

SearchRewrite (_+(_-_)).

SearchAbout ge.

Lemma ex16 : 1 <= 3.
Proof.
Search le.
apply le_S.
apply le_S.
apply le_n.
Qed.           (* The automatic tactic "firstorder" would solve the goal. *)


Lemma ex17 : forall x y:nat, x <= 5 -> 5 <= y -> x <= y.
Proof.
intros.
Search le.
Check le_trans.
apply le_trans with (m:=5).   (* or simply "apply le_trans with 5." *)
assumption.
assumption.
Qed.


Lemma ex18 : forall x y:nat, (x + y) * (x + y) = x*x + 2*x*y + y*y.
Proof.
intros.
SearchRewrite (_ * (_ + _)).
rewrite mult_plus_distr_l.    (* rewrite – rewrites a goal using an equality. *)
SearchRewrite ((_ + _) * _).
rewrite mult_plus_distr_r.
rewrite mult_plus_distr_r.
SearchRewrite (_ + (_ + _)).
rewrite plus_assoc.
rewrite <- plus_assoc with (n := x * x).  (* rewrite <- – rewrites a goal using an equality in the reverse direction. *)
SearchPattern (?x * ?y = ?y * ?x).
rewrite mult_comm with (n:= y) (m:=x).
SearchRewrite (S _ * _).
pattern (x * y) at 1.        (* pattern – performs a beta-expansion on the goal. *)
Check  mult_1_l.
rewrite <- mult_1_l.
rewrite <- mult_succ_l.
SearchRewrite (_ * ( _ * _)).
rewrite mult_assoc.
reflexivity.                 (* reflexivity – reflexivity property for equality. *)
Qed.


Lemma ex19 : forall n:nat, n <= 2*n.
Proof.
induction n.                 (* induction – performs induction on an identifier. *)
simpl.                       (* simpl – performs evaluation. *)
Search le.
apply le_refl.
simpl.
Search le.
apply le_n_S.
SearchPattern (_<= _ + _).
apply le_plus_l.
Qed.


End ExamplesFOL.