(* A very simple Lemma 	*)
(* The proof script generates the lambda term "trivial" of the
   type (x:A)(P x) -> (P x)
   The Print command shows this term *)
Section triv.

Variable A:Set.
Variable P:A->Prop.

Lemma trivial : (x:A)(P x) -> (P x).
Intros x H.
Exact H.
Qed.

Print trivial.
End triv.



(* Defining the function nfib as an executable algorithm, showing
   that Coq is a (small) functional programming language *)
Require Arith.
Print nat.
Check nat_ind.
Check nat_rec.

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

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

(* Computationally equal terms are eual by reflexivity *)
Lemma simp_eq: (nfib (5)) = (15).
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.