Commit 12305b37 authored by Andrew Hirsch's avatar Andrew Hirsch
Browse files

Comments for maps.

parent e7cd0f54
......@@ -6,12 +6,15 @@ Require Import Coq.Lists.SetoidList.
Require Import Coq.FSets.FMapInterface.
Require Import Coq.Program.Wf.
(*
Implements LocationMap via a function with a (tracked) finite domain.
*)
Module FunLMap (L : Locations) <: (LocationMap L).
Record funlmap (elt : Set) : Set :=
{
the_fun : L.t -> option elt;
dom : list L.t;
the_fun : L.t -> option elt; (* the underlying funcion *)
dom : list L.t; (* we track the (finite) domain of the function *)
dom_spec : forall l, In l dom -> the_fun l <> None
}.
Definition t := funlmap.
......@@ -34,6 +37,7 @@ Module FunLMap (L : Locations) <: (LocationMap L).
| nil => true
| cons _ _ => false
end.
Definition add (l : L.t) (e : elt) (m : t elt) : t elt.
refine ({|
the_fun := fun l' =>
......@@ -49,6 +53,10 @@ Module FunLMap (L : Locations) <: (LocationMap L).
apply (dom_spec m); auto.
Defined.
(*
We define this boolean in function for locations as a convenience. We then use it
to define find for maps.
*)
Fixpoint inb (l : L.t) ( : list L.t) : bool :=
match with
| nil => false
......@@ -70,6 +78,10 @@ Module FunLMap (L : Locations) <: (LocationMap L).
Definition find (l : L.t) (m : t elt) : option elt :=
if inb l (dom m) then the_fun m l else None.
(*
We start by focusing on removing a location from a list. We prove several results about
this list operation before using it to define the operation on maps.
*)
Fixpoint remove_location ( : list L.t) (l : L.t) : list L.t :=
match with
| nil => nil
......@@ -109,7 +121,13 @@ Module FunLMap (L : Locations) <: (LocationMap L).
destruct i as [eq | i]; [subst; destruct (neq eq_refl)|]. apply IH; auto.
destruct i as [eq | i]; [subst; left; reflexivity|right; apply IH; auto].
Qed.
(*
To remove a location, we both remove it from the domain of our function and we ensure
that the underlying function returns None. We use refine here so that we can use tactics
to prove dom_spec still holds. This will be a common pattern throughout this module.
*)
Definition remove (l : L.t) (m : t elt) : t elt.
refine ({|
the_fun := fun l' => if L.eq_dec l l'
......@@ -123,8 +141,7 @@ Module FunLMap (L : Locations) <: (LocationMap L).
apply l_not_in_remove_l in H; destruct H.
apply remove_location_lift_In in H. apply (dom_spec m); auto.
Defined.
Definition mem (l : L.t) (m : t elt) : bool := inb l (dom m).
Program Fixpoint elements' (f : L.t -> option elt) (ls : list L.t) :
......@@ -251,19 +268,6 @@ Module FunLMap (L : Locations) <: (LocationMap L).
1,2: apply IHl0; auto.
Defined.
(* Definition fold {A : Type} (f : L.t -> elt -> A -> A) (m : t elt) (a : A) : A. *)
(* refine ((fix g (ls : list L.t) (ls_dom : forall l, In l ls -> the_fun m l <> None) : A := *)
(* match ls as ls' return ls = ls' -> A with *)
(* | nil => fun _ => a *)
(* | l :: ls => fun eq => match the_fun m l as oe return the_fun m l = oe -> A with *)
(* | Some e => fun eq' => f l e (g ls _) *)
(* | None => fun eq' => _ *)
(* end eq_refl *)
(* end eq_refl) (dom m) (dom_spec m)). *)
(* intros l' i; subst; apply ls_dom; right; auto. *)
(* subst; exfalso; apply (ls_dom l); [left|]; auto. *)
(* Defined. *)
Fixpoint subsetlistb (ls1 ls2: list L.t) : bool :=
match ls1 with
| nil => true
......
......@@ -6,15 +6,15 @@ Require Import Coq.Lists.SetoidList.
Require Import Coq.FSets.FMapInterface.
Require Import Coq.Program.Wf.
(* Maps keyed by locations *)
(* Finite maps keyed by locations. *)
Module Type LocationMap (L : Locations).
(* Include (LocationNotations L). *)
Parameter t : Set -> Set.
Set Implicit Arguments.
Section Types.
Variable elt : Set.
(* Map operations *)
Parameter empty : t elt.
Parameter is_empty : t elt -> bool.
Parameter add : L.t -> elt -> t elt -> t elt.
......@@ -22,29 +22,20 @@ Module Type LocationMap (L : Locations).
Parameter remove : L.t -> t elt -> t elt.
Parameter mem : L.t -> t elt -> bool.
Parameter elements : t elt -> list (L.t * elt).
(* Parameter cardinal : t elt -> nat. *)
Variable elt' elt'' : Set.
(* Parameter map : (elt -> elt') -> t elt -> t elt'. *)
(* Parameter mapi : (L.t -> elt -> elt') -> t elt -> t elt'. *)
(* Parameter map2 : (option elt -> option elt' -> option elt'') -> t elt -> t elt' -> t elt''. *)
(* (* Parameter fold : forall {A : Type}, (L.t -> elt -> A -> A) -> t elt -> A -> A. *) *)
(* Parameter equal : (elt -> elt -> bool) -> t elt -> t elt -> bool. *)
(* Specifications of the map operations. *)
Section spec.
Variable m m' m'' : t elt.
Variable x y z : L.t.
Variable e e' : elt.
Variable m m' m'' : t elt. (* Maps *)
Variable x y z : L.t. (* Locations/Keys *)
Variable e e' : elt. (* Elements *)
Parameter MapsTo : L.t -> elt -> t elt -> Prop.
Definition In (k : L.t) (m : t elt) : Prop := exists e : elt, MapsTo k e m.
Definition Empty m := forall (a : L.t) (e : elt), ~ MapsTo a e m.
Definition eq_key (p p' : L.t * elt) := fst p = fst p'.
(* Definition eq_key_elt (p p' : L.t * elt) := fst p = fst p' /\ snd p = snd p'. *)
(* Definition lt_key (p p' : L.t * elt) := fst p < fst p'. *)
Parameter mem_1 : In x m -> mem x m = true.
Parameter mem_2 : mem x m = true -> In x m.
......@@ -70,58 +61,57 @@ Module Type LocationMap (L : Locations).
Parameter elements_3w : NoDupA eq_key (elements m).
(* Parameter cardinal_1 : cardinal m = length (elements m). *)
(* Parameter fold_1 : forall (A : Type) (i : A) (f : L.t -> elt -> A -> A), *)
(* fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i. *)
Definition Equal m m' := forall y, find y m = find y m'.
Definition Equiv (eq_elt : elt -> elt -> Prop) m m' :=
(forall k, In k m <-> In k m') /\ (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e').
Definition Equivb (cmp : elt -> elt -> bool) := Equiv (fun e1 e2 => cmp e1 e2 = true).
Variable cmp : elt -> elt -> bool.
(* Parameter equal_1 : Equivb cmp m m' -> equal cmp m m' = true. *)
(* Parameter equal_2 : equal cmp m m' = true -> Equivb cmp m m'. *)
End spec.
End Types.
Arguments empty {elt}.
(* Parameter map_1 : forall (elt elt' : Set) (m : t elt) (x : L.t) (e : elt)(f : elt -> elt'), MapsTo x e m -> MapsTo x (f e) (map f m). *)
(* Parameter map_2 : forall (elt elt' : Set) (m : t elt) (x : L.t) (f : elt -> elt'), In x (map f m) -> In x m. *)
(* Parameter mapi_1 : forall (elt elt' : Set) (m : t elt) (x : L.t) (e : elt) (f: L.t -> elt -> elt'), MapsTo x e m -> MapsTo x (f x e) (mapi f m). *)
(* Parameter mapi_2 : forall (elt elt' : Set) (m : t elt) (x : L.t) (f : L.t -> elt -> elt'), In x (mapi f m) -> In x m. *)
(* Parameter map2_1 : forall (elt elt' elt'' : Set) (m : t elt) (m' : t elt') (x : L.t) (f : option elt -> option elt' -> option elt''), *)
(* In x m \/ In x m' -> find x (map2 f m m') = f (find x m) (find x m'). *)
(* Parameter map2_2 : forall (elt elt' elt'' : Set) (m : t elt) (m' : t elt') (x : L.t) (f : option elt -> option elt' -> option elt''), *)
(* In x (map2 f m m') -> In x m \/ In x m'. *)
Global Hint Immediate mem_2 is_empty_2 add_3 remove_3 find_2 : lmap.
Global Hint Resolve mem_1 is_empty_1 add_1 add_2 remove_1 remove_2 find_1 : lmap.
End LocationMap.
(*
Things provable about any LocationMap. These are in another module so that they do not
need to be repeated in every LocationMap module.
*)
Module LocationMapFacts (L : Locations) (LM : LocationMap L).
(*
Locations do not mapt to two different elements.
*)
Lemma MapsToUnique : forall {elt : Set} {m : LM.t elt} {l : L.t} {e1 e2 : elt}, LM.MapsTo l e1 m -> LM.MapsTo l e2 m -> e1 = e2.
Proof using.
intros elt m l e1 e2 mt1 mt2; apply LM.find_1 in mt1; apply LM.find_1 in mt2; rewrite mt1 in mt2; inversion mt2; reflexivity.
Qed.
Lemma MapsTo2In : forall {elt : Set} {m : LM.t elt} {l : L.t} {e : elt}, LM.MapsTo l e m -> LM.In l m.
Proof using.
intros elt m l e mt; exists e; exact mt.
Qed.
Lemma find_None : forall {elt : Set} {m : LM.t elt} {l : L.t}, LM.find l m = None -> forall (e : elt), ~ LM.MapsTo l e m.
(*
`find l m` returns `None` if and only if `l` is not bound in `m`.
*)
Lemma find_None_1 : forall {elt : Set} {m : LM.t elt} {l : L.t}, LM.find l m = None -> forall (e : elt), ~ LM.MapsTo l e m.
Proof using.
intros elt m l eq e mt; apply LM.find_1 in mt; rewrite mt in eq; inversion eq.
Qed.
Lemma find_None_2 : forall {elt : Set} {m : LM.t elt} {l : L.t}, ~ LM.In l m -> LM.find l m = None.
Proof using.
intros elt m l H. destruct (LM.find l m) eqn:eq; auto.
apply LM.find_2 in eq. destruct (H (ex_intro _ e eq)).
Qed.
(*
`find_add_1` and `find_add_2` tell us how find behaves on a map of the form `add l e m`.
*)
Lemma find_add_1 : forall {elt : Set} (m : LM.t elt) (l : L.t) (e : elt), LM.find l (LM.add l e m) = Some e.
Proof using.
intros elt m l e. apply LM.find_1. apply LM.add_1.
Qed.
Lemma find_add_2 : forall {elt : Set} (m : LM.t elt) (l l' : L.t) (e : elt), l <> l' -> LM.find l (LM.add l' e m) = LM.find l m.
Proof using.
intros elt m l l' e H. destruct (LM.find l (LM.add l' e m)) eqn:eq. apply LM.find_2 in eq. apply LM.add_3 in eq; auto. apply LM.find_1 in eq; auto.
......@@ -129,6 +119,10 @@ Module LocationMapFacts (L : Locations) (LM : LocationMap L).
transitivity (LM.find l (LM.add l' e m)); auto.
Qed.
(*
find_remove_1 and find_remove_2 tell us how find behaves on a map of the form
`remove l m`.
*)
Lemma find_remove_1 : forall {elt : Set} (m : LM.t elt) (l : L.t), LM.find l (LM.remove l m) = None.
Proof using.
intros elt m l; destruct (LM.find l (LM.remove l m)) eqn:eq; [|reflexivity].
......@@ -142,14 +136,9 @@ Module LocationMapFacts (L : Locations) (LM : LocationMap L).
apply LM.find_1 in eq'; rewrite eq' in eq; inversion eq.
Qed.
(* Lemma map2_3 : forall {elt1 elt2 elt3 : Set} {f : option elt1 -> option elt2 -> option elt3} {m1 : LM.t elt1} {m2 : LM.t elt2} {l : L.t}, *)
(* LM.find l m1 = None -> LM.find l m2 = None -> LM.find l (LM.map2 f m1 m2) = None. *)
(* Proof using. *)
(* intros elt1 elt2 elt3 f m1 m2 l H H0. *)
(* destruct (LM.find l (LM.map2 f m1 m2)) eqn:eq; auto. *)
(* assert (LM.In l (LM.map2 f m1 m2)) as i by (apply LM.find_2 in eq; exists e; auto). *)
(* apply LM.map2_2 in i; destruct i as [i|i]; destruct i as [n mt]; apply LM.find_1 in mt; exfalso; [rewrite mt in H; inversion H | rewrite mt in H0; inversion H0]. *)
(* Qed. *)
(*
Equal is a equivalence relation.
*)
Instance lm_Equal_refl : forall {elt : Set}, Reflexive (@LM.Equal elt).
Proof using.
intros elt. unfold Reflexive; intro m; unfold LM.Equal; intro y; reflexivity.
......@@ -163,33 +152,8 @@ Module LocationMapFacts (L : Locations) (LM : LocationMap L).
intros elt; unfold Transitive; intros m1 m2 m3; unfold LM.Equal; intros H1 H2 l;
transitivity (LM.find l m2); auto.
Qed.
(* Lemma elements_1a : forall {elt : Set} (l : L.t) (e : elt) (m : LM.t elt), LM.MapsTo l e m -> In (l, e) (LM.elements m). *)
(* Proof using. *)
(* intros elt l e m mt. apply LM.elements_1 in mt. induction (LM.elements m). inversion mt. *)
(* inversion mt; subst. *)
(* destruct a. inversion H0. cbn in H; cbn in H1; subst; left; auto. *)
(* right; apply IHl0; auto. *)
(* Qed. *)
(* Definition map_option {elt elt' : Set} (f : elt -> option elt') (m : LM.t elt) : LM.t elt' := *)
(* LM.map2 (fun (x : option elt) (_ : option elt) => match x with *)
(* | Some y => f y *)
(* | None => None *)
(* end) m m. *)
(* Lemma map_option_1 : forall {elt elt' : Set} (f : elt -> option elt') (m : LM.t elt) (l : L.t) (e : elt) (e' : elt'), *)
(* LM.MapsTo l e m -> LM.find l (map_option f m) = f e. *)
(* Proof using. *)
(* intros elt elt' f m l e e' mt. *)
(* unfold map_option. *)
(* rewrite LM.map2_1. rewrite LM.find_1 with (e := e); auto. *)
(* left; unfold LM.In; exists e; auto. *)
(* Qed. *)
Lemma find_None_2 : forall {elt : Set} {m : LM.t elt} {l : L.t}, ~ LM.In l m -> LM.find l m = None.
Proof using.
intros elt m l H. destruct (LM.find l m) eqn:eq; auto.
apply LM.find_2 in eq. destruct (H (ex_intro _ e eq)).
Qed.
End LocationMapFacts.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment