Library Asm.Util.Map
Require Import Bool Peano_dec Compare_dec Omega List.
Set Implicit Arguments.
Definition eq_dec (t : Set) := forall (e1 e2 : t), {e1 = e2} + {e1 <> e2}.
Inductive ord (T : Set) : T -> T -> Prop :=
| OrdEq : forall e1 e2, e1 = e2 -> ord e1 e2
| OrdLt : forall e1 e2, e1 <> e2 -> ord e1 e2
| OrdGt : forall e1 e2, e1 <> e2 -> ord e1 e2.
Definition ord_dec (t : Set) := forall (e1 e2 : t), ord e1 e2.
Module Type ORDERED_SET.
Parameter t : Set.
Axiom eq_dec : eq_dec t.
Parameter lt : t -> t -> Prop.
Axiom lt_dec : forall e1 e2, {lt e1 e2} + {~lt e1 e2}.
Axiom lt_irr : forall e, ~lt e e.
Axiom neq_lt : forall e1 e2, e1 <> e2 -> lt e1 e2 \/ lt e2 e1.
Axiom lt_asym : forall e1 e2, lt e1 e2 -> ~lt e2 e1.
End ORDERED_SET.
Module Type FINITE.
Parameter t : Set.
Parameter to_nat : t -> nat.
Axiom inj : forall t1 t2, t1 = t2 <-> to_nat t1 = to_nat t2.
End FINITE.
Module FiniteOrderedSet (S : FINITE).
Import S.
Definition t := t.
Theorem eq_dec : eq_dec t.
Definition lt a b := to_nat a < to_nat b.
Theorem lt_dec : forall e1 e2, {lt e1 e2} + {~lt e1 e2}.
Theorem lt_irr : forall e, ~lt e e.
Theorem neq_lt : forall e1 e2, e1 <> e2 -> lt e1 e2 \/ lt e2 e1.
Theorem lt_asym : forall e1 e2, lt e1 e2 -> ~lt e2 e1.
End FiniteOrderedSet.
Definition eq_dec_to_eq (T : Set) (eq_dec : forall (e1 e2 : T), {e1 = e2} + {e1 <> e2}) e1 e2 :=
if eq_dec e1 e2 then true else false.
Module TotalMap (T : ORDERED_SET).
Import T.
Parameter map : Set -> Set.
Parameter empty : forall (V : Set), V -> map V.
Parameter sel : forall V, map V -> t -> V.
Parameter upd : forall V, map V -> t -> V -> map V.
Axiom sel_empty : forall (V : Set) (v : V) x,
sel (empty v) x = v.
Axiom sel_eq : forall (V : Set) m x (v : V),
sel (upd m x v) x = v.
Axiom sel_neq : forall (V : Set) m x (v : V) x',
x <> x' -> sel (upd m x v) x' = sel m x'.
Parameter subMap : forall (V : Set)
(P : V -> V -> bool) (Prefl : forall v, P v v = true)
(M1 M2 : map V), {b : bool |
b = true -> forall n, P (sel M1 n) (sel M2 n) = true}.
Parameter eq_dec : forall ran : Set, (forall (x y : ran), {x = y} + {x <> y})
-> forall (m1 m2 : map ran),
{m1 = m2} + {m1 <> m2}.
Parameter mapMap : forall (V V' : Set) (f : V -> V')
(m : map V), {m' : map V'
| forall k, sel m' k = f (sel m k)}.
Parameter mapMapi : forall (V V' : Set) (f : t -> V -> V')
(m : map V), {m' : map V'
| forall k, sel m' k = f k (sel m k)}.
End TotalMap.
Index
This page has been generated by coqdoc