Various small changes.

* Define the standard strict order on pre orders.
* Prove that this strict order is well founded for finite sets and finite maps.
  We also provide some utilities to compute with well founded recursion.
* Improve the "simplify_option_equality" tactic to handle more cases.
* Axiomatize finiteness of finite maps by translation to lists, instead of by
  them having a finite domain.
* Prove many additional properties of finite maps.
* Add many functions and theorems on lists, including: permutations, resize,
  filter, ...

theories/ars.v

@@ -48,13 +48,15 @@ Hint Constructors rtc nsteps bsteps tc : ars.
 Section rtc.
   Context `{R : relation A}.
 
-  Global Instance: Reflexive (rtc R).
-  Proof rtc_refl R.
-  Global Instance rtc_trans: Transitive (rtc R).
-  Proof. red; induction 1; eauto with ars. Qed.
+  Instance rtc_preorder: PreOrder (rtc R).
+  Proof.
+    split.
+    * red. apply rtc_refl.
+    * red. induction 1; eauto with ars.
+  Qed.
   Lemma rtc_once x y : R x y → rtc R x y.
   Proof. eauto with ars. Qed.
-  Global Instance: subrelation R (rtc R).
+  Instance rtc_once_subrel: subrelation R (rtc R).
   Proof. exact @rtc_once. Qed.
   Lemma rtc_r x y z : rtc R x y → R y z → rtc R x z.
   Proof. intros. etransitivity; eauto with ars. Qed.
@@ -142,7 +144,7 @@ Section rtc.
   Proof. intros. etransitivity; eauto with ars. Qed.
   Lemma tc_rtc x y : tc R x y → rtc R x y.
   Proof. induction 1; eauto with ars. Qed.
-  Global Instance: subrelation (tc R) (rtc R).
+  Instance tc_once_subrel: subrelation (tc R) (rtc R).
   Proof. exact @tc_rtc. Qed.
 
   Lemma looping_red x : looping R x → red R x.
@@ -163,6 +165,14 @@ Section rtc.
   Qed.
 End rtc.
 
+(* Avoid too eager type class resolution *)
+Hint Extern 5 (subrelation _ (rtc _)) =>
+  eapply @rtc_once_subrel : typeclass_instances.
+Hint Extern 5 (subrelation _ (tc _)) =>
+  eapply @tc_once_subrel : typeclass_instances.
+Hint Extern 5 (PreOrder (rtc _)) =>
+  eapply @rtc_preorder : typeclass_instances.
+
 Hint Resolve
   rtc_once rtc_r
   tc_r
@@ -186,3 +196,35 @@ Section subrel.
   Global Instance tc_subrel: subrelation (tc R1) (tc R2).
   Proof. induction 1; [left|eright]; eauto; by apply Hsub. Qed.
 End subrel.
+
+Notation wf := well_founded.
+
+Section wf.
+  Context `{R : relation A}.
+
+  (** A trick by Thomas Braibant to compute with well-founded recursions:
+  it lazily adds [2^n] [Acc_intro] constructors in front of a well foundedness
+  proof, so that the actual proof is never reached in practise. *)
+  Fixpoint wf_guard (n : nat) (wfR : wf R) : wf R :=
+    match n with
+    | 0 => wfR
+    | S n => λ x, Acc_intro x (λ y _, wf_guard n (wf_guard n wfR) y)
+    end.
+
+  Lemma wf_projected `(R2 : relation B) (f : A → B) :
+    (∀ x y, R x y → R2 (f x) (f y)) →
+    wf R2 → wf R.
+  Proof.
+    intros Hf Hwf.
+    cut (∀ y, Acc R2 y → ∀ x, y = f x → Acc R x).
+    { intros aux x. apply (aux (f x)); auto. }
+    induction 1 as [y _ IH]. intros x ?. subst.
+    constructor. intros. apply (IH (f y)); auto.
+  Qed.
+End wf.
+
+(* Generally we do not want [wf_guard] to be expanded (neither by tactics,
+nor by conversion tests in the kernel), but in some cases we do need it for
+computation (that is, we cannot make it opaque). We use the [Strategy]
+command to make its expanding behavior less eager. *)
+Strategy 100 [wf_guard].

theories/base.v

@@ -12,9 +12,11 @@ Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid NArith.
 (** The following coercion allows us to use Booleans as propositions. *)
 Coercion Is_true : bool >-> Sortclass.
 
-(** Ensure that [simpl] unfolds [id] and [compose] when fully applied. *)
+(** Ensure that [simpl] unfolds [id], [compose], and [flip] when fully
+applied. *)
 Arguments id _ _/.
 Arguments compose _ _ _ _ _ _ /.
+Arguments flip _ _ _ _ _ _/.
 
 (** Change [True] and [False] into notations in order to enable overloading.
 We will use this in the file [assertions] to give [True] and [False] a
@@ -23,6 +25,9 @@ semantics. *)
 Notation "'True'" := True : type_scope.
 Notation "'False'" := False : type_scope.
 
+Notation curry := prod_curry.
+Notation uncurry := prod_uncurry.
+
 (** Throughout this development we use [C_scope] for all general purpose
 notations that do not belong to a more specific scope. *)
 Delimit Scope C_scope with C.
@@ -159,6 +164,17 @@ Notation "( ⊈ X )" := (λ Y, Y ⊈ X) (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.
+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.
+
 Class ElemOf A B := elem_of: A → B → Prop.
 Instance: Params (@elem_of) 3.
 Infix "∈" := elem_of (at level 70) : C_scope.
@@ -192,6 +208,10 @@ Proof. inversion_clear 1; auto. Qed.
 Instance generic_disjoint `{ElemOf A B} : Disjoint B | 100 :=
   λ X Y, ∀ x, x ∉ X ∨ x ∉ Y.
 
+Class Filter A B :=
+  filter: ∀ (P : A → Prop) `{∀ x, Decision (P x)}, B → B.
+(* Arguments filter {_ _ _} _ {_} !_ / : simpl nomatch. *)
+
 (** ** Monadic operations *)
 (** We define operational type classes for the monadic operations bind, join 
 and fmap. These type classes are defined in a non-standard way by taking the
@@ -230,9 +250,13 @@ Instance: Params (@fmap) 6.
 Arguments fmap {_ _ _} _ {_} !_ / : simpl nomatch.
 
 Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : C_scope.
+Notation "( m ≫=)" := (λ f, mbind f m) (only parsing) : C_scope.
+Notation "(≫= f )" := (mbind f) (only parsing) : C_scope.
+Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : C_scope.
+
 Notation "x ← y ; z" := (y ≫= (λ x : _, z))
   (at level 65, only parsing, next at level 35, right associativity) : C_scope.
-Infix "<$>" := fmap (at level 65, right associativity, only parsing) : C_scope.
+Infix "<$>" := fmap (at level 65, right associativity) : C_scope.
 
 Class MGuard (M : Type → Type) :=
   mguard: ∀ P {dec : Decision P} {A}, M A → M A.
@@ -243,7 +267,7 @@ Notation "'guard' P ; o" := (mguard P o)
 (** In this section we define operational type classes for the operations
 on maps. In the file [fin_maps] we will axiomatize finite maps.
 The function lookup [m !! k] should yield the element at key [k] in [m]. *)
-Class Lookup (K M A : Type) :=
+Class Lookup (K A M : Type) :=
   lookup: K → M → option A.
 Instance: Params (@lookup) 4.
 
@@ -255,7 +279,7 @@ Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch.
 
 (** The function insert [<[k:=a]>m] should update the element at key [k] with
 value [a] in [m]. *)
-Class Insert (K M A : Type) :=
+Class Insert (K A M : Type) :=
   insert: K → A → M → M.
 Instance: Params (@insert) 4.
 Notation "<[ k := a ]>" := (insert k a)
@@ -272,9 +296,9 @@ Arguments delete _ _ _ !_ !_ / : simpl nomatch.
 
 (** The function [alter f k m] should update the value at key [k] using the
 function [f], which is called with the original value. *)
-Class AlterD (K M A : Type) (f : A → A) :=
+Class AlterD (K A M : Type) (f : A → A) :=
   alter: K → M → M.
-Notation Alter K M A := (∀ (f : A → A), AlterD K M A f)%type.
+Notation Alter K A M := (∀ (f : A → A), AlterD K A M f)%type.
 Instance: Params (@alter) 5.
 Arguments alter {_ _ _} _ {_} !_ !_ / : simpl nomatch.
 
@@ -282,7 +306,7 @@ Arguments alter {_ _ _} _ {_} !_ !_ / : simpl nomatch.
 function [f], which is called with the original value at key [k] or [None]
 if [k] is not a member of [m]. The value at [k] should be deleted if [f] 
 yields [None]. *)
-Class PartialAlter (K M A : Type) :=
+Class PartialAlter (K A M : Type) :=
   partial_alter: (option A → option A) → K → M → M.
 Instance: Params (@partial_alter) 4.
 Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch.
@@ -297,39 +321,43 @@ Arguments dom _ _ _ _ _ _ _ !_ / : simpl nomatch.
 (** The function [merge f m1 m2] should merge the maps [m1] and [m2] by
 constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)]
 provided that [k] is a member of either [m1] or [m2].*)
-Class Merge (M : Type → Type) :=
-  merge: ∀ {A}, (option A → option A → option A) → M A → M A → M A.
+Class Merge (A M : Type) :=
+  merge: (option A → option A → option A) → M → M → M.
 Instance: Params (@merge) 3.
 Arguments merge _ _ _ _ !_ !_ / : simpl nomatch.
 
 (** We lift the insert and delete operation to lists of elements. *)
-Definition insert_list `{Insert K M A} (l : list (K * A)) (m : M) : M :=
+Definition insert_list `{Insert K A M} (l : list (K * A)) (m : M) : M :=
   fold_right (λ p, <[ fst p := snd p ]>) m l.
 Instance: Params (@insert_list) 4.
 Definition delete_list `{Delete K M} (l : list K) (m : M) : M :=
   fold_right delete m l.
 Instance: Params (@delete_list) 3.
 
-Definition insert_consecutive `{Insert nat M A}
+Definition insert_consecutive `{Insert nat A M}
     (i : nat) (l : list A) (m : M) : M :=
   fold_right (λ x f i, <[i:=x]>(f (S i))) (λ _, m) l i.
 Instance: Params (@insert_consecutive) 3.
 
-(** The function [union_with f m1 m2] should yield the union of [m1] and [m2]
-using the function [f] to combine values of members that are in both [m1] and
-[m2]. *)
-Class UnionWith (M : Type → Type) :=
-  union_with: ∀ {A}, (A → A → A) → M A → M A → M A.
+(** The function [union_with f m1 m2] is supposed to yield the union of [m1]
+and [m2] using the function [f] to combine values of members that are in
+both [m1] and [m2]. *)
+Class UnionWith (A M : Type) :=
+  union_with: (A → A → option A) → M → M → M.
 Instance: Params (@union_with) 3.
 
-(** Similarly for the intersection and difference. *)
-Class IntersectionWith (M : Type → Type) :=
-  intersection_with: ∀ {A}, (A → A → A) → M A → M A → M A.
+(** Similarly for intersection and difference. *)
+Class IntersectionWith (A M : Type) :=
+  intersection_with: (A → A → option A) → M → M → M.
 Instance: Params (@intersection_with) 3.
-Class DifferenceWith (M : Type → Type) :=
-  difference_with: ∀ {A}, (A → A → option A) → M A → M A → M A.
+Class DifferenceWith (A M : Type) :=
+  difference_with: (A → A → option A) → M → M → M.
 Instance: Params (@difference_with) 3.
 
+Definition intersection_with_list `{IntersectionWith A M}
+  (f : A → A → option A) : M → list M → M := fold_right (intersection_with f).
+Arguments intersection_with_list _ _ _ _ _ !_ /.
+
 (** ** Common properties *)
 (** These operational type classes allow us to refer to common mathematical
 properties in a generic way. For example, for injectivity of [(k ++)] it
@@ -350,6 +378,8 @@ Class LeftAbsorb {A} R (i : A) (f : A → A → A) :=
   left_absorb: ∀ x, R (f i x) i.
 Class RightAbsorb {A} R (i : A) (f : A → A → A) :=
   right_absorb: ∀ x, R (f x i) i.
+Class AntiSymmetric {A} (R : A → A → Prop) :=
+  anti_symmetric: ∀ x y, R x y → R y x → x = y.
 
 Arguments injective {_ _ _ _} _ {_} _ _ _.
 Arguments idempotent {_ _} _ {_} _.
@@ -359,6 +389,7 @@ Arguments right_id {_ _} _ _ {_} _.
 Arguments associative {_ _} _ {_} _ _ _.
 Arguments left_absorb {_ _} _ _ {_} _.
 Arguments right_absorb {_ _} _ _ {_} _.
+Arguments anti_symmetric {_} _ {_} _ _ _ _.
 
 (** The following lemmas are more specific versions of the projections of the
 above type classes. These lemmas allow us to enforce Coq not to use the setoid
@@ -391,6 +422,10 @@ Class BoundedPreOrder A `{Empty A} `{SubsetEq A} := {
   bounded_preorder :>> PreOrder (⊆);
   subseteq_empty x : ∅ ⊆ x
 }.
+Class PartialOrder A `{SubsetEq A} := {
+  po_preorder :>> PreOrder (⊆);
+  po_antisym :> AntiSymmetric (⊆)
+}.
 
 (** 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.
@@ -423,11 +458,13 @@ Class SimpleCollection A C `{ElemOf A C}
   elem_of_singleton (x y : A) : x ∈ {[ y ]} ↔ x = y;
   elem_of_union X Y (x : A) : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y
 }.
-Class Collection A C `{ElemOf A C} `{Empty C} `{Singleton A C} `{Union C}
-    `{Intersection C} `{Difference C} := {
+Class Collection A C `{ElemOf A C} `{Empty C} `{Singleton A C}
+    `{Union C} `{Intersection C} `{Difference C} `{IntersectionWith A C} := {
   collection_simple :>> SimpleCollection A C;
   elem_of_intersection X Y (x : A) : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y;
-  elem_of_difference X Y (x : A) : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y
+  elem_of_difference X Y (x : A) : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y;
+  elem_of_intersection_with (f : A → A → option A) X Y (x : A) :
+    x ∈ intersection_with f X Y ↔ ∃ x1 x2, x1 ∈ X ∧ x2 ∈ Y ∧ f x1 x2 = Some x
 }.
 
 (** We axiomative a finite collection as a collection whose elements can be
@@ -448,10 +485,12 @@ Inductive NoDup {A} : list A → Prop :=
 
 (** Decidability of equality of the carrier set is admissible, but we add it
 anyway so as to avoid cycles in type class search. *)
-Class FinCollection A C `{ElemOf A C} `{Empty C} `{Union C}
-    `{Intersection C} `{Difference C} `{Singleton A C}
-    `{Elements A C} `{∀ x y : A, Decision (x = y)} := {
+Class FinCollection A C `{ElemOf A C} `{Empty C} `{Singleton A C}
+    `{Union C} `{Intersection C} `{Difference C} `{IntersectionWith A C}
+    `{Filter A C} `{Elements A C} `{∀ x y : A, Decision (x = y)} := {
   fin_collection :>> Collection A C;
+  elem_of_filter X P `{∀ x, Decision (P x)} x :
+    x ∈ filter P X ↔ P x ∧ x ∈ X;
   elements_spec X x : x ∈ X ↔ x ∈ elements X;
   elements_nodup X : NoDup (elements X)
 }.
@@ -471,13 +510,13 @@ Class CollectionMonad M `{∀ A, ElemOf A (M A)}
     `{∀ A, Empty (M A)} `{∀ A, Singleton A (M A)} `{∀ A, Union (M A)}
     `{!MBind M} `{!MRet M} `{!FMap M} `{!MJoin M} := {
   collection_monad_simple A :> SimpleCollection A (M A);
-  elem_of_bind {A B} (f : A → M B) (x : B) (X : M A) :
+  elem_of_bind {A B} (f : A → M B) (X : M A) (x : B) :
     x ∈ X ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ X;
   elem_of_ret {A} (x y : A) :
     x ∈ mret y ↔ x = y;
-  elem_of_fmap {A B} (f : A → B) (x : B) (X : M A) :
+  elem_of_fmap {A B} (f : A → B) (X : M A) (x : B) :
     x ∈ f <$> X ↔ ∃ y, x = f y ∧ y ∈ X;
-  elem_of_join {A} (x : A) (X : M (M A)) :
+  elem_of_join {A} (X : M (M A)) (x : A) :
     x ∈ mjoin X ↔ ∃ Y, x ∈ Y ∧ Y ∈ X
 }.
 
@@ -520,6 +559,24 @@ Definition fst_map {A A' B} (f : A → A') (p : A * B) : A' * B :=
   (f (fst p), snd p).
 Definition snd_map {A B B'} (f : B → B') (p : A * B) : A * B' :=
   (fst p, f (snd p)).
+Arguments fst_map {_ _ _} _ !_ /.
+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.
+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.
+
 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).
 

theories/collections.v

@@ -39,7 +39,7 @@ Section simple_collection.
   Global Instance elem_of_proper: Proper ((=) ==> (≡) ==> iff) (∈) | 5.
   Proof. intros ???. subst. firstorder. Qed.
 
-  Lemma elem_of_union_list (x : A) (Xs : list C) :
+  Lemma elem_of_union_list (Xs : list C) (x : A) :
     x ∈ ⋃ Xs ↔ ∃ X, X ∈ Xs ∧ x ∈ X.
   Proof.
     split.
@@ -60,7 +60,7 @@ Section simple_collection.
   Lemma not_elem_of_union x X Y : x ∉ X ∪ Y ↔ x ∉ X ∧ x ∉ Y.
   Proof. rewrite elem_of_union. tauto. Qed.
 
-  Context `{∀ (X Y : C), Decision (X ⊆ Y)}.
+  Context `{∀ X Y : C, Decision (X ⊆ Y)}.
 
   Global Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100.
   Proof.
@@ -69,37 +69,6 @@ Section simple_collection.
   Defined.
 End simple_collection.
 
-Section collection.
-  Context `{Collection A C}.
-
-  Global Instance: LowerBoundedLattice C.
-  Proof. split. apply _. firstorder auto. Qed.
-
-  Lemma intersection_twice x : {[x]} ∩ {[x]} ≡ {[x]}.
-  Proof.
-    split; intros y; rewrite elem_of_intersection, !elem_of_singleton; tauto.
-  Qed.
-
-  Context `{∀ (X Y : C), Decision (X ⊆ Y)}.
-
-  Lemma not_elem_of_intersection x X Y : x ∉ X ∩ Y ↔ x ∉ X ∨ x ∉ Y.
-  Proof.
-    rewrite elem_of_intersection.
-    destruct (decide (x ∈ X)); tauto.
-  Qed.
-  Lemma not_elem_of_difference x X Y : x ∉ X ∖ Y ↔ x ∉ X ∨ x ∈ Y.
-  Proof.
-    rewrite elem_of_difference.
-    destruct (decide (x ∈ Y)); tauto.
-  Qed.
-  Lemma union_difference X Y : X ∪ Y ∖ X ≡ X ∪ Y.
-  Proof.
-    split; intros x; rewrite !elem_of_union, elem_of_difference.
-    * tauto.
-    * destruct (decide (x ∈ X)); tauto.
-  Qed.
-End collection.
-
 Ltac decompose_empty := repeat
   match goal with
   | H : _ ∪ _ ≡ ∅ |- _ => apply empty_union in H; destruct H
@@ -116,6 +85,7 @@ Ltac unfold_elem_of :=
   repeat_on_hyps (fun H =>
     repeat match type of H with
     | context [ _ ⊆ _ ] => setoid_rewrite elem_of_subseteq in H
+    | context [ _ ⊂ _ ] => setoid_rewrite subset_spec in H
     | context [ _ ≡ _ ] => setoid_rewrite elem_of_equiv_alt in H
     | context [ _ ∈ ∅ ] => setoid_rewrite elem_of_empty in H
     | context [ _ ∈ {[ _ ]} ] => setoid_rewrite elem_of_singleton in H
@@ -129,6 +99,7 @@ Ltac unfold_elem_of :=
     end);
   repeat match goal with
   | |- context [ _ ⊆ _ ] => setoid_rewrite elem_of_subseteq
+  | |- context [ _ ⊂ _ ] => setoid_rewrite subset_spec
   | |- context [ _ ≡ _ ] => setoid_rewrite elem_of_equiv_alt
   | |- context [ _ ∈ ∅ ] => setoid_rewrite elem_of_empty
   | |- context [ _ ∈ {[ _ ]} ] => setoid_rewrite elem_of_singleton
@@ -194,6 +165,79 @@ Tactic Notation "decompose_elem_of" hyp(H) :=
 Tactic Notation "decompose_elem_of" :=
   repeat_on_hyps (fun H => decompose_elem_of H).
 
+Section collection.
+  Context `{Collection A C}.
+
+  Global Instance: LowerBoundedLattice C.
+  Proof. split. apply _. firstorder auto. Qed.
+
+  Lemma intersection_singletons x : {[x]} ∩ {[x]} ≡ {[x]}.
+  Proof. esolve_elem_of. Qed.
+  Lemma difference_twice X Y : (X ∖ Y) ∖ Y ≡ X ∖ Y.
+  Proof. esolve_elem_of. Qed.
+
+  Lemma empty_difference X Y : X ⊆ Y → X ∖ Y ≡ ∅.
+  Proof. esolve_elem_of. Qed.
+  Lemma difference_diag X : X ∖ X ≡ ∅.
+  Proof. esolve_elem_of. Qed.
+  Lemma difference_union_distr_l X Y Z : (X ∪ Y) ∖ Z ≡ X ∖ Z ∪ Y ∖ Z.
+  Proof. esolve_elem_of. Qed.
+  Lemma difference_intersection_distr_l X Y Z : (X ∩ Y) ∖ Z ≡ X ∖ Z ∩ Y ∖ Z.
+  Proof. esolve_elem_of. Qed.
+
+  Lemma elem_of_intersection_with_list (f : A → A → option A) Xs Y x :
+    x ∈ intersection_with_list f Y Xs ↔ ∃ xs y,
+      Forall2 (∈) xs Xs ∧ y ∈ Y ∧ foldr (λ x, (≫= f x)) (Some y) xs = Some x.
+  Proof.
+    split.
+    * revert x. induction Xs; simpl; intros x HXs.
+      + eexists [], x. intuition.
+      + rewrite elem_of_intersection_with in HXs.
+        destruct HXs as (x1 & x2 & Hx1 & Hx2 & ?).
+        destruct (IHXs x2) as (xs & y & hy & ? & ?); trivial.
+        eexists (x1 :: xs), y. intuition (simplify_option_equality; auto).
+    * intros (xs & y & Hxs & ? & Hx). revert x Hx.
+      induction Hxs; intros; simplify_option_equality; [done |].
+      rewrite elem_of_intersection_with. naive_solver.
+  Qed.
+
+  Lemma intersection_with_list_ind (P Q : A → Prop) f Xs Y :
+    (∀ y, y ∈ Y → P y) →
+    Forall (λ X, ∀ x, x ∈ X → Q x) Xs →
+    (∀ x y z, Q x → P y → f x y = Some z → P z) →
+    ∀ x, x ∈ intersection_with_list f Y Xs → P x.
+  Proof.
+    intros HY HXs Hf.
+    induction Xs; simplify_option_equality; [done |].
+    intros x Hx. rewrite elem_of_intersection_with in Hx.
+    decompose_Forall. destruct Hx as (? & ? & ? & ? & ?). eauto.
+  Qed.
+
+  Context `{∀ X Y : C, Decision (X ⊆ Y)}.
+
+  Lemma not_elem_of_intersection x X Y : x ∉ X ∩ Y ↔ x ∉ X ∨ x ∉ Y.
+  Proof.
+    rewrite elem_of_intersection.
+    destruct (decide (x ∈ X)); tauto.
+  Qed.
+  Lemma not_elem_of_difference x X Y : x ∉ X ∖ Y ↔ x ∉ X ∨ x ∈ Y.
+  Proof.
+    rewrite elem_of_difference.
+    destruct (decide (x ∈ Y)); tauto.
+  Qed.
+  Lemma union_difference X Y : X ⊆ Y → Y ≡ X ∪ Y ∖ X.
+  Proof.
+    split; intros x; rewrite !elem_of_union, elem_of_difference.
+    * destruct (decide (x ∈ X)); intuition.
+    * intuition.
+  Qed.
+  Lemma non_empty_difference X Y : X ⊂ Y → Y ∖ X ≢ ∅.
+  Proof.
+    intros [HXY1 HXY2] Hdiff. destruct HXY2. intros x.
+    destruct (decide (x ∈ X)); esolve_elem_of.
+  Qed.
+End collection.
+
 (** * Sets without duplicates up to an equivalence *)
 Section no_dup.
   Context `{SimpleCollection A B} (R : relation A) `{!Equivalence R}.
@@ -202,7 +246,7 @@ Section no_dup.
   Definition no_dup (X : B) := ∀ x y, x ∈ X → y ∈ X → R x y → x = y.
 
   Global Instance: Proper ((≡) ==> iff) (elem_of_upto x).
-  Proof. firstorder. Qed.
+  Proof. intros ??? E. unfold elem_of_upto. by setoid_rewrite E. Qed.
   Global Instance: Proper (R ==> (≡) ==> iff) elem_of_upto.
   Proof.
     intros ?? E1 ?? E2. split; intros [z [??]]; exists z.
@@ -390,10 +434,13 @@ Section collection_monad.
     l ∈ mapM f k →
     Forall (λ x, ∀ y, y ∈ f x → P y) k →
     Forall P l.
-  Proof. rewrite elem_of_mapM. apply Forall2_Forall_1. Qed.
-
-  Lemma mapM_non_empty {A B} (f : A → M B) l :
-    Forall (λ x, ∃ y, y ∈ f x) l →
-    ∃ k, k ∈ mapM f l.
-  Proof. induction 1; esolve_elem_of. Qed.
+  Proof. rewrite elem_of_mapM. apply Forall2_Forall_l. Qed.
+  Lemma elem_of_mapM_Forall2_l {A B C} (f : A → M B) (P : B → C → Prop) l1 l2 k :
+    l1 ∈ mapM f k →
+    Forall2 (λ x y, ∀ z, z ∈ f x → P z y) k l2 →
+    Forall2 P l1 l2.
+  Proof.
+    rewrite elem_of_mapM. intros Hl1. revert l2.
+    induction Hl1; inversion_clear 1; constructor; auto.
+  Qed.
 End collection_monad.

theories/decidable.v

@@ -5,6 +5,8 @@ with a decidable equality. Such propositions are collected by the [Decision]
 type class. *)
 Require Export base tactics.
 
+Hint Extern 200 (Decision _) => progress (lazy beta) : typeclass_instances.
+
 Lemma dec_stable `{Decision P} : ¬¬P → P.
 Proof. firstorder. Qed.
 
@@ -82,6 +84,8 @@ combination with the [refine] tactic. *)
 Notation cast_if S := (if S then left _ else right _).
 Notation cast_if_and S1 S2 := (if S1 then cast_if S2 else right _).
 Notation cast_if_and3 S1 S2 S3 := (if S1 then cast_if_and S2 S3 else right _).
+Notation cast_if_and4 S1 S2 S3 S4 :=
+  (if S1 then cast_if_and3 S2 S3 S4 else right _).
 Notation cast_if_or S1 S2 := (if S1 then left _ else cast_if S2).
 Notation cast_if_not S := (if S then right _ else left _).
 
@@ -104,14 +108,24 @@ Section prop_dec.
 End prop_dec.
 
 (** Instances of [Decision] for common data types. *)
+Instance bool_eq_dec (x y : bool) : Decision (x = y).
+Proof. solve_decision. Defined.
 Instance unit_eq_dec (x y : unit) : Decision (x = y).
 Proof. refine (left _); by destruct x, y. Defined.
 Instance prod_eq_dec `(A_dec : ∀ x y : A, Decision (x = y))
-    `(B_dec : ∀ x y : B, Decision (x = y)) (x y : A * B) : Decision (x = y).
+  `(B_dec : ∀ x y : B, Decision (x = y)) (x y : A * B) : Decision (x = y).
 Proof.
   refine (cast_if_and (A_dec (fst x) (fst y)) (B_dec (snd x) (snd y)));
     abstract (destruct x, y; simpl in *; congruence).
 Defined.
 Instance sum_eq_dec `(A_dec : ∀ x y : A, Decision (x = y))
-    `(B_dec : ∀ x y : B, Decision (x = y)) (x y : A + B) : Decision (x = y).
+  `(B_dec : ∀ x y : B, Decision (x = y)) (x y : A + B) : Decision (x = y).
 Proof. solve_decision. Defined.
+
+Instance curry_dec `(P_dec : ∀ (x : A) (y : B), Decision (P x y)) p :
+    Decision (curry P p) :=
+  match p as p return Decision (curry P p) with
+  | (x,y) => P_dec x y
+  end.
+Instance uncurry_dec `(P_dec : ∀ (p : A * B), Decision (P p)) x y :
+  Decision (uncurry P x y) := P_dec (x,y).

theories/fin_collections.v

@@ -3,7 +3,7 @@
 (** This file collects definitions and theorems on finite collections. Most
 importantly, it implements a fold and size function and some useful induction
 principles on finite collections . *)
-Require Import Permutation.
+Require Import Permutation ars.
 Require Export collections numbers listset.
 
 Instance collection_size `{Elements A C} : Size C := length ∘ elements.
@@ -37,6 +37,8 @@ Proof.
 Qed.
 Lemma size_empty_iff (X : C) : size X = 0 ↔ X ≡ ∅.
 Proof. split. apply size_empty_inv. intros E. by rewrite E, size_empty. Qed.
+Lemma size_non_empty_iff (X : C) : size X ≠ 0 ↔ X ≢ ∅.
+Proof. by rewrite size_empty_iff. Qed.
 
 Lemma size_singleton (x : A) : size {[ x ]} = 1.
 Proof.
@@ -123,54 +125,38 @@ Qed.
 
 Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X).
 Proof.
-  rewrite <-size_union. by rewrite union_difference. solve_elem_of.
-Qed.
-Lemma size_add X x : x ∉ X → size ({[ x ]} ∪ X) = S (size X).
-Proof.
-  intros. rewrite size_union. by rewrite size_singleton. solve_elem_of.
-Qed.
-
-Lemma size_difference X Y : X ⊆ Y → size X + size (Y ∖ X) = size Y.
-Proof. intros. by rewrite <-size_union_alt, subseteq_union_1. Qed.
-Lemma size_remove X x : x ∈ X → S (size (X ∖ {[ x ]})) = size X.
-Proof.
-  intros. rewrite <-(size_difference {[ x ]} X).
-  * rewrite size_singleton. auto with arith.
-  * solve_elem_of.
+  rewrite <-size_union by solve_elem_of.
+  setoid_replace (Y ∖ X) with ((Y ∪ X) ∖ X) by esolve_elem_of.
+  rewrite <-union_difference, (commutative (∪)); solve_elem_of.
 Qed.
 
 Lemma subseteq_size X Y : X ⊆ Y → size X ≤ size Y.
 Proof.
-  intros. rewrite <-(subseteq_union_1 X Y) by done.
-  rewrite <-(union_difference X Y), size_union by solve_elem_of.
-  auto with arith.
+  intros. rewrite (union_difference X Y), size_union_alt by done. lia.
 Qed.
-
-Lemma collection_wf_ind (P : C → Prop) :
-  (∀ X, (∀ Y, size Y < size X → P Y) → P X) →
-  ∀ X, P X.
+Lemma subset_size X Y : X ⊂ Y → size X < size Y.
 Proof.
-  intros Hind. cut (∀ n X, size X < n → P X).
-  { intros help X. apply help with (S (size X)). auto with arith. }
-  induction n; intros.
-  * by destruct (Lt.lt_n_0 (size X)).
-  * apply Hind. intros. apply IHn. eauto with arith.
+  intros. rewrite (union_difference X Y) by solve_elem_of.
+  rewrite size_union_alt, difference_twice.
+  cut (size (Y ∖ X) ≠ 0); [lia |].
+  by apply size_non_empty_iff, non_empty_difference.
 Qed.
 
+Lemma collection_wf : wf (@subset C _).
+Proof. apply well_founded_lt_compat with size, subset_size. Qed.
+
 Lemma collection_ind (P : C → Prop) :
   Proper ((≡) ==> iff) P →
   P ∅ →
   (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) →
   ∀ X, P X.
 Proof.
-  intros ? Hemp Hadd. apply collection_wf_ind.
-  intros X IH. destruct (Compare_dec.zerop (size X)).
-  * by rewrite size_empty_inv.
-  * destruct (size_pos_choose X); auto.
-    rewrite <-(subseteq_union_1 {[ x ]} X) by solve_elem_of.
-    rewrite <-union_difference.
-    apply Hadd; [solve_elem_of |]. apply IH.
-    rewrite <-(size_remove X x); auto with arith.
+  intros ? Hemp Hadd. apply well_founded_induction with (⊂).
+  { apply collection_wf. }
+  intros X IH. destruct (elem_of_or_empty X) as [[x ?]|HX].
+  * rewrite (union_difference {[ x ]} X) by solve_elem_of.
+    apply Hadd. solve_elem_of. apply IH. esolve_elem_of.
+  * by rewrite HX.
 Qed.
 
 Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
@@ -182,16 +168,12 @@ Proof.
   intros ? Hemp Hadd.
   cut (∀ l, NoDup l → ∀ X, (∀ x, x ∈ X ↔ x ∈ l) → P (foldr f b l) X).
   { intros help ?. apply help. apply elements_nodup. apply elements_spec. }
-  induction 1 as [|x l ?? IHl].
+  induction 1 as [|x l ?? IH]; simpl.
   * intros X HX. setoid_rewrite elem_of_nil in HX.
-    rewrite equiv_empty; firstorder.
+    rewrite equiv_empty. done. esolve_elem_of.
   * intros X HX. setoid_rewrite elem_of_cons in HX.
-    rewrite <-(subseteq_union_1 {[ x ]} X) by esolve_elem_of.
-    rewrite <-union_difference.
-    apply Hadd. solve_elem_of. apply IHl.
-    intros y. split.
-    + intros. destruct (proj1 (HX y)); solve_elem_of.
-    + esolve_elem_of.
+    rewrite (union_difference {[ x ]} X) by esolve_elem_of.
+    apply Hadd. solve_elem_of. apply IH. esolve_elem_of.
 Qed.
 
 Lemma collection_fold_proper {B} (R : relation B)

theories/listset.v

@@ -20,29 +20,44 @@ Instance listset_empty: Empty (listset A) :=
 Instance listset_singleton: Singleton A (listset A) := λ x,
   Listset [x].
 Instance listset_union: Union (listset A) := λ l k,
-  Listset (listset_car l ++ listset_car k).
+  match l, k with
+  | Listset l', Listset k' => Listset (l' ++ k')
+  end.
 
 Global Instance: SimpleCollection A (listset A).
 Proof.
   split.
   * by apply not_elem_of_nil.
   * by apply elem_of_list_singleton.
-  * intros. apply elem_of_app.
+  * intros [?] [?]. apply elem_of_app.
 Qed.
 
 Context `{∀ x y : A, Decision (x = y)}.
 
 Instance listset_intersection: Intersection (listset A) := λ l k,
-  Listset (list_intersection (listset_car l) (listset_car k)).
+  match l, k with
+  | Listset l', Listset k' => Listset (list_intersection l' k')
+  end.
 Instance listset_difference: Difference (listset A) := λ l k,
-  Listset (list_difference (listset_car l) (listset_car k)).
+  match l, k with
+  | Listset l', Listset k' => Listset (list_difference l' k')
+  end.
+Instance listset_intersection_with: IntersectionWith A (listset A) := λ f l k,
+  match l, k with
+  | Listset l', Listset k' => Listset (list_intersection_with f l' k')
+  end.
+Instance listset_filter: Filter A (listset A) := λ P _ l,
+  match l with
+  | Listset l' => Listset (filter P l')
+  end.
 
 Global Instance: Collection A (listset A).
 Proof.
   split.
   * apply _.
-  * intros. apply elem_of_list_intersection.
-  * intros. apply elem_of_list_difference.
+  * intros [?] [?]. apply elem_of_list_intersection.
+  * intros [?] [?]. apply elem_of_list_difference.
+  * intros ? [?] [?]. apply elem_of_list_intersection_with.
 Qed.
 
 Instance listset_elems: Elements A (listset A) :=
@@ -52,6 +67,7 @@ Global Instance: FinCollection A (listset A).
 Proof.
   split.
   * apply _.
+  * intros [?] ??. apply elem_of_list_filter.
   * symmetry. apply elem_of_remove_dups.
   * intros. apply remove_dups_nodup.
 Qed.
@@ -69,27 +85,35 @@ Hint Extern 1 (Union (listset _)) =>
   eapply @listset_union : typeclass_instances.
 Hint Extern 1 (Intersection (listset _)) =>
   eapply @listset_intersection : typeclass_instances.
+Hint Extern 1 (IntersectionWith _ (listset _)) =>
+  eapply @listset_intersection_with : typeclass_instances.
 Hint Extern 1 (Difference (listset _)) =>
   eapply @listset_difference : typeclass_instances.
 Hint Extern 1 (Elements _ (listset _)) =>
   eapply @listset_elems : typeclass_instances.
+Hint Extern 1 (Filter _ (listset _)) =>
+  eapply @listset_filter : typeclass_instances.
 
 Instance listset_ret: MRet listset := λ A x,
   {[ x ]}.
 Instance listset_fmap: FMap listset := λ A B f l,
-  Listset (f <$> listset_car l).
+  match l with
+  | Listset l' => Listset (f <$> l')
+  end.
 Instance listset_bind: MBind listset := λ A B f l,
-  Listset (mbind (listset_car ∘ f) (listset_car l)).
+  match l with
+  | Listset l' => Listset (mbind (listset_car ∘ f) l')
+  end.
 Instance listset_join: MJoin listset := λ A, mbind id.
 
 Instance: CollectionMonad listset.
 Proof.
   split.
   * intros. apply _.
-  * intros. apply elem_of_list_bind.
+  * intros ??? [?] ?. apply elem_of_list_bind.
   * intros. apply elem_of_list_ret.
-  * intros. apply elem_of_list_fmap.
-  * intros ?? [l].
+  * intros ??? [?]. apply elem_of_list_fmap.
+  * intros ? [?] ?.
     unfold mjoin, listset_join, elem_of, listset_elem_of.
     simpl. by rewrite elem_of_list_bind.
 Qed.

theories/listset_nodup.v

+(* Copyright (c) 2012, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** This file implements finite as unordered lists without duplicates.
+Although this implementation is slow, it is very useful as decidable equality
+is the only constraint on the carrier set. *)
+Require Export base decidable collections list.
+
+Record listset_nodup A := ListsetNoDup {
+  listset_nodup_car : list A;
+  listset_nodup_prf : NoDup listset_nodup_car
+}.
+Arguments ListsetNoDup {_} _ _.
+Arguments listset_nodup_car {_} _.
+Arguments listset_nodup_prf {_} _.
+
+Section list_collection.
+Context {A : Type} `{∀ x y : A, Decision (x = y)}.
+
+Notation C := (listset_nodup A).
+Notation LS := ListsetNoDup.
+
+Instance listset_nodup_elem_of: ElemOf A C := λ x l,
+  x ∈ listset_nodup_car l.
+Instance listset_nodup_empty: Empty C :=
+  LS [] (@NoDup_nil_2 _).
+Instance listset_nodup_singleton: Singleton A C := λ x,
+  LS [x] (NoDup_singleton x).
+Instance listset_nodup_difference: Difference C := λ l k,
+  LS _ (list_difference_nodup _ (listset_nodup_car k) (listset_nodup_prf l)).
+
+Definition listset_nodup_union_raw (l k : list A) : list A :=
+  list_difference l k ++ k.
+Lemma elem_of_listset_nodup_union_raw l k x :
+  x ∈ listset_nodup_union_raw l k ↔ x ∈ l ∨ x ∈ k.
+Proof.
+  unfold listset_nodup_union_raw.
+  rewrite elem_of_app, elem_of_list_difference.
+  intuition. case (decide (x ∈ k)); intuition.
+Qed.
+Lemma listset_nodup_union_raw_nodup l k :
+  NoDup l → NoDup k → NoDup (listset_nodup_union_raw l k).
+Proof.
+  intros. apply NoDup_app. repeat split.
+  * by apply list_difference_nodup.
+  * intro. rewrite elem_of_list_difference. intuition.
+  * done.
+Qed.
+Instance listset_nodup_union: Union C := λ l k,
+  LS _ (listset_nodup_union_raw_nodup _ _
+     (listset_nodup_prf l) (listset_nodup_prf k)).
+Instance listset_nodup_intersection: Intersection C := λ l k,
+  LS _ (list_intersection_nodup _
+     (listset_nodup_car k) (listset_nodup_prf l)).
+Instance listset_nodup_intersection_with:
+    IntersectionWith A C := λ f l k,
+  LS (remove_dups
+      (list_intersection_with f (listset_nodup_car l) (listset_nodup_car k)))
+    (remove_dups_nodup _).
+Instance listset_nodup_filter: Filter A C :=
+  λ P _ l, LS _ (filter_nodup P _ (listset_nodup_prf l)).
+
+Global Instance: Collection A C.
+Proof.
+  split; [split | | |].
+  * by apply not_elem_of_nil.
+  * by apply elem_of_list_singleton.
+  * intros. apply elem_of_listset_nodup_union_raw.
+  * intros. apply elem_of_list_intersection.
+  * intros. apply elem_of_list_difference.
+  * intros. unfold intersection_with, listset_nodup_intersection_with,
+      elem_of, listset_nodup_elem_of. simpl.
+    rewrite elem_of_remove_dups.
+    by apply elem_of_list_intersection_with.
+Qed.
+
+Global Instance listset_nodup_elems: Elements A C := listset_nodup_car.
+
+Global Instance: FinCollection A C.
+Proof.
+  split.
+  * apply _.
+  * intros. apply elem_of_list_filter.
+  * done.
+  * by intros [??].
+Qed.
+End list_collection.
+
+Hint Extern 1 (ElemOf _ (listset_nodup _)) =>
+  eapply @listset_nodup_elem_of : typeclass_instances.
+Hint Extern 1 (Empty (listset_nodup _)) =>
+  eapply @listset_nodup_empty : typeclass_instances.
+Hint Extern 1 (Singleton _ (listset_nodup _)) =>
+  eapply @listset_nodup_singleton : typeclass_instances.
+Hint Extern 1 (Union (listset_nodup _)) =>
+  eapply @listset_nodup_union : typeclass_instances.
+Hint Extern 1 (Intersection (listset_nodup _)) =>
+  eapply @listset_nodup_intersection : typeclass_instances.
+Hint Extern 1 (Difference (listset_nodup _)) =>
+  eapply @listset_nodup_difference : typeclass_instances.
+Hint Extern 1 (Elements _ (listset_nodup _)) =>
+  eapply @listset_nodup_elems : typeclass_instances.
+Hint Extern 1 (Filter _ (listset_nodup _)) =>
+  eapply @listset_nodup_filter : typeclass_instances.

theories/nmap.v

@@ -17,21 +17,22 @@ Instance Pmap_dec `{∀ x y : A, Decision (x = y)} :
 Proof. solve_decision. Defined.
 
 Instance Nempty {A} : Empty (Nmap A) := NMap None ∅.
-Instance Nlookup {A} : Lookup N (Nmap A) A := λ i t,
+Instance Nlookup {A} : Lookup N A (Nmap A) := λ i t,
   match i with
   | N0 => Nmap_0 t
   | Npos p => Nmap_pos t !! p
   end.
-Instance Npartial_alter {A} : PartialAlter N (Nmap A) A := λ f i t,
+Instance Npartial_alter {A} : PartialAlter N A (Nmap A) := λ f i t,
   match i, t with
   | N0, NMap o t => NMap (f o) t
   | Npos p, NMap o t => NMap o (partial_alter f p t)
   end.
-Instance Ndom {A} : Dom N (Nmap A) := λ C _ _ _ t,
+Instance Nto_list {A} : FinMapToList N A (Nmap A) := λ t,
   match t with
-  | NMap o t => option_case (λ _, {[ 0 ]}) ∅ o ∪ (Pdom_raw Npos (`t))
+  | NMap o t => option_case (λ x, [(0,x)]) [] o ++
+     (fst_map Npos <$> finmap_to_list t)
   end.
-Instance Nmerge: Merge Nmap := λ A f t1 t2,
+Instance Nmerge {A} : Merge A (Nmap A) := λ f t1 t2,
   match t1, t2 with
   | NMap o1 t1, NMap o2 t2 => NMap (f o1 o2) (merge f t1 t2)
   end.
@@ -53,9 +54,26 @@ Proof.
   * intros ? f [? t] [|i] [|j]; simpl; try intuition congruence.
     intros. apply lookup_partial_alter_ne. congruence.
   * intros ??? [??] []; simpl. done. apply lookup_fmap.
-  * intros ?? ??????? [o t] n; simpl.
-    rewrite elem_of_union, Plookup_raw_dom.
-    destruct o, n; esolve_elem_of (inv_is_Some; eauto).
+  * intros ? [[x|] t]; unfold finmap_to_list; simpl.
+    + constructor.
+      - rewrite elem_of_list_fmap. by intros [[??] [??]].
+      - rewrite (NoDup_fmap _). apply finmap_to_list_nodup.
+    + rewrite (NoDup_fmap _). apply finmap_to_list_nodup.
+  * intros ? t i x. unfold finmap_to_list. split.
+    + destruct t as [[y|] t]; simpl.
+      - rewrite elem_of_cons, elem_of_list_fmap.
+        intros [? | [[??] [??]]]; simplify_equality; simpl; [done |].
+        by apply elem_of_finmap_to_list.
+      - rewrite elem_of_list_fmap.
+        intros [[??] [??]]; simplify_equality; simpl.
+        by apply elem_of_finmap_to_list.
+    + destruct t as [[y|] t]; simpl.
+      - rewrite elem_of_cons, elem_of_list_fmap.
+        destruct i as [|i]; simpl; [intuition congruence |].
+        intros. right. exists (i, x). by rewrite elem_of_finmap_to_list.
+      - rewrite elem_of_list_fmap.
+        destruct i as [|i]; simpl; [done |].
+        intros. exists (i, x). by rewrite elem_of_finmap_to_list.
   * intros ? f ? [o1 t1] [o2 t2] [|?]; simpl.
     + done.
     + apply (merge_spec f t1 t2).

theories/numbers.v

@@ -31,10 +31,23 @@ Proof. auto with arith. Qed.
 Lemma lt_n_SSS n : n < S (S (S n)).
 Proof. auto with arith. Qed.
 
+Definition sum_list_with {A} (f : A → nat) : list A → nat :=
+  fix go l :=
+  match l with
+  | [] => 0
+  | x :: l => f x + go l
+  end.
+Notation sum_list := (sum_list_with id).
+
 Instance positive_eq_dec: ∀ x y : positive, Decision (x = y) := Pos.eq_dec.
 Notation "(~0)" := xO (only parsing) : positive_scope.
 Notation "(~1)" := xI (only parsing) : positive_scope.
 
+Instance: Injective (=) (=) xO.
+Proof. by injection 1. Qed.
+Instance: Injective (=) (=) xI.
+Proof. by injection 1. Qed.
+
 Infix "≤" := N.le : N_scope.
 Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%N : N_scope.
 Notation "x ≤ y < z" := (x ≤ y ∧ y < z)%N : N_scope.
@@ -46,6 +59,9 @@ Notation "(<)" := N.lt (only parsing) : N_scope.
 Infix "`div`" := N.div (at level 35) : N_scope.
 Infix "`mod`" := N.modulo (at level 35) : N_scope.
 
+Instance: Injective (=) (=) Npos.
+Proof. by injection 1. Qed.
+
 Instance N_eq_dec: ∀ x y : N, Decision (x = y) := N.eq_dec.
 Program Instance N_le_dec (x y : N) : Decision (x ≤ y)%N :=
   match Ncompare x y with

theories/option.v

@@ -22,9 +22,9 @@ Definition option_case {A B} (f : A → B) (b : B) (x : option A) : B :=
   | Some a => f a
   end.
 
-(** The [maybe] function allows us to get the value out of the option type
-by specifying a default value. *)
-Definition maybe {A} (a : A) (x : option A) : A :=
+(** The [from_option] function allows us to get the value out of the option
+type by specifying a default value. *)
+Definition from_option {A} (a : A) (x : option A) : A :=
   match x with
   | None => a
   | Some b => b
@@ -62,22 +62,31 @@ Ltac inv_is_Some := repeat
   | H : is_Some _ |- _ => inversion H; clear H; subst
   end.
 
-Definition is_Some_sigT `(x : option A) : is_Some x → { a | x = Some a } :=
+Definition is_Some_proj `{x : option A} : is_Some x → A :=
   match x with
+  | Some a => λ _, a
   | None => False_rect _ ∘ is_Some_None
-  | Some a => λ _, a ↾ eq_refl
   end.
-
+Definition Some_dec `(x : option A) : { a | x = Some a } + { x = None } :=
+  match x return { a | x = Some a } + { x = None } with
+  | Some a => inleft (a ↾ eq_refl _)
+  | None => inright eq_refl
+  end.
 Instance is_Some_dec `(x : option A) : Decision (is_Some x) :=
   match x with
   | Some x => left (make_is_Some x)
   | None => right is_Some_None
   end.
+Instance None_dec `(x : option A) : Decision (x = None) :=
+  match x with
+  | Some x => right (Some_ne_None x)
+  | None => left eq_refl
+  end.
 
 Lemma eq_None_not_Some `(x : option A) : x = None ↔ ¬is_Some x.
 Proof. split. by destruct 2. destruct x. by intros []. done. Qed.
 Lemma not_eq_None_Some `(x : option A) : x ≠ None ↔ is_Some x.
-Proof. rewrite eq_None_not_Some. intuition auto using dec_stable. Qed.
+Proof. rewrite eq_None_not_Some. split. apply dec_stable. tauto. Qed.
 
 Lemma make_eq_Some {A} (x : option A) a :
   is_Some x → (∀ b, x = Some b → b = a) → x = Some a.
@@ -90,17 +99,17 @@ Instance option_eq_dec `{dec : ∀ x y : A, Decision (x = y)}
   | Some a =>
     match y with
     | Some b =>
-      match dec a b with
-      | left H => left (f_equal _ H)
-      | right H => right (H ∘ injective Some _ _)
-      end
+       match dec a b with
+       | left H => left (f_equal _ H)
+       | right H => right (H ∘ injective Some _ _)
+       end
     | None => right (Some_ne_None _)
     end
   | None =>
-    match y with
-    | Some _ => right (None_ne_Some _)
-    | None => left eq_refl
-    end
+     match y with
+     | Some _ => right (None_ne_Some _)
+     | None => left eq_refl
+     end
   end.
 
 (** * Monadic operations *)
@@ -126,97 +135,132 @@ Lemma option_fmap_is_None {A B} (f : A → B) (x : option A) :
   x = None ↔ f <$> x = None.
 Proof. unfold fmap, option_fmap. by destruct x. Qed.
 
+Lemma option_bind_assoc {A B C} (f : A → option B)
+    (g : B → option C) (x : option A) : (x ≫= f) ≫= g = x ≫= (mbind g ∘ f).
+Proof. by destruct x; simpl. Qed.
+
 Tactic Notation "simplify_option_equality" "by" tactic3(tac) := repeat
   match goal with
   | _ => first [progress simpl in * | progress simplify_equality]
-  | H : mbind (M:=option) (A:=?A) ?f ?o = ?x |- _ =>
-    let x := fresh in evar (x:A);
-    let x' := eval unfold x in x in clear x;
+  | H : context [mbind (M:=option) (A:=?A) ?f ?o] |- _ =>
     let Hx := fresh in
-    assert (o = Some x') as Hx by tac;
+    first
+      [ let x := fresh in evar (x:A);
+        let x' := eval unfold x in x in clear x;
+        assert (o = Some x') as Hx by tac
+      | assert (o = None) as Hx by tac ];
     rewrite Hx in H; clear Hx
+  | H : context [fmap (M:=option) (A:=?A) ?f ?o] |- _ =>
+    let Hx := fresh in
+    first
+      [ let x := fresh in evar (x:A);
+        let x' := eval unfold x in x in clear x;
+        assert (o = Some x') as Hx by tac
+      | assert (o = None) as Hx by tac ];
+    rewrite Hx in H; clear Hx
+  | H : context [ match ?o with _ => _ end ] |- _ =>
+    match type of o with
+    | option ?A =>
+      let Hx := fresh in
+      first
+        [ let x := fresh in evar (x:A);
+          let x' := eval unfold x in x in clear x;
+          assert (o = Some x') as Hx by tac
+        | assert (o = None) as Hx by tac ];
+      rewrite Hx in H; clear Hx
+    end
   | H : mbind (M:=option) ?f ?o = ?x |- _ =>
     match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
     match x with Some _ => idtac | None => idtac | _ => fail 1 end;
     destruct o eqn:?
-  | |- mbind (M:=option) (A:=?A) ?f ?o = ?x =>
-    let x := fresh in evar (x:A);
-    let x' := eval unfold x in x in clear x;
+  | H : ?x = mbind (M:=option) ?f ?o |- _ =>
+    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
+    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
+    destruct o eqn:?
+  | H : fmap (M:=option) ?f ?o = ?x |- _ =>
+    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
+    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
+    destruct o eqn:?
+  | H : ?x = fmap (M:=option) ?f ?o |- _ =>
+    match o with Some _ => fail 1 | None => fail 1 | _ => idtac end;
+    match x with Some _ => idtac | None => idtac | _ => fail 1 end;
+    destruct o eqn:?
+  | |- context [mbind (M:=option) (A:=?A) ?f ?o] =>
     let Hx := fresh in
-    assert (o = Some x') as Hx by tac;
+    first
+      [ let x := fresh in evar (x:A);
+        let x' := eval unfold x in x in clear x;
+        assert (o = Some x') as Hx by tac
+      | assert (o = None) as Hx by tac ];
     rewrite Hx; clear Hx
+  | |- context [fmap (M:=option) (A:=?A) ?f ?o] =>
+    let Hx := fresh in
+    first
+      [ let x := fresh in evar (x:A);
+        let x' := eval unfold x in x in clear x;
+        assert (o = Some x') as Hx by tac
+      | assert (o = None) as Hx by tac ];
+    rewrite Hx; clear Hx
+  | |- context [ match ?o with _ => _ end ] =>
+    match type of o with
+    | option ?A =>
+      let Hx := fresh in
+      first
+        [ let x := fresh in evar (x:A);
+          let x' := eval unfold x in x in clear x;
+          assert (o = Some x') as Hx by tac
+        | assert (o = None) as Hx by tac ];
+      rewrite Hx; clear Hx
+    end
   | H : context C [@mguard option _ ?P ?dec _ ?x] |- _ =>
     let X := context C [ if dec then x else None ] in
     change X in H; destruct dec
   | |- context C [@mguard option _ ?P ?dec _ ?x] =>
     let X := context C [ if dec then x else None ] in
     change X; destruct dec
+  | H1 : ?o = Some ?x, H2 : ?o = Some ?y |- _ =>
+    assert (y = x) by congruence; clear H2
+  | H1 : ?o = Some ?x, H2 : ?o = None |- _ =>
+    congruence
   end.
-Tactic Notation "simplify_option_equality" := simplify_option_equality by eauto.
+Tactic Notation "simplify_option_equality" :=
+  simplify_option_equality by eauto.
+
+Hint Extern 100 => simplify_option_equality : simplify_option_equality.
 
 (** * Union, intersection and difference *)
-Instance option_union: UnionWith option := λ A f x y,
+Instance option_union_with {A} : UnionWith A (option A) := λ f x y,
   match x, y with
-  | Some a, Some b => Some (f a b)
+  | Some a, Some b => f a b
   | Some a, None => Some a
   | None, Some b => Some b
   | None, None => None
   end.
-Instance option_intersection: IntersectionWith option := λ A f x y,
+Instance option_intersection_with {A} :
+    IntersectionWith A (option A) := λ f x y,
   match x, y with
-  | Some a, Some b => Some (f a b)
+  | Some a, Some b => f a b
   | _, _ => None
   end.
-Instance option_difference: DifferenceWith option := λ A f x y,
+Instance option_difference_with {A} :
+    DifferenceWith A (option A) := λ f x y,
   match x, y with
   | Some a, Some b => f a b
   | Some a, None => Some a
   | None, _ => None
   end.
 
-Section option_union_intersection.
-  Context {A} (f : A → A → A).
+Section option_union_intersection_difference.
+  Context {A} (f : A → A → option A).
 
   Global Instance: LeftId (=) None (union_with f).
   Proof. by intros [?|]. Qed.
   Global Instance: RightId (=) None (union_with f).
   Proof. by intros [?|]. Qed.
   Global Instance: Commutative (=) f → Commutative (=) (union_with f).
-  Proof.
-    intros ? [?|] [?|]; compute; try reflexivity.
-    by rewrite (commutative f).
-  Qed.
-  Global Instance: Associative (=) f → Associative (=) (union_with f).
-  Proof.
-    intros ? [?|] [?|] [?|]; compute; try reflexivity.
-    by rewrite (associative f).
-  Qed.
-  Global Instance: Idempotent (=) f → Idempotent (=) (union_with f).
-  Proof.
-    intros ? [?|]; compute; try reflexivity.
-    by rewrite (idempotent f).
-  Qed.
-
+  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
   Global Instance: Commutative (=) f → Commutative (=) (intersection_with f).
-  Proof.
-    intros ? [?|] [?|]; compute; try reflexivity.
-    by rewrite (commutative f).
-  Qed.
-  Global Instance: Associative (=) f → Associative (=) (intersection_with f).
-  Proof.
-    intros ? [?|] [?|] [?|]; compute; try reflexivity.
-    by rewrite (associative f).
-  Qed.
-  Global Instance: Idempotent (=) f → Idempotent (=) (intersection_with f).
-  Proof.
-    intros ? [?|]; compute; try reflexivity.
-    by rewrite (idempotent f).
-  Qed.
-End option_union_intersection.
-
-Section option_difference.
-  Context {A} (f : A → A → option A).
-
+  Proof. by intros ? [?|] [?|]; compute; rewrite 1?(commutative f). Qed.
   Global Instance: RightId (=) None (difference_with f).
   Proof. by intros [?|]. Qed.
-End option_difference.
+End option_union_intersection_difference.

theories/orders.v

@@ -28,10 +28,48 @@ 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_subseteq X Y : X ⊂ Y → X ⊆ Y.
+  Proof. by intros [? _]. Qed.
+  Lemma subset_trans_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_trans_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_trans_r, subset_subseteq.
+  Qed.
+  Global Instance: Proper ((≡) ==> (≡) ==> iff) (⊂).
+  Proof. unfold subset, preorder_subset. solve_proper. Qed.
+
   Context `{∀ X Y : A, Decision (X ⊆ Y)}.
   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.
+    destruct (decide (Y ⊆ X)).
+    * by right.
+    * by left.
+  Qed.
 End preorder.
+
 Typeclasses Opaque preorder_equiv.
 Hint Extern 0 (@Equivalence _ (≡)) =>
   class_apply preorder_equivalence : typeclass_instances.

theories/pmap.v

@@ -79,18 +79,18 @@ 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 (Pmap_raw A) A :=
+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 =>
-    match i with
-    | 1 => o
-    | i~0 => @lookup _ _ _ Plookup_raw i l
-    | i~1 => @lookup _ _ _ Plookup_raw i r
-    end
+     match i with
+     | 1 => o
+     | i~0 => @lookup _ _ _ Plookup_raw i l
+     | i~1 => @lookup _ _ _ Plookup_raw i r
+     end
   end.
-Instance Plookup {A} : Lookup positive (Pmap A) A := λ i t, `t !! i.
+Instance Plookup {A} : Lookup positive A (Pmap A) := λ i t, `t !! i.
 
 Lemma Plookup_raw_empty {A} i : (∅ : Pmap_raw A) !! i = None.
 Proof. by destruct i. Qed.
@@ -179,20 +179,20 @@ Ltac Pnode_canon_rewrite := repeat (
   rewrite Pnode_canon_lookup_xO ||
   rewrite Pnode_canon_lookup_xI).
 
-Instance Ppartial_alter_raw {A} : PartialAlter positive (Pmap_raw A) A :=
+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 =>
-    match f None with
-    | None => Pleaf
-    | Some x => Psingleton_raw i x
-    end
+     match f None with
+     | None => Pleaf
+     | Some x => Psingleton_raw i x
+     end
   | 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)
-    end
+     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)
+     end
   end.
 
 Lemma Ppartial_alter_raw_wf {A} f i (t : Pmap_raw A) :
@@ -204,7 +204,7 @@ Proof.
   * intros [?|?|]; simpl; intuition.
 Qed.
 
-Instance Ppartial_alter {A} : PartialAlter positive (Pmap A) A := λ f i t,
+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)).
 
 Lemma Plookup_raw_alter {A} f i (t : Pmap_raw A) :
@@ -257,35 +257,63 @@ Lemma Plookup_raw_fmap `(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.
 
-(** The [dom] function is rather inefficient, but since we do not intend to
-use it for computation it does not really matter to us. *)
-Section dom.
-  Context `{Collection B D}.
-
-  Fixpoint Pdom_raw (f : positive → B) `(t : Pmap_raw A) : D :=
-    match t with
-    | Pleaf => ∅
-    | Pnode l o r =>
-       option_case (λ _, {[ f 1 ]}) ∅ o
-         ∪ Pdom_raw (f ∘ (~0)) l ∪ Pdom_raw (f ∘ (~1)) r
-    end.
-
-  Lemma Plookup_raw_dom f `(t : Pmap_raw A) x :
-    x ∈ Pdom_raw f t ↔ ∃ i, x = f i ∧ is_Some (t !! i).
-  Proof.
-    split.
-    * revert f. induction t as [|? IHl [?|] ? IHr]; esolve_elem_of.
-    * intros [i [? Hlookup]]; subst. revert f i Hlookup.
-      induction t as [|? IHl [?|] ? IHr]; intros f [?|?|];
-       solve_elem_of (first
-        [ by apply (IHl (f ∘ (~0)))
-        | by apply (IHr (f ∘ (~1)))
-        | inv_is_Some; eauto ]).
-  Qed.
-End dom.
-
-Global Instance Pdom {A} : Dom positive (Pmap A) := λ C _ _ _ t,
-  Pdom_raw id (`t).
+(** The [finmap_to_list] function is rather inefficient, but since we do not
+use it for computation at this moment, we do not care. *)
+Fixpoint Pto_list_raw {A} (t : Pmap_raw A) : list (positive * A) :=
+  match t with
+  | Pleaf => []
+  | Pnode l o r =>
+     option_case (λ x, [(1,x)]) [] o ++ 
+       (fst_map (~0) <$> Pto_list_raw l) ++ 
+       (fst_map (~1) <$> Pto_list_raw r)
+  end.
+
+Lemma Pto_list_raw_nodup {A} (t : Pmap_raw A) : NoDup (Pto_list_raw t).
+Proof.
+  induction t as [|? IHl [?|] ? IHr]; simpl.
+  * constructor.
+  * rewrite NoDup_cons, NoDup_app, !(NoDup_fmap _).
+    repeat split; trivial.
+    + rewrite elem_of_app, !elem_of_list_fmap.
+      intros [[[??] [??]] | [[??] [??]]]; simpl in *; simplify_equality.
+    + intro. rewrite !elem_of_list_fmap.
+      intros [[??] [??]] [[??] [??]]; simpl in *; simplify_equality.
+  * rewrite NoDup_app, !(NoDup_fmap _).
+    repeat split; trivial.
+    intro. rewrite !elem_of_list_fmap.
+    intros [[??] [??]] [[??] [??]]; simpl in *; simplify_equality.
+Qed.
+
+Lemma Pelem_of_to_list_raw {A} (t : Pmap_raw A) i x :
+  (i,x) ∈ Pto_list_raw t ↔ t !! i = Some x.
+Proof.
+  split.
+  * revert i. induction t as [|? IHl [?|] ? IHr]; intros i; simpl.
+    + by rewrite ?elem_of_nil.
+    + rewrite elem_of_cons, !elem_of_app, !elem_of_list_fmap.
+      intros [? | [[[??] [??]] | [[??] [??]]]]; naive_solver.
+    + rewrite !elem_of_app, !elem_of_list_fmap.
+      intros [[[??] [??]] | [[??] [??]]]; naive_solver.
+  * revert i. induction t as [|? IHl [?|] ? IHr]; simpl.
+    + done.
+    + intros i. rewrite elem_of_cons, elem_of_app.
+      destruct i as [i|i|]; simpl.
+      - right. right. rewrite elem_of_list_fmap.
+        exists (i,x); simpl; auto.
+      - right. left. rewrite elem_of_list_fmap.
+        exists (i,x); simpl; auto.
+      - left. congruence.
+    + intros i. rewrite elem_of_app.
+      destruct i as [i|i|]; simpl.
+      - right. rewrite elem_of_list_fmap.
+        exists (i,x); simpl; auto.
+      - left. rewrite elem_of_list_fmap.
+        exists (i,x); simpl; auto.
+      - done.
+Qed.
+
+Global Instance Pto_list {A} : FinMapToList positive A (Pmap A) :=
+  λ t, Pto_list_raw (`t).
 
 Fixpoint Pmerge_aux `(f : option A → option B) (t : Pmap_raw A) : Pmap_raw B :=
   match t with
@@ -306,21 +334,21 @@ Proof.
   intros [?|?|]; simpl; Pnode_canon_rewrite; auto.
 Qed.
 
-Global Instance Pmerge_raw: Merge Pmap_raw :=
-  fix Pmerge_raw A f (t1 t2 : Pmap_raw A) : Pmap_raw A :=
+Global Instance Pmerge_raw {A} : Merge A (Pmap_raw A) :=
+  fix Pmerge_raw f (t1 t2 : Pmap_raw A) : Pmap_raw A :=
   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 _ f l1 l2)
-      (f o1 o2) (@merge _ Pmerge_raw _ f r1 r2)
+     Pnode_canon (@merge _ _ Pmerge_raw f l1 l2)
+      (f o1 o2) (@merge _ _ Pmerge_raw f r1 r2)
   end.
 Local Arguments Pmerge_aux _ _ _ _ : simpl never.
 
 Lemma Pmerge_wf {A} f (t1 t2 : Pmap_raw A) :
   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 f t1 t2,
+Global Instance Pmerge {A} : Merge A (Pmap A) := λ f t1 t2,
   dexist (merge f (`t1) (`t2))
     (Pmerge_wf _ _ _ (proj2_dsig t1) (proj2_dsig t2)).
 
@@ -343,9 +371,7 @@ Proof.
   * intros ?? [??] ?. by apply Plookup_raw_alter.
   * intros ?? [??] ??. by apply Plookup_raw_alter_ne.
   * intros ??? [??]. by apply Plookup_raw_fmap.
-  * intros ????????? [??] i. unfold dom, Pdom.
-    rewrite Plookup_raw_dom. unfold id. split.
-    + intros [? [??]]. by subst.
-    + naive_solver.
+  * intros ? [??]. apply Pto_list_raw_nodup.
+  * intros ? [??]. apply Pelem_of_to_list_raw.
   * intros ??? [??] [??] ?. by apply Pmerge_raw_spec.
 Qed.

theories/prelude.v

@@ -8,9 +8,9 @@ Require Export
   option
   vector
   numbers
+  ars
   collections
   fin_collections
   listset
-  listset_nodup
   fresh_numbers
   list.

theories/tactics.v

@@ -36,6 +36,12 @@ Ltac done :=
 Tactic Notation "by" tactic(tac) :=
   tac; done.
 
+Ltac case_match :=
+  match goal with
+  | H : context [ match ?x with _ => _ end ] |- _ => destruct x eqn:?
+  | |- context [ match ?x with _ => _ end ] => destruct x eqn:?
+  end.
+
 (** The tactic [clear dependent H1 ... Hn] clears the hypotheses [Hi] and
 their dependencies. *)
 Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) :=
@@ -114,6 +120,8 @@ Ltac simplify_equality := repeat
   | H : ?x = _ |- _ => subst x
   | H : _ = ?x |- _ => subst x
   | H : _ = _ |- _ => discriminate H
+  | H : ?f _ = ?f _ |- _ => apply (injective f) in H
+    (* before [injection'] to circumvent bug #2939 in some situations *)
   | H : _ = _ |- _ => injection' H
   end.