Library MapLib
The map library implemented with ordered list : list (A * B)
The module defintion for the domain of the list map
Module Type MAP_DOMAIN.
Parameter A : Set.
Axiom beq : A -> A -> bool.
Axiom blt : A -> A -> bool.
Axiom beq_true_eq : forall a a´ : A,
beq a a´ = true -> a = a´.
Axiom beq_false_neq : forall a a´ : A,
beq a a´ = false -> a <> a´.
Axiom eq_beq_true : forall a a´ : A,
a = a´ -> beq a a´ = true.
Axiom neq_beq_false : forall a a´ : A,
a <> a´ -> beq a a´ = false.
Axiom blt_trans : forall a a´ a´´ : A,
blt a a´ = true -> blt a´ a´´ = true -> blt a a´´ = true.
Axiom blt_irrefl : forall a : A,
blt a a = false.
Axiom blt_asym : forall a b : A,
blt a b = true -> blt b a = false.
Axiom blt_beq_dec : forall a b : A,
{blt a b = true} + {beq a b = true} + {blt b a = true}.
End MAP_DOMAIN.
The module defintion for the range of the list map
Module MapFun (Domain : MAP_DOMAIN) (Range : MAP_RANGE).
Import Domain.
Import Range.
Lemma beq_dec : forall a a´ : A, {beq a a´ = true} + {beq a a´ = false}.
Lemma eq_dec : forall a a´ : A, {a = a´} + {a <> a´}.
Ltac beq_case_tac x y :=
let Hb := fresh "Hb" in
(destruct (beq_dec x y) as [Hb | Hb]; trivial).
Lemma beq_sym : forall a a´ b,
beq a a´ = b -> beq a´ a = b.
Lemma beq_refl : forall a, beq a a = true.
Lemma beq_trans : forall a a´ a´´ b, beq a a´ = true
-> beq a´ a´´ = b
-> beq a a´´ = b.
Ltac beq_simpl_tac :=
match goal with
| [H : beq ?x ?y = ?f
|- context [(beq ?x ?y)]] =>
rewrite H; beq_simpl_tac
| [H : beq ?x ?y = ?f,
H0 : context [(beq ?x ?y)] |- _ ] =>
rewrite H in H0; beq_simpl_tac
| [ |- context [(beq ?x ?x)] ] =>
rewrite (@beq_refl x); beq_simpl_tac
| [H : context [(beq ?x ?x)] |- _ ] =>
rewrite (@beq_refl x) in H; beq_simpl_tac
| [ H : beq ?x ?y = ?b
|- context [(beq ?y ?x)] ] =>
rewrite (@beq_sym x y b H); beq_simpl_tac
| [H : beq ?x ?y = ?b,
H0 : context [(beq ?y ?x)] |- _ ] =>
rewrite (@beq_sym x y b H) in H0; beq_simpl_tac
| [ H : ?x <> ?y |- context [(beq ?x ?y)] ] =>
rewrite (neq_beq_false H); beq_simpl_tac
| [ H : ?x <> ?y,
H0 : context [(beq ?x ?y)] |- _ ] =>
rewrite (neq_beq_false H) in H0; beq_simpl_tac
| [ H : ?x <> ?y |- context [(beq ?y ?x)] ] =>
rewrite (beq_sym (neq_beq_false H)); beq_simpl_tac
| [ H : ?x <> ?y,
H0 : context [(beq ?y ?x)] |- _ ] =>
rewrite (beq_sym (neq_beq_false H)) in H0; beq_simpl_tac
| [ H : (beq ?x ?y = false) |- ?x <> ?y ] =>
apply (beq_false_neq H); beq_simpl_tac
| [ H : (beq ?x ?y = false) |- ?y <> ?x ] =>
apply (beq_false_neq (beq_sym H)); beq_simpl_tac
| [H : ?x = ?x |- _ ] => clear H; beq_simpl_tac
| [H : true = false |- _ ] => discriminate H
| [H : false = true |- _ ] => discriminate H
| [|- true = true ] => trivial
| [|- false = false ] => trivial
| [|- context [beq ?x ?y] ] => simpl; trivial
| [ H: context [beq ?x ?y] |- _ ] => simpl in H
| _ => idtac
end.
Tactic Notation "beq" "simpl" := beq_simpl_tac.
Ltac beq_rewrite_tac H :=
match type of H with
| beq ?a ?b = true =>
match goal with
| [ |- context [(?a)]] =>
rewrite (@beq_true_eq a b H)
| [ |- context [(?b)]] =>
rewrite <- (@beq_true_eq a b H)
end
| _ => fail
end.
Tactic Notation "beq" "rewrite" constr(t) := beq_rewrite_tac t.
Ltac beq_rewriteH_tac H H´ :=
match type of H with
| beq ?a ?b = true =>
match type of H´ with
| context [(?a)] =>
rewrite (@beq_true_eq a b H) in H´
| context [(?b)] =>
rewrite <- (@beq_true_eq a b H) in H´
end
| _ => fail
end.
Tactic Notation "beq" "rewrite" constr(t) "in" hyp(H) := beq_rewriteH_tac t H.
Section Test.
Variables a b a´ : A.
Goal beq a b = true -> beq a a´ = true -> False.
End Test.
Lemma blt_dec : forall a b,
{blt a b = true} + {blt a b = false}.
Lemma blt_t_beq_f :
forall m n, blt m n = true
-> beq m n = false.
Lemma bgt_t_beq_f :
forall m n, blt n m = true
-> beq m n = false.
Lemma beq_t_blt_f :
forall m n, beq m n = true
-> blt m n = false.
Lemma beq_t_bgt_f :
forall m n, beq m n = true
-> blt n m = false.
Lemma blt_beq_blt : forall a a´,
blt a a´ = false -> beq a a´ = false -> blt a´ a = true.
Ltac blt_simpl_tac :=
match goal with
| [H : blt ?x ?y = ?f
|- context [(blt ?x ?y)]] =>
rewrite H; blt_simpl_tac
| [H : blt ?x ?y = ?f,
H0 : context [(blt ?x ?y)]
|- _ ] =>
rewrite H in H0; blt_simpl_tac
| [H : blt ?x ?y = true
|- context[(beq ?x ?y)]] =>
rewrite (blt_t_beq_f H); blt_simpl_tac
| [H : blt ?x ?y = true,
H0 : context[(beq ?x ?y)] |- _ ] =>
rewrite (blt_t_beq_f H) in H0; blt_simpl_tac
| [H : blt ?y ?x = true
|- context[(beq ?x ?y)]] =>
rewrite (bgt_t_beq_f H); blt_simpl_tac
| [H : blt ?y ?x = true,
H0 : context[(beq ?x ?y)] |- _ ] =>
rewrite (bgt_t_beq_f H) in H0; blt_simpl_tac
| [H : beq ?y ?x = true
|- context[(blt ?x ?y)]] =>
rewrite (beq_t_blt_f H); blt_simpl_tac
| [H : beq ?y ?x = true,
H0 : context[(blt ?x ?y)] |- _ ] =>
rewrite (beq_t_blt_f H) in H0; blt_simpl_tac
| [H : beq ?y ?x = true
|- context[(blt ?y ?x)]] =>
rewrite (beq_t_bgt_f H); blt_simpl_tac
| [H : beq ?y ?x = true,
H0 : context[(blt ?y ?x)] |- _ ] =>
rewrite (beq_t_bgt_f H) in H0; blt_simpl_tac
| [ |- context [blt ?x ?x]] =>
rewrite (@blt_irrefl x); blt_simpl_tac
| [H : context [blt ?x ?x] |- _ ] =>
rewrite (@blt_irrefl x) in H; blt_simpl_tac
| [H : blt ?x ?y = true
|- context [blt ?y ?x]] =>
rewrite (blt_asym x y H); blt_simpl_tac
| [H : blt ?x ?y = true,
H0 : context [blt ?y ?x] |- _ ] =>
rewrite (blt_asym x y H) in H0; blt_simpl_tac
| [H : blt ?x ?y = false,
H1 : beq ?x ?y = false
|- context [blt ?y ?x]] =>
apply (blt_beq_blt H H1); blt_simpl_tac
| [H : blt ?x ?y = false,
H1 : beq ?y ?x = false
|- context [blt ?y ?x]] =>
apply (blt_beq_blt H (beq_sym H1)); blt_simpl_tac
| [H : ?x = ?x |- _ ] => clear H; blt_simpl_tac
| [H : true = false |- _ ] => discriminate H
| [H : false = true |- _ ] => discriminate H
| _ => idtac
end.
Ltac blt_dec_tac x y :=
let Hb := fresh "Hb" in
(destruct (blt_dec x y) as [Hb | Hb]; blt_simpl_tac).
Definition of map
Definition rlist := list (prod A B).
Fixpoint lb (a : A) (rl : rlist) {struct rl} : Prop :=
match rl with
| nil => True
| (a´, b´) :: rl´ => (blt a a´ = true) /\ (lb a rl´)
end.
Lemma lb_trans :
forall rl a1 a2, lb a2 rl -> blt a1 a2 = true -> lb a1 rl.
Fixpoint is_orderset (rl : rlist) : Prop :=
match rl with
| nil => True
| (a´, b´) :: rl´ => (lb a´ rl´) /\ (is_orderset rl´)
end.
map
Inductive listset :=
| listset_con : forall lst : rlist,
is_orderset lst -> listset.
Definition map := listset.
Definition lst (m : listset) := let (lst, _) := m in lst.
Definition prf (m : listset) :=
let (lst, prf) as m return (is_orderset (lst m))
:= m in prf.
Fixpoint get´ (rl : rlist) (a : A) {struct rl} : option B :=
match rl with
| nil => None
| (a´, b´) :: rl´ =>
match (beq a a´) with
| true => Some b´
| false => get´ rl´ a
end
end.
Lemma lb_notin :
forall rl a, lb a rl -> get´ rl a = None.
Lemma in_notlb :
forall rl a b, get´ rl a = Some b -> ~ lb a rl.
Definition get (m : map) (a : A) := get´ (lst m) a.
Lemma get_dec :
forall (m : map) (a : A),
{exists b, get m a = Some b} + {get m a = None}.
Definition emp´ : rlist := nil.
Lemma is_orderset_emp´ : is_orderset emp´.
Definition emp : map := listset_con is_orderset_emp´.
Lemma emp_sem :
forall a : A, get emp a = None.
Definition sig´ (a : A) (b : B) := (a, b) :: nil.
Lemma is_orderset_sig´ : forall a b, is_orderset (sig´ a b).
Definition sig (a : A) (b : B) :=
@listset_con (sig´ a b) (is_orderset_sig´ a b).
Lemma sig_sem : forall (a a´ : A) (b : B),
get (sig a b) a´ =
match (beq a a´) with
| true => Some b
| false => None
end.
Require Import Coq.Logic.Classical_Prop.
Fixpoint set´ (a : A) (b : B) (rl : rlist)
{struct rl}: rlist :=
match rl with
| nil => (a, b) :: nil
| (a´, b´) :: rl´ =>
match blt a a´ with
| true => (a, b) :: rl
| false =>
match beq a a´ with
| true => (a´, b) :: rl´
| false => (a´, b´) :: (set´ a b rl´)
end
end
end.
Lemma get´_set´ : forall rl a b,
get´ (set´ a b rl) a = Some b.
Lemma get´_set´_neq : forall rl a a0 b,
a <> a0 -> get´ (set´ a b rl) a0 = get´ rl a0.
Lemma lb_set´_lt : forall rl a a0 b,
lb a rl -> blt a0 a = true -> lb a0 (set´ a b rl).
Lemma lb_set´_gt : forall rl a a0 b,
lb a0 rl -> blt a0 a = true -> lb a0 (set´ a b rl).
Lemma is_orderset_set´ : forall rl : rlist,
is_orderset rl -> forall a b, is_orderset (set´ a b rl).
Definition set (m : map) (a : A) (b : B) : map :=
@listset_con (set´ a b (lst m))
(@is_orderset_set´ (lst m) (prf m) a b).
Lemma set_sem_old : forall m a a´ b,
match (beq a a´) with
| true => get (set m a b) a = Some b
| false => get (set m a b) a´ = get m a´
end.
Lemma set_sem : forall m a a´ b,
get (set m a b) a´ =
match (beq a a´) with
| true => Some b
| false => get m a´
end.
extensionality
Lemma equal_ext: forall m1 m2, (lst m1) = (lst m2) -> m1 = m2.
Lemma extensionality: forall (m1 m2 : map),
(forall a, get m1 a = get m2 a) -> m1 = m2.
Lemma get_set_same : forall m a b, get m a = Some b -> set m a b = m.
Lemmas Tactics
indom lookup
Definition indom (m : map) (a : A) :=
exists b : B, get m a = Some b.
Definition lookup (m : map) (a : A) (b : B) :=
get m a = Some b.
sub meq compat
Definition sub (m1 m2 : map) :=
forall (a : A) (b : B),
lookup m1 a b -> lookup m2 a b.
Definition meq (m1 m2 : map) :=
sub m1 m2 /\ sub m2 m1.
Definition compat (m1 m2 : map) : Prop :=
forall a : A,
match get m1 a, get m2 a with
| Some b1, Some b2 => b1 = b2
| _, _ => True
end.
disj
Definition disj (m1 m2 : map) : Prop :=
forall a : A,
match get m1 a, get m2 a with
| Some b, None => True
| None, Some b => True
| None, None => True
| _ , _ => False
end.
merge
Fixpoint app´ (rl1 rl2 : rlist) {struct rl1} : rlist :=
match rl1 with
| nil => rl2
| (a,b) :: rl1´ =>
(set´ a b (app´ rl1´ rl2))
end.
Lemma is_set_app´ : forall (rl1 rl2 : rlist),
is_orderset rl1 -> is_orderset rl2 -> is_orderset (app´ rl1 rl2).
Definition merge (m1 : map) (m2 : map) : map :=
@listset_con (app´ (lst m1) (lst m2))
(@is_set_app´ _ _ (prf m1) (prf m2)).
Lemma merge_sem : forall (m1 m2 : map) (a : A),
get (merge m1 m2) a
= match (get m1 a, get m2 a) with
| (Some b1, Some b2) => Some b1
| (Some b1, None) => Some b1
| (None, Some b2) => Some b2
| (None, None) => None
end.
Fixpoint minus´ (rl1 rl2 : rlist) {struct rl1} : rlist :=
match rl1 with
| nil => nil
| (a,b) :: rl1´ =>
match (get´ rl2 a) with
| Some b´ => (minus´ rl1´ rl2)
| None => set´ a b (minus´ rl1´ rl2)
end
end.
Lemma is_orderset_minus´ : forall (rl1 rl2 : rlist),
is_orderset rl1 -> is_orderset (minus´ rl1 rl2).
Definition minus (m : map) (m1 : map) : map :=
@listset_con (minus´ (lst m) (lst m1))
(@is_orderset_minus´ _ _ (prf m)).
Lemma lb_minus´ : forall (rl1 rl2 : rlist) (a : A),
lb a rl1 -> lb a (minus´ rl1 rl2).
Lemma minus_sem : forall (m m1 : map) (a : A),
get (minus m m1) a
= match (get m a, get m1 a) with
| (Some b, Some b1) => None
| (Some b1, None) => Some b1
| (None, Some b2) => None
| (None, None) => None
end.
join
Definition join (m1 m2 m: map) :=
forall a : A,
match get m1 a, get m2 a, get m a with
| None, Some b1, Some b2 => b1 = b2
| Some b1, None, Some b2 => b1 = b2
| None, None, None => True
| _, _, _ => False
end.
Definition join3 (m1 m2 m3 m: map) :=
forall a : A,
match get m1 a, get m2 a, get m3 a, get m a with
| Some b1, None, None, Some b2 => b1 = b2
| None, Some b1, None, Some b2 => b1 = b2
| None, None, Some b1, Some b2 => b1 = b2
| None, None, None, None => True
| _, _, _, _ => False
end.
Lemmas Tactics
get set
Ltac destruct_get :=
match goal with
| H: context [ get ?m ?a ] |- _ =>
destruct (get m a);
destruct_get
| |- context [ get ?m ?a ] =>
destruct (get m a);
destruct_get
| _ => idtac
end.
Ltac rewrite_get :=
match goal with
| H: context [ get (merge ?m1 ?m2) ?a ] |- _ =>
rewrite (merge_sem m1 m2 a) in H;
rewrite_get
| H: context [ get (set ?m ?a ?b) ?a´ ] |- _ =>
rewrite (set_sem m a a´ b) in H;
beq simpl;
rewrite_get
| H: context [ get (sig ?a ?b) ?a´ ] |- _ =>
rewrite (sig_sem a a´ b) in H;
beq simpl;
rewrite_get
| H: context [ get emp ?a ] |- _ =>
rewrite (emp_sem a) in H;
rewrite_get
| |- context [ get (merge ?m1 ?m2) ?a ] =>
rewrite (merge_sem m1 m2 a);
rewrite_get
| |- context [ get (set ?m ?a ?b) ?a´ ] =>
rewrite (set_sem m a a´ b);
beq simpl;
rewrite_get
| |- context [ get (sig ?a ?b) ?a´ ] =>
rewrite (sig_sem a a´ b);
beq simpl;
rewrite_get
| |- context [ get emp ?a ] =>
rewrite (emp_sem a);
rewrite_get
| _ => idtac
end.
Ltac solve_sn :=
match goal with
| H: context [ Some ?x = Some ?y ] |-
context [ ?x = ?y ] =>
injection H;
solve_sn
| H: context [ Some ?y = Some ?x ] |-
context [ ?x = ?y ] =>
injection H;
solve_sn
| H: context [ Some ?x = None ] |- _=>
apply False_ind;
discriminate;
solve_sn
| H: context [ None = Some ?x ] |- _ =>
apply False_ind;
discriminate;
solve_sn
| H: context [ ?x = ?y ] |-
context [ Some ?x = Some ?z ] =>
subst;
solve_sn
| H: context [ ?y = ?x ] |-
context [ Some ?x = Some ?z ] =>
subst;
solve_sn
| H: context [ _ -> Some ?x = Some ?y] |-
context [ Some ?x = Some ?y ] =>
apply H;
solve_sn
| H: context [ _ -> Some ?x = None ] |-
context [ Some ?x = None ] =>
apply H;
solve_sn
| H: context [ _ -> None = Some ?x] |-
context [ None = Some ?x] =>
apply H;
solve_sn
| |- context [_ -> _] =>
intros;
solve_sn
| _ => try tauto || auto
end.
Lemma get_sig : forall (a a´ : A) (b : B),
get (sig a b) a´ = match (eq_dec a a´) with
| left _ => Some b
| right _ => None
end.
Lemma get_sig_some : forall (a : A) (b : B),
get (sig a b) a = Some b.
Lemma get_sig_none : forall (a a´ : A) (b : B),
a <> a´
-> get (sig a b) a´ = None.
Lemma get_a_sig_a : forall (a a´ : A) (b : B),
beq a a´ = true -> get (sig a b) a´ = Some b.
Lemma get_a_sig_a´ : forall (a a´ : A) (b : B),
beq a a´ = false -> get (sig a b) a´ = None.
Lemma get_sig_some_eq : forall (a a´ : A) (b : B),
get (sig a b) a´ = Some b -> a = a´.
Lemma get_sig_some_eq´ : forall (a a´ : A) (b b´ : B),
get (sig a b) a´ = Some b´ -> a = a´ /\ b = b´.
Lemma set_a_get_a : forall (m : map) (a a´ : A) (b : B),
beq a a´ = true -> get (set m a b) a´ = Some b.
Lemma set_a_get_a´ : forall (m : map) (a a´ : A) (b : B),
beq a a´ = false -> get (set m a b) a´ = get m a´.
Lemma set_sig : forall a b b´,
set (sig a b) a b´ = sig a b´.
Lemma set_emp_sig : forall a b,
set emp a b = sig a b.
lookup
Lemma lookup_emp : forall (a : A) (b : B),
lookup emp a b -> False.
Lemma lookup_get : forall (m : map) (a : A) (b : B),
lookup m a b
-> get m a = Some b.
Lemma get_lookup : forall (m : map) (a : A) (b : B),
get m a = Some b
-> lookup m a b.
Lemma lookup_unique : forall (m : map) (a : A) (b b´ :B),
lookup m a b -> lookup m a b´ -> b = b´.
indom <--> lookup
Lemma lookup_indom : forall (m : map) (a : A) (b : B),
lookup m a b -> indom m a.
Lemma indom_lookup : forall (m : map) (a : A),
indom m a
-> exists b : B,
lookup m a b.
indom <---> get
Lemma indom_get : forall (m : map) (a : A),
indom m a
-> exists b : B,
get m a = Some b.
Lemma get_indom : forall (m : map) (a : A),
(exists b : B, get m a = Some b)
-> indom m a.
Lemma nindom_get :
forall (m : map) (a : A),
~ indom m a -> get m a = None.
sub meq compat
Lemma sub_refl : forall (m : map),
sub m m.
Implicit Arguments sub_refl[].
Lemma sub_asym : forall (m1 m2 : map),
sub m1 m2
-> sub m2 m1
-> meq m1 m2.
Lemma sub_trans : forall (m1 m2 m3 : map),
sub m1 m2
-> sub m2 m3
-> sub m1 m3.
Implicit Arguments sub_trans[m1 m2 m3].
Lemma sub_sig : forall m a b,
get m a = Some b
-> sub (sig a b) m.
Lemma meq_refl : forall (m : map),
meq m m.
Lemma meq_sym : forall (m1 m2 : map),
meq m1 m2 -> meq m2 m1.
Lemma meq_trans : forall (m1 m2 m3 : map),
meq m1 m2
-> meq m2 m3
-> meq m1 m3.
Lemma meq_sem : forall (m1 m2 : map),
meq m1 m2 ->
forall (a : A),
match get m1 a, get m2 a with
| Some b1, Some b2 => b1 = b2
| None, None => True
| _, _ => False
end.
Lemma meq_eq : forall m1 m2 : map,
meq m1 m2 -> m1 = m2.
Lemma compat_refl : forall m : map,
compat m m.
Lemma compat_sym : forall (m1 m2 : map),
compat m1 m2 -> compat m2 m1.
get <--> sub lookup <--> sub
Lemma get_sub_get : forall (m1 m2 : map) (a : A) (b : B),
get m1 a = Some b -> sub m1 m2 -> get m2 a = Some b.
Lemma lookup_sub_lookup : forall (m1 m2 : map) (a : A) (b : B),
lookup m1 a b -> sub m1 m2 -> lookup m2 a b.
Lemma indom_sub_indom : forall m1 m2 a,
indom m1 a -> sub m1 m2 -> indom m2 a.
lookup <--> meq
Lemma lookup_meq_lookup : forall (m1 m2 : map) (a : A) (b : B),
lookup m1 a b -> meq m1 m2 -> lookup m2 a b.
Lemma indom_meq_indom : forall m1 m2 a,
indom m1 a -> meq m1 m2 -> indom m2 a.
disj
Lemma disj_emp_l : forall (m : map),
disj (emp) m.
Lemma disj_emp_r : forall (m : map),
disj m (emp).
Lemma disj_sym : forall (m1 m2 : map),
disj m1 m2
-> disj m2 m1.
Lemma disj_sig : forall (a a´ : A) (b b´ : B),
beq a a´ = false
-> disj (sig a b) (sig a´ b´).
indom <---> disj
Lemma disj_indom :
forall (m1 m2 : map),
disj m1 m2
-> (forall a : A,
(indom m1 a -> ~ indom m2 a)
/\ (indom m2 a -> ~ indom m1 a)).
Lemma indom_disj : forall (m1 m2 : map),
(forall a : A,
(indom m1 a -> ~ indom m2 a)
/\ (indom m2 a -> ~ indom m1 a))
-> disj m1 m2.
disj <--> meq
Lemma disj_meq_disj_r : forall (m1 m2 m3 : map),
disj m1 m2
-> meq m2 m3
-> disj m1 m3.
Lemma disj_meq_disj_l : forall (m1 m2 m3 : map),
disj m1 m2
-> meq m1 m3
-> disj m3 m2.
disj --> compat
sub <--> compat
Lemma compat_sub_l : forall (m1 m2 : map),
compat m1 m2 -> sub m1 (merge m1 m2).
Lemma compat_sub_r : forall (m1 m2 : map),
compat m1 m2 -> sub m2 (merge m1 m2).
Lemma sub_compat :
forall (m1 m2 : map),
sub m1 m2 -> compat m1 m2.
Lemma sub_merge_l :
forall (m1 m2 : map),
compat m1 m2
-> sub m1 (merge m1 m2).
Lemma sub_merge_r :
forall (m1 m2 : map),
compat m1 m2
-> sub m2 (merge m1 m2).
Lemma sub_merge_elim_l :
forall (m1 m2 m3: map),
compat m1 m2
-> sub (merge m1 m2) m3
-> sub m1 m3.
Implicit Arguments sub_merge_elim_l [m1 m2 m3].
Lemma sub_merge_elim_r :
forall (m1 m2 m3: map),
compat m1 m2
-> sub (merge m1 m2) m3
-> sub m2 m3.
Implicit Arguments sub_merge_elim_r [m1 m2 m3].
Lemma sub_merge_intro_l :
forall (m1 m2 m3: map),
compat m1 m2
-> sub m3 m1
-> sub m3 (merge m1 m2).
Implicit Arguments sub_merge_intro_l [m1 m2 m3].
Lemma sub_merge_intro_r :
forall (m1 m2 m3: map),
compat m1 m2
-> sub m3 m2
-> sub m3 (merge m1 m2).
Implicit Arguments sub_merge_intro_r [m1 m2 m3].
Lemma merge_sub_intro : forall (m m1 m2 : map),
sub m1 m
-> sub m2 m
-> sub (merge m1 m2) m.
Implicit Arguments merge_sub_intro [m m1 m2].
Lemma meq_merge_sym : forall (m1 m2 : map),
compat m1 m2
-> meq (merge m1 m2) (merge m2 m1).
Lemma meq_merge_assoc_l : forall (m1 m2 m3 : map),
meq
(merge (merge m1 m2) m3)
(merge m1 (merge m2 m3)).
Lemma meq_merge_assoc_r : forall (m1 m2 m3 : map),
meq
(merge m1 (merge m2 m3))
(merge (merge m1 m2) m3).
Lemma meq_merge_emp_l : forall (m : map),
meq (merge emp m) m.
Lemma meq_merge_emp_r : forall (m : map),
meq (merge m emp) m.
Lemma meq_merge_meq :
forall m1 m2 m3 m4,
meq m1 m3 -> meq m2 m4
-> meq (merge m1 m2) (merge m3 m4).
lookup <--> merge
Lemma lookup_merge_elim :
forall (m1 m2 : map) (a : A) (b : B),
lookup (merge m1 m2) a b
-> lookup m1 a b \/ lookup m2 a b.
Lemma lookup_merge_intro :
forall (m1 m2 : map) (a : A) (b : B),
lookup m1 a b \/ lookup m2 a b
-> compat m1 m2
-> lookup (merge m1 m2) a b.
indom <--> merge
Lemma indom_merge_intro :
forall (m1 m2 : map) (a : A),
indom m1 a \/ indom m2 a
-> indom (merge m1 m2) a.
Lemma indom_merge_elim :
forall (m1 m2 : map) (a : A),
indom (merge m1 m2) a
-> indom m1 a \/ indom m2 a.
disj <--> disj merge
Lemma disj_merge_intro_l :
forall (m1 m2 m3 : map),
disj m1 m3 /\ disj m2 m3
-> disj (merge m1 m2) m3.
Lemma disj_merge_elim_l :
forall (m1 m2 m3 : map),
disj (merge m1 m2) m3
-> disj m1 m3 /\ disj m2 m3.
Lemma disj_merge_intro_r :
forall (m1 m2 m3 : map),
disj m1 m2 /\ disj m1 m3
-> disj m1 (merge m2 m3).
Lemma disj_merge_elim_r :
forall (m1 m2 m3 : map),
disj m1 (merge m2 m3)
-> disj m1 m2 /\ disj m1 m3.
Lemma disj_merge_intro_lr :
forall (m1 m2 m1´ m2´ : map),
disj m1 m1´
-> disj m1 m2´
-> disj m2 m1´
-> disj m2 m2´
-> disj (merge m1 m2) (merge m1´ m2´).
Lemma disj_merge_elim_lr :
forall (m1 m2 m1´ m2´ : map),
disj (merge m1´ m2´) (merge m1 m2)
-> (disj m1 m1´ /\ disj m1 m2´)
/\ (disj m2 m1´ /\ disj m2 m2´).
Lemma join_comm :
forall ma mb mab : map,
join ma mb mab -> join mb ma mab.
Lemma join_assoc_l :
forall ma mb mc mab mabc,
join ma mb mab->
join mab mc mabc ->
exists mbc, join mb mc mbc /\
join ma mbc mabc.
Lemma join_assoc_r :
forall ma mb mc mbc mabc,
join mb mc mbc->
join ma mbc mabc ->
exists mab, join ma mb mab /\
join mab mc mabc.
Lemma join_disj_meq :
forall (m1 m2 m : map),
join m1 m2 m
-> disj m1 m2 /\ meq (merge m1 m2) m.
Lemma disj_meq_join :
forall (m1 m2 m: map),
disj m1 m2 /\ meq (merge m1 m2) m
-> join m1 m2 m.
Lemma join_sub_l :
forall m1 m2 m,
join m1 m2 m
-> sub m1 m.
Lemma join_sub_r :
forall m1 m2 m,
join m1 m2 m
-> sub m2 m.
Implicit Arguments join_sub_r [m1 m2 m].
Lemma join_unique :
forall m1 m2 m m´,
join m1 m2 m ->
join m1 m2 m´ ->
m = m´.
Lemma join_lookup_lookup_l :
forall m1 m2 m a b,
join m1 m2 m
-> lookup m1 a b
-> lookup m a b.
Lemma join_lookup_lookup_r :
forall m1 m2 m a b,
join m1 m2 m
-> lookup m2 a b
-> lookup m a b.
Lemma join_get_get_l :
forall m1 m2 m a b,
join m1 m2 m
-> get m1 a = Some b
-> get m a = Some b.
Lemma join_get_get_r :
forall m1 m2 m a b,
join m1 m2 m
-> get m2 a = Some b
-> get m a = Some b.
Lemma join_merge_disj :
forall m1 m2,
disj m1 m2 ->
join m1 m2 (merge m1 m2).
Lemma join_lookup_or :
forall m1 m2 m a b,
join m1 m2 m ->
lookup m a b ->
(lookup m1 a b) \/ (lookup m2 a b).
Lemma join_get_or :
forall m1 m2 m a b,
join m1 m2 m ->
get m a = Some b ->
(get m1 a = Some b) \/ (get m2 a = Some b).
Lemma join_set_l :
forall m1 m2 m a b,
join m1 m2 m
-> indom m1 a
-> join (set m1 a b) m2 (set m a b).
Lemma join_set_r :
forall m1 m2 m a b,
join m1 m2 m
-> indom m2 a
-> join m1 (set m2 a b) (set m a b).
Lemma join_set_l_rev :
forall m1 m2 m a b,
join (set m1 a b) m2 m
-> exists m´, join m1 m2 m´
/\ m = (set m´ a b).
Lemma join_set_nindom_l :
forall m1 m2 m m1´ m´ l v, join m1 m2 m ->
m1´ = set m1 l v ->
m´ = set m l v ->
~indom m l ->
join m1´ m2 m´.
Lemma join_set_nindom_r :
forall m1 m2 m m2´ m´ l v, join m1 m2 m ->
m2´ = set m2 l v ->
m´ = set m l v ->
~indom m l ->
join m1 m2´ m´.
Lemma join_emp :
forall m m´,
m = m´ ->
join emp m m´.
Lemma join_sig_set :
forall m a b,
~indom m a ->
join m (sig a b) (set m a b).
Lemma join_unique_r :
forall m1 m2 m2´ m,
join m1 m2 m ->
join m1 m2´ m ->
m2 = m2´.
Lemma join_meq :
forall m m´,
join emp m m´ -> meq m m´.
Lemma join_emp_eq :
forall m m´,
join emp m m´ -> m = m´.
Lemma sub_exists_join :
forall m1 m,
sub m1 m ->
exists m2, join m1 m2 m.
Lemma join_sub_minus : forall m m1,
sub m1 m
-> join m1 (minus m m1) m.
Lemma join_sub_sub : forall m1 m2 m m´,
join m1 m2 m
-> sub m1 m´
-> sub m2 m´
-> sub m m´.
Lemma join_join_join3 : forall m1 m2 m3 m12 m,
join m1 m2 m12
-> join m12 m3 m
-> join3 m1 m2 m3 m.
Lemma join3_join_join : forall m1 m2 m3 m23 m,
join3 m1 m2 m3 m
-> join m1 m23 m
-> join m2 m3 m23.
Lemma join3_comm_213 : forall m1 m2 m3 m,
join3 m1 m2 m3 m
-> join3 m2 m1 m3 m.
Lemma join3_comm_312 : forall m1 m2 m3 m,
join3 m1 m2 m3 m
-> join3 m3 m1 m2 m.
Lemma join3_comm_231 : forall m1 m2 m3 m,
join3 m1 m2 m3 m
-> join3 m2 m3 m1 m.
Lemma join3_comm_132 : forall m1 m2 m3 m,
join3 m1 m2 m3 m
-> join3 m1 m3 m2 m.
Lemma join3_2join : forall m1 m2 m3 m,
join3 m1 m2 m3 m
-> exists m12,
join m1 m2 m12
/\ join m12 m3 m.
Ltac unfoldlookup H :=
unfold lookup in H.
Lemma join_index_beq_false : forall m1 m2 m3 a b x y,
join m1 m2 m3 -> get m1 a = Some x -> get m2 b = Some y -> beq a b = false.
Lemma join_sig_get : forall a x m1 m2,
join (sig a x) m1 m2 -> get m2 a = Some x.
Definition joinsig x v m1 m2 := join (sig x v) m1 m2.
Lemma join_joinsig_get : forall v´24 v´25 v´16 x8 x13 x12 ,
join v´24 v´25 v´16 -> joinsig x8 x13 x12 v´25 ->
get v´16 x8 = Some x13.
Lemma joinsig_set :
forall x8 x13 x12 v´25 v,
joinsig x8 x13 x12 v´25 ->
joinsig x8 v x12 (set v´25 x8 v).
Lemma joinsig_set_set : forall x8 x13 x12 v´24 v´25 v´16 v,
joinsig x8 x13 x12 v´25 ->
join v´24 v´25 v´16 ->
join v´24 (set v´25 x8 v) (set v´16 x8 v).
Lemma disj_set_disj_1 : forall M1 M2 x v v´,
disj M1 M2 -> get M1 x = Some v -> disj (set M1 x v´) M2.
Lemma disj_set_disj_2 : forall M1 M2 x v v´,
disj M1 M2 -> get M2 x = Some v -> disj M1 (set M2 x v´).
Lemma index_beq_false_1 : forall M a b v,
get M a = Some v -> get M b = None -> beq a b = false.
Lemma merge_set_eq_1 : forall M1 M2 x v,
merge (set M1 x v) M2 = set (merge M1 M2) x v.
Lemma merge_set_eq_2 : forall M1 M2 x v v´,
disj M1 M2 -> get M2 x = Some v ->
merge M1 (set M2 x v´) = set (merge M1 M2) x v´.
Lemma join_shift_l : forall m1 m2 m3 mx a v,
join m1 m2 m3 -> joinsig a v mx m2 -> join (merge m1 (sig a v)) mx m3.
Lemma joinsig_merge_sig : forall a1 v1 m1 m2 a2 v2,
joinsig a1 v1 m1 m2 -> a1 <> a2 ->
joinsig a1 v1 (merge m1 (sig a2 v2)) (merge m2 (sig a2 v2)).
Definition eqdom M1 M2 := forall x, indom M1 x <-> indom M2 x.
Lemma eqdom_merge_set : forall O Of x v v´,
get O x = Some v -> eqdom (merge O Of) (merge (set O x v´) Of).
Lemma option2val:
forall T (x y: T),
Some x = Some y -> x = y.
Lemma option2false:
forall T (x : T),
None = Some x -> False.
Lemma disj_comm:
forall ma mb,
disj ma mb ->
disj mb ma.
Ltac find_join_eql :=
match goal with
| H: join ?ma _ _ |-
join ?ma ?mb ?mab =>
eapply H
| H: join _ ?ma _ |-
join ?ma ?mb ?mab =>
apply join_comm; eapply H
| H: join ?mb _ _ |-
join ?ma ?mb ?mab =>
apply join_comm; eapply H
| H: join _ ?mb _ |-
join ?ma ?mb ?mab =>
eapply H
| H: join _ _ ?mab |-
join ?ma ?mb ?mab =>
eapply H
end.
Lemma join_meq_sub_1st:
forall m1 m2 m3 m12,
join m1 m2 m12 ->
meq m1 m3 ->
join m3 m2 m12.
Lemma disj_trans_sub:
forall m1 m2 m3,
sub m1 m2 ->
disj m3 m2 ->
disj m3 m1.
Lemma join_assoc:
forall ma mb mc mab mbc mabc,
join ma mb mab ->
join mab mc mabc ->
join mb mc mbc ->
join ma mbc mabc.
Lemma join_assoc_spec_1:
forall ma mb mc mab mabc,
join ma mb mab ->
join mc mab mabc ->
exists mac, join mc ma mac /\
join mac mb mabc.
Lemma my_joinsig_join_set:
forall x1 v1 v2 ma mb mb´ mab,
joinsig x1 v1 mb´ mb ->
join ma mb mab ->
join ma (set mb x1 v2) (set mab x1 v2).
Lemma join_join_disj_r:
forall ma mb mab mc mabc,
join ma mb mab ->
join mab mc mabc ->
disj mb mc.
Lemma join_join_disj_l:
forall ma mb mab mc mabc,
join ma mb mab ->
join mab mc mabc ->
disj ma mc.
Lemma join_whole2part:
forall ma mb mab mc mabc,
join ma mb mab ->
join mab mc mabc ->
join mb mc (merge mb mc).
Lemma my_join_sig_abc:
forall ma mb mc mc´ x1 v1 v2 mbc mabc,
join mb mc mbc ->
join ma mbc mabc ->
joinsig x1 v1 mc´ mc ->
join ma (set mbc x1 v2)
(set mabc x1 v2).
Lemma my_joinsig_set:
forall x1 v1 v2 m´ m,
joinsig x1 v1 m´ m ->
joinsig x1 v2 m´ (set m x1 v2).
Lemma join_get_r:
forall ma mb mab x1 v1,
join ma mb mab ->
get mb x1 = Some v1 ->
get mab x1 = Some v1.
Lemma join_get_l:
forall ma mb mab x1 v1,
join ma mb mab ->
get ma x1 = Some v1 ->
get mab x1 = Some v1.
Lemma disj_get_neq:
forall ma mb x1 v1 x2 v2,
disj ma mb ->
get ma x1 = Some v1 ->
get mb x2 = Some v2 ->
x1 <> x2.
Lemma my_join_disj:
forall ma mb mab,
join ma mb mab ->
disj ma mb.
Lemma join_meq_eql:
forall ma mb mab,
join ma mb mab ->
mab = merge ma mb.
Ltac solve_get :=
match goal with
| H: get ?m ?x = _ |-
get ?m ?x = _ =>
eapply H
| H: join (sig ?x _) _ ?m |-
get ?m ?x = Some _ =>
eapply join_sig_get;
eapply H
| |- get (sig ?x _) ?x = Some _ =>
eapply get_sig_some
| H: join ?ma ?mb ?mab |-
get ?mab ?x = Some ?v =>
match goal with
| H´: get ?ma ?x = Some ?v |- _ =>
eapply join_get_l; [eapply H | eapply H´]
| H´: get ?mb ?x = Some ?v |- _ =>
eapply join_get_r; [eapply H | eapply H´]
end
end.
Ltac solve_sub :=
match goal with
| H: join ?ma ?mb ?mab |-
sub ?ma ?mab =>
eapply join_sub_l; eapply H
| H: join ?ma ?mb ?mab |-
sub ?mb ?mab =>
eapply join_sub_r; eapply H
end.
Ltac solve_disj :=
match goal with
| H: disj ?ma ?mb |-
disj ?ma ?mb =>
apply H
| H: disj ?ma ?mb |-
disj ?mb ?ma =>
apply disj_sym; apply H
| H: join ?ma ?mb ?mab |-
disj ?ma ?mb =>
eapply my_join_disj; eapply H
| H: join ?ma ?mb ?mab |-
disj ?mb ?ma =>
eapply disj_sym; eapply my_join_disj; eapply H
end.
Ltac solve_join :=
match goal with
| H: join _ _ ?mab |-
join _ _ ?mab =>
first [eapply H | apply join_comm; eapply H | idtac]
end.
Ltac solve_map :=
match goal with
| |- get _ _ = _ =>
try solve_get
| |- sub _ _ =>
try solve_sub
| |- disj _ _ =>
try solve_disj
| |- join _ _ _ =>
try solve_join
| _ => idtac
end.
Lemma join_get_get_neq:
forall ma mb mab x1 v1 x2 v2,
join ma mb mab ->
get ma x1 = Some v1 ->
get mb x2 = Some v2 ->
x1 <> x2.
End MapFun.
Unset Implicit Arguments.