Library Maps
Require Import List TheoryList.
Require Import ListUtil Tactics.
Set Implicit Arguments.
Axiom ext_eq : forall (S T : Set) (f g : S -> T),
(forall x, f x = g x) -> f = g.
Module Type EQ.
Parameter dom : Set.
Parameter dom_eq_dec : forall (x y : dom), {x = y} + {x <> y}.
End EQ.
Module Type MAP.
Variable dom : Set.
Parameter map : Set -> Set.
Parameter init : forall (ran : Set), ran -> map ran.
Parameter sel : forall (ran : Set), map ran -> dom -> ran.
Parameter upd : forall (ran : Set), map ran -> dom -> ran -> map ran.
Axiom sel_init : forall (ran : Set) (v : ran) a,
sel (init v) a = v.
Axiom sel_upd : forall (ran : Set) (m : map ran) a v a',
(a = a' /\ sel (upd m a v) a' = v)
\/ (a <> a' /\ sel (upd m a v) a' = sel m a').
Axiom sel_upd_eq : forall (ran : Set) (m : map ran) a v,
sel (upd m a v) a = v.
Axiom sel_upd_neq : forall (ran : Set) (m : map ran) a v a',
a <> a'
-> sel (upd m a v) a' = sel m a'.
Axiom upd_self : forall (ran : Set) (m : map ran) a,
upd m a (sel m a) = m.
End MAP.
Module FuncMap (Param : EQ) : MAP with Definition dom := Param.dom.
Import Param.
Section Map.
Variable ran : Set.
Definition map := dom -> ran.
Definition init (r : ran) : map :=
fun _ => r.
Definition sel (m : map) (d : dom) : ran :=
m d.
Definition upd (m : map) (d : dom) (r : ran) : map :=
fun d' =>
if dom_eq_dec d d'
then r
else m d'.
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 v,
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'.
Theorem upd_self : forall m a,
upd m a (sel m a) = m.
End Map.
Definition dom := dom.
End FuncMap.
Module Type SET.
Variable dom : Set.
Parameter set : Set.
Parameter empty : set.
Parameter In : dom -> set -> bool.
Parameter add : set -> dom -> set.
Parameter remove : set -> dom -> set.
Parameter union : set -> set -> set.
Parameter intersect : set -> set -> set.
Parameter incl : set -> set -> bool.
Parameter elems : set -> list dom.
Axiom In_add : forall s v v',
In v' (add s v) = true
<-> v = v' \/ In v' s = true.
Axiom In_add_eq : forall s v,
In v (add s v) = true.
Axiom In_add_neq : forall s v v',
v <> v'
-> In v' (add s v) = In v' s.
Axiom In_union : forall s s' v,
In v (union s s') = true
-> In v s = true \/ In v s' = true.
Axiom In_union' : forall s s' v,
In v s = true
-> In v s' = true
-> In v (union s s') = true.
Axiom union_idempotent : forall s,
union s s = s.
Axiom In_intersect : forall v s' s,
In v (intersect s s') = true
-> In v s = true /\ In v s' = true.
Axiom In_intersect' : forall v s' s,
In v (intersect s s') = false
-> In v s = false \/ In v s' = false.
Axiom incl_ok : forall s1 s2,
incl s1 s2 = true <-> (forall x, In x s1 = true -> In x s2 = true).
Axiom incl_empty : forall s,
incl empty s = true.
Axiom In_empty : forall x,
In x empty = false.
Axiom incl_refl : forall s,
incl s s = true.
Axiom incl_false : forall s1 s2,
incl s1 s2 = false
-> exists x, In x s1 = true /\ In x s2 = false.
Axiom incl_trans : forall s1 s2,
incl s1 s2 = true
-> forall s3, incl s2 s3 = true
-> incl s1 s3 = true.
Axiom incl_In : forall s1 s2,
incl s1 s2 = true
-> forall x, In x s1 = true
-> In x s2 = true.
Axiom incl_union_left : forall s1 s2,
incl s1 (union s1 s2) = true.
Axiom incl_union_right : forall s1 s2,
incl s2 (union s1 s2) = true.
Axiom elems_ok : forall s x,
List.In x (elems s) <-> In x s = true.
Axiom elems_remove : forall s x ls,
elems s = x :: ls
-> elems (remove s x) = ls.
Axiom In_remove : forall x x' s,
In x s = true
-> x <> x'
-> In x (remove s x') = true.
End SET.
Module ListSet (Param : EQ) : SET with Definition dom := Param.dom.
Import Param.
Section Map.
Definition set := list dom.
Definition empty : set := nil.
Definition In (v : dom) (s : set) : bool :=
if In_eq_dec dom_eq_dec v s
then true
else false.
Definition add (s : set) (v : dom) : set :=
if In_eq_dec dom_eq_dec v s
then s
else v :: s.
Fixpoint remove (s : set) (v : dom) {struct s} : set :=
match s with
| nil => nil
| v' :: s' =>
if dom_eq_dec v v'
then s'
else v' :: remove s' v
end.
Fixpoint union (s1 s2 : set) {struct s1} : set :=
match s1 with
| nil => s2
| v :: s1' => add (union s1' s2) v
end.
Fixpoint intersect (s1 s2 : set) {struct s1} : set :=
match s1 with
| nil => nil
| v :: s1' =>
if In_eq_dec dom_eq_dec v s2
then v :: intersect s1' s2
else intersect s1' s2
end.
Definition incl (s1 s2 : set) : bool :=
if incl_eq_dec dom_eq_dec s1 s2
then true
else false.
Definition elems (s : set) : list dom := s.
Theorem In_add : forall s v v',
In v' (add s v) = true
<-> v = v' \/ In v' s = true.
Theorem In_add_eq : forall s v,
In v (add s v) = true.
Theorem In_add_neq : forall s v v',
v <> v'
-> In v' (add s v) = In v' s.
Theorem In_union : forall s s' v,
In v (union s s') = true
-> In v s = true \/ In v s' = true.
Theorem In_union' : forall s s' v,
In v s = true
-> In v s' = true
-> In v (union s s') = true.
Theorem incl_ok : forall s1 s2,
incl s1 s2 = true <-> (forall x, In x s1 = true -> In x s2 = true).
Lemma union_idempotent' : forall s s',
List.incl s s'
-> union s s' = s'.
Theorem In_intersect : forall v s' s,
In v (intersect s s') = true
-> In v s = true /\ In v s' = true.
Theorem In_intersect' : forall v s' s,
In v (intersect s s') = false
-> In v s = false \/ In v s' = false.
Theorem union_idempotent : forall s,
union s s = s.
Theorem incl_empty : forall s,
incl empty s = true.
Theorem In_empty : forall x,
In x empty = false.
Theorem incl_refl : forall s,
incl s s = true.
Theorem incl_false : forall s1 s2,
incl s1 s2 = false
-> exists x, In x s1 = true /\ In x s2 = false.
Theorem incl_trans : forall s1 s2,
incl s1 s2 = true
-> forall s3, incl s2 s3 = true
-> incl s1 s3 = true.
Theorem incl_In : forall s1 s2,
incl s1 s2 = true
-> forall x, In x s1 = true
-> In x s2 = true.
Theorem incl_union_left : forall s1 s2,
incl s1 (union s1 s2) = true.
Theorem incl_union_right : forall s1 s2,
incl s2 (union s1 s2) = true.
Theorem elems_ok : forall s x,
List.In x (elems s) <-> In x s = true.
Theorem elems_remove : forall s x ls,
elems s = x :: ls
-> elems (remove s x) = ls.
Theorem In_remove : forall x x' s,
In x s = true
-> x <> x'
-> In x (remove s x') = true.
End Map.
Definition dom := dom.
End ListSet.
Index
This page has been generated by coqdoc