https://gitlab.com/nomadic-labs/mi-cho-coq
Tip revision: 2b4e968b2ada06ba5f1d43705c1e38224c1f0b56 authored by Tom Jack on 20 June 2019, 16:39:23 UTC
Install Coq libraries
Install Coq libraries
Tip revision: 2b4e968
map.v
(* Open Source License *)
(* Copyright (c) 2019 Nomadic Labs. <contact@nomadic-labs.com> *)
(* Permission is hereby granted, free of charge, to any person obtaining a *)
(* copy of this software and associated documentation files (the "Software"), *)
(* to deal in the Software without restriction, including without limitation *)
(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *)
(* and/or sell copies of the Software, and to permit persons to whom the *)
(* Software is furnished to do so, subject to the following conditions: *)
(* The above copyright notice and this permission notice shall be included *)
(* in all copies or substantial portions of the Software. *)
(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR *)
(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *)
(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *)
(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER *)
(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *)
(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *)
(* DEALINGS IN THE SOFTWARE. *)
(* Finite maps implemented as finite sets of pairs. *)
Require set.
Require Import error.
Section map.
Variable A : Set.
Variable B : Set.
Variable compare : A -> A -> comparison.
Hypothesis compare_eq_iff : forall a b, compare a b = Eq <-> a = b.
Hypothesis lt_trans : Relations_1.Transitive (fun a b => compare a b = Lt).
Hypothesis gt_trans : Relations_1.Transitive (fun a b => compare a b = Gt).
Lemma compare_refl a : compare a a = Eq.
Proof.
apply (compare_eq_iff a a).
reflexivity.
Qed.
Lemma compare_diff : forall a b, compare a b = Lt \/ compare a b = Gt <-> a <> b.
Proof.
intros. split.
- (* -> *)
intros [Hdiff|Hdiff] contra;
rewrite <- compare_eq_iff in contra; rewrite Hdiff in contra; discriminate contra.
- (* <- *)
intro Hdiff. destruct (compare a b) eqn:Hab.
+ apply compare_eq_iff in Hab. contradiction.
+ left. reflexivity.
+ right. reflexivity.
Qed.
Definition map_compare (x_ y_ : A * B) :=
match x_, y_ with (x, _), (y, _) => compare x y end.
Definition map := set.set (A * B) map_compare.
Fixpoint list_mem (x : A) (l : list (A * B)) : bool :=
match l with
| nil => false
| cons y l =>
let (k, v) := y in
match compare x k with
| Lt => false
| Eq => true
| Gt => list_mem x l
end
end.
Definition mem (x : A) (m : map) : bool :=
let (l, _) := m in list_mem x l.
Fixpoint list_remove (x : A) (l : list (A * B)) : list (A * B) :=
match l with
| nil => nil
| cons y l =>
let (k, v) := y in
match compare x k with
| Lt => cons y l
| Eq => l
| Gt => cons y (list_remove x l)
end
end.
Lemma remove_in x v y l : List.In (x, v) (list_remove y l) -> List.In (x, v) l.
Proof.
induction l as [|(z, v') l]; simpl.
- auto.
- case_eq (compare y z).
+ intuition.
+ intros Hlt Hin.
simpl in Hin.
assumption.
+ intros Hgt Hin.
simpl in Hin.
intuition.
Qed.
Fixpoint list_replace (x : A) (v : B) (l : list (A * B)) : list (A * B) :=
match l with
| nil => cons (x, v) nil
| cons y l =>
let (k, _) := y in
match compare x k with
| Lt => cons (x, v) (cons y l)
| Eq => cons (x, v) l
| Gt => cons y (list_replace x v l)
end
end.
Lemma list_replace_same x v v' l :
Sorted.StronglySorted (set.lt _ map_compare) l ->
List.In (x, v) (list_replace x v' l) <-> v = v'.
Proof.
induction l as [|(y, v'') l].
- simpl.
intuition congruence.
- simpl.
case_eq (compare x y).
+ intros He Hs.
apply Sorted.StronglySorted_inv in Hs.
destruct Hs as (Hs, Hf).
rewrite compare_eq_iff in He.
simpl.
split.
* intros [He2|Hin].
{
congruence.
}
{
rewrite List.Forall_forall in Hf.
specialize (Hf (x, v) Hin).
unfold set.lt, map_compare in Hf.
symmetry in He.
rewrite <- compare_eq_iff in He.
congruence.
}
* intro; left; congruence.
+ intros Hlt Hs.
apply Sorted.StronglySorted_inv in Hs.
destruct Hs as (Hs, Hf).
simpl.
split.
* intros [He2|Hin].
{
congruence.
}
{
rewrite List.Forall_forall in Hf.
specialize (Hf (x, v)).
unfold set.lt, map_compare in Hf.
simpl in Hin.
destruct Hin as [He|Hin].
- injection He.
intros _ He2.
symmetry in He2.
rewrite <- compare_eq_iff in He2.
congruence.
- specialize (Hf Hin).
assert (compare x x = Lt) by (apply (lt_trans x y x); assumption).
assert (compare x x = Eq) by (apply (compare_eq_iff x x); reflexivity).
congruence.
}
* intro He.
destruct He.
left; reflexivity.
+ simpl.
intros Hgt Hs.
rewrite IHl.
* split; [|intuition].
intros [He|He]; [|auto].
injection He.
intros _ He2.
symmetry in He2.
rewrite <- compare_eq_iff in He2.
congruence.
* inversion Hs.
assumption.
Qed.
Lemma list_replace_diff x v y v' l :
Sorted.StronglySorted (set.lt _ map_compare) l ->
x <> y ->
List.In (x, v) (list_replace y v' l) <-> List.In (x, v) l.
Proof.
induction l as [|(z, v'') l]; simpl.
- intuition congruence.
- intros Hs Hd.
case_eq (compare y z).
+ intro He.
simpl.
rewrite compare_eq_iff in He.
destruct He.
intuition congruence.
+ intro Hlt.
simpl.
intuition congruence.
+ intro Hgt.
simpl.
rewrite IHl.
* intuition congruence.
* inversion Hs.
assumption.
* assumption.
Qed.
Lemma list_replace_in x v y v' l :
Sorted.StronglySorted (set.lt _ map_compare) l ->
List.In (x, v) (list_replace y v' l) <->
(match compare x y with Eq => v = v' | _ => List.In (x, v) l end).
Proof.
case_eq (compare x y).
- intro He.
apply compare_eq_iff in He.
destruct He.
apply list_replace_same.
- intros Hlt Hs.
apply list_replace_diff.
+ assumption.
+ intro He.
rewrite <- compare_eq_iff in He.
congruence.
- intros Hgt Hs.
apply list_replace_diff.
+ assumption.
+ intro He.
rewrite <- compare_eq_iff in He.
congruence.
Qed.
Definition list_update (x : A) (vo : option B) (l : list (A * B)) : list (A * B) :=
match vo with
| None => list_remove x l
| Some v => list_replace x v l
end.
Program Definition update (x : A) (vo : option B) (m : map) : map :=
let (l, _) := m in
exist _ (list_update x vo l) _.
Next Obligation.
destruct vo as [v|]; simpl.
- induction l as [|(k, v') l]; simpl.
+ constructor.
* assumption.
* constructor.
+ apply Sorted.StronglySorted_inv in H.
destruct H as (Hl, Hf).
specialize (IHl Hl).
case_eq (compare x k).
* intro He.
apply compare_eq_iff in He.
destruct He.
constructor.
{
assumption.
}
{
rewrite List.Forall_forall.
intros (z, v'') Hin.
rewrite List.Forall_forall in Hf.
specialize (Hf (z, v'') Hin).
generalize Hf.
unfold set.lt, map_compare.
auto.
}
* intro Hxk.
constructor.
{
constructor; assumption.
}
{
apply List.Forall_forall.
intros (z, v'') Hin.
rewrite List.Forall_forall in Hf.
specialize (Hf (z, v'')).
simpl in Hin.
destruct Hin as [He | Hin].
- injection He.
intros _ He2.
destruct He2.
exact Hxk.
- apply (lt_trans _ k).
+ assumption.
+ apply Hf.
assumption.
}
* intro Hgt.
constructor; try assumption.
apply List.Forall_forall.
intros (y, v'').
rewrite list_replace_in; try assumption.
case_eq (compare y x).
{
intro He.
rewrite compare_eq_iff in He.
destruct He.
intros _.
unfold set.lt, map_compare.
apply set.compare_gt_lt; assumption.
}
{
intro Hlt.
rewrite List.Forall_forall in Hf.
exact (Hf (y, v'')).
}
{
intros Hgt2 _.
unfold set.lt, map_compare.
apply set.compare_gt_lt; try assumption.
apply (gt_trans _ x); assumption.
}
- induction l as [|(k, v') l]; simpl.
+ assumption.
+ case_eq (compare x k).
* intros _.
inversion H.
assumption.
* intros _.
assumption.
* apply Sorted.StronglySorted_inv in H.
destruct H as (Hs, Hf).
intro Hgt.
constructor.
{
auto.
}
{
apply List.Forall_forall.
intros (y, v'').
intro Hy.
apply remove_in in Hy.
rewrite List.Forall_forall in Hf.
exact (Hf _ Hy).
}
Qed.
Program Definition empty : map :=
exist _ nil _.
Next Obligation.
constructor.
Defined.
Fixpoint list_get (x : A) (l : list (A * B)) : option B :=
match l with
| nil => None
| cons y l =>
let (k, v) := y in
match compare x k with
| Lt => None
| Eq => Some v
| Gt => list_get x l
end
end.
Definition get (x : A) (m : map) : option B :=
let (l, _) := m in list_get x l.
Lemma StronglySorted_inv_iff (A' : Type) (R : A' -> A' -> Prop) (a : A')
(l : list A') :
Sorted.StronglySorted R (a :: l) <->
Sorted.StronglySorted R l /\ List.Forall (R a) l.
Proof.
split.
- apply Sorted.StronglySorted_inv.
- generalize Sorted.SSorted_cons.
intuition.
Qed.
Lemma forall_cons (A' : Type) (P : A' -> Prop) (a : A') (l : list A') :
List.Forall P (cons a l) <-> (P a /\ List.Forall P l).
Proof.
split.
- intro H.
inversion H.
split; assumption.
- intros (HPa, Hf).
constructor; assumption.
Qed.
Lemma list_sorted_map_fst (l : list (A * B)) :
Sorted.StronglySorted (fun x y => map_compare x y = Lt) l <->
Sorted.StronglySorted (fun x y => compare x y = Lt) (List.map fst l).
Proof.
induction l as [|(x, v) l]; simpl.
- split; constructor.
- rewrite StronglySorted_inv_iff.
rewrite StronglySorted_inv_iff.
rewrite IHl.
clear IHl.
assert (List.Forall (fun y : A * B => map_compare (x, v) y = Lt) l <->
List.Forall (fun y : A => compare x y = Lt) (List.map fst l)) as H.
+ induction l as [|(y, v') l]; simpl.
* split; constructor.
* rewrite forall_cons.
rewrite forall_cons.
rewrite IHl.
intuition.
+ rewrite H.
intuition.
Qed.
Definition size (m : map) : nat :=
let (l, _) := m in List.length l.
Lemma list_get_lt a b l :
List.Forall (fun y => map_compare (a, b) y = Lt) l ->
Sorted.StronglySorted (fun x y => map_compare x y = Lt) l ->
list_get a l = None.
Proof.
intros Hf Hl.
destruct l as [|(a2, b2) l].
- reflexivity.
- simpl.
rewrite List.Forall_forall in Hf.
specialize (Hf (a2, b2) (or_introl eq_refl)).
simpl in Hf.
rewrite Hf.
reflexivity.
Qed.
Lemma extensionality (m1 m2 : map) :
(forall x, get x m1 = get x m2) -> m1 = m2.
Proof.
destruct m1 as (l1, H1).
destruct m2 as (l2, H2).
simpl.
intro Hf.
assert (l1 = l2).
- generalize l2 H2 Hf; clear l2 H2 Hf; induction l1 as [|(a1, b1) l1]; intros [|(a2, b2) l2] H2 Hf.
+ reflexivity.
+ exfalso.
specialize (Hf a2).
simpl in Hf.
rewrite compare_refl in Hf.
discriminate.
+ exfalso.
specialize (Hf a1).
simpl in Hf.
rewrite compare_refl in Hf.
discriminate.
+ assert (a1 = a2 /\ b1 = b2).
* generalize (Hf a1); intro Ha1.
simpl in Ha1.
rewrite compare_refl in Ha1.
generalize (Hf a2); intro Ha2.
simpl in Ha2.
rewrite compare_refl in Ha2.
case_eq (compare a1 a2).
-- intro He.
rewrite compare_eq_iff in He.
split; [assumption|].
subst a2.
rewrite compare_refl in Ha1.
injection Ha1.
auto.
-- intro Hlt.
rewrite Hlt in Ha1.
discriminate.
-- intro Hgt.
rewrite Hgt in Ha1.
rewrite <- set.compare_gt_lt in Hgt;
[|assumption|assumption|assumption].
rewrite Hgt in Ha2.
discriminate.
* destruct H; subst a2; subst b2.
f_equal.
apply IHl1.
-- inversion H1.
assumption.
-- inversion H2.
assumption.
-- intro a3.
specialize (Hf a3).
simpl in Hf.
case_eq (compare a3 a1).
** intro Heq.
rewrite compare_eq_iff in Heq.
subst a3.
rewrite (list_get_lt a1 b1 l1); [|inversion H1; assumption|inversion H1; assumption].
rewrite (list_get_lt a1 b1 l2); [|inversion H2; assumption|inversion H2; assumption].
reflexivity.
** intro Hlt.
rewrite (list_get_lt a3 b1 l1);
[rewrite (list_get_lt a3 b1 l2)| |].
--- reflexivity.
--- apply (@List.Forall_impl _ (fun y => map_compare (a1, b1) y = Lt)); [|inversion H2; assumption].
intros (a4, b4).
simpl.
apply lt_trans.
assumption.
--- inversion H2; assumption.
--- apply (@List.Forall_impl _ (fun y => map_compare (a1, b1) y = Lt)); [|inversion H1; assumption].
intros (a4, b4).
simpl.
apply lt_trans.
assumption.
--- inversion H1; assumption.
** intro Hgt.
rewrite Hgt in Hf.
exact Hf.
- destruct H.
f_equal.
apply set.sorted_irrel.
Qed.
(* Interesting lemmas to use when working with maps *)
Lemma map_getmem : forall k m v,
get k m = Some v -> mem k m.
Proof.
intros.
destruct m as [l]. simpl. simpl in H.
induction l.
- (* nil *)
simpl in H. inversion H.
- (* h::t *)
simpl. simpl in H.
destruct a as [k' v']. destruct (compare k k').
+ (* Eq *) exact ITT.
+ (* Lt *) inversion H.
+ (* Gt *) apply IHl. inversion s. assumption. assumption.
Qed.
Lemma map_memget : forall k m,
mem k m -> exists v, get k m = Some v.
Proof.
intros.
destruct m as [l]. simpl. simpl in H.
induction l.
- (* nil *)
exfalso. simpl in H. inversion H.
- (* h::t *)
inversion s; subst.
specialize (IHl H2).
simpl in H. simpl.
destruct a as [k' v']. destruct (compare k k').
+ (* Eq *) exists v'. reflexivity.
+ (* Lt *) inversion H.
+ (* Gt *)
specialize (IHl H). destruct IHl as [v'' IHl].
exists v''. assumption.
Qed.
Lemma map_updateeq: forall k m v,
get k (update k (Some v) m) = (Some v).
Proof.
intros.
destruct m as [l]. unfold get, update.
assert ((compare k k) = Eq) as Hkk by (apply compare_eq_iff; reflexivity).
induction l.
- (* nil *)
simpl. rewrite Hkk. reflexivity.
- (* h::t *)
simpl. inversion s; subst.
specialize (IHl H1). simpl in IHl.
destruct a as [k' v'].
destruct (compare k k') eqn:Hkk'; simpl.
+ (* Eq *) simpl. rewrite Hkk. reflexivity.
+ (* Lt *) simpl. rewrite Hkk. reflexivity.
+ (* Gt *) rewrite Hkk'. assumption.
Qed.
Lemma map_updateneq: forall k k' m v,
k <> k' ->
get k' (update k (Some v) m) =
get k' m.
Proof.
intros.
destruct m as [l]. unfold get, update; simpl.
induction l; simpl.
- (* nil *)
destruct (compare k' k) eqn:Hcp; try reflexivity.
apply compare_eq_iff in Hcp. symmetry in Hcp. contradiction.
- (* h::t *)
inversion s; subst.
specialize (IHl H2). simpl in IHl.
destruct a as [k'' v''].
destruct (compare k k'') eqn:Hkk''; destruct (compare k' k'') eqn:Hk'k''; simpl;
try apply compare_eq_iff in Hkk''; try apply compare_eq_iff in Hk'k''; subst;
assert (compare k'' k'' = Eq) as Hk'' by (apply compare_eq_iff; reflexivity);
try (rewrite Hk'k''; auto).
+ contradiction.
+ rewrite Hk''. apply set.compare_gt_lt in Hkk''; try assumption.
rewrite Hkk''. reflexivity.
+ destruct (compare k' k) eqn:Hk'k; try reflexivity.
apply compare_eq_iff in Hk'k. symmetry in Hk'k. contradiction.
+ apply set.compare_gt_lt in Hkk''; try assumption.
unfold Relations_1.Transitive in gt_trans.
assert (compare k' k = Gt) as Hk'k by (eapply gt_trans; eassumption).
rewrite Hk'k. reflexivity.
+ rewrite Hk''. reflexivity.
Qed.
Lemma map_updateSome_spec : forall k v m nm,
nm = update k (Some v) m <->
(get k nm = (Some v) /\
(forall k', k <> k' -> map.get k' nm = map.get k' m)).
Proof.
intros. split.
- (* -> *)
intros Hnm. subst. split.
apply map_updateeq. intros k' Hdiff. apply map_updateneq. assumption.
- (* <- *)
intros [HSame HDiff].
apply map.extensionality; try assumption.
intro k'.
specialize (compare_diff k k') as HKeyDiff.
destruct (compare k k') eqn:Hkk'.
+ (* Eq *)
apply compare_eq_iff in Hkk'; subst.
rewrite HSame. symmetry. apply map_updateeq.
+ (* Lt *)
assert (k <> k') by (apply HKeyDiff; left; reflexivity).
assert (k <> k') as H2 by assumption.
apply HDiff in H. rewrite H. symmetry.
apply map_updateneq. assumption.
+ (* Gt *)
assert (k <> k') by (apply HKeyDiff; right; reflexivity).
assert (k <> k') as H2 by assumption.
apply HDiff in H. rewrite H. symmetry.
apply map_updateneq. assumption.
Qed.
Lemma map_updatemem : forall k m v,
mem k m ->
forall k', mem k (map.update k' (Some v) m).
Proof.
intros.
destruct m as [l]. unfold get, update. simpl. simpl in H.
induction l; simpl; simpl in H.
- (* nil *) inversion H.
- (* h::t *)
inversion s; subst. specialize (IHl H2).
destruct a as [k'' v''].
destruct (compare k k'') eqn:Hkk''; destruct (compare k' k'') eqn:Hk'k'';
simpl in H; simpl;
try rewrite compare_eq_iff in Hkk''; try rewrite compare_eq_iff in Hk'k''; subst;
assert (compare k'' k'' = Eq) as Hk'' by (apply compare_eq_iff; reflexivity);
try inversion H;
try rewrite Hk''; try rewrite Hkk''; try exact ITT.
+ apply set.compare_gt_lt in Hk'k''; try assumption. rewrite Hk'k''. exact ITT.
+ apply set.compare_gt_lt in Hk'k''; try assumption.
unfold Relations_1.Transitive in gt_trans.
assert (compare k k' = Gt) as Hkk' by (eapply gt_trans; eassumption).
rewrite Hkk'. exact ITT.
+ apply IHl. assumption.
Qed.
Lemma map_updatemem_rev : forall k k' m v,
k <> k' ->
mem k (map.update k' (Some v) m) ->
mem k m.
Proof.
intros.
destruct m as [l]. unfold map.get, map.update. simpl. simpl in H0.
induction l; simpl; simpl in H0.
- (* nil *)
rewrite <- (compare_diff k k') in H.
destruct H; rewrite H in H0; inversion H0.
- (* h::t *)
destruct a as [k'' v''].
destruct (compare k k'') eqn:Hkk''; destruct (compare k' k'') eqn:Hk'k''; try exact ITT;
inversion H0; try rewrite compare_eq_iff in Hk'k''; subst;
try rewrite Hkk'' in H2; inversion H2; try clear H3.
+ rewrite <- (compare_diff k k') in H.
destruct H; rewrite H in H2; inversion H2.
+ exact ITT.
+ apply set.compare_gt_lt in Hk'k''; try assumption.
unfold Relations_1.Transitive in gt_trans.
assert (compare k k' = Gt) by (eapply gt_trans; eassumption). rewrite H1 in H2.
unfold is_true. rewrite <- H2. exact ITT.
+ inversion s; subst. apply IHl. assumption.
unfold is_true. rewrite <- H2. exact ITT.
Qed.
End map.
Fixpoint list_map (B B' : Set) (f : B -> M B') (l : list B) : M (list B') :=
match l with
| nil => Return _ nil
| cons x l =>
error.bind (fun b' =>
error.bind (fun l' =>
Return _ (cons b' l')) (list_map _ _ f l)) (f x)
end.
Definition list_map_pair (A B B' : Set) (f : (A * B) -> M B') :
list (A * B) -> M (list (A * B')) :=
list_map (A * B) (A * B')
(fun ab => error.bind (fun b' => Return _ (fst ab, b')) (f ab)).
Lemma list_map_fst A B B' f l l' :
list_map_pair A B B' f l = Return _ l' ->
List.map fst l = List.map fst l'.
Proof.
generalize l'. clear l'.
induction l as [|(x, v) l].
- simpl.
intros l' H.
injection H.
intro He.
destruct He.
reflexivity.
- simpl.
intro l'.
unfold list_map_pair.
simpl.
case_eq (f (x, v)); simpl; try congruence.
intros b' He.
case_eq (list_map (A * B) (A * B') (fun ab : A * B =>
error.bind (fun b'0 : B' => Return (A * B') (fst ab, b'0)) (f ab)) l); simpl; try congruence.
intros l'' He2.
specialize (IHl l'').
intro H3.
injection H3.
intro Hl'.
destruct Hl'.
simpl.
f_equal.
apply IHl.
assumption.
Qed.
Program Definition map_fun_aux (A B B' : Set) compare (f : A * B -> M B') (l : list (A * B))
(H : Sorted.StronglySorted (fun x y => map_compare _ _ compare x y = Lt) l): M (map A B' compare) :=
match (list_map_pair _ _ _ f l) with
| Return _ l' => Return _ (exist _ l' _)
| Failed _ e => Failed _ e
end.
Next Obligation.
unfold set.lt.
rewrite list_sorted_map_fst.
rewrite <- (list_map_fst _ _ _ f l).
+ apply list_sorted_map_fst.
assumption.
+ symmetry.
assumption.
Defined.
Definition map_fun (A B B' : Set) comp
(f : A * B -> M B')
(m : map A B comp) : M (map A B' comp) :=
let (l, H) := m in
map_fun_aux _ _ _ comp f l H.