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 |
|