(* Type for maps *)

(*
Variable I : Set.
Variable I_eq_dec : forall i1 i2:I, {i1 = i2} + {i1 <> i2}.

Variable V : Set.
Definition t := I -> V.

Definition cte (v:V) : t := fun i => v.

Definition find (x:t) (i: I) : V := x i.
Definition add (m:t) (i:I) (v:V) : t :=
  fun i' => if I_eq_dec i i' then v else m i'.

Lemma find_add : forall (m:t) (i:I) (v:V), find (add m i v) i = v.
Proof.
unfold find, add in |- *; intros.
case (I_eq_dec i i); intros; auto.
case n; trivial.
Qed.

Lemma find_add_eq :
 forall (m:t) (i i':I) (v:V), i = i' -> find (add m i v) i' = v.
Proof.
intros.
rewrite <- H; apply find_add.
Qed.

Lemma find_add_other :
 forall (m:t) (i i':I) (v:V), i <> i' -> find (add m i v) i' = find m i'.
Proof.
unfold find, add in |- *; intros.
case (I_eq_dec i i'); intros; auto.
case H; trivial.
Qed.
*)

(* Instanciation *)
Require Export ZArith.
Open Scope Z_scope.

(*
Definition I := Z.
Lemma I_eq_dec : forall i1 i2:I, {i1 = i2} + {i1 <> i2}.
exact Z_eq_dec.
Save.

Variable V : Set.
Definition t := I -> V.

Definition cte (v:V) : t := fun i => v.

Definition find (x:t) (i: I) : V := x i.
Definition add (m:t) (i:I) (v:V) : t :=
  fun i' => if I_eq_dec i i' then v else m i'.



Lemma find_add : forall (m:t) (i:I) (v:V), find (add m i v) i = v.
Proof.
unfold find, add in |- *; intros.
case (I_eq_dec i i); intros; auto.
case n; trivial.
Qed.

Lemma find_add_eq :
 forall (m:t) (i i':I) (v:V), i = i' -> find (add m i v) i' = v.
Proof.
intros.
rewrite <- H; apply find_add.
Qed.

Lemma find_add_other :
 forall (m:t) (i i':I) (v:V), i <> i' -> find (add m i v) i' = find m i'.
Proof.
unfold find, add in |- *; intros.
case (I_eq_dec i i'); intros; auto.
case H; trivial.
Qed.

(*
Variables x y : V.
Definition m : t := 
     add (add (cte x) 0 y) 2 y.

(* 
Hint Resolve find_add find_add_eq find_add_other.
*)

Lemma lem : find m 0 = y.
unfold m.
rewrite find_add_other; auto.
discriminate.
Save.

Eval compute in (find m 0).
*)
*)

(*

Section Map.

Variable I : Set.
Variable I_eq_dec : forall i1 i2:I, {i1 = i2} + {i1 <> i2}.

Variable V : Set.
Definition t := I -> V.

Definition cte (v:V) : t := fun i => v.

Definition find (x:t) (i: I) : V := x i.
Definition add (m:t) (i:I) (v:V) : t :=
  fun i' => if I_eq_dec i i' then v else m i'.

Lemma find_add : forall (m:t) (i:I) (v:V), find (add m i v) i = v.
Proof.
unfold find, add in |- *; intros.
case (I_eq_dec i i); intros; auto.
case n; trivial.
Qed.

Lemma find_add_eq :
 forall (m:t) (i i':I) (v:V), i = i' -> find (add m i v) i' = v.
Proof.
intros.
rewrite <- H; apply find_add.
Qed.

Lemma find_add_other :
 forall (m:t) (i i':I) (v:V), i <> i' -> find (add m i v) i' = m i'.
Proof.
unfold find, add in |- *; intros.
case (I_eq_dec i i'); intros; auto.
case H; trivial.
Qed.

End Map.

Print t.
Check cte.
Check find.
Check add.


Variable V : Set.

Definition Zt := t Z V.
Definition Zcte := cte Z V.
Definition Zfind := find Z V.
Definition Zadd := add Z Z_eq_dec V.

Variables x y : V.
Definition m : Zt := 
     Zadd (Zadd (Zcte x) 0 y) 2 y.

Eval compute in (Zfind m 2).

Lemma lem : Zfind m 2 = y.
unfold Zfind,m,Zadd.
apply find_add_eq.
trivial.
Save.

*)

Module Type Mpar.
Variable I : Set.
Variable I_eq_dec : forall i1 i2:I, {i1 = i2} + {i1 <> i2}.
Variable V : Set.
End Mpar.


Module Map (P:Mpar).

Import P.

Definition t := I -> V.

Definition cte (v:V) : t := fun i => v.

Definition find (x:t) (i: I) : V := x i.
Definition add (m:t) (i:I) (v:V) : t :=
  fun i' => if I_eq_dec i i' then v else m i'.

Lemma find_add : forall (m:t) (i:I) (v:V), find (add m i v) i = v.
Proof.
unfold find, add in |- *; intros.
case (I_eq_dec i i); intros; auto.
case n; trivial.
Qed.

Lemma find_add_eq :
 forall (m:t) (i i':I) (v:V), i = i' -> find (add m i v) i' = v.
Proof.
intros.
rewrite <- H; apply find_add.
Qed.

Lemma find_add_other :
 forall (m:t) (i i':I) (v:V), i <> i' -> find (add m i v) i' = find m i'.
Proof.
unfold find, add in |- *; intros.
case (I_eq_dec i i'); intros; auto.
case H; trivial.
Qed.

Notation "m [ i ]" := (find m i) (at level 50).
Notation "m [ i <- v ]" := (add m i v) (at level 50).

End Map.

Module ZVpar : Mpar.
Definition I:=Z.

Definition I_eq_dec : forall i1 i2:I, {i1 = i2} + {i1 <> i2}
:= Z_eq_dec.

Variable V : Set.
End ZVpar.

Module ZMap := Map ZVpar.
Import ZMap.
Import ZVpar.

Variables x y : V.
Definition m : t := (cte x) [0 <- y] [2 <- y] .


Eval compute in (m [2]).