Commit 8caf0587 authored by Andrew Hirsch's avatar Andrew Hirsch
Browse files

Updated LocationMap to not use a bunch of things that I'm not using.

parent 2617def4
......@@ -4445,14 +4445,10 @@ Module ChoreographyCompiler (Import E : Expression) (L : Locations) (LM : Locati
pose proof (InAddFromMap1 (LM.elements Π1) Π21);
intros p E1 E2 E3; split; [intro i; split; [|split] | intros [mt1 [mt2 mt3]]];
[ apply H2 in i; destruct i; apply H3 in H4; destruct H4;
apply LM.elements_2; unfold LM.eq_key_elt; apply InA_altdef;
apply Exists_exists; exists (p,E1); split; [|split]; cbn ;auto
apply LM.elements_2; auto
| apply H2 in i; destruct i; apply H3 in H4; apply H4
| apply H2 in i; apply i
| apply LM.elements_1 in mt1; unfold LM.eq_key_elt in mt1;
apply InA_altdef in mt1; apply Exists_exists in mt1;
destruct mt1 as [[q E1'] [i1 [eq1 eq2]]]; cbn in *;
symmetry in eq1; symmetry in eq2; subst;
| apply LM.elements_1 in mt1;
pose proof (proj2 (H3 p E1 E2) ltac:(split; auto));
apply H2; split ; auto]).
assert (forall p E1 E2 E3, In (p, E1, E2, E3) l -> LessNondet E2 E1 /\ ConExprStep E1 L E3).
......
......@@ -4286,14 +4286,10 @@ Module InternalConcurrentLambda (Import E : Expression) (L : Locations) (LM : Lo
pose proof (InAddFromMap1 (LM.elements Π1) Π21);
intros p E1 E2 E3; split; [intro i; split; [|split] | intros [mt1 [mt2 mt3]]];
[ apply H2 in i; destruct i; apply H3 in H4; destruct H4;
apply LM.elements_2; unfold LM.eq_key_elt; apply InA_altdef;
apply Exists_exists; exists (p,E1); split; [|split]; cbn ;auto
apply LM.elements_2; auto
| apply H2 in i; destruct i; apply H3 in H4; apply H4
| apply H2 in i; apply i
| apply LM.elements_1 in mt1; unfold LM.eq_key_elt in mt1;
apply InA_altdef in mt1; apply Exists_exists in mt1;
destruct mt1 as [[q E1'] [i1 [eq1 eq2]]]; cbn in *;
symmetry in eq1; symmetry in eq2; subst;
| apply LM.elements_1 in mt1;
pose proof (proj2 (H3 p E1 E2) ltac:(split; auto));
apply H2; split ; auto]).
assert (forall p E1 E2 E3, In (p, E1, E2, E3) l -> LessNondet E1 E2 /\ ConExprStep E1 L E3).
......
This diff is collapsed.
Require Export Locations LocationMap.
Require Import Coq.Structures.Orders Coq.Structures.Equalities.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Lists.SetoidList.
Require Import Coq.FSets.FMapInterface.
Require Import Coq.Program.Wf.
Module ListLMap (L : Locations) <: (LocationMap L).
Import ListNotations.
Definition t (elt : Set) := list (L.t * elt) : Set.
Definition empty (elt : Set) := @nil (L.t * elt).
Definition is_empty elt : t elt -> bool :=
fun m => match m with
| [] => true
| _ :: _ => false
end.
Definition add (elt : Set) (l : L.t) (e : elt) (m : t elt) : t elt := (l, e) :: m.
Fixpoint find (elt : Set) (l : L.t) (m : t elt) : option elt :=
match m with
| [] => None
| (l', e) :: m => if L.eq_dec l l'
then Some e
else find elt l m
end.
Fixpoint remove elt (l : L.t) (m : t elt) : t elt :=
match m with
| [] => []
| (l', e) :: m => if L.eq_dec l l'
then remove elt l m
else (l', e) :: remove elt l m
end.
Lemma remove_length : forall {elt} l m, length (remove elt l m) <= length m.
Proof using.
intros elt l m; induction m; cbn; auto.
destruct a as [l' e]. destruct (L.eq_dec l l'); subst.
transitivity (length m); auto.
cbn. apply le_n_S; auto.
Qed.
Fixpoint mem elt (l : L.t) (m : t elt) : bool :=
match m with
| [] => false
| (l', e) :: m => if L.eq_dec l l'
then true
else mem elt l m
end.
(* Fixpoint elements' {elt : Type} (m : t elt) (n : nat) : list (L.t * elt) := *)
(* match n with *)
(* | 0 => [] *)
(* | S n => match m with *)
(* | [] => [] *)
(* | (l, e) :: m => (l, e) :: elements' (remove elt l m) n *)
(* end *)
(* end. *)
(* Lemma elements'_mono : forall {elt : Type} (m : t elt) (n k : nat) (l : L.t) (e : elt), *)
(* n <= k -> List.In (l, e) (elements' m n) -> List.In (l, e) (elements' m k). *)
(* Proof using. *)
(* intros elt m n; revert m; induction n as [|n]; intros m k l e bd i; cbn in *. *)
(* destruct i. *)
(* destruct k. destruct (PeanoNat.Nat.nle_succ_0 _ bd). *)
(* cbn. destruct m as [|[l' e'] m]; auto. *)
(* destruct i; [left|right]; auto. *)
(* apply IHn; auto. apply le_S_n; auto. *)
(* Qed. *)
(* Definition elements elt (m : t elt) : list (L.t * elt) := elements' m (length m). *)
(* Fixpoint cardinal' {elt : Type} (m : t elt) (n : nat) : nat := *)
(* match n with *)
(* | 0 => 0 *)
(* | S n => match m with *)
(* | [] => 0 *)
(* | (l, e) :: m => S (cardinal' (remove elt l m) n) *)
(* end *)
(* end. *)
(* Definition cardinal elt (m : t elt) : nat := cardinal' m (length m). *)
(* Fixpoint map elt elt' (f : elt -> elt') (m : t elt) : t elt' := *)
(* match m with *)
(* | [] => [] *)
(* | (l, e) :: m => (l, f e) :: (map elt elt' f m) *)
(* end. *)
(* Fixpoint mapi elt elt' (f : L.t -> elt -> elt') (m : t elt) : t elt' := *)
(* match m with *)
(* | [] => [] *)
(* | (l, e) :: m => (l, f l e) :: mapi elt elt' f m *)
(* end. *)
(* Fixpoint addones_l {elt elt'} (m2 : t elt') : list (L.t * option elt * option elt') := *)
(* match m2 with *)
(* | [] => [] *)
(* | (l, e) :: m => (l, None, Some e) :: addones_l m *)
(* end. *)
(* Fixpoint zip {elt elt'} (m1 : t elt) (m2 : t elt') : list (L.t * option elt * option elt') := *)
(* match m1 with *)
(* | [] => addones_l m2 *)
(* | (l, e) :: m1 => (l, Some e, find elt' l m2) :: zip m1 (remove elt' l m2) *)
(* end. *)
(* Fixpoint map_zip {elt elt' elt''} (f : option elt -> option elt' -> option elt'') *)
(* (ls : list (L.t * option elt * option elt')) : t elt'' := *)
(* match ls with *)
(* | [] => [] *)
(* | (l, oe1, oe2) :: ls => match f oe1 oe2 with *)
(* | Some e => (l, e) :: map_zip f ls *)
(* | None => map_zip f ls *)
(* end *)
(* end. *)
(* Fixpoint fold_zip {elt elt' A} (f : option elt -> option elt' -> A -> A) (ls : list (L.t * option elt * option elt')) (a : A) : A := *)
(* match ls with *)
(* | [] => a *)
(* | (l, oe1, oe2) :: ls => f oe1 oe2 (fold_zip f ls a) *)
(* end. *)
(* Definition map2 elt elt' elt'' (f : option elt -> option elt' -> option elt'') (m1 : t elt) (m2 : t elt') : t elt'' := *)
(* map_zip f (zip m1 m2). *)
(* Fixpoint fold elt {A : Type} (f : L.t -> elt -> A -> A) (m : t elt) (a : A) : A := *)
(* match m with *)
(* | [] => a *)
(* | (l, e) :: m => f l e (fold elt f m a) *)
(* end. *)
(* Definition equal elt (test: elt -> elt -> bool) (m1 m2 : t elt) : bool := *)
(* fold_zip (fun oe1 oe2 b => match oe1, oe2 with *)
(* | Some e1, Some e2 => andb (test e1 e2) b *)
(* | _, _ => false *)
(* end) (zip m1 m2) true. *)
Definition MapsTo (elt : Set) (l : L.t) (e : elt) (m : t elt) : Prop :=
find elt l m = Some e.
Definition In elt (k : L.t) (m : t elt) : Prop := exists e : elt, MapsTo elt k e m.
Definition Empty (elt : Set) m := forall (a : L.t) (e : elt), ~ MapsTo elt a e m.
Definition eq_key (elt : Set) (p p' : L.t * elt) := fst p = fst p'.
Definition eq_key_elt (elt : Set) (p p' : L.t * elt) := fst p = fst p' /\ snd p = snd p'.
Theorem mem_1 (elt : Set) (m : t elt) (x : L.t) : In elt x m -> mem elt x m = true.
Proof using.
intros i; unfold In in i; destruct i as [e mt]; unfold MapsTo in mt.
induction m as [| [l e'] m]; cbn in *.
inversion mt. destruct (L.eq_dec x l); subst; auto.
Qed.
Theorem mem_2 (elt : Set) (m : t elt) (x : L.t) : mem elt x m = true -> In elt x m.
Proof using.
unfold In; unfold MapsTo; intro eq.
induction m as [| [l e] m]; cbn in *; try discriminate.
destruct (L.eq_dec x l); subst.
exists e; reflexivity.
apply IHm; auto.
Qed.
Theorem empty_1 (elt : Set) : Empty elt (empty elt).
Proof using.
unfold Empty; intros a e mt; unfold MapsTo in mt; cbn in mt; inversion mt.
Qed.
Theorem is_empty_1 (elt : Set) (m : t elt) : Empty elt m -> is_empty elt m = true.
Proof using.
unfold Empty; unfold MapsTo; intros empt; induction m as [|[l e] m]; cbn in *; auto.
specialize (empt l e). destruct (L.eq_dec l l).
destruct (empt eq_refl). destruct (n eq_refl).
Qed.
Theorem is_empty_2 (elt : Set) (m : t elt) : is_empty elt m = true -> Empty elt m.
Proof using.
unfold Empty; unfold MapsTo; intros ie l e;
induction m as [| [l' e'] m]; cbn in *; discriminate.
Qed.
Theorem add_1 (elt : Set) (m : t elt) (x : L.t) (e : elt) : MapsTo elt x e (add elt x e m).
Proof using.
unfold MapsTo; cbn. destruct (L.eq_dec x x) as [_ | n]; [| destruct (n eq_refl)].
reflexivity.
Qed.
Theorem add_2 (elt : Set) (m : t elt) (x y : L.t) (e e' : elt) :
x <> y -> MapsTo elt y e m -> MapsTo elt y e (add elt x e' m).
Proof using.
unfold MapsTo; intros neq mt; cbn.
destruct (L.eq_dec y x) as [eq | _] ; [destruct (neq (eq_sym eq))|]; auto.
Qed.
Theorem add_3 (elt : Set) (m : t elt) (x y : L.t) (e e' : elt) :
x <> y -> MapsTo elt y e (add elt x e' m) -> MapsTo elt y e m.
Proof using.
unfold MapsTo; intros neq mt; cbn in *.
destruct (L.eq_dec y x) as [eq | _ ]; [destruct (neq (eq_sym eq))|]; auto.
Qed.
Theorem remove_1 (elt : Set) (m : t elt) (x : L.t) : ~ In elt x (remove elt x m).
Proof using.
unfold In; unfold MapsTo. induction m as [|[l e] m]; cbn.
intros [e eq]; inversion eq.
intros [e' eq]. destruct (L.eq_dec x l); subst.
apply IHm; exists e'; auto.
cbn in eq. destruct (L.eq_dec x l); subst. destruct (n eq_refl).
apply IHm; exists e'; auto.
Qed.
Theorem remove_2 (elt : Set) (m : t elt) (x y : L.t) (e : elt)
: x <> y -> MapsTo elt y e m -> MapsTo elt y e (remove elt x m).
Proof using.
intros neq mt; unfold MapsTo in *.
induction m as [| [l e'] m]; cbn in *; auto.
destruct (L.eq_dec y l); destruct (L.eq_dec x l); subst.
destruct (neq eq_refl).
cbn; destruct (L.eq_dec l l) as [_ | n']; [|destruct (n' eq_refl)]; auto.
apply IHm; auto.
cbn. destruct (L.eq_dec y l) as [eq | _]; [destruct (n eq)|]; apply IHm; auto.
Qed.
Theorem remove_3 (elt : Set) (m : t elt) (x y : L.t) (e : elt) :
x <> y -> MapsTo elt y e (remove elt x m) -> MapsTo elt y e m.
Proof using.
unfold MapsTo; intros neq mt; induction m as [|[l e'] m]; cbn in *; auto.
destruct (L.eq_dec x l); destruct (L.eq_dec y l) ;subst.
destruct (neq eq_refl).
apply IHm; auto.
cbn in mt; destruct (L.eq_dec l l) as [_|n'];[|destruct (n' eq_refl)]; auto.
apply IHm; auto.
cbn in mt; destruct (L.eq_dec y l) as [eq|_];[destruct (n0 eq)|]; auto.
Qed.
Theorem find_1 (elt : Set) (m : t elt) (x : L.t) (e : elt) :
MapsTo elt x e m -> find elt x m = Some e.
Proof using.
unfold MapsTo; auto.
Qed.
Theorem find_2 (elt : Set) (m : t elt) (x : L.t) (e : elt) :
find elt x m = Some e -> MapsTo elt x e m.
Proof using.
unfold MapsTo; auto.
Qed.
Lemma InA_eq_key_elt : forall {elt} l e ls, InA (eq_key_elt elt) (l, e) ls <-> List.In (l, e) ls.
Proof using.
intros elt l e ls; induction ls as [| [l' e'] ls]; cbn; split; auto; intro i.
1,2: inversion i.
inversion i; subst. unfold eq_key_elt in H0; destruct H0; cbn in *; subst.
left; auto. right; apply IHls; auto.
destruct i as [eq | i]; [destruct eq; subst|].
left. unfold eq_key_elt; split; cbn; reflexivity. right; apply IHls; auto.
Qed.
(* Theorem elements'_1 (elt : Type) (m : t elt) (x : L.t) (e : elt) : *)
(* MapsTo elt x e m -> forall n, length m <= n -> InA (eq_key_elt elt) (x, e) (elements' m n). *)
(* Proof using. *)
(* unfold MapsTo; intros mt n len. *)
(* induction m as [|[l e'] m]; cbn in *; try discriminate. *)
(* destruct n. destruct (PeanoNat.Nat.nle_succ_0 _ len). *)
(* cbn. destruct (L.eq_dec x l); subst. left; unfold eq_key_elt; cbn. *)
(* inversion mt; subst; split; auto. *)
(* right. rewrite InA_eq_key_elt. rewrite InA_eq_key_elt in IHm. *)
(* eapply elements'_mono. [|apply IHm]. *)
(* Theorem elements_1 (elt : Type) (m : t elt) (x : L.t) (e : elt) : *)
(* MapsTo elt x e m -> InA (eq_key_elt elt) (x, e) (elements elt m). *)
(* Proof using. *)
(* unfold MapsTo; unfold eq_key_elt; intros eq. *)
(* induction m as [|[l e'] m]; cbn in *. inversion eq. *)
(* destruct (remove elt l m) as [|m']. *)
(* Parameter elements_2 : InA eq_key_elt (x, e) (elements m) -> MapsTo x e m. *)
(* Parameter elements_3w : NoDupA eq_key (elements m). *)
(* Parameter elements_3 : sort lt_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 (elt : Set) (m m' : t elt) := forall y : L.t, find elt y m = find elt y m'.
Definition Equiv (elt : Set) (eq_elt : elt -> elt -> Prop) m m' :=
(forall k, In elt k m <-> In elt k m') /\ (forall k e e', MapsTo elt k e m -> MapsTo elt k e' m' -> eq_elt e e').
Definition Equivb (elt : Set) (cmp : elt -> elt -> bool) := Equiv elt (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'. *)
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'. *)
End ListLMap.
......@@ -22,16 +22,16 @@ 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.
(* 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 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.
(* Parameter equal : (elt -> elt -> bool) -> t elt -> t elt -> bool. *)
Section spec.
......@@ -43,7 +43,7 @@ Module Type LocationMap (L : Locations).
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 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.
......@@ -65,15 +65,15 @@ Module Type LocationMap (L : Locations).
Parameter find_1 : MapsTo x e m -> find x m = Some e.
Parameter find_2 : find x m = Some e -> MapsTo x e m.
Parameter elements_1 : MapsTo x e m -> InA eq_key_elt (x, e) (elements m).
Parameter elements_2 : InA eq_key_elt (x, e) (elements m) -> MapsTo x e m.
Parameter elements_1 : MapsTo x e m -> List.In (x, e) (elements m).
Parameter elements_2 : List.In (x, e) (elements m) -> MapsTo x e m.
Parameter elements_3w : NoDupA eq_key (elements m).
(* Parameter elements_3 : sort lt_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.
(* 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' :=
......@@ -82,25 +82,25 @@ Module Type LocationMap (L : Locations).
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'.
(* 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 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 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'.
(* 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 map_2 mapi_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 fold_1 map_1 mapi_1 mapi_2 : lmap.
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.
Module LocationMapFacts (L : Locations) (LM : LocationMap L).
......@@ -142,14 +142,14 @@ 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.
(* 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. *)
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,27 +163,27 @@ 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 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.
......
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