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

Definition double (x:nat) : nat := 2 * x.

(*check the type of an expression*)
Check double.

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


(*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).


(* INDUCTIVE DATATYPES *)

(* List type constructor *)

Inductive list (A:Set) : Set := 
  nil : list A 
| cons : A -> list A -> list A. 

Print list.
Check list_rec.
Check nil.
Check cons.


(*RECURSIVE FUNCTIONS ON LISTS*)

(*Length of a list*)
Definition length' (A:Set) : list A -> nat := 
  list_rec A (fun _=>nat) 0 (fun x xs r=> 1+r). 

Eval cbv delta beta iota in (length' nat (cons nat 1 (cons nat 1 (nil nat)))).

(*Concatenation of lists*)
Definition app' (A:Set) (l1 l2:list A) : list A := 
  list_rec A (fun _=>list A) l2 (fun x xs r=> cons A x r) l1.

Eval compute in (app' nat (cons nat 1 (nil nat)) (cons nat 2 (nil nat))).

(*IMPLICIT ARGUMENTS...*)

Implicit Arguments nil [A].
Implicit Arguments cons [A].
Implicit Arguments length' [A].
Implicit Arguments app' [A].

Eval compute in (length' (cons 1 (cons 1 nil))).

Eval compute in (app' (cons 1 nil) (cons 2 nil)).

Set Implicit Arguments.

(*USING Fixpoint*)
Fixpoint length (A:Set) (l:list A) : nat := 
  match l with 
  | nil => 0 
  | cons x xs => 1 + (length xs) 
  end. 

(* Coq forces recursive calls to act upon strict subterms of the argument. 
In the presence of multiple arguments, the recursive one is singled out by 
the keyword "struct" *)

Fixpoint app (A:Set) (l1 l2:list A) {struct l1} : list A := 
  match l1 with 
  | nil => l2 
  | cons x xs => cons x (app xs l2) 
  end.


(*DEPENDENT TYPES IN PROGRAMMING...*)
Inductive Vec (A:Set) : nat -> Set :=
| Vnil : Vec A O
| Vcons : forall (x:A) (n:nat), Vec A n -> Vec A (S n).

Check (Vcons 5 (Vnil nat)).

(* The syntax inthe "match" construct is extended to copoe with different types in each branch and how the return type is conditionated *)

Fixpoint appVec (A:Set)(n1 n2:nat)(v1:Vec A n1)(v2:Vec A n2){struct v1}:Vec A (n1+n2) :=
  match v1 in Vec _ m return Vec A (m+n2) with
  | Vnil => v2
  | Vcons x m' v' => Vcons x (appVec v' v2)
  end.

Eval compute in appVec (Vcons 1 (Vnil nat)) (Vcons 2 (Vcons 3 (Vnil nat))).


(********************************************************
   Coq as an Interactive Proof-Development Environment
*********************************************************)



(*Proof-term defined explicitly*)
Definition simple_proof (A:Prop) (x:A) : A := x.

Check simple_proof.

Theorem ex1 : forall A B:Prop, A -> (A->B) -> B.
intros A B H H0.
apply H0.
exact H.
Qed.

(*Interactive definition of the S combinator
  "Definition Scomb (A B C:Set) (x:A->B->C) (y:A->B) (z:A) : C := x z (y z)."
*)
Definition Scomb (A B C:Set) : (A->B->C) -> (A->B) -> A -> C. 
intros A B C x y z.
apply x.
  exact z.
  apply y; exact z.
Defined.
(*Note: the use of the command "Defined" (instead of "Qed") makes the
definition transparent (it can be unfolded) *)

Print Scomb.


(* ============ LOGICAL REASONING ============ *)

(* ------------ Propositional ------------ *)

(* see aula1.v *)

Lemma ex3 :  forall P Q:Prop, ~(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.
apply H; assumption.
apply H0; assumption.
Qed.

(* Exercise:    Lemma ex4 : forall P Q R:Prop, (P\/Q -> R) -> P -> R.
*)


(* ------------ First-order ------------ *)

Theorem ex7 : forall (X:Set) (P:X->Prop), ~(exists x, P x) -> (forall x, ~(P x)).
unfold not.
intros.
apply H.
exists x.
assumption.
Qed.



(* SECTIONS *)

Section Test.

Variable U : Set.

Hypothesis Q R: U->Prop.

Theorem ex9: (forall x, Q x)/\(forall x, R x) -> (forall x, Q x /\ R x).
intro H.
(* case H. intros.*)
(* destruct H as [H0 H1]. *)
 elim H. 
intros H1 H2. split. apply H1. apply H2.
(* intro H; elim H; intros H1 H2; split; [apply H1 | apply H2]. *)
Qed.

Let conj (a b:Prop) := a/\b.

Hypothesis W Z:Prop.

Definition ex10 := conj W Z. 

Check ex9.
Print ex10.

End Test.

(*Note that local variables are abstracted*)
Check ex9.
Print ex10.



(* ------------ CLASSICAL REASONING ------------ *)


Section Classical.

Axiom EM : forall P:Prop, P \/ ~P.

Theorem ex11 : forall (X:Set) (P:X->Prop), ~(forall x, ~(P x)) -> (exists x, P x).
intros.
elim (EM ((exists x, P x))).
intro; assumption.
intro H0. elim H. red. intros. apply H0.
exists x. assumption.
Qed.

Check ex11.

End Classical.

(* CAUTION: Axiom is a global declaration. Even after the section is closed EM is assumed in the enviroment, and can be used. To avoid this we should decalre EM using the command Hypothesis *)
Check ex11.
Check EM.


(*
  Exercise: prove forall P:Prop, ~~P -> P.
*)


Theorem NNE : forall P:Prop, ~~P -> P.
intros.
elim (EM P). intros.
 assumption.
(* intros; absurd (~P); [assumption | assumption]. *)
 contradiction.
Qed.



(*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.

Axiom ABSURD : False.

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

End Caution.



(* EQUALITY *)
Section Equality.

(* eq definition
Inductive eq (A : Type) (x : A) : A -> Prop :=  refl_equal : x = x.
*)

Variable X:Set.

Check eq_ind.

Lemma ex13 : forall a b c:X, a=b -> b=c -> a=c.
intros a b c H1 H2.
elim H2 (*apply eq_ind with X b*).
(*now, assumption kills the goal... instead, we proceed with rewriting...*)
elim H1.
reflexivity (*apply refl_equal*).
Qed.

Lemma ex13' : forall a b c:X, a=b -> b=c -> a=c.
intros.
rewrite H.
rewrite <- H0. (* rewrite H0 *)
reflexivity.
Abort.

(*
   Exercise: prove symmetry 
*)

End Equality.


(* CONVERTIBILITY *)
Section Convertibility.

Print list.
Print app.

Lemma app_nil : forall (A:Set) (l:list A), app nil l = l.
intros.
simpl.
reflexivity.
Qed.

End Convertibility.





(* ============ INDUCTION ============ *)


Section Induction.


Theorem app_l_nil : forall (A:Set) (l:list A), app l nil = l.
intros A l. 
pattern l. (* pattern performs a beta-expansion *)
apply list_ind.
reflexivity.
intros a l0 IH. simpl. rewrite IH. reflexivity.
Qed.


Theorem app_l_nil' : forall (A:Set) (l:list A), app l nil = l.
intros A l.
elim l.
reflexivity.
intros a l0 IH; simpl; rewrite IH; reflexivity.
Abort.



Theorem app_l_nil'' : forall (A:Set) (l:list A), app l nil = l.
intros A l.
induction l.
reflexivity.
simpl.
rewrite IHl.
reflexivity.
Abort.



(* 
 Exercise: prove the following lemma

Lemma app_length : forall (A:Set) (l1 l2:list A), 
                    length (app l1 l2) = length l1 + length l2.
*)




(* INDUCTIVE PREDICATES *)

Print nat.

(* A property (predicate) on natural numbers *)
Inductive Even : nat -> Prop :=
| Even_base : Even 0
| Even_step : forall n, Even n -> Even (S (S n)).


(* An inductive relation "x is the last element of list l" *)
Inductive last (A:Set) (x:A) : list A -> Prop :=
| last_base : last x (cons x nil)
| last_step : forall l y, last x l -> last x (cons y l).



Lemma ex15 : forall (A:Set) (x:A), ~(last x nil).
intros.
intro.
inversion H.
Qed.


Theorem ex16 : forall (A:Set) l (x:A), last x l -> l=nil -> False.
intros A l x H. elim H.
intro H0. discriminate H0.
intros.
discriminate H2.
Qed.

(*
  Exercise (difficult): define the "Odd" predicate and prove that 
                         (Even n)->(Odd (S n)).
*)





(* An example of mutually defined inductive types *)
Inductive EVEN : nat -> Prop :=
| EVEN_base : EVEN 0
| EVEN_step : forall n, ODD n -> EVEN (S n)
with ODD : nat -> Prop :=
| ODD_step : forall n, EVEN n -> ODD (S n).




(* ============ Use of libraries ============ *)

Require Import List.

Check map.

SearchAbout map.

SearchPattern (map _ _ = _).