(* 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 : forall x:A, P x -> P x.
intro x.
intro 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 :=
match n with
 | 0     => 0
 | S m => match m with
              | 0     => 1
              | S p  =>  nfib p + nfib m
             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 equal by reflexivity *)
Lemma simp_eq: nfib 10 = 55.
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 0
    | ccons : forall (n:nat)(a:A), vect A n -> vect A (S n).

Check vect_ind.

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

Fixpoint head (n:nat)(v: vect A (S n)){struct v} : A :=
match v with
  | nnil => a0
  | ccons n a w => a
end.

Fixpoint tail (n:nat)(v: vect A (S n)){struct v} : vect A n :=
match v with
  | nnil => nnil
  | ccons n a w => w
end.

Check tail.

 Eval compute in (tail 0 (ccons A 0 a0 (nnil A))).
 Eval compute in (tail _ (ccons _ _ a0 (nnil _))).


(* Eval compute in (tail 0 nnil). *)

Fixpoint map (n:nat)(v: vect A n){struct v} : A :=
match v with
  | nnil => a0
  | ccons n a w => F a (map _ w)
end.

End Vect.

(* Mapping the plus-function over a vector of naturals,
    with start value 0
                                                                             *)
(* Ex: map plus over [1,2]		               			     *) 
(* NOTE: We have closed the section, so map has three "extra" arguments now! *)

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: *)
Notation NNil := (nnil _).
Notation CCons := (ccons _ _).
Notation Map := (fun n 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' : forall (A:Set)(n:nat), (vect A (S n))->(vect A n).
intros A n v.
inversion v.
exact H0.
Save.

Print tail'.
Print tail.
(* -------------------------------------------------------------------------------- *)
Section Group_example.

Definition Group_ax (A:Set)(op: A->A->A)(e:A)(inv:A->A):=
  forall x y z :A, op x (op y z) = op (op x y) z
  /\ 
  forall x :A, op e x = x
  /\
  forall x :A, op (inv x) x = e.

Definition Group (A:Set) :=
  { op :A->A->A & {e :A & {inv :A -> A | Group_ax A op e inv}}}.

Variable A:Set.
Variable G : Group A.

Check projT1.
Check projT2.
Check (projT1 (projT2 G)).

Lemma natgroup: Group nat.
exists plus.
exists 0.
exists (fun x => minus 0 x).
unfold Group_ax.
repeat split; auto with arith.
induction x1; auto with arith.
(* This may look true, but *)
Eval compute in (0- (S x1)).
(* shows it is not! *)
Abort.

End Group_example.
(* -------------------------------------------------------------------------------- *)
Section Group_record.

Record Group_axioms (A:Set)(op: A->A->A)(e:A)(inv:A->A):=
{ assoc:  (forall x y z :A, op x (op y z) = op (op x y) z);
  is_unit :  (forall x :A, op e x = x);
  is_inverse: (forall x :A, op (inv x) x = e)}.

Record Group_rec :=
{ cr   : Set;
  op   : cr -> cr -> cr;
  unit : cr;
  inv  : cr -> cr;
  group_prop: Group_axioms cr op unit inv}.

Variable G : Group_rec.

Check  cr G.
Check  unit G.
Check group_prop G.

Lemma natgroup: Group_rec.
apply Build_Group_rec with nat plus 0 (fun x => minus 0 x).
apply Build_Group_axioms.
Abort.

(* Axiom nat_prop : Group_axioms nat plus 0 (fun x => minus 0 x). *)
(* Instance natgroup : Group_rec := 
  { cr := nat;
    op := plus;
    inv := fun x => minus 0 x;
    group_prop := nat_prop}.
*)

Check cr.
End Group_record.


(* -------------------------------------------------------------------------------- *)
(* Coercions
   Coercion cr : Group_rec >-> Sortclass.
   Variable x :G.

OR: add > to the cr, so write:
    { cr :> Set;    
    
*)
(* -------------------------------------------------------------------------------- *)
(* Type Classes
   Class Group_rec
   Instance nat_group : Group_rec
*)

(* -------------------------------------------------------------------------------- *)
(* Rewriting with setoid equality 
   Simple example from Coq Reference Manual
*)

Require Import Relation_Definitions Setoid.

Record Setoid: Type :=
{ car:Type;
  eq:car->car->Prop;
  refl: reflexive _ eq;
  sym: symmetric _ eq;
  trans: transitive _ eq
}.

Add Parametric Relation (s : Setoid) : (@car s) (@eq s)
 reflexivity proved by (refl s)
 symmetry proved by (sym s)
 transitivity proved by (trans s) as eq_rel.

Record Morphism (S1 S2:Setoid): Type :=
{ f:car S1 ->car S2;
  compat: forall (x1 x2: car S1), eq S1 x1 x2 -> eq S2 (f x1) (f x2) }.

Add Parametric Morphism (S1 S2 : Setoid) (M : Morphism S1 S2) :
 (@f S1 S2 M) with signature (@eq S1 ==> @eq S2) as apply_mor.

Proof. apply (compat S1 S2 M). Qed.

Lemma test: forall (S1 S2:Setoid) (m: Morphism S1 S2)
 (x y: car S1), eq S1 x y -> eq S2 (f _ _ m x) (f _ _ m y).

Proof. intros. rewrite H. reflexivity. Qed.