Require Arith.
(* nat as an inductive type 
   Look at its definition and the types of the eliminators *)

Print nat.
Check nat_ind.
Check nat_rec.

(* Define addition in two ways, by recursion over the second 
   and by recursion over the first argument *)
Fixpoint plus [n,m:nat] : nat :=
Cases m of
 | O     => n
 | (S p) => (S (plus n p))
end.


Fixpoint pluss [n:nat] : nat->nat := [m:nat]
Cases n of
 | O     => m
 | (S p) => (S (pluss p m))
end.


(* Defining the function fib as an executable algorithm, showing
   that Coq is a (small) functional programming language *)

Fixpoint fib [n:nat] : nat :=
Cases n of
 | O     => (1)
 | (S m) => Cases m of 
              | O     => (1)
              | (S p) => (plus (plus (fib p)(fib m)) (1))
             end
end.

Print fib.

(* Eval Compute computes the "value" (normal form) of a term *)
Eval Compute in (fib (5)).
Eval Compute in (fib (10)).

(* Computationally equal terms are eual by reflexivity *)
Lemma simp_eq: (fib (5)) = (15).
Reflexivity. 
Qed.


Inductive LIST [A:Set] :Set := 
NIL : (LIST A)
| CONS : A -> (LIST A) -> (LIST A).

Fixpoint LENGTH [A:Set;l:(LIST A)] :nat :=
Cases l of
| NIL => O
| (CONS a k) => (S (LENGTH A k))
end.

Eval Compute in (LENGTH ? (CONS ? O (CONS ? O (CONS ? O (NIL ?))))).

Syntactic Definition Nil := (NIL ?).
Syntactic Definition Cons := (CONS ?).
Syntactic Definition Length := (LENGTH ?).

Eval Compute in (Length (Cons O (Cons O (Cons  O Nil)))).

Fixpoint SUMLIST [l:(LIST nat)]: nat :=
Cases l of
| NIL => O
| (CONS n k) => (plus (SUMLIST k) n)
end.

Eval Compute in (SUMLIST (Cons (2) (Cons (2) (Cons  (1) Nil)))).


Lemma triv0 : (n:nat) (plus O n ) = n. 
Induction n.
Simpl.
Auto.
Intros n0 H.
Simpl.
Auto.
Qed.


(* Dependently typed data types, "vectors of length n over A"
   (vect A n) *)
Section Vect.

Inductive vect [A:Set] : nat -> Set :=
	|  nnil : (vect A O)
	| ccons : (n:nat;a:A)(vect A n)->(vect A (S n)).

Check vect_ind.

Variable A:Set; a0:A; F:A->A->A.

Fixpoint map [n:nat;v:(vect A n)] : A :=
Cases v of
  | nnil => a0
  | (ccons n a w) => (F a (map ? w))
end.
End Vect.

(* Mapping the plus-function over a vector of naturals 		*)
(* Ex: map plus over [1,2]					*) 
Eval Compute in (map nat (0) plus (2) 
	(ccons nat (1) (1) (ccons nat (0) (2) (nnil nat)))).

(* Lots of notational overhead. Improve by using "implicit syntax":
   suppressing parameters ("?") that can be inferred by the type 
   checker*)

Eval Compute in (map ? (0) plus ? (ccons ? ? (1) (ccons ? ? (2) (nnil ?)))).

(* Even better: introduce special syntax: *)
Syntactic Definition NNil := (nnil ?).
Syntactic Definition CCons := (ccons ??).
Syntactic Definition Map := [n:nat;g:?](map ? n g ?).

Eval Compute in (Map (0) plus (CCons (1) (CCons (2) NNil))).

(* Object and Proofs are the same kind of things [terms], so why
   not use the tactic language to construct an object ...
   Example of an "interactive definition" of the function tail *)

Definition tail :(A:Set;n:nat)(vect A (S n))->(vect A n).
Intros A n v.
Inversion v.
Exact H0.
Save.

Print tail.


Print or.
Print and.
Print exists.

Lemma or_and :(A,B,C:Prop) (A->C)->(A/\B->C).
Intros A B C Ha Hab.
Elim Hab. 
Intros H1 H2.
Apply Ha.
Assumption.
Qed.

Lemma and_or :(A,B,C:Prop) (A\/B->C) -> (A->C).
Intros A B C H H0.
Apply H.
Apply or_introl.
Assumption.

Lemma ex_all :(A:Set; P:A->Prop;C:Prop)
	(EX x:A | (P x)) ->((x:A) (P x) ->C) -> C. 
Intros.
Elim H.
Auto.
Qed.















Fixpoint sum [n:nat;v:(vect nat n)] : nat :=
Cases v of
  | nnil => O
  | (ccons n m w) => (plus m (sum ? w))
end.

Eval Compute in (sum (2) (ccons nat (1) (1) (ccons nat (0) (2) (nnil nat)))).

Eval Compute in (sum ? (ccons ? ? (1) (ccons ? ? (2) (nnil ?)))).

Syntactic Definition NNil := (nnil ?).
Syntactic Definition CCons := (ccons ??).
Syntactic Definition Sum := (sum ?).

Eval Compute in (Sum (CCons (1) (CCons (2) NNil))).


Definition tail :(A:Set;n:nat)(vect A (S n))->(vect A n).
Intros A n v.
Inversion v.
Exact H0.
Save.

Print tail.