Library lib.Emaps


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