``` ```

# Total maps over types with decideable equality

``` ```
 version 1.0
``` ```
 Usage example for a set of naturals ```Require Emaps. Module NatEq <: Emaps.EQ. Definition dom := nat. Definition dom_eq_dec := eq_nat_dec. End NatEq. Module NatMap := Emaps.MakeMap(NatEq). ```
``` Require Import List. Set Implicit Arguments. Module Type EQ.   Parameter dom : Set.   Parameter dom_eq_dec : forall (x y : dom), {x = y} + {x <> y}. End EQ. Module MakeMap (Param : EQ).   Import Param.    Section Map.    Variable ran : Set.   Definition map : Set := dom -> ran. ```
 An initial constant map
```   Definition init (r : ran) : map := fun _ => r. ```
 Reading from a map
```   Definition sel (m : map) (d : dom) : ran :=     m d. ```
 Updating a map
```   Definition upd (m : map) (d : dom) (r : ran) : map :=     fun d' =>       if dom_eq_dec d d'         then r         else m d'. ```

## Theorems

```   Theorem sel_init : forall v a,     sel (init v) a = v.   Theorem sel_upd : forall m a v a',     (a = a' /\ sel (upd m a v) a' = v)     \/ (a <> a' /\ sel (upd m a v) a' = sel m a').   Theorem sel_upd_eq : forall m a a' v,     a = a' -> sel (upd m a v) a' = v.   Theorem sel_upd_neq : forall m a v a',     a <> a'     -> sel (upd m a v) a' = sel m a'.   Axiom ext_eq: forall (f g: map), (forall x, f x = g x) -> f = g.   Theorem upd_self : forall m a,     upd m a (sel m a) = m.    End Map.   Definition dom := dom. ```
 This is like "rewrite H in *"
```     Ltac rewriteall H :=         let n := fresh "val" in         (match type of H with            ?E1 = ?E2 =>                set (n:= E1) in * ;                clearbody n;                subst n          end). ```
 One case analysis for sel/upd. Helper tactic
```     Ltac sel_upd_case m adu vu ads :=      let H4 := fresh "H" in      (destruct (dom_eq_dec adu ads);       [ assert (H4 : (sel (upd m adu vu) ads = vu));            [ apply sel_upd_eq; intuition; (* should not fail *) fail | rewriteall H4; try trivial ]                     | assert (H4 : (sel (upd m adu vu) ads = (sel m ads)));           [ apply sel_upd_neq; intuition; (* should not fail *) fail | rewriteall H4; try trivial ]       ]).     ```
 Apply repeatedly the case analysis for sel (upd ...)
```     Ltac sel_upd :=       repeat match goal with         [ H : context[sel (upd ?M ?ADU ?VU) ?ADS] |- _ ] =>               sel_upd_case M ADU VU ADS       | [ |- context[sel (upd ?M ?ADU ?VU) ?ADS] ] =>               sel_upd_case M ADU VU ADS       end. End MakeMap. ```

## History

``` ```
 version 1.0 (Oct 21, 2006). First version.
``` ```
Index
This page has been generated by coqdoc