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

(* Trees *)

Inductive tree (A:Set) : Set := 
| empty : tree A 
| node : tree A -> A -> tree A -> tree A.


Check list_rec.

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

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 1 (Vnil nat)).

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


(*An example of a program that is impossible to read (write?) *) 
Fixpoint VecHead (A : Set) (n : nat) (v : Vec A (S n)) {struct v}: A :=
(match v in (Vec _ l) return (l <> 0 -> A) with
 | Vnil => fun h : 0 <> 0 => False_rec A (h (refl_equal 0))
 | Vcons x m' _ => fun _ : S m' <> 0 => x
 end)
  (* proof of Sn<>0 *)
  (fun H : S n = 0 =>
   let H0 :=
     eq_ind (S n)
       (fun e : nat => match e with
                       | 0 => False
                       | S _ => True
                       end) I 0 H in
   False_ind False H0).



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

Print Scomb.

(*
  Mixing interactive and definitional styles.
  REFINE tactic

  (a reasonable way to define "VecHead")
*)
Definition VecHead' (A:Set) (n:nat) (v:Vec A (S n)) : A. 
refine (fun A n v => match v in Vec _ l return (l<>0)->A with
                     | Vnil => _
                     | Vcons x m' v => _
                     end _).
intro h; elim h; reflexivity.
intro h; exact x.
discriminate.
Defined.


(* LOGICAL REASONING *)

(*definitions*)

(*
(* False (absurd) is encoded as an empty type *)
Inductive False : Prop :=.
(* NEGATION - notation: ~A *)
Definition not (A:Prop) : Prop := A -> False.
(* AND - notation: A /\ B *)
Inductive and (A B:Prop) : Prop := conj : A -> B -> and A B.
(* OR - notation: A \/ B *)
Inductive or (A B:Prop) : Prop :=
| or_introl : A -> or A B
| or_intror : B -> or A B.
(* EXISTENCIAL QUANT. - notation "exists x, P x" *)
Inductive ex (A : Type) (P : A -> Prop) : Prop :=
    ex_intro : forall x : A, P x -> ex P
*)



Theorem ex2 : forall A B, A/\B -> A\/B.
intros; apply or_introl.
apply and_ind with A B; try assumption.
intros; assumption.
Qed.

Theorem ex2' : forall A B, A/\B -> A\/B.
intros A B H; left; elim H; intros; assumption.
Qed.




(*First-order reasoning*)

Theorem ex3 : forall (X:Set) (P:X->Prop), ~(exists x, P x) -> (forall x, ~(P x)).
unfold not; intros.
apply H.
exists x (*apply ex_intro with x*); assumption.
Qed.


(*
  Exercise: prove the reverse implication

Theorem ex3' : forall (X:Set) (P:X->Prop), (forall x, ~(P x)) -> ~(exists x, P x).

*)


(* CLASSICAL REASONING *)

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

Theorem ex4 : 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.


(*
  Exercise: prove the other formulas...

Theorem Pierce : forall P Q, ((P->Q)->P)->P.

Theorem NNE : forall P, ~~P -> P.

Theorem deMorgan1 : forall U P, ~(forall n:U, ~ P n) -> (exists n : U, P n).

Theorem deMorgan2 : forall U (P:U->Prop), ~ (forall n:U, P n) -> exists n:U, ~ P n.

Theorem deMorgan3 : forall U P, ~ (exists n : U, ~ P n) -> forall n:U, P n.

*)


(* SECTIONS *)

Section Test.

Variable U : Set.

Hypothesis Q R: U->Prop.

Theorem ex6: (forall x, Q x)/\(forall x, R x) -> (forall x, Q x /\ R x).
intro H; elim H; intros H1 H2; split; [apply H1 | apply H2]; assumption.
Qed.

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

Hypothesis W Z:Prop.

Definition ex7 := conj W Z. 

Check ex6.

Print ex7.

End Test.

(*Note that local variables are abstracted*)
Check ex6.

Print ex7.

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

Check False_ind.


Axiom ABSURD : False.

Theorem ex8 : 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 ex9 : 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.


End Equality.



(* CONVERTIBILITY *)
Section Convertibility.

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.
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.
Qed.

(* INDUCTIVE PREDICATES *)

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



(*
  Exercise: Use the inversion tactic to prove that forall x, ~(last x nil). Can you avoid using that tactic? (second part is difficult)

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


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



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


End Induction.




(* Use of libraries *)


Require Import List.

Check map.