From bc659ba4d1b18dcd5a69c7460016691fefcd2948 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 12 Aug 2013 10:07:53 +0200
Subject: [PATCH] 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.
---
 theories/assoc.v           | 283 +++++++++++++++++++++++++++++
 theories/base.v            | 104 ++++++-----
 theories/fin_collections.v |   2 +-
 theories/fin_maps.v        |   8 +-
 theories/lexico.v          | 186 ++++++++++++++++++++
 theories/nmap.v            |   3 +-
 theories/numbers.v         |  11 +-
 theories/orders.v          | 352 ++++++++++++++++++++++++++++++++-----
 theories/pmap.v            | 224 ++++++++++++-----------
 theories/prelude.v         |   3 +-
 10 files changed, 965 insertions(+), 211 deletions(-)
 create mode 100644 theories/assoc.v
 create mode 100644 theories/lexico.v

diff --git a/theories/assoc.v b/theories/assoc.v
new file mode 100644
index 00000000..bfd254d0
--- /dev/null
+++ b/theories/assoc.v
@@ -0,0 +1,283 @@
+(* 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.
diff --git a/theories/base.v b/theories/base.v
index dc7953fd..f4af422b 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -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) :
diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index ba6f96b1..f0af0c92 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -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) :
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 9329ffc3..eb2e0554 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -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.
 
diff --git a/theories/lexico.v b/theories/lexico.v
new file mode 100644
index 00000000..3e00b4e6
--- /dev/null
+++ b/theories/lexico.v
@@ -0,0 +1,186 @@
+(* 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 _).
+Proof. unfold lexico, nat_lexico. apply _. Qed.
+Instance nat_lexico_trichotomy: TrichotomyT (@lexico nat _).
+Proof.
+ red; refine (λ n1 n2,
+  match Nat.compare n1 n2 as c return Nat.compare n1 n2 = c → _ with
+  | Lt => λ H,
+    inleft (left (proj2 (nat_lexico_strict _ _) (nat_compare_Lt_lt _ _ H)))
+  | Eq => λ H, inleft (right (nat_compare_eq _ _ H))
+  | Gt => λ H,
+    inright (proj2 (nat_lexico_strict _ _) (nat_compare_Gt_gt _ _ H))
+  end eq_refl).
+Defined.
+
+Lemma N_lexico_strict (x1 x2 : N) : strict lexico x1 x2 ↔ (x1 < x2)%N.
+Proof. unfold strict, lexico, N_lexico. lia. Qed.
+Instance N_lexico_po : PartialOrder (@lexico N _).
+Proof. unfold lexico, N_lexico. apply _. Qed.
+Instance N_lexico_trichotomy: TrichotomyT (@lexico N _).
+Proof.
+ red; refine (λ n1 n2,
+  match N.compare n1 n2 as c return N.compare n1 n2 = c → _ with
+  | Lt => λ H,
+    inleft (left (proj2 (N_lexico_strict _ _) (proj2 (N.compare_lt_iff _ _) H)))
+  | Eq => λ H, inleft (right (N.compare_eq _ _ H))
+  | Gt => λ H,
+    inright (proj2 (N_lexico_strict _ _) (proj1 (N.compare_gt_iff _ _) H))
+  end eq_refl).
+Defined.
+
+Lemma Z_lexico_strict (x1 x2 : Z) : strict lexico x1 x2 ↔ (x1 < x2)%Z.
+Proof. unfold strict, lexico, Z_lexico. lia. Qed.
+Instance Z_lexico_po : PartialOrder (@lexico Z _).
+Proof. unfold lexico, Z_lexico. apply _. Qed.
+Instance Z_lexico_trichotomy: TrichotomyT (@lexico Z _).
+Proof.
+ red; refine (λ n1 n2,
+  match Z.compare n1 n2 as c return Z.compare n1 n2 = c → _ with
+  | Lt => λ H,
+    inleft (left (proj2 (Z_lexico_strict _ _) (proj2 (Z.compare_lt_iff _ _) H)))
+  | Eq => λ H, inleft (right (Z.compare_eq _ _ H))
+  | Gt => λ H,
+    inright (proj2 (Z_lexico_strict _ _) (proj1 (Z.compare_gt_iff _ _) H))
+  end eq_refl).
+Defined.
+
+Instance list_lexico_po `{Lexico A} `{!PartialOrder (@lexico A _)} :
+  PartialOrder (@lexico (list A) _).
+Proof.
+  repeat split.
+  * intros l. induction l. done. by apply prod_lexico_reflexive.
+  * intros l1. induction l1 as [|x1 l1]; intros [|x2 l2] [|x3 l3] ??; try done.
+    eapply prod_lexico_transitive; eauto.
+  * intros l1. induction l1 as [|x1 l1]; intros [|x2 l2] ??; try done.
+    destruct (prod_lexico_anti_symmetric x1 x2 l1 l2); naive_solver.
+Qed.
+Instance list_lexico_trichotomy `{Lexico A} `{!TrichotomyT (@lexico A _)} :
+  TrichotomyT (@lexico (list A) _).
+Proof.
+ refine (
+  fix go l1 l2 :=
+  let go' : TrichotomyT (@lexico (list A) _) := @go in
+  match l1, l2 with
+  | [], [] => inleft (right _)
+  | [], _ :: _ => inleft (left _)
+  | _ :: _, [] => inright _
+  | x1 :: l1, x2 :: l2 => cast_trichotomy (trichotomyT lexico (x1,l1) (x2,l2))
+  end); clear go go';
+  abstract (repeat (done || constructor || congruence || by inversion 1)).
+Defined.
+
+Instance sig_lexico_po `{Lexico A} `{!PartialOrder (@lexico A _)}
+  (P : A → Prop) `{∀ x, ProofIrrel (P x)} : PartialOrder (@lexico (sig P) _).
+Proof.
+  unfold lexico, sig_lexico. repeat split.
+  * by intros [??].
+  * intros [x1 ?] [x2 ?] [x3 ?] ??. by simplify_order.
+  * intros [x1 ?] [x2 ?] ??. apply (sig_eq_pi _). by simplify_order.
+Qed.
+Instance sig_lexico_trichotomy `{Lexico A} `{tA: !TrichotomyT (@lexico A _)}
+  (P : A → Prop) `{∀ x, ProofIrrel (P x)} : TrichotomyT (@lexico (sig P) _).
+Proof.
+ red; refine (λ x1 x2, cast_trichotomy (trichotomyT lexico (`x1) (`x2)));
+  abstract (repeat (done || constructor || apply (sig_eq_pi P))).
+Defined.
diff --git a/theories/nmap.v b/theories/nmap.v
index 0bf1f153..49fab13d 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -79,7 +79,8 @@ Proof.
     apply (lookup_merge f t1 t2).
 Qed.
 
-(** Finally, we can construct sets of [N]s satisfying extensional equality. *)
+(** * Finite sets *)
+(** We construct sets of [N]s satisfying extensional equality. *)
 Notation Nset := (mapset Nmap).
 Instance Nmap_dom {A} : Dom (Nmap A) Nset := mapset_dom.
 Instance: FinMapDom N Nmap Nset := mapset_dom_spec.
diff --git a/theories/numbers.v b/theories/numbers.v
index 5cda50af..8bc8ca50 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -187,6 +187,11 @@ Program Instance N_lt_dec (x y : N) : Decision (x < y)%N :=
   end.
 Next Obligation. congruence. Qed.
 Instance N_inhabited: Inhabited N := populate 1%N.
+Instance: PartialOrder (≤)%N.
+Proof.
+  repeat split; red. apply N.le_refl. apply N.le_trans. apply N.le_antisymm.
+Qed.
+Hint Extern 0 (_ ≤ _)%N => reflexivity.
 
 (** * Notations and properties of [Z] *)
 Open Scope Z_scope.
@@ -210,6 +215,10 @@ Instance Z_eq_dec: ∀ x y : Z, Decision (x = y) := Z.eq_dec.
 Instance Z_le_dec: ∀ x y : Z, Decision (x ≤ y) := Z_le_dec.
 Instance Z_lt_dec: ∀ x y : Z, Decision (x < y) := Z_lt_dec.
 Instance Z_inhabited: Inhabited Z := populate 1.
+Instance: PartialOrder (≤).
+Proof.
+  repeat split; red. apply Z.le_refl. apply Z.le_trans. apply Z.le_antisymm.
+Qed.
 
 Lemma Z_pow_pred_r n m : 0 < m → n * n ^ (Z.pred m) = n ^ m.
 Proof.
@@ -362,7 +371,7 @@ Proof. apply Z_to_option_nat_Some_alt. auto using Nat2Z.is_nonneg. Qed.
 
 (** The function [Z_of_sumbool] converts a sumbool [P] into an integer
 by yielding one if [P] and zero if [Q]. *)
-Definition Z_of_sumbool {P Q : Prop} (p : {P} + {Q}) : Z :=
+Definition Z_of_sumbool {P Q : Prop} (p : {P} + {Q} ) : Z :=
   (if p then 1 else 0)%Z.
 
 (** Some correspondence lemmas between [nat] and [N] that are not part of the
diff --git a/theories/orders.v b/theories/orders.v
index 7c7790de..c2592bc8 100644
--- a/theories/orders.v
+++ b/theories/orders.v
@@ -2,11 +2,311 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects common properties of pre-orders and semi lattices. This
 theory will mainly be used for the theory on collections and finite maps. *)
+Require Export Sorted.
 Require Export base decidable tactics list.
 
-(** * Pre-orders *)
-(** We extend a pre-order to a partial order by defining equality as
-[λ X Y, X ⊆ Y ∧ Y ⊆ X]. We prove that this indeed gives rise to a setoid. *)
+(** * Arbitrary pre-, parial and total orders *)
+(** Properties about arbitrary pre-, partial, and total orders. We do not use
+the relation [⊆] because we often have multiple orders on the same structure *)
+Section orders.
+  Context {A} {R : relation A}.
+  Implicit Types X Y : A.
+
+  Infix "⊆" := R.
+  Notation "X ⊈ Y" := (¬X ⊆ Y).
+  Infix "⊂" := (strict R).
+
+  Lemma reflexive_eq `{!Reflexive R} X Y : X = Y → X ⊆ Y.
+  Proof. by intros <-. Qed.
+  Lemma anti_symmetric_iff `{!PartialOrder R} X Y : X = Y ↔ R X Y ∧ R Y X.
+  Proof. intuition (subst; auto). Qed.
+
+  Lemma strict_spec X Y : X ⊂ Y ↔ X ⊆ Y ∧ Y ⊈ X.
+  Proof. done. Qed.
+  Lemma strict_include X Y : X ⊂ Y → X ⊆ Y.
+  Proof. by intros [? _]. Qed.
+  Lemma strict_ne X Y : X ⊂ Y → X ≠ Y.
+  Proof. by intros [??] <-. Qed.
+  Lemma strict_ne_sym X Y : X ⊂ Y → Y ≠ X.
+  Proof. by intros [??] <-. Qed.
+  Lemma strict_transitive_l `{!Transitive R} X Y Z : X ⊂ Y → Y ⊆ Z → X ⊂ Z.
+  Proof.
+    intros [? HXY] ?. split.
+    * by transitivity Y.
+    * contradict HXY. by transitivity Z.
+  Qed.
+  Lemma strict_transitive_r `{!Transitive R} X Y Z : X ⊆ Y → Y ⊂ Z → X ⊂ Z.
+  Proof.
+    intros ? [? HYZ]. split.
+    * by transitivity Y.
+    * contradict HYZ. by transitivity X.
+  Qed.
+
+  Global Instance: Irreflexive (strict R).
+  Proof. firstorder. Qed.
+  Global Instance: Transitive R → StrictOrder (strict R).
+  Proof.
+    split; try apply _.
+    eauto using strict_transitive_r, strict_include.
+  Qed.
+
+  Global Instance preorder_subset_dec_slow `{∀ X Y, Decision (X ⊆ Y)}
+    (X Y : A) : Decision (X ⊂ Y) | 100 := _.
+
+  Lemma strict_spec_alt `{!PartialOrder R} X Y : X ⊂ Y ↔ X ⊆ Y ∧ X ≠ Y.
+  Proof.
+    split.
+    * intros [? HYX]. split. done. by intros <-.
+    * intros [? HXY]. split. done. by contradict HXY; apply (anti_symmetric R).
+  Qed.
+  Lemma po_eq_dec `{!PartialOrder R} `{∀ X Y, Decision (X ⊆ Y)} (X Y : A) :
+    Decision (X = Y).
+  Proof.
+    refine (cast_if_and (decide (X ⊆ Y)) (decide (Y ⊆ X)));
+     abstract (rewrite anti_symmetric_iff; tauto).
+  Defined.
+
+  Lemma total_not `{!Total R} X Y : X ⊈ Y → Y ⊆ X.
+  Proof. intros. destruct (total R X Y); tauto. Qed.
+  Lemma total_not_strict `{!Total R} X Y : X ⊈ Y → Y ⊂ X.
+  Proof. red; auto using total_not. Qed.
+
+  Global Instance trichotomyT_dec `{!TrichotomyT R} `{!Reflexive R} X Y :
+      Decision (X ⊆ Y) :=
+    match trichotomyT R X Y with
+    | inleft (left H) => left (proj1 H)
+    | inleft (right H) => left (reflexive_eq _ _ H)
+    | inright H => right (proj2 H)
+    end.
+  Global Instance trichotomyT_trichotomy `{!TrichotomyT R} : Trichotomy R.
+  Proof. intros X Y. destruct (trichotomyT R X Y) as [[|]|]; tauto. Qed.
+  Global Instance trichotomy_total `{!Trichotomy R} `{!Reflexive R} : Total R.
+  Proof.
+    intros X Y. destruct (trichotomy R X Y) as [[??]|[<-|[??]]]; intuition.
+  Qed.
+End orders.
+
+Ltac simplify_order := repeat
+  match goal with
+  | _ => progress simplify_equality
+  | H : strict _ ?x ?x |- _ => by destruct (irreflexivity _ _ H)
+  | H1 : ?R ?x ?y |- _ =>
+    match goal with
+    | H2 : R y x |- _ =>
+      assert (x = y) by (by apply (anti_symmetric R)); clear H1 H2
+    | H2 : R y ?z |- _ =>
+      unless (R x z) by done;
+      assert (R x z) by (by transitivity y)
+    end
+  end.
+
+(** * Sorting *)
+(** Merge sort. Adapted from the implementation of Hugo Herbelin in the Coq
+standard library, but without using the module system. *)
+Section merge_sort.
+  Context  {A} (R : relation A) `{∀ x y, Decision (R x y)}.
+
+  Fixpoint list_merge (l1 : list A) : list A → list A :=
+    fix list_merge_aux l2 :=
+    match l1, l2 with
+    | [], _ => l2
+    | _, [] => l1
+    | x1 :: l1, x2 :: l2 =>
+       if decide_rel R x1 x2 then x1 :: list_merge l1 (x2 :: l2)
+       else x2 :: list_merge_aux l2
+    end.
+  Global Arguments list_merge !_ !_ /.
+
+  Local Notation stack := (list (option (list A))).
+  Fixpoint merge_list_to_stack (st : stack) (l : list A) : stack :=
+    match st with
+    | [] => [Some l]
+    | None :: st => Some l :: st
+    | Some l' :: st => None :: merge_list_to_stack st (list_merge l' l)
+    end.
+  Fixpoint merge_stack (st : stack) : list A :=
+    match st with
+    | [] => []
+    | None :: st => merge_stack st
+    | Some l :: st => list_merge l (merge_stack st)
+    end.
+  Fixpoint merge_sort_aux (st : stack) (l : list A) : list A :=
+    match l with
+    | [] => merge_stack st
+    | x :: l => merge_sort_aux (merge_list_to_stack st [x]) l
+    end.
+  Definition merge_sort : list A → list A := merge_sort_aux [].
+End merge_sort.
+
+(** ** Properties of the [Sorted] and [StronglySorted] predicate *)
+Section sorted.
+  Context {A} (R : relation A).
+
+  Lemma Sorted_StronglySorted `{!Transitive R} l :
+    Sorted R l → StronglySorted R l.
+  Proof. by apply Sorted.Sorted_StronglySorted. Qed.
+  Lemma StronglySorted_unique `{!AntiSymmetric (=) R} l1 l2 :
+    StronglySorted R l1 → StronglySorted R l2 → l1 ≡ₚ l2 → l1 = l2.
+  Proof.
+    intros Hl1; revert l2. induction Hl1 as [|x1 l1 ? IH Hx1]; intros l2 Hl2 E.
+    { symmetry. by apply Permutation_nil. }
+    destruct Hl2 as [|x2 l2 ? Hx2].
+    { by apply Permutation_nil in E. }
+    assert (x1 = x2); subst.
+    { rewrite Forall_forall in Hx1, Hx2.
+      assert (x2 ∈ x1 :: l1) as Hx2' by (by rewrite E; left).
+      assert (x1 ∈ x2 :: l2) as Hx1' by (by rewrite <-E; left).
+      inversion Hx1'; inversion Hx2'; simplify_equality; auto. }
+    f_equal. by apply IH, (injective (x2 ::)).
+  Qed.
+  Lemma Sorted_unique `{!Transitive R} `{!AntiSymmetric (=) R} l1 l2 :
+    Sorted R l1 → Sorted R l2 → l1 ≡ₚ l2 → l1 = l2.
+  Proof. auto using StronglySorted_unique, Sorted_StronglySorted. Qed.
+
+  Global Instance HdRel_dec x `{∀ y, Decision (R x y)} l :
+    Decision (HdRel R x l).
+  Proof.
+   refine
+    match l with
+    | [] => left _
+    | y :: l => cast_if (decide (R x y))
+    end; abstract first [by constructor | by inversion 1].
+  Defined.
+
+  Global Instance Sorted_dec `{∀ x y, Decision (R x y)} : ∀ l,
+    Decision (Sorted R l).
+  Proof.
+   refine
+    (fix go l :=
+    match l return Decision (Sorted R l) with
+    | [] => left _
+    | x :: l => cast_if_and (decide (HdRel R x l)) (go l)
+    end); clear go; abstract first [by constructor | by inversion 1].
+  Defined.
+  Global Instance StronglySorted_dec `{∀ x y, Decision (R x y)} : ∀ l,
+    Decision (StronglySorted R l).
+  Proof.
+   refine
+    (fix go l :=
+    match l return Decision (StronglySorted R l) with
+    | [] => left _
+    | x :: l => cast_if_and (decide (Forall (R x) l)) (go l)
+    end); clear go; abstract first [by constructor | by inversion 1].
+  Defined.
+
+  Context {B} (f : A → B).
+  Lemma HdRel_fmap (R1 : relation A) (R2 : relation B) x l :
+    (∀ y, R1 x y → R2 (f x) (f y)) → HdRel R1 x l → HdRel R2 (f x) (f <$> l).
+  Proof. destruct 2; constructor; auto. Qed.
+  Lemma Sorted_fmap (R1 : relation A) (R2 : relation B) l :
+    (∀ x y, R1 x y → R2 (f x) (f y)) → Sorted R1 l → Sorted R2 (f <$> l).
+  Proof. induction 2; simpl; constructor; eauto using HdRel_fmap. Qed.
+  Lemma StronglySorted_fmap (R1 : relation A) (R2 : relation B) l :
+    (∀ x y, R1 x y → R2 (f x) (f y)) →
+    StronglySorted R1 l → StronglySorted R2 (f <$> l).
+  Proof.
+    induction 2; simpl; constructor;
+      rewrite ?Forall_fmap; eauto using Forall_impl.
+  Qed.
+End sorted.
+
+(** ** Correctness of merge sort *)
+Section merge_sort_correct.
+  Context  {A} (R : relation A) `{∀ x y, Decision (R x y)} `{!Total R}.
+
+  Lemma list_merge_cons x1 x2 l1 l2 :
+    list_merge R (x1 :: l1) (x2 :: l2) =
+      if decide (R x1 x2) then x1 :: list_merge R l1 (x2 :: l2)
+      else x2 :: list_merge R (x1 :: l1) l2.
+  Proof. done. Qed.
+
+  Lemma HdRel_list_merge x l1 l2 :
+    HdRel R x l1 → HdRel R x l2 → HdRel R x (list_merge R l1 l2).
+  Proof.
+    destruct 1 as [|x1 l1 IH1], 1 as [|x2 l2 IH2];
+      rewrite ?list_merge_cons; simpl; repeat case_decide; auto.
+  Qed.
+  Lemma Sorted_list_merge l1 l2 :
+    Sorted R l1 → Sorted R l2 → Sorted R (list_merge R l1 l2).
+  Proof.
+    intros Hl1. revert l2. induction Hl1 as [|x1 l1 IH1];
+      induction 1 as [|x2 l2 IH2]; rewrite ?list_merge_cons; simpl;
+      repeat case_decide;
+      constructor; eauto using HdRel_list_merge, HdRel_cons, total_not.
+  Qed.
+  Lemma merge_Permutation l1 l2 : list_merge R l1 l2 ≡ₚ l1 ++ l2.
+  Proof.
+    revert l2. induction l1 as [|x1 l1 IH1]; intros l2;
+      induction l2 as [|x2 l2 IH2]; rewrite ?list_merge_cons; simpl;
+      repeat case_decide; auto.
+    * by rewrite (right_id_L [] (++)).
+    * by rewrite IH2, Permutation_middle.
+  Qed.
+
+  Local Notation stack := (list (option (list A))).
+  Inductive merge_stack_Sorted : stack → Prop :=
+    | merge_stack_Sorted_nil : merge_stack_Sorted []
+    | merge_stack_Sorted_cons_None st :
+       merge_stack_Sorted st → merge_stack_Sorted (None :: st)
+    | merge_stack_Sorted_cons_Some l st :
+       Sorted R l → merge_stack_Sorted st → merge_stack_Sorted (Some l :: st).
+  Fixpoint merge_stack_flatten (st : stack) : list A :=
+    match st with
+    | [] => []
+    | None :: st => merge_stack_flatten st
+    | Some l :: st => l ++ merge_stack_flatten st
+    end.
+
+  Lemma Sorted_merge_list_to_stack st l :
+    merge_stack_Sorted st → Sorted R l →
+    merge_stack_Sorted (merge_list_to_stack R st l).
+  Proof.
+    intros Hst. revert l.
+    induction Hst; repeat constructor; naive_solver auto using Sorted_list_merge.
+  Qed.
+  Lemma merge_list_to_stack_Permutation st l :
+    merge_stack_flatten (merge_list_to_stack R st l) ≡ₚ
+      l ++ merge_stack_flatten st.
+  Proof.
+    revert l. induction st as [|[l'|] st IH]; intros l; simpl; auto.
+    by rewrite IH, merge_Permutation, (associative_L _), (commutative (++) l).
+  Qed.
+  Lemma Sorted_merge_stack st :
+    merge_stack_Sorted st → Sorted R (merge_stack R st).
+  Proof. induction 1; simpl; auto using Sorted_list_merge. Qed.
+  Lemma merge_stack_Permutation st : merge_stack R st ≡ₚ merge_stack_flatten st.
+  Proof.
+    induction st as [|[] ? IH]; intros; simpl; auto.
+    by rewrite merge_Permutation, IH.
+  Qed.
+  Lemma Sorted_merge_sort_aux st l :
+    merge_stack_Sorted st → Sorted R (merge_sort_aux R st l).
+  Proof.
+    revert st. induction l; simpl;
+      auto using Sorted_merge_stack, Sorted_merge_list_to_stack.
+  Qed.
+  Lemma merge_sort_aux_Permutation st l :
+    merge_sort_aux R st l ≡ₚ merge_stack_flatten st ++ l.
+  Proof.
+    revert st. induction l as [|?? IH]; simpl; intros.
+    * by rewrite (right_id_L [] (++)), merge_stack_Permutation.
+    * rewrite IH, merge_list_to_stack_Permutation; simpl.
+      by rewrite Permutation_middle.
+  Qed.
+
+  Lemma Sorted_merge_sort l : Sorted R (merge_sort R l).
+  Proof. apply Sorted_merge_sort_aux. by constructor. Qed.
+  Lemma merge_sort_Permutation l : merge_sort R l ≡ₚ l.
+  Proof. unfold merge_sort. by rewrite merge_sort_aux_Permutation. Qed.
+  Lemma StronglySorted_merge_sort `{!Transitive R} l :
+    StronglySorted R (merge_sort R l).
+  Proof. auto using Sorted_StronglySorted, Sorted_merge_sort. Qed.
+End merge_sort_correct.
+
+(** * Canonical pre and partial orders *)
+(** We extend the canonical pre-order [⊆] to a partial order by defining setoid
+equality as [λ X Y, X ⊆ Y ∧ Y ⊆ X]. We prove that this indeed gives rise to a
+setoid. *)
 Section preorder.
   Context `{SubsetEq A} `{!PreOrder (⊆)}.
 
@@ -27,45 +327,18 @@ Section preorder.
     * transitivity y1. tauto. transitivity y2; tauto.
   Qed.
 
-  Global Instance preorder_subset: Subset A := λ X Y, X ⊆ Y ∧ Y ⊈ X.
-  Lemma subset_spec X Y : X ⊂ Y ↔ X ⊆ Y ∧ Y ⊈ X.
-  Proof. done. Qed.
-  Lemma subset_spec_alt X Y : X ⊂ Y ↔ X ⊆ Y ∧ X ≢ Y.
+  Lemma subset_spec X Y : X ⊂ Y ↔ X ⊆ Y ∧ X ≢ Y.
   Proof.
     split.
     * intros [? HYX]. split. done. contradict HYX. by rewrite HYX.
     * intros [? HXY]. split. done. by contradict HXY.
   Qed.
 
-  Lemma subset_subseteq X Y : X ⊂ Y → X ⊆ Y.
-  Proof. by intros [? _]. Qed.
-  Lemma subset_transitive_l X Y Z : X ⊂ Y → Y ⊆ Z → X ⊂ Z.
-  Proof.
-    intros [? HXY] ?. split.
-    * by transitivity Y.
-    * contradict HXY. by transitivity Z.
-  Qed.
-  Lemma subset_transitive_r X Y Z : X ⊆ Y → Y ⊂ Z → X ⊂ Z.
-  Proof.
-    intros ? [? HYZ]. split.
-    * by transitivity Y.
-    * contradict HYZ. by transitivity X.
-  Qed.
-
-  Global Instance: StrictOrder (⊂).
-  Proof.
-    split.
-    * firstorder.
-    * eauto using subset_transitive_r, subset_subseteq.
-  Qed.
-  Global Instance: Proper ((≡) ==> (≡) ==> iff) (⊂).
-  Proof. unfold subset, preorder_subset. solve_proper. Qed.
-
   Section leibniz.
     Context `{!LeibnizEquiv A}.
 
-    Lemma subset_spec_alt_L X Y : X ⊂ Y ↔ X ⊆ Y ∧ X ≠ Y.
-    Proof. unfold_leibniz. apply subset_spec_alt. Qed.
+    Lemma subset_spec_L X Y : X ⊂ Y ↔ X ⊆ Y ∧ X ≠ Y.
+    Proof. unfold_leibniz. apply subset_spec. Qed.
   End leibniz.
 
   Section dec.
@@ -73,13 +346,11 @@ Section preorder.
 
     Global Instance preorder_equiv_dec_slow (X Y : A) :
       Decision (X ≡ Y) | 100 := _.
-    Global Instance preorder_subset_dec_slow (X Y : A) :
-      Decision (X ⊂ Y) | 100 := _.
 
     Lemma subseteq_inv X Y : X ⊆ Y → X ⊂ Y ∨ X ≡ Y.
-    Proof. rewrite subset_spec_alt. destruct (decide (X ≡ Y)); tauto. Qed.
+    Proof. rewrite subset_spec. destruct (decide (X ≡ Y)); tauto. Qed.
     Lemma not_subset_inv X Y : X ⊄ Y → X ⊈ Y ∨ X ≡ Y.
-    Proof. rewrite subset_spec_alt. destruct (decide (X ≡ Y)); tauto. Qed.
+    Proof. rewrite subset_spec. destruct (decide (X ≡ Y)); tauto. Qed.
 
     Context `{!LeibnizEquiv A}.
 
@@ -91,7 +362,6 @@ Section preorder.
 End preorder.
 
 Typeclasses Opaque preorder_equiv.
-Typeclasses Opaque preorder_subset.
 Hint Extern 0 (@Equivalence _ (≡)) =>
   class_apply preorder_equivalence : typeclass_instances.
 
@@ -102,7 +372,7 @@ Section partialorder.
   Global Instance: LeibnizEquiv A.
   Proof.
     split.
-    * intros [??]. by apply (anti_symmetric _).
+    * intros [??]. by apply (anti_symmetric (⊆)).
     * intros. by subst.
   Qed.
 End partialorder.
@@ -337,7 +607,6 @@ Section lower_bounded_lattice.
   Qed.
   Global Instance: RightAbsorb (≡) ∅ (∩).
   Proof. intros ?. by rewrite (commutative _), (left_absorb _ _). Qed.
-
   Global Instance: LeftDistr (≡) (∪) (∩).
   Proof.
     intros x y z. split.
@@ -350,7 +619,6 @@ Section lower_bounded_lattice.
   Qed.
   Global Instance: RightDistr (≡) (∪) (∩).
   Proof. intros x y z. by rewrite !(commutative _ _ z), (left_distr _ _). Qed.
-
   Global Instance: LeftDistr (≡) (∩) (∪).
   Proof.
     intros x y z. split.
@@ -378,12 +646,10 @@ Section lower_bounded_lattice.
     Proof. intros ?. unfold_leibniz. apply (left_absorb _ _). Qed.
     Global Instance: RightAbsorb (=) ∅ (∩).
     Proof. intros ?. unfold_leibniz. apply (right_absorb _ _). Qed.
-
     Global Instance: LeftDistr (=) (∪) (∩).
     Proof. intros ???. unfold_leibniz. apply (left_distr _ _). Qed.
     Global Instance: RightDistr (=) (∪) (∩).
     Proof. intros ???. unfold_leibniz. apply (right_distr _ _). Qed.
-
     Global Instance: LeftDistr (=) (∩) (∪).
     Proof. intros ???. unfold_leibniz. apply (left_distr _ _). Qed.
     Global Instance: RightDistr (=) (∩) (∪).
diff --git a/theories/pmap.v b/theories/pmap.v
index f09b7ff9..6553162a 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -8,7 +8,7 @@ However, we extend Leroy's implementation by packing the trees into a Sigma
 type such that canonicity of representation is ensured. This is necesarry for
 Leibniz equality to become extensional. *)
 Require Import PArith mapset.
-Require Export prelude fin_maps.
+Require Export fin_maps.
 
 Local Open Scope positive_scope.
 Local Hint Extern 0 (@eq positive _ _) => congruence.
@@ -20,10 +20,10 @@ not ensure canonical representations of maps. For example the empty map can
 be represented as a binary tree of an arbitrary size that contains [None] at
 all nodes. *)
 Inductive Pmap_raw A :=
-  | Pleaf: Pmap_raw A
-  | Pnode: Pmap_raw A → option A → Pmap_raw A → Pmap_raw A.
-Arguments Pleaf {_}.
-Arguments Pnode {_} _ _ _.
+  | PLeaf: Pmap_raw A
+  | PNode: Pmap_raw A → option A → Pmap_raw A → Pmap_raw A.
+Arguments PLeaf {_}.
+Arguments PNode {_} _ _ _.
 
 Instance Pmap_raw_eq_dec `{∀ x y : A, Decision (x = y)} (x y : Pmap_raw A) :
   Decision (x = y).
@@ -31,38 +31,42 @@ Proof. solve_decision. Defined.
 
 (** The following decidable predicate describes non empty trees. *)
 Inductive Pmap_ne {A} : Pmap_raw A → Prop :=
-  | Pmap_ne_val l x r : Pmap_ne (Pnode l (Some x) r)
-  | Pmap_ne_l l r : Pmap_ne l → Pmap_ne (Pnode l None r)
-  | Pmap_ne_r l r : Pmap_ne r → Pmap_ne (Pnode l None r).
+  | Pmap_ne_val l x r : Pmap_ne (PNode l (Some x) r)
+  | Pmap_ne_l l r : Pmap_ne l → Pmap_ne (PNode l None r)
+  | Pmap_ne_r l r : Pmap_ne r → Pmap_ne (PNode l None r).
 Local Hint Constructors Pmap_ne.
 
-Instance Pmap_ne_dec `(t : Pmap_raw A) : Decision (Pmap_ne t).
+Instance Pmap_ne_dec {A} : ∀ t : Pmap_raw A, Decision (Pmap_ne t).
 Proof.
-  red. induction t as [|? IHl [?|] ? IHr].
-  * right. by inversion 1.
-  * intuition.
-  * destruct IHl, IHr; try (by left; auto); right; by inversion_clear 1.
-Qed.
+ refine (
+  fix go t :=
+  match t return Decision (Pmap_ne t) with
+  | PLeaf => right _
+  | PNode _ (Some x) _ => left _
+  | PNode l Node r => cast_if_or (go l) (go r)
+  end); clear go; abstract first [constructor (by auto)|by inversion 1].
+Defined.
 
 (** The following predicate describes well well formed trees. A tree is well
 formed if it is empty or if all nodes at the bottom contain a value. *)
 Inductive Pmap_wf {A} : Pmap_raw A → Prop :=
-  | Pmap_wf_leaf : Pmap_wf Pleaf
-  | Pmap_wf_node l x r : Pmap_wf l → Pmap_wf r → Pmap_wf (Pnode l (Some x) r)
+  | Pmap_wf_leaf : Pmap_wf PLeaf
+  | Pmap_wf_node l x r : Pmap_wf l → Pmap_wf r → Pmap_wf (PNode l (Some x) r)
   | Pmap_wf_empty l r :
-     Pmap_wf l → Pmap_wf r → (Pmap_ne l ∨ Pmap_ne r) → Pmap_wf (Pnode l None r).
+     Pmap_wf l → Pmap_wf r → (Pmap_ne l ∨ Pmap_ne r) → Pmap_wf (PNode l None r).
 Local Hint Constructors Pmap_wf.
 
-Instance Pmap_wf_dec `(t : Pmap_raw A) : Decision (Pmap_wf t).
+Instance Pmap_wf_dec {A} : ∀ t : Pmap_raw A, Decision (Pmap_wf t).
 Proof.
-  red. induction t as [|l IHl [?|] r IHr]; simpl.
-  * intuition.
-  * destruct IHl, IHr; try solve [left; intuition];
-      right; by inversion_clear 1.
-  * destruct IHl, IHr, (decide (Pmap_ne l)), (decide (Pmap_ne r));
-      try solve [left; intuition];
-      right; inversion_clear 1; intuition.
-Qed.
+ refine (
+  fix go t :=
+  match t return Decision (Pmap_wf t) with
+  | PLeaf => left _
+  | PNode l (Some x) r => cast_if_and (go l) (go r)
+  | PNode l Node r =>
+     cast_if_and3 (decide (Pmap_ne l ∨ Pmap_ne r)) (go l) (go r)
+  end); clear go; abstract first [constructor (by auto)|by inversion 1].
+Defined.
 
 (** Now we restrict the data type of trees to those that are well formed and
 thereby obtain a data type that ensures canonicity. *)
@@ -76,15 +80,15 @@ Global Instance Pmap_eq_dec `{∀ x y : A, Decision (x = y)} (t1 t2 : Pmap A) :
   | right H => right (H ∘ proj1 (dsig_eq _ t1 t2))
   end.
 
-Instance Pempty_raw {A} : Empty (Pmap_raw A) := Pleaf.
+Instance Pempty_raw {A} : Empty (Pmap_raw A) := PLeaf.
 Global Instance Pempty {A} : Empty (Pmap A) :=
   (∅ : Pmap_raw A) ↾ bool_decide_pack _ Pmap_wf_leaf.
 
 Instance Plookup_raw {A} : Lookup positive A (Pmap_raw A) :=
   fix Plookup_raw (i : positive) (t : Pmap_raw A) {struct t} : option A :=
   match t with
-  | Pleaf => None
-  | Pnode l o r =>
+  | PLeaf => None
+  | PNode l o r =>
      match i with
      | 1 => o
      | i~0 => @lookup _ _ _ Plookup_raw i l
@@ -93,7 +97,7 @@ Instance Plookup_raw {A} : Lookup positive A (Pmap_raw A) :=
   end.
 Instance Plookup {A} : Lookup positive A (Pmap A) := λ i t, `t !! i.
 
-Lemma Plookup_raw_empty {A} i : (∅ : Pmap_raw A) !! i = None.
+Lemma Plookup_empty {A} i : (∅ : Pmap_raw A) !! i = None.
 Proof. by destruct i. Qed.
 
 Lemma Pmap_ne_lookup `(t : Pmap_raw A) : Pmap_ne t → ∃ i x, t !! i = Some x.
@@ -137,65 +141,65 @@ Qed.
 
 Fixpoint Psingleton_raw {A} (i : positive) (x : A) : Pmap_raw A :=
   match i with
-  | 1 => Pnode Pleaf (Some x) Pleaf
-  | i~0 => Pnode (Psingleton_raw i x) None Pleaf
-  | i~1 => Pnode Pleaf None (Psingleton_raw i x)
+  | 1 => PNode PLeaf (Some x) PLeaf
+  | i~0 => PNode (Psingleton_raw i x) None PLeaf
+  | i~1 => PNode PLeaf None (Psingleton_raw i x)
   end.
 
-Lemma Psingleton_raw_ne {A} i (x : A) : Pmap_ne (Psingleton_raw i x).
+Lemma Psingleton_ne {A} i (x : A) : Pmap_ne (Psingleton_raw i x).
 Proof. induction i; simpl; intuition. Qed.
-Local Hint Resolve Psingleton_raw_ne.
-Lemma Psingleton_raw_wf {A} i (x : A) : Pmap_wf (Psingleton_raw i x).
+Local Hint Resolve Psingleton_ne.
+Lemma Psingleton_wf {A} i (x : A) : Pmap_wf (Psingleton_raw i x).
 Proof. induction i; simpl; intuition. Qed.
-Local Hint Resolve Psingleton_raw_wf.
+Local Hint Resolve Psingleton_wf.
 
-Lemma Plookup_raw_singleton {A} i (x : A) : Psingleton_raw i x !! i = Some x.
+Lemma Plookup_singleton {A} i (x : A) : Psingleton_raw i x !! i = Some x.
 Proof. by induction i. Qed.
-Lemma Plookup_raw_singleton_ne {A} i j (x : A) :
+Lemma Plookup_singleton_ne {A} i j (x : A) :
   i ≠ j → Psingleton_raw i x !! j = None.
 Proof. revert j. induction i; intros [?|?|]; simpl; auto. congruence. Qed.
 
-Definition Pnode_canon `(l : Pmap_raw A) (o : option A) (r : Pmap_raw A) :=
+Definition PNode_canon `(l : Pmap_raw A) (o : option A) (r : Pmap_raw A) :=
   match l, o, r with
-  | Pleaf, None, Pleaf => Pleaf
-  | _, _, _ => Pnode l o r
+  | PLeaf, None, PLeaf => PLeaf
+  | _, _, _ => PNode l o r
   end.
 
-Lemma Pnode_canon_wf `(l : Pmap_raw A) (o : option A) (r : Pmap_raw A) :
-  Pmap_wf l → Pmap_wf r → Pmap_wf (Pnode_canon l o r).
+Lemma PNode_canon_wf `(l : Pmap_raw A) (o : option A) (r : Pmap_raw A) :
+  Pmap_wf l → Pmap_wf r → Pmap_wf (PNode_canon l o r).
 Proof. intros H1 H2. destruct H1, o, H2; simpl; intuition. Qed.
-Local Hint Resolve Pnode_canon_wf.
+Local Hint Resolve PNode_canon_wf.
 
-Lemma Pnode_canon_lookup_xH `(l : Pmap_raw A) o (r : Pmap_raw A) :
-  Pnode_canon l o r !! 1 = o.
+Lemma PNode_canon_lookup_xH `(l : Pmap_raw A) o (r : Pmap_raw A) :
+  PNode_canon l o r !! 1 = o.
 Proof. by destruct l,o,r. Qed.
-Lemma Pnode_canon_lookup_xO `(l : Pmap_raw A) o (r : Pmap_raw A) i :
-  Pnode_canon l o r !! i~0 = l !! i.
+Lemma PNode_canon_lookup_xO `(l : Pmap_raw A) o (r : Pmap_raw A) i :
+  PNode_canon l o r !! i~0 = l !! i.
 Proof. by destruct l,o,r. Qed.
-Lemma Pnode_canon_lookup_xI `(l : Pmap_raw A) o (r : Pmap_raw A) i :
-  Pnode_canon l o r !! i~1 = r !! i.
+Lemma PNode_canon_lookup_xI `(l : Pmap_raw A) o (r : Pmap_raw A) i :
+  PNode_canon l o r !! i~1 = r !! i.
 Proof. by destruct l,o,r. Qed.
-Ltac Pnode_canon_rewrite := repeat (
-  rewrite Pnode_canon_lookup_xH || rewrite Pnode_canon_lookup_xO ||
-  rewrite Pnode_canon_lookup_xI).
+Ltac PNode_canon_rewrite := repeat (
+  rewrite PNode_canon_lookup_xH || rewrite PNode_canon_lookup_xO ||
+  rewrite PNode_canon_lookup_xI).
 
 Instance Ppartial_alter_raw {A} : PartialAlter positive A (Pmap_raw A) :=
   fix go f i t {struct t} : Pmap_raw A :=
   match t with
-  | Pleaf =>
+  | PLeaf =>
      match f None with
-     | None => Pleaf
+     | None => PLeaf
      | Some x => Psingleton_raw i x
      end
-  | Pnode l o r =>
+  | PNode l o r =>
      match i with
-     | 1 => Pnode_canon l (f o) r
-     | i~0 => Pnode_canon (@partial_alter _ _ _ go f i l) o r
-     | i~1 => Pnode_canon l o (@partial_alter _ _ _ go f i r)
+     | 1 => PNode_canon l (f o) r
+     | i~0 => PNode_canon (@partial_alter _ _ _ go f i l) o r
+     | i~1 => PNode_canon l o (@partial_alter _ _ _ go f i r)
      end
   end.
 
-Lemma Ppartial_alter_raw_wf {A} f i (t : Pmap_raw A) :
+Lemma Ppartial_alter_wf {A} f i (t : Pmap_raw A) :
   Pmap_wf t → Pmap_wf (partial_alter f i t).
 Proof.
   intros twf. revert i. induction twf.
@@ -205,67 +209,62 @@ Proof.
 Qed.
 
 Instance Ppartial_alter {A} : PartialAlter positive A (Pmap A) := λ f i t,
-  dexist (partial_alter f i (`t)) (Ppartial_alter_raw_wf f i _ (proj2_dsig t)).
+  dexist (partial_alter f i (`t)) (Ppartial_alter_wf f i _ (proj2_dsig t)).
 
-Lemma Plookup_raw_alter {A} f i (t : Pmap_raw A) :
+Lemma Plookup_alter {A} f i (t : Pmap_raw A) :
   partial_alter f i t !! i = f (t !! i).
 Proof.
   revert i. induction t.
   * intros i. change (
      match f None with
-     | Some x => Psingleton_raw i x
-     | None => Pleaf
+     | Some x => Psingleton_raw i x | None => PLeaf
      end !! i = f None). destruct (f None).
-    + intros. apply Plookup_raw_singleton.
+    + intros. apply Plookup_singleton.
     + by destruct i.
-  * intros [?|?|]; simpl; by Pnode_canon_rewrite.
+  * intros [?|?|]; simpl; by PNode_canon_rewrite.
 Qed.
-Lemma Plookup_raw_alter_ne {A} f i j (t : Pmap_raw A) :
+Lemma Plookup_alter_ne {A} f i j (t : Pmap_raw A) :
   i ≠ j → partial_alter f i t !! j = t !! j.
 Proof.
   revert i j. induction t as [|l IHl ? r IHr].
   * intros. change (
      match f None with
-     | Some x => Psingleton_raw i x
-     | None => Pleaf
+     | Some x => Psingleton_raw i x | None => PLeaf
      end !! j = None). destruct (f None).
-    + intros. by apply Plookup_raw_singleton_ne.
+    + intros. by apply Plookup_singleton_ne.
     + done.
-  * intros [?|?|] [?|?|]; simpl; Pnode_canon_rewrite; auto; congruence.
+  * intros [?|?|] [?|?|]; simpl; PNode_canon_rewrite; auto; congruence.
 Qed.
 
 Instance Pfmap_raw {A B} (f : A → B) : FMapD Pmap_raw f :=
   fix go (t : Pmap_raw A) : Pmap_raw B :=
   let _ : FMapD Pmap_raw f := @go in
   match t with
-  | Pleaf => Pleaf
-  | Pnode l x r => Pnode (f <$> l) (f <$> x) (f <$> r)
+  | PLeaf => PLeaf
+  | PNode l x r => PNode (f <$> l) (f <$> x) (f <$> r)
   end.
 
-Lemma Pfmap_raw_ne `(f : A → B) (t : Pmap_raw A) :
-  Pmap_ne t → Pmap_ne (fmap f t).
+Lemma Pfmap_ne `(f : A → B) (t : Pmap_raw A) : Pmap_ne t → Pmap_ne (fmap f t).
 Proof. induction 1; simpl; auto. Qed.
-Local Hint Resolve Pfmap_raw_ne.
-Lemma Pfmap_raw_wf `(f : A → B) (t : Pmap_raw A) :
-  Pmap_wf t → Pmap_wf (fmap f t).
+Local Hint Resolve Pfmap_ne.
+Lemma Pfmap_wf `(f : A → B) (t : Pmap_raw A) : Pmap_wf t → Pmap_wf (fmap f t).
 Proof. induction 1; simpl; intuition. Qed.
 
 Global Instance Pfmap {A B} (f : A → B) : FMapD Pmap f := λ t,
-  dexist _ (Pfmap_raw_wf f _ (proj2_dsig t)).
+  dexist _ (Pfmap_wf f _ (proj2_dsig t)).
 
-Lemma Plookup_raw_fmap `(f : A → B) (t : Pmap_raw A) i :
+Lemma Plookup_fmap {A B} (f : A → B) (t : Pmap_raw A) i :
   fmap f t !! i = fmap f (t !! i).
 Proof. revert i. induction t. done. by intros [?|?|]; simpl. Qed.
 
-Fixpoint Pto_list_raw {A} (j : positive) (t : Pmap_raw A) :
-    list (positive * A) :=
+Fixpoint Pto_list_raw {A} (j: positive) (t: Pmap_raw A) : list (positive * A) :=
   match t with
-  | Pleaf => []
-  | Pnode l o r => default [] o (λ x, [(Preverse j, x)]) ++ 
+  | PLeaf => []
+  | PNode l o r => default [] o (λ x, [(Preverse j, x)]) ++ 
      Pto_list_raw (j~0) l ++ Pto_list_raw (j~1) r
   end%list.
 
-Lemma Pelem_of_to_list_raw_aux {A} (t : Pmap_raw A) j i x :
+Lemma Pelem_of_to_list_aux {A} (t : Pmap_raw A) j i x :
   (i,x) ∈ Pto_list_raw j t ↔ ∃ i', i = i' ++ Preverse j ∧ t !! i' = Some x.
 Proof.
   split.
@@ -298,31 +297,29 @@ Proof.
         rewrite Preverse_xO, (associative_L _) in IHl. auto.
       - done.
 Qed.
-Lemma Pelem_of_to_list_raw {A} (t : Pmap_raw A) i x :
+Lemma Pelem_of_to_list {A} (t : Pmap_raw A) i x :
   (i,x) ∈ Pto_list_raw 1 t ↔ t !! i = Some x.
 Proof.
-  rewrite Pelem_of_to_list_raw_aux. split.
-  * by intros (i' &?&?); subst.
-  * intros. by exists i.
+  rewrite Pelem_of_to_list_aux. split. by intros (i'&->&?). intros. by exists i.
 Qed.
 
-Lemma Pto_list_raw_nodup {A} j (t : Pmap_raw A) : NoDup (Pto_list_raw j t).
+Lemma Pto_list_nodup {A} j (t : Pmap_raw A) : NoDup (Pto_list_raw j t).
 Proof.
   revert j. induction t as [|? IHl [?|] ? IHr]; simpl.
   * constructor.
   * intros. rewrite NoDup_cons, NoDup_app. split_ands; trivial.
-    + rewrite elem_of_app, !Pelem_of_to_list_raw_aux.
+    + rewrite elem_of_app, !Pelem_of_to_list_aux.
       intros [(i&Hi&?)|(i&Hi&?)].
       - rewrite Preverse_xO in Hi. apply (f_equal Plength) in Hi.
         rewrite !Papp_length in Hi. simpl in Hi. lia.
       - rewrite Preverse_xI in Hi. apply (f_equal Plength) in Hi.
         rewrite !Papp_length in Hi. simpl in Hi. lia.
-    + intros [??]. rewrite !Pelem_of_to_list_raw_aux.
+    + intros [??]. rewrite !Pelem_of_to_list_aux.
       intros (i1&?&?) (i2&Hi&?); subst.
       rewrite Preverse_xO, Preverse_xI, !(associative_L _) in Hi.
       by apply (injective (++ _)) in Hi.
   * intros. rewrite NoDup_app. split_ands; trivial.
-    intros [??]. rewrite !Pelem_of_to_list_raw_aux.
+    intros [??]. rewrite !Pelem_of_to_list_aux.
     intros (i1&?&?) (i2&Hi&?); subst.
     rewrite Preverse_xO, Preverse_xI, !(associative_L _) in Hi.
     by apply (injective (++ _)) in Hi.
@@ -333,8 +330,8 @@ Global Instance Pto_list {A} : FinMapToList positive A (Pmap A) :=
 
 Fixpoint Pmerge_aux `(f : option A → option B) (t : Pmap_raw A) : Pmap_raw B :=
   match t with
-  | Pleaf => Pleaf
-  | Pnode l o r => Pnode_canon (Pmerge_aux f l) (f o) (Pmerge_aux f r)
+  | PLeaf => PLeaf
+  | PNode l o r => PNode_canon (Pmerge_aux f l) (f o) (Pmerge_aux f r)
   end.
 
 Lemma Pmerge_aux_wf `(f : option A → option B) (t : Pmap_raw A) :
@@ -343,20 +340,19 @@ Proof. induction 1; simpl; auto. Qed.
 Local Hint Resolve Pmerge_aux_wf.
 
 Lemma Pmerge_aux_spec `(f : option A → option B) (Hf : f None = None)
-    (t : Pmap_raw A) i :
-  Pmerge_aux f t !! i = f (t !! i).
+  (t : Pmap_raw A) i : Pmerge_aux f t !! i = f (t !! i).
 Proof.
   revert i. induction t as [| l IHl o r IHr ]; [done |].
-  intros [?|?|]; simpl; Pnode_canon_rewrite; auto.
+  intros [?|?|]; simpl; PNode_canon_rewrite; auto.
 Qed.
 
 Global Instance Pmerge_raw : Merge Pmap_raw :=
   fix Pmerge_raw A B C f t1 t2 : Pmap_raw C :=
   match t1, t2 with
-  | Pleaf, t2 => Pmerge_aux (f None) t2
-  | t1, Pleaf => Pmerge_aux (flip f None) t1
-  | Pnode l1 o1 r1, Pnode l2 o2 r2 =>
-     Pnode_canon (@merge _ Pmerge_raw A B C f l1 l2)
+  | PLeaf, t2 => Pmerge_aux (f None) t2
+  | t1, PLeaf => Pmerge_aux (flip f None) t1
+  | PNode l1 o1 r1, PNode l2 o2 r2 =>
+     PNode_canon (@merge _ Pmerge_raw A B C f l1 l2)
       (f o1 o2) (@merge _ Pmerge_raw A B C f r1 r2)
   end.
 Local Arguments Pmerge_aux _ _ _ _ : simpl never.
@@ -365,10 +361,9 @@ Lemma Pmerge_wf {A B C} (f : option A → option B → option C) t1 t2 :
   Pmap_wf t1 → Pmap_wf t2 → Pmap_wf (merge f t1 t2).
 Proof. intros t1wf. revert t2. induction t1wf; destruct 1; simpl; auto. Qed.
 Global Instance Pmerge: Merge Pmap := λ A B C f t1 t2,
-  dexist (merge f (`t1) (`t2))
-    (Pmerge_wf _ _ _ (proj2_dsig t1) (proj2_dsig t2)).
+  dexist _ (Pmerge_wf f _ _ (proj2_dsig t1) (proj2_dsig t2)).
 
-Lemma Pmerge_raw_spec {A B C} (f : option A → option B → option C)
+Lemma Pmerge_spec {A B C} (f : option A → option B → option C)
     (Hf : f None None = None) (t1 : Pmap_raw A) t2 i :
   merge f t1 t2 !! i = f (t1 !! i) (t2 !! i).
 Proof.
@@ -376,7 +371,7 @@ Proof.
   * intros. unfold merge. simpl. by rewrite Pmerge_aux_spec.
   * destruct t2 as [| l2 o2 r2 ].
     + unfold merge, Pmerge_raw. intros. by rewrite Pmerge_aux_spec.
-    + intros [?|?|]; simpl; by Pnode_canon_rewrite.
+    + intros [?|?|]; simpl; by PNode_canon_rewrite.
 Qed.
 
 (** * Instantiation of the finite map interface *)
@@ -386,15 +381,16 @@ Proof.
   * intros ? [t1?] [t2?]. intros. apply dsig_eq. simpl.
     apply Pmap_wf_eq_get; trivial; by apply (bool_decide_unpack _).
   * by destruct i.
-  * intros ?? [??] ?. by apply Plookup_raw_alter.
-  * intros ?? [??] ??. by apply Plookup_raw_alter_ne.
-  * intros ??? [??]. by apply Plookup_raw_fmap.
-  * intros ? [??]. apply Pto_list_raw_nodup.
-  * intros ? [??]. apply Pelem_of_to_list_raw.
-  * intros ??? ?? [??] [??] ?. by apply Pmerge_raw_spec.
+  * intros ?? [??] ?. by apply Plookup_alter.
+  * intros ?? [??] ??. by apply Plookup_alter_ne.
+  * intros ??? [??]. by apply Plookup_fmap.
+  * intros ? [??]. apply Pto_list_nodup.
+  * intros ? [??]. apply Pelem_of_to_list.
+  * intros ??? ?? [??] [??] ?. by apply Pmerge_spec.
 Qed.
 
-(** Finally, we can construct sets of [positive]s satisfying extensional equality. *)
+(** * Finite sets *)
+(** We construct sets of [positives]s satisfying extensional equality. *)
 Notation Pset := (mapset Pmap).
 Instance Pmap_dom {A} : Dom (Pmap A) Pset := mapset_dom.
 Instance: FinMapDom positive Pmap Pset := mapset_dom_spec.
diff --git a/theories/prelude.v b/theories/prelude.v
index 46dcf9b1..a0e6f2bf 100644
--- a/theories/prelude.v
+++ b/theories/prelude.v
@@ -13,4 +13,5 @@ Require Export
   fin_collections
   listset
   fresh_numbers
-  list.
+  list
+  lexico.
-- 
GitLab