Commit bc659ba4 authored by Robbert Krebbers's avatar Robbert Krebbers

Finite maps and sets using ordered association lists.

This commit includes the following changes:
* More theorems about pre-, partial and total orders.
* Define the lexicographic order on various commonly used data types.
* Mergesort and its correctness proof.
* Implement finite maps and sets using ordered association lists.
parent 46304c52
(* Copyright (c) 2012-2013, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** An implementation of finite maps and finite sets using association lists
ordered by keys. Although the lookup and insert operation are linear-time, the
main advantage of these association lists compared to search trees, is that it
has canonical representatives and thus extensional Leibniz equality. Compared
to a naive unordered association list, the merge operation (used for unions,
intersections, and difference) is also linear-time. *)
Require Import mapset.
Require Export fin_maps.
(** Because the association list is sorted using [strict lexico] instead of
[lexico], it automatically guarantees that no duplicates exist. *)
Definition assoc (K : Type) `{Lexico K} `{!TrichotomyT lexico}
`{!PartialOrder lexico} (A : Type) : Type :=
dsig (λ l : list (K * A), StronglySorted (strict lexico) (fst <$> l)).
Section assoc.
Context `{Lexico K} `{!PartialOrder lexico}.
Context `{ x y : K, Decision (x = y)} `{!TrichotomyT lexico}.
Infix "⊂" := (strict lexico).
Notation assoc_before j l :=
(Forall (strict lexico j) (fst <$> l)) (only parsing).
Notation assoc_wf l :=
(StronglySorted (strict lexico) (fst <$> l)) (only parsing).
Lemma assoc_before_transitive {A} (l : list (K * A)) i j :
i j assoc_before j l assoc_before i l.
Proof. intros. eapply Forall_impl; eauto. intros. by transitivity j. Qed.
Hint Resolve assoc_before_transitive.
Hint Extern 1 (StronglySorted _ []) => constructor.
Hint Extern 1 (StronglySorted _ (_ :: _)) => constructor.
Hint Extern 1 (Forall _ []) => constructor.
Hint Extern 1 (Forall _ (_ :: _)) => constructor.
Hint Extern 100 => progress simpl.
Ltac simplify_assoc := intros;
repeat match goal with
| H : Forall _ [] |- _ => clear H
| H : Forall _ (_ :: _) |- _ => inversion_clear H
| H : StronglySorted _ [] |- _ => clear H
| H : StronglySorted _ (_ :: _) |- _ => inversion_clear H
| _ => progress decompose_elem_of_list
| _ => progress simplify_equality'
end;
repeat first
[ progress simplify_order
| progress autorewrite with assoc in *; simplify_equality'
| destruct (trichotomyT lexico) as [[?|?]|?]; simplify_equality' ];
eauto 9.
Fixpoint assoc_lookup_raw {A} (i : K) (l : list (K * A)) : option A :=
match l with
| [] => None
| (j,x) :: l =>
match trichotomyT lexico i j with
| (**i i ⊂ j *) inleft (left _) => None
| (**i i = j *) inleft (right _) => Some x
| (**i j ⊂ i *) inright _ => assoc_lookup_raw i l
end
end.
Global Instance assoc_lookup {A} : Lookup K A (assoc K A) := λ k m,
assoc_lookup_raw k (`m).
Lemma assoc_lookup_before {A} (l : list (K * A)) i :
assoc_before i l assoc_lookup_raw i l = None.
Proof. induction l as [|[??]]; simplify_assoc. Qed.
Hint Rewrite @assoc_lookup_before using (by eauto) : assoc.
Lemma assoc_eq {A} (l1 l2 : list (K * A)) :
assoc_wf l1 assoc_wf l2
( i, assoc_lookup_raw i l1 = assoc_lookup_raw i l2) l1 = l2.
Proof.
revert l2. induction l1 as [|[i x] l1 IH]; intros [|[j y] l2]; intros ?? E.
{ done. }
{ specialize (E j); simplify_assoc; by repeat constructor. }
{ specialize (E i); simplify_assoc; by repeat constructor. }
pose proof (E i); pose proof (E j); simplify_assoc.
f_equal. apply IH; auto. intros i'. specialize (E i'); simplify_assoc.
Qed.
Definition assoc_empty_wf {A} : assoc_wf (@nil (K * A)).
Proof. constructor. Qed.
Global Instance assoc_empty {A} : Empty (assoc K A) := dexist _ assoc_empty_wf.
Definition assoc_cons {A} (i : K) (o : option A) (l : list (K * A)) :
list (K * A) := match o with None => l | Some z => (i,z) :: l end.
Lemma assoc_cons_before {A} (l : list (K * A)) i j o :
assoc_before i l i j assoc_before i (assoc_cons j o l).
Proof. destruct o; simplify_assoc. Qed.
Lemma assoc_cons_wf {A} (l : list (K * A)) i o :
assoc_wf l assoc_before i l assoc_wf (assoc_cons i o l).
Proof. destruct o; simplify_assoc. Qed.
Hint Resolve assoc_cons_before assoc_cons_wf.
Lemma assoc_lookup_cons {A} (l : list (K * A)) i o :
assoc_before i l assoc_lookup_raw i (assoc_cons i o l) = o.
Proof. destruct o; simplify_assoc. Qed.
Lemma assoc_lookup_cons_lt {A} (l : list (K * A)) i j o :
i j assoc_before i l assoc_lookup_raw i (assoc_cons j o l) = None.
Proof. destruct o; simplify_assoc. Qed.
Lemma assoc_lookup_cons_gt {A} (l : list (K * A)) i j o :
j i assoc_lookup_raw i (assoc_cons j o l) = assoc_lookup_raw i l.
Proof. destruct o; simplify_assoc. Qed.
Hint Rewrite @assoc_lookup_cons @assoc_lookup_cons_lt
@assoc_lookup_cons_gt using (by eauto 8) : assoc.
Fixpoint assoc_alter_raw {A} (f : option A option A)
(i : K) (l : list (K * A)) : list (K * A) :=
match l with
| [] => assoc_cons i (f None) []
| (j,x) :: l =>
match trichotomyT lexico i j with
| (**i i ⊂ j *) inleft (left _) => assoc_cons i (f None) ((j,x) :: l)
| (**i i = j *) inleft (right _) => assoc_cons j (f (Some x)) l
| (**i j ⊂ i *) inright _ => (j,x) :: assoc_alter_raw f i l
end
end.
Lemma assoc_alter_wf {A} (f : option A option A) i l :
assoc_wf l assoc_wf (assoc_alter_raw f i l).
Proof.
revert l. assert ( j l,
j i assoc_before j l assoc_before j (assoc_alter_raw f i l)).
{ intros j l. induction l as [|[??]]; simplify_assoc. }
intros l. induction l as [|[??]]; simplify_assoc.
Qed.
Global Instance assoc_alter {A} : PartialAlter K A (assoc K A) := λ f i m,
dexist _ (assoc_alter_wf f i _ (proj2_dsig m)).
Lemma assoc_lookup_raw_alter {A} f (l : list (K * A)) i :
assoc_wf l
assoc_lookup_raw i (assoc_alter_raw f i l) = f (assoc_lookup_raw i l).
Proof. induction l as [|[??]]; simplify_assoc. Qed.
Lemma assoc_lookup_raw_alter_ne {A} f (l : list (K * A)) i j :
assoc_wf l i j
assoc_lookup_raw j (assoc_alter_raw f i l) = assoc_lookup_raw j l.
Proof.
induction l as [|[??]]; simplify_assoc; unfold assoc_cons;
destruct (f _); simplify_assoc.
Qed.
Lemma assoc_fmap_wf {A B} (f : A B) (l : list (K * A)) :
assoc_wf l assoc_wf (snd_map f <$> l).
Proof.
intros. by rewrite <-list_fmap_compose,
(list_fmap_ext _ fst l l) by (done; by intros []).
Qed.
Global Program Instance assoc_fmap: FMap (assoc K) := λ A B f m,
dexist _ (assoc_fmap_wf f _ (proj2_dsig m)).
Lemma assoc_lookup_fmap {A B} (f : A B) (l : list (K * A)) i :
assoc_lookup_raw i (snd_map f <$> l) = fmap f (assoc_lookup_raw i l).
Proof. induction l as [|[??]]; simplify_assoc. Qed.
Fixpoint assoc_merge_aux {A B} (f : option A option B)
(l : list (K * A)) : list (K * B) :=
match l with
| [] => []
| (i,x) :: l => assoc_cons i (f (Some x)) (assoc_merge_aux f l)
end.
Fixpoint assoc_merge_raw {A B C} (f : option A option B option C)
(l : list (K * A)) : list (K * B) list (K * C) :=
fix go (k : list (K * B)) :=
match l, k with
| [], _ => assoc_merge_aux (f None) k
| _, [] => assoc_merge_aux (flip f None) l
| (i,x) :: l, (j,y) :: k =>
match trichotomyT lexico i j with
| (**i i ⊂ j *) inleft (left _) =>
assoc_cons i (f (Some x) None) (assoc_merge_raw f l ((j,y) :: k))
| (**i i = j *) inleft (right _) =>
assoc_cons i (f (Some x) (Some y)) (assoc_merge_raw f l k)
| (**i j ⊂ i *) inright _ =>
assoc_cons j (f None (Some y)) (go k)
end
end.
Section assoc_merge_raw.
Context {A B C} (f : option A option B option C).
Lemma assoc_merge_nil_l k :
assoc_merge_raw f [] k = assoc_merge_aux (f None) k.
Proof. by destruct k. Qed.
Lemma assoc_merge_nil_r l :
assoc_merge_raw f l [] = assoc_merge_aux (flip f None) l.
Proof. by destruct l as [|[??]]. Qed.
Lemma assoc_merge_cons i x j y l k :
assoc_merge_raw f ((i,x) :: l) ((j,y) :: k) =
match trichotomyT lexico i j with
| (**i i ⊂ j *) inleft (left _) =>
assoc_cons i (f (Some x) None) (assoc_merge_raw f l ((j,y) :: k))
| (**i i = j *) inleft (right _) =>
assoc_cons i (f (Some x) (Some y)) (assoc_merge_raw f l k)
| (**i j ⊂ i *) inright _ =>
assoc_cons j (f None (Some y)) (assoc_merge_raw f ((i,x) :: l) k)
end.
Proof. done. Qed.
End assoc_merge_raw.
Arguments assoc_merge_raw _ _ _ _ _ _ : simpl never.
Hint Rewrite @assoc_merge_nil_l @assoc_merge_nil_r @assoc_merge_cons : assoc.
Lemma assoc_merge_aux_before {A B} (f : option A option B) l j :
assoc_before j l assoc_before j (assoc_merge_aux f l).
Proof. induction l as [|[??]]; simplify_assoc. Qed.
Hint Resolve assoc_merge_aux_before.
Lemma assoc_merge_before {A B C} (f : option A option B option C) l1 l2 j :
assoc_before j l1 assoc_before j l2
assoc_before j (assoc_merge_raw f l1 l2).
Proof.
revert l2. induction l1 as [|[??] l1 IH];
intros l2; induction l2 as [|[??] l2 IH2]; simplify_assoc.
Qed.
Hint Resolve assoc_merge_before.
Lemma assoc_merge_wf {A B C} (f : option A option B option C) l1 l2 :
assoc_wf l1 assoc_wf l2 assoc_wf (assoc_merge_raw f l1 l2).
Proof.
revert A B C f l1 l2. assert ( A B (f : option A option B) l,
assoc_wf l assoc_wf (assoc_merge_aux f l)).
{ intros ?? j l. induction l as [|[??]]; simplify_assoc. }
intros A B C f l1. induction l1 as [|[i x] l1 IH];
intros l2; induction l2 as [|[j y] l2 IH2]; simplify_assoc.
Qed.
Global Instance assoc_merge: Merge (assoc K) := λ A B C f m1 m2,
dexist (merge f (`m1) (`m2))
(assoc_merge_wf _ _ _ (proj2_dsig m1) (proj2_dsig m2)).
Lemma assoc_merge_aux_spec {A B} (f : option A option B) l i :
f None = None assoc_wf l
assoc_lookup_raw i (assoc_merge_aux f l) = f (assoc_lookup_raw i l).
Proof. intros. induction l as [|[??]]; simplify_assoc. Qed.
Hint Rewrite @assoc_merge_aux_spec using (by eauto) : assoc.
Lemma assoc_merge_spec {A B C} (f : option A option B option C) l1 l2 i :
f None None = None assoc_wf l1 assoc_wf l2
assoc_lookup_raw i (assoc_merge_raw f l1 l2) =
f (assoc_lookup_raw i l1) (assoc_lookup_raw i l2).
Proof.
intros ?. revert l2. induction l1 as [|[??] l1 IH]; intros l2;
induction l2 as [|[??] l2 IH2]; simplify_assoc; rewrite ?IH; simplify_assoc.
Qed.
Global Instance assoc_to_list {A} : FinMapToList K A (assoc K A) :=
@proj1_sig _ _.
Lemma assoc_to_list_nodup {A} (l : list (K * A)) : assoc_wf l NoDup l.
Proof.
revert l. assert ( i x (l : list (K * A)), assoc_before i l (i,x) l).
{ intros i x l. rewrite Forall_fmap, Forall_forall. intros Hl Hi.
destruct (irreflexivity (strict lexico) i). by apply (Hl (i,x) Hi). }
induction l as [|[??]]; simplify_assoc; constructor; auto.
Qed.
Lemma assoc_to_list_elem_of {A} (l : list (K * A)) i x :
assoc_wf l (i,x) l assoc_lookup_raw i l = Some x.
Proof.
split.
* induction l as [|[??]]; simplify_assoc; naive_solver.
* induction l as [|[??]]; simplify_assoc; [left| right]; eauto.
Qed.
(** * Instantiation of the finite map interface *)
Hint Extern 1 (assoc_wf _) => by apply (bool_decide_unpack _).
Global Instance: FinMap K (assoc K).
Proof.
split.
* intros ? [l1 ?] [l2 ?] ?. apply (sig_eq_pi _), assoc_eq; auto.
* done.
* intros ?? [??] ?. apply assoc_lookup_raw_alter; auto.
* intros ?? [??] ???. apply assoc_lookup_raw_alter_ne; auto.
* intros ??? [??] ?. apply assoc_lookup_fmap.
* intros ? [??]. apply assoc_to_list_nodup; auto.
* intros ? [??] ??. apply assoc_to_list_elem_of; auto.
* intros ????? [??] [??] ?. apply assoc_merge_spec; auto.
Qed.
End assoc.
(** * Finite sets *)
(** We construct finite sets using the above implementation of maps. *)
Notation assoc_set K := (mapset (assoc K)).
Instance assoc_map_dom `{Lexico K} `{!TrichotomyT (@lexico K _)}
`{!PartialOrder lexico} {A} : Dom (assoc K A) (assoc_set K) := mapset_dom.
Instance assoc_map_dom_spec `{Lexico K} `{!TrichotomyT (@lexico K _)}
`{!PartialOrder lexico} `{ x y : K, Decision (x = y)} :
FinMapDom K (assoc K) (assoc_set K) := mapset_dom_spec.
......@@ -14,9 +14,9 @@ Coercion Is_true : bool >-> Sortclass.
(** Ensure that [simpl] unfolds [id], [compose], and [flip] when fully
applied. *)
Arguments id _ _/.
Arguments id _ _ /.
Arguments compose _ _ _ _ _ _ /.
Arguments flip _ _ _ _ _ _/.
Arguments flip _ _ _ _ _ _ /.
Typeclasses Transparent id compose flip.
(** Change [True] and [False] into notations in order to enable overloading.
......@@ -211,7 +211,7 @@ Notation "{[ x , y ]}" := (singleton (x,y))
Notation "{[ x , y , z ]}" := (singleton (x,y,z))
(at level 1, y at next level, z at next level) : C_scope.
Class SubsetEq A := subseteq: A A Prop.
Class SubsetEq A := subseteq: relation A.
Instance: Params (@subseteq) 2.
Infix "⊆" := subseteq (at level 70) : C_scope.
Notation "(⊆)" := subseteq (only parsing) : C_scope.
......@@ -226,17 +226,22 @@ Notation "(⊆*)" := (Forall2 subseteq) (only parsing) : C_scope.
Hint Extern 0 (_ _) => reflexivity.
Class Subset A := subset: A A Prop.
Instance: Params (@subset) 2.
Infix "⊂" := subset (at level 70) : C_scope.
Notation "(⊂)" := subset (only parsing) : C_scope.
Notation "( X ⊂ )" := (subset X) (only parsing) : C_scope.
Notation "( ⊂ X )" := (λ Y, subset Y X) (only parsing) : C_scope.
Definition strict {A} (R : relation A) : relation A := λ X Y, R X Y ¬R Y X.
Instance: Params (@strict) 2.
Infix "⊂" := (strict subseteq) (at level 70) : C_scope.
Notation "(⊂)" := (strict subseteq) (only parsing) : C_scope.
Notation "( X ⊂ )" := (strict subseteq X) (only parsing) : C_scope.
Notation "( ⊂ X )" := (λ Y, strict subseteq Y X) (only parsing) : C_scope.
Notation "X ⊄ Y" := (¬X Y) (at level 70) : C_scope.
Notation "(⊄)" := (λ X Y, X Y) (only parsing) : C_scope.
Notation "( X ⊄ )" := (λ Y, X Y) (only parsing) : C_scope.
Notation "( ⊄ X )" := (λ Y, Y X) (only parsing) : C_scope.
(** The class [Lexico A] is used for the lexicographic order on [A]. This order
is used to create finite maps, finite sets, etc, and is typically different from
the order [(⊆)]. *)
Class Lexico A := lexico: relation A.
Class ElemOf A B := elem_of: A B Prop.
Instance: Params (@elem_of) 3.
Infix "∈" := elem_of (at level 70) : C_scope.
......@@ -472,6 +477,11 @@ Class RightDistr {A} (R : relation A) (f g : A → A → A) : Prop :=
right_distr: y z x, R (f (g y z) x) (g (f y x) (f z x)).
Class AntiSymmetric {A} (R S : relation A) : Prop :=
anti_symmetric: x y, S x y S y x R x y.
Class Total {A} (R : relation A) := total x y : R x y R y x.
Class Trichotomy {A} (R : relation A) :=
trichotomy : x y, strict R x y x = y strict R y x.
Class TrichotomyT {A} (R : relation A) :=
trichotomyT : x y, {strict R x y} + {x = y} + {strict R y x}.
Arguments irreflexivity {_} _ {_} _ _.
Arguments injective {_ _ _ _} _ {_} _ _ _.
......@@ -488,6 +498,9 @@ Arguments right_absorb {_ _} _ _ {_} _.
Arguments left_distr {_ _} _ _ {_} _ _ _.
Arguments right_distr {_ _} _ _ {_} _ _ _.
Arguments anti_symmetric {_ _} _ {_} _ _ _ _.
Arguments total {_} _ {_} _ _.
Arguments trichotomy {_} _ {_} _ _.
Arguments trichotomyT {_} _ {_} _ _.
(** The following lemmas are specific versions of the projections of the above
type classes for Leibniz equality. These lemmas allow us to enforce Coq not to
......@@ -518,15 +531,22 @@ Lemma right_distr_L {A} (f g : A → A → A) `{!RightDistr (=) f g} y z x :
Proof. auto. Qed.
(** ** Axiomatization of ordered structures *)
(** The classes [PreOrder], [PartialOrder], and [TotalOrder] do not use the
relation [⊆] because we often have multiple orders on the same structure. *)
Class PartialOrder {A} (R : relation A) : Prop := {
po_preorder :> PreOrder R;
po_anti_symmetric :> AntiSymmetric (=) R
}.
Class TotalOrder {A} (R : relation A) : Prop := {
to_po :> PartialOrder R;
to_trichotomy :> Trichotomy R
}.
(** A pre-order equipped with a smallest element. *)
Class BoundedPreOrder A `{Empty A} `{SubsetEq A} : Prop := {
bounded_preorder :>> PreOrder ();
subseteq_empty x : x
}.
Class PartialOrder {A} (R : relation A) : Prop := {
po_preorder :> PreOrder R;
po_antisym :> AntiSymmetric (=) R
}.
(** We do not include equality in the following interfaces so as to avoid the
need for proofs that the relations and operations respect setoid equality.
......@@ -678,18 +698,10 @@ Arguments snd_map {_ _ _} _ !_ /.
Instance: {A A' B} (f : A A'),
Injective (=) (=) f Injective (=) (=) (@fst_map A A' B f).
Proof.
intros ????? [??] [??]; simpl; intro; f_equal.
* apply (injective f). congruence.
* congruence.
Qed.
Proof. intros ????? [??] [??]; injection 1; firstorder congruence. Qed.
Instance: {A B B'} (f : B B'),
Injective (=) (=) f Injective (=) (=) (@snd_map A B B' f).
Proof.
intros ????? [??] [??]; simpl; intro; f_equal.
* congruence.
* apply (injective f). congruence.
Qed.
Proof. intros ????? [??] [??]; injection 1; firstorder congruence. Qed.
Definition prod_relation {A B} (R1 : relation A) (R2 : relation B) :
relation (A * B) := λ x y, R1 (fst x) (fst y) R2 (snd x) (snd y).
......@@ -781,51 +793,51 @@ Proof. intros y. exists (g y). auto. Qed.
Lemma impl_transitive (P Q R : Prop) : (P Q) (Q R) (P R).
Proof. tauto. Qed.
Instance: Commutative () (@eq A).
Proof. red. intuition. Qed.
Proof. red; intuition. Qed.
Instance: Commutative () (λ x y, @eq A y x).
Proof. red. intuition. Qed.
Proof. red; intuition. Qed.
Instance: Commutative () ().
Proof. red. intuition. Qed.
Proof. red; intuition. Qed.
Instance: Commutative () ().
Proof. red. intuition. Qed.
Proof. red; intuition. Qed.
Instance: Associative () ().
Proof. red. intuition. Qed.
Proof. red; intuition. Qed.
Instance: Idempotent () ().
Proof. red. intuition. Qed.
Proof. red; intuition. Qed.
Instance: Commutative () ().
Proof. red. intuition. Qed.
Proof. red; intuition. Qed.
Instance: Associative () ().
Proof. red. intuition. Qed.
Proof. red; intuition. Qed.
Instance: Idempotent () ().
Proof. red. intuition. Qed.
Proof. red; intuition. Qed.
Instance: LeftId () True ().
Proof. red. intuition. Qed.
Proof. red; intuition. Qed.
Instance: RightId () True ().
Proof. red. intuition. Qed.
Proof. red; intuition. Qed.
Instance: LeftAbsorb () False ().
Proof. red. intuition. Qed.
Proof. red; intuition. Qed.
Instance: RightAbsorb () False ().
Proof. red. intuition. Qed.
Proof. red; intuition. Qed.
Instance: LeftId () False ().
Proof. red. intuition. Qed.
Proof. red; intuition. Qed.
Instance: RightId () False ().
Proof. red. intuition. Qed.
Proof. red; intuition. Qed.
Instance: LeftAbsorb () True ().
Proof. red. intuition. Qed.
Proof. red; intuition. Qed.
Instance: RightAbsorb () True ().
Proof. red. intuition. Qed.
Proof. red; intuition. Qed.
Instance: LeftId () True impl.
Proof. unfold impl. red. intuition. Qed.
Proof. unfold impl. red; intuition. Qed.
Instance: RightAbsorb () True impl.
Proof. unfold impl. red. intuition. Qed.
Proof. unfold impl. red; intuition. Qed.
Instance: LeftDistr () () ().
Proof. red. intuition. Qed.
Proof. red; intuition. Qed.
Instance: RightDistr () () ().
Proof. red. intuition. Qed.
Proof. red; intuition. Qed.
Instance: LeftDistr () () ().
Proof. red. intuition. Qed.
Proof. red; intuition. Qed.
Instance: RightDistr () () ().
Proof. red. intuition. Qed.
Proof. red; intuition. Qed.
Lemma not_injective `{Injective A B R R' f} x y : ¬R x y ¬R' (f x) (f y).
Proof. intuition. Qed.
Instance injective_compose {A B C} R1 R2 R3 (f : A B) (g : B C) :
......
......@@ -144,7 +144,7 @@ Proof.
by apply size_non_empty_iff, non_empty_difference.
Qed.
Lemma collection_wf : wf (@subset C _).
Lemma collection_wf : wf (strict (@subseteq C _)).
Proof. apply well_founded_lt_compat with size, subset_size. Qed.
Lemma collection_ind (P : C Prop) :
......
......@@ -372,7 +372,7 @@ Lemma insert_subset_inv {A} (m1 m2 : M A) i x :
m2', m2 = <[i:=x]>m2' m1 m2' m2' !! i = None.
Proof.
intros Hi Hm1m2. exists (delete i m2). split_ands.
* rewrite insert_delete. done. eapply lookup_weaken, subset_subseteq; eauto.
* rewrite insert_delete. done. eapply lookup_weaken, strict_include; eauto.
by rewrite lookup_insert.
* eauto using insert_delete_subset.
* by rewrite lookup_delete.
......@@ -564,7 +564,7 @@ Proof.
rewrite !map_to_list_insert; simpl; auto with arith.
Qed.
Lemma map_wf {A} : wf (@subset (M A) _).
Lemma map_wf {A} : wf (strict (@subseteq (M A) _)).
Proof.
apply (wf_projected (<) (length map_to_list)).
* by apply map_to_list_length.
......@@ -1013,13 +1013,13 @@ Qed.
Lemma map_union_cancel_l {A} (m1 m2 m3 : M A) :
m1 m3 m2 m3 m3 m1 = m3 m2 m1 = m2.
Proof.
intros. by apply (anti_symmetric _);
intros. by apply (anti_symmetric ());
apply map_union_reflecting_l with m3; auto with congruence.
Qed.
Lemma map_union_cancel_r {A} (m1 m2 m3 : M A) :
m1 m3 m2 m3 m1 m3 = m2 m3 m1 = m2.
Proof.
intros. apply (anti_symmetric _);
intros. apply (anti_symmetric ());
apply map_union_reflecting_r with m3; auto with congruence.
Qed.
......
(* Copyright (c) 2012-2013, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
(** This files defines a lexicographic order on various common data structures
and proves that it is a partial order having a strong variant of trichotomy. *)
Require Import orders.
Notation cast_trichotomy T :=
match T with
| inleft (left _) => inleft (left _)
| inleft (right _) => inleft (right _)
| inright _ => inright _
end.
Instance prod_lexico `{Lexico A} `{Lexico B} : Lexico (A * B) := λ p1 p2,
(**i 1.) *) strict lexico (fst p1) (fst p2)
(**i 2.) *) fst p1 = fst p2 lexico (snd p1) (snd p2).
Lemma prod_lexico_strict `{Lexico A} `{Lexico B} (p1 p2 : A * B) :
strict lexico p1 p2
strict lexico (fst p1) (fst p2)
fst p1 = fst p2 strict lexico (snd p1) (snd p2).
Proof.
destruct p1, p2. repeat (unfold lexico, prod_lexico, strict). naive_solver.
Qed.
Instance bool_lexico : Lexico bool := ().
Instance nat_lexico : Lexico nat := ().
Instance N_lexico : Lexico N := ()%N.
Instance Z_lexico : Lexico Z := ()%Z.
Typeclasses Opaque bool_lexico nat_lexico N_lexico Z_lexico.
Instance list_lexico `{Lexico A} : Lexico (list A) :=
fix go l1 l2 :=
let _ : Lexico (list A) := @go in
match l1, l2 with
| [], _ => True
| _ :: _, [] => False
| x1 :: l1, x2 :: l2 => lexico (x1,l1) (x2,l2)
end.
Instance sig_lexico `{Lexico A} (P : A Prop) `{ x, ProofIrrel (P x)} :
Lexico (sig P) := λ x1 x2, lexico (`x1) (`x2).
Lemma prod_lexico_reflexive `{Lexico A} `{!PartialOrder (@lexico A _)}
`{Lexico B} (x : A) (y : B) : lexico y y lexico (x,y) (x,y).
Proof. by right. Qed.
Lemma prod_lexico_transitive `{Lexico A} `{!PartialOrder (@lexico A _)}
`{Lexico B} (x1 x2 x3 : A) (y1 y2 y3 : B) :
lexico (x1,y1) (x2,y2) lexico (x2,y2) (x3,y3)
(lexico y1 y2 lexico y2 y3 lexico y1 y3) lexico (x1,y1) (x3,y3).
Proof.
intros Hx12 Hx23 ?; revert Hx12 Hx23. unfold lexico, prod_lexico.
intros [|[??]] [?|[??]]; simplify_equality'; auto. left. by transitivity x2.
Qed.
Lemma prod_lexico_anti_symmetric `{Lexico A} `{!PartialOrder (@lexico A _)}
`{Lexico B} (x1 x2 : A) (y1 y2 : B) :
lexico (x1,y1) (x2,y2) lexico (x2,y2) (x1,y1)
(lexico y1 y2 lexico y2 y1 y1 = y2) x1 = x2 y1 = y2.
Proof. by intros [[??]|[??]] [[??]|[??]] ?; simplify_equality'; auto. Qed.
Instance prod_lexico_po `{Lexico A} `{Lexico B} `{!PartialOrder (@lexico A _)}
`{!PartialOrder (@lexico B _)} : PartialOrder (@lexico (A * B) _).
Proof.
repeat split.
* by intros [??]; apply prod_lexico_reflexive.
* intros [??] [??] [??] ??.
eapply prod_lexico_transitive; eauto. apply @transitivity, _.
* intros [x1 y1] [x2 y2] ??.
destruct (prod_lexico_anti_symmetric x1 x2 y1 y2); try intuition congruence.
apply (anti_symmetric _).
Qed.
Instance prod_lexico_trichotomyT `{Lexico A} `{tA: !TrichotomyT (@lexico A _)}
`{Lexico B} `{tB:!TrichotomyT (@lexico B _)}: TrichotomyT (@lexico (A * B) _).
Proof.
red; refine (λ p1 p2,
match trichotomyT lexico (fst p1) (fst p2) with
| inleft (left _) => inleft (left _)
| inleft (right _) =>
cast_trichotomy (trichotomyT lexico (snd p1) (snd p2))
| inright _ => inright _
end); clear tA tB; abstract (rewrite ?prod_lexico_strict;
intuition (auto using injective_projections with congruence)).
Defined.
Instance bool_lexico_po : PartialOrder (@lexico bool _).
Proof.
unfold lexico, bool_lexico. repeat split.
* intros []; simpl; tauto.
* intros [] [] []; simpl; tauto.
* intros [] []; simpl; tauto.
Qed.
Instance bool_lexico_trichotomy: TrichotomyT (@lexico bool _).
Proof.
red; refine (λ b1 b2,
match b1, b2 with
| false, false => inleft (right _)
| false, true => inleft (left _)
| true, false => inright _
| true, true => inleft (right _)
end); abstract (unfold strict, lexico, bool_lexico; naive_solver).
Defined.
Lemma nat_lexico_strict (x1 x2 : nat) : strict lexico x1 x2 x1 < x2.
Proof. unfold strict, lexico, nat_lexico. lia. Qed.
Instance nat_lexico_po : PartialOrder (@lexico nat _).