From e82cda6cd47ca4a55fa6c203aa1a93e9540c8c3f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 19 Oct 2012 14:46:47 +0200
Subject: [PATCH] Add non-deterministic expressions with side-effects.

The following things have been changed in this revision:

* We now give a small step semantics for expressions. The denotational semantics
  only works for side-effect free expressions.
* Dynamically allocated memory through alloc and free is now supported.
* The following expressions are added: assignment, function call, unary
  operators, conditional, alloc, and free.
* Some customary induction schemes for expressions are proven.
* The axiomatic semantics (and its interpretation) have been changed in order
  to deal with non-deterministic expressions.
* We have added inversion schemes based on small inversions for the operational
  semantics. Inversions using these schemes are much faster.
* We improved the statement preservation proof of the operational semantics.
* We now use a variant of SsReflect's [by] and [done], instead of Coq's [now]
  and [easy]. The [done] tactic is much faster as it does not perform
  inversions.
* Add theory, definitions and notations on vectors.
* Separate theory on contexts.
* Change [Arguments] declarations to ensure better unfolding.
---
 theories/ars.v             |  51 +++-
 theories/base.v            | 120 +++++---
 theories/collections.v     | 139 ++++++---
 theories/decidable.v       |  86 +++---
 theories/fin_collections.v | 157 +++++-----
 theories/fin_maps.v        | 143 ++++-----
 theories/fresh_numbers.v   |  35 +++
 theories/list.v            | 577 +++++++++++++++++++++++++------------
 theories/listset.v         |  24 +-
 theories/nmap.v            |  26 +-
 theories/numbers.v         |  63 ++--
 theories/option.v          |  70 ++---
 theories/orders.v          |  54 +++-
 theories/pmap.v            | 111 ++++---
 theories/prelude.v         |   4 +-
 theories/subset.v          |   2 +-
 theories/tactics.v         | 122 ++++++--
 theories/vector.v          | 341 ++++++++++++++++++++++
 18 files changed, 1486 insertions(+), 639 deletions(-)
 create mode 100644 theories/fresh_numbers.v
 create mode 100644 theories/vector.v

diff --git a/theories/ars.v b/theories/ars.v
index 9a4fb224..d56f995a 100644
--- a/theories/ars.v
+++ b/theories/ars.v
@@ -4,6 +4,7 @@
 These are particularly useful as we define the operational semantics as a
 small step semantics. This file defines a hint database [ars] containing
 some theorems on abstract rewriting systems. *)
+Require Import Omega Wf_nat.
 Require Export tactics base.
 
 (** * Definitions *)
@@ -62,8 +63,9 @@ Section rtc.
   Proof. inversion_clear 1; eauto. Qed.
 
   Lemma rtc_ind_r (P : A → A → Prop)
-    (Prefl : ∀ x, P x x) (Pstep : ∀ x y z, rtc R x y → R y z → P x y → P x z) :
-    ∀ y z, rtc R y z → P y z.
+    (Prefl : ∀ x, P x x)
+    (Pstep : ∀ x y z, rtc R x y → R y z → P x y → P x z) :
+    ∀ x z, rtc R x z → P x z.
   Proof.
     cut (∀ y z, rtc R y z → ∀ x, rtc R x y → P x y → P x z).
     { eauto using rtc_refl. }
@@ -99,7 +101,7 @@ Section rtc.
     bsteps R n x y → bsteps R (m + n) x y.
   Proof. apply bsteps_weaken. auto with arith. Qed.
   Lemma bsteps_S n x y :  bsteps R n x y → bsteps R (S n) x y.
-  Proof. apply bsteps_weaken. auto with arith. Qed.
+  Proof. apply bsteps_weaken. omega. Qed.
   Lemma bsteps_trans n m x y z :
     bsteps R n x y → bsteps R m y z → bsteps R (n + m) x z.
   Proof. induction 1; simpl; eauto using bsteps_plus_l with ars. Qed.
@@ -108,7 +110,31 @@ Section rtc.
   Lemma bsteps_rtc n x y : bsteps R n x y → rtc R x y.
   Proof. induction 1; eauto with ars. Qed.
   Lemma rtc_bsteps x y : rtc R x y → ∃ n, bsteps R n x y.
-  Proof. induction 1. exists 0. auto with ars. firstorder eauto with ars. Qed.
+  Proof.
+    induction 1.
+    * exists 0. constructor.
+    * naive_solver eauto with ars.
+  Qed.
+
+  Lemma bsteps_ind_r (P : nat → A → Prop) (x : A)
+    (Prefl : ∀ n, P n x)
+    (Pstep : ∀ n y z, bsteps R n x y → R y z → P n y → P (S n) z) :
+    ∀ n z, bsteps R n x z → P n z.
+  Proof.
+    cut (∀ m y z, bsteps R m y z → ∀ n,
+      bsteps R n x y →
+      (∀ m', n ≤ m' ∧ m' ≤ n + m → P m' y) →
+      P (n + m) z).
+    { intros help ?. change n with (0 + n). eauto with ars. }
+    induction 1 as [|m x' y z p2 p3 IH]; [by eauto with arith|].
+    intros n p1 H. rewrite <-plus_n_Sm.
+    apply (IH (S n)); [by eauto using bsteps_r |].
+    intros [|m'] [??]; [omega |].
+    apply Pstep with x'.
+    * apply bsteps_weaken with n; intuition omega.
+    * done.
+    * apply H; intuition omega.
+  Qed.
 
   Global Instance tc_trans: Transitive (tc R).
   Proof. red; induction 1; eauto with ars. Qed.
@@ -137,23 +163,26 @@ Section rtc.
   Qed.
 End rtc.
 
-Hint Resolve rtc_once rtc_r tc_r : ars.
+Hint Resolve
+  rtc_once rtc_r
+  tc_r
+  bsteps_once bsteps_r bsteps_refl bsteps_trans : ars.
 
 (** * Theorems on sub relations *)
 Section subrel.
   Context {A} (R1 R2 : relation A) (Hsub : subrelation R1 R2).
 
   Lemma red_subrel x : red R1 x → red R2 x.
-  Proof. intros [y ?]. exists y. now apply Hsub. Qed.
+  Proof. intros [y ?]. exists y. by apply Hsub. Qed.
   Lemma nf_subrel x : nf R2 x → nf R1 x.
-  Proof. intros H1 H2. destruct H1. now apply red_subrel. Qed.
+  Proof. intros H1 H2. destruct H1. by apply red_subrel. Qed.
 
   Global Instance rtc_subrel: subrelation (rtc R1) (rtc R2).
-  Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed.
+  Proof. induction 1; [left|eright]; eauto; by apply Hsub. Qed.
   Global Instance nsteps_subrel: subrelation (nsteps R1 n) (nsteps R2 n).
-  Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed.
+  Proof. induction 1; [left|eright]; eauto; by apply Hsub. Qed.
   Global Instance bsteps_subrel: subrelation (bsteps R1 n) (bsteps R2 n).
-  Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed.
+  Proof. induction 1; [left|eright]; eauto; by apply Hsub. Qed.
   Global Instance tc_subrel: subrelation (tc R1) (tc R2).
-  Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed.
+  Proof. induction 1; [left|eright]; eauto; by apply Hsub. Qed.
 End subrel.
diff --git a/theories/base.v b/theories/base.v
index 38fdebfd..7b027c68 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -41,8 +41,12 @@ Hint Extern 0 (?x = ?x) => reflexivity.
 Notation "(→)" := (λ x y, x → y) (only parsing) : C_scope.
 Notation "( T →)" := (λ y, T → y) (only parsing) : C_scope.
 Notation "(→ T )" := (λ y, y → T) (only parsing) : C_scope.
+
 Notation "t $ r" := (t r)
   (at level 65, right associativity, only parsing) : C_scope.
+Notation "($)" := (λ f x, f x) (only parsing) : C_scope.
+Notation "($ x )" := (λ f, f x) (only parsing) : C_scope.
+
 Infix "∘" := compose : C_scope.
 Notation "(∘)" := compose (only parsing) : C_scope.
 Notation "( f ∘)" := (compose f) (only parsing) : C_scope.
@@ -61,12 +65,12 @@ Class PropHolds (P : Prop) := prop_holds: P.
 
 Hint Extern 0 (PropHolds _) => assumption : typeclass_instances.
 Instance: Proper (iff ==> iff) PropHolds.
-Proof. now repeat intro. Qed.
+Proof. repeat intro; trivial. Qed.
 
 Ltac solve_propholds :=
   match goal with
-  | [ |- PropHolds (?P) ] => apply _
-  | [ |- ?P ] => change (PropHolds P); apply _
+  | |- PropHolds (?P) => apply _
+  | |- ?P => change (PropHolds P); apply _
   end.
 
 (** ** Decidable propositions *)
@@ -99,13 +103,14 @@ Instance: Params (@equiv) 2.
 (for types that have an [Equiv] instance) rather than the standard Leibniz
 equality. *)
 Instance equiv_default_relation `{Equiv A} : DefaultRelation (≡) | 3.
-Hint Extern 0 (?x ≡ ?x) => reflexivity.
+Hint Extern 0 (_ ≡ _) => reflexivity.
+Hint Extern 0 (_ ≡ _) => symmetry; assumption.
 
 (** ** Operations on collections *)
-(** We define operational type classes for the standard operations and
+(** We define operational type classes for the traditional operations and
 relations on collections: the empty collection [∅], the union [(∪)],
-intersection [(∩)], difference [(∖)], and the singleton [{[_]}]
-operation, and the subset [(⊆)] and element of [(∈)] relation. *)
+intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
+[(⊆)] and element of [(∈)] relation, and disjointess [(⊥)]. *)
 Class Empty A := empty: A.
 Notation "∅" := empty : C_scope.
 
@@ -116,6 +121,11 @@ Notation "(∪)" := union (only parsing) : C_scope.
 Notation "( x ∪)" := (union x) (only parsing) : C_scope.
 Notation "(∪ x )" := (λ y, union y x) (only parsing) : C_scope.
 
+Definition union_list `{Empty A}
+  `{Union A} : list A → A := fold_right (∪) ∅.
+Arguments union_list _ _ _ !_ /.
+Notation "⋃ l" := (union_list l) (at level 20, format "⋃  l") : C_scope.
+
 Class Intersection A := intersection: A → A → A.
 Instance: Params (@intersection) 2.
 Infix "∩" := intersection (at level 40) : C_scope.
@@ -147,7 +157,7 @@ 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.
 
-Hint Extern 0 (?x ⊆ ?x) => reflexivity.
+Hint Extern 0 (_ ⊆ _) => reflexivity.
 
 Class ElemOf A B := elem_of: A → B → Prop.
 Instance: Params (@elem_of) 3.
@@ -167,6 +177,9 @@ Notation "(⊥)" := disjoint (only parsing) : C_scope.
 Notation "( X ⊥)" := (disjoint X) (only parsing) : C_scope.
 Notation "(⊥ X )" := (λ Y, disjoint Y X) (only parsing) : C_scope.
 
+Instance generic_disjoint `{ElemOf A B} : Disjoint B | 100 :=
+  λ X Y, ∀ x, x ∉ X ∨ x ∉ Y.
+
 (** ** Operations on maps *)
 (** In this section we define operational type classes for the operations
 on maps. In the file [fin_maps] we will axiomatize finite maps.
@@ -179,6 +192,7 @@ Notation "m !! i" := (lookup i m) (at level 20) : C_scope.
 Notation "(!!)" := lookup (only parsing) : C_scope.
 Notation "( m !!)" := (λ i, lookup i m) (only parsing) : C_scope.
 Notation "(!! i )" := (lookup i) (only parsing) : C_scope.
+Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch.
 
 (** The function insert [<[k:=a]>m] should update the element at key [k] with
 value [a] in [m]. *)
@@ -187,6 +201,7 @@ Class Insert (K : Type) (M : Type → Type) :=
 Instance: Params (@insert) 4.
 Notation "<[ k := a ]>" := (insert k a)
   (at level 5, right associativity, format "<[ k := a ]>") : C_scope.
+Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch.
 
 (** The function delete [delete k m] should delete the value at key [k] in
 [m]. If the key [k] is not a member of [m], the original map should be
@@ -194,12 +209,14 @@ returned. *)
 Class Delete (K : Type) (M : Type → Type) :=
   delete: ∀ {A}, K → M A → M A.
 Instance: Params (@delete) 4.
+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 Alter (K : Type) (M : Type → Type) :=
   alter: ∀ {A}, (A → A) → K → M A → M A.
 Instance: Params (@alter) 4.
+Arguments alter _ _ _ _ _ !_ !_ / : 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 at key [k] or [None]
@@ -208,12 +225,14 @@ yields [None]. *)
 Class PartialAlter (K : Type) (M : Type → Type) :=
   partial_alter: ∀ {A}, (option A → option A) → K → M A → M A.
 Instance: Params (@partial_alter) 4.
+Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch.
 
 (** The function [dom C m] should yield the domain of [m]. That is a finite
 collection of type [C] that contains the keys that are a member of [m]. *)
 Class Dom (K : Type) (M : Type → Type) :=
   dom: ∀ {A} C `{Empty C} `{Union C} `{Singleton K C}, M A → C.
 Instance: Params (@dom) 8.
+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)]
@@ -221,6 +240,7 @@ 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.
 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 A) : M A :=
@@ -261,6 +281,10 @@ Class RightId {A} R (i : A) (f : A → A → A) :=
   right_id: ∀ x, R (f x i) x.
 Class Associative {A} R (f : A → A → A) :=
   associative: ∀ x y z, R (f x (f y z)) (f (f x y) z).
+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.
 
 Arguments injective {_ _ _ _} _ {_} _ _ _.
 Arguments idempotent {_ _} _ {_} _.
@@ -268,6 +292,8 @@ Arguments commutative {_ _ _} _ {_} _ _.
 Arguments left_id {_ _} _ _ {_} _.
 Arguments right_id {_ _} _ _ {_} _.
 Arguments associative {_ _} _ {_} _ _ _.
+Arguments left_absorb {_ _} _ _ {_} _.
+Arguments right_absorb {_ _} _ _ {_} _.
 
 (** 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
@@ -287,28 +313,44 @@ Proof. auto. Qed.
 Lemma associative_eq {A} (f : A → A → A) `{!Associative (=) f} x y z :
   f x (f y z) = f (f x y) z.
 Proof. auto. Qed.
+Lemma left_absorb_eq {A} (i : A) (f : A → A → A) `{!LeftAbsorb (=) i f} x :
+  f i x = i.
+Proof. auto. Qed.
+Lemma right_absorb_eq {A} (i : A) (f : A → A → A) `{!RightAbsorb (=) i f} x :
+  f x i = i.
+Proof. auto. Qed.
 
 (** ** Monadic operations *)
-(** We do use the operation type classes for monads merely for convenient
-overloading of notations and do not formalize any theory on monads (we do not
-define a class with the monad laws). *)
+(** 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
+function as a parameter of the class. For example, we define
+<<
+  Class FMap := fmap: ∀ {A B}, (A → B) → M A → M B.
+>>
+instead of
+<<
+  Class FMap {A B} (f : A → B) := fmap: M A → M B.
+>>
+This approach allows us to define [fmap] on lists such that [simpl] unfolds it
+in the appropriate way, and so that it can be used for mutual recursion
+(the mapped function [f] is not part of the fixpoint) as well.
+We use these type classes merely for convenient overloading of notations and do
+not formalize any theory on monads (we do not even define a class with the
+monad laws). *)
 Section monad_ops.
   Context (M : Type → Type).
 
-  Class MRet := mret: ∀ {A}, A → M A.
-  Class MBind := mbind: ∀ {A B}, (A → M B) → M A → M B.
-  Class MJoin := mjoin: ∀ {A}, M (M A) → M A.
-  Class FMap := fmap: ∀ {A B}, (A → B) → M A → M B.
+  Class MBind {A B} (f : A → M B) := mbind: M A → M B.
+  Class MJoin {A} := mjoin: M (M A) → M A.
+  Class FMap {A B} (f : A → B) := fmap: M A → M B.
 End monad_ops.
 
-Instance: Params (@mret) 3.
-Arguments mret {M MRet A} _.
 Instance: Params (@mbind) 4.
-Arguments mbind {M MBind A B} _ _.
+Arguments mbind {_ _ _} _ {_} !_ / : simpl nomatch.
 Instance: Params (@mjoin) 3.
-Arguments mjoin {M MJoin A} _.
+Arguments mjoin {_ _ _} !_ / : simpl nomatch.
 Instance: Params (@fmap) 4.
-Arguments fmap {M FMap A B} _ _.
+Arguments fmap {_ _ _} _ {_} !_ / : simpl nomatch.
 
 Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : C_scope.
 Notation "x ← y ; z" := (y ≫= (λ x : _, z))
@@ -327,7 +369,7 @@ need for proofs that the  relations and operations respect setoid equality.
 Instead, we will define setoid equality in a generic way as
 [λ X Y, X ⊆ Y ∧ Y ⊆ X]. *)
 Class BoundedJoinSemiLattice A `{Empty A} `{SubsetEq A} `{Union A} := {
-  jsl_preorder :>> BoundedPreOrder A;
+  bjsl_preorder :>> BoundedPreOrder A;
   subseteq_union_l x y : x ⊆ x ∪ y;
   subseteq_union_r x y : y ⊆ x ∪ y;
   union_least x y z : x ⊆ z → y ⊆ z → x ∪ y ⊆ z
@@ -338,7 +380,11 @@ Class MeetSemiLattice A `{Empty A} `{SubsetEq A} `{Intersection A} := {
   subseteq_intersection_r x y : x ∩ y ⊆ y;
   intersection_greatest x y z : z ⊆ x → z ⊆ y → z ⊆ x ∩ y
 }.
-
+Class LowerBoundedLattice A `{Empty A} `{SubsetEq A}
+    `{Union A} `{Intersection A} := {
+  lbl_bjsl :>> BoundedJoinSemiLattice A;
+  lbl_msl :>> MeetSemiLattice A
+}.
 (** ** Axiomatization of collections *)
 (** The class [Collection A C] axiomatizes a collection of type [C] with
 elements of type [A]. Since [C] is not dependent on [A], we use the monomorphic
@@ -360,8 +406,12 @@ enumerated as a list. These elements, given by the [elements] function, may be
 in any order and should not contain duplicates. *)
 Class Elements A C := elements: C → list A.
 Instance: Params (@elements) 3.
-Class FinCollection A C `{Empty C} `{Union C} `{Intersection C} `{Difference C}
-    `{Singleton A C} `{ElemOf A C} `{Map A C} `{Elements A C} := {
+
+(** 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} `{Map A C}
+    `{Elements A C} `{∀ x y : A, Decision (x = y)} := {
   fin_collection :>> Collection A C;
   elements_spec X x : x ∈ X ↔ In x (elements X);
   elements_nodup X : NoDup (elements X)
@@ -382,7 +432,7 @@ Class FreshSpec A C `{!Fresh A C} `{!ElemOf A C} := {
 (** * Miscellaneous *)
 Lemma proj1_sig_inj {A} (P : A → Prop) x (Px : P x) y (Py : P y) :
   x↾Px = y↾Py → x = y.
-Proof. now injection 1. Qed.
+Proof. injection 1; trivial. Qed.
 
 Lemma symmetry_iff `(R : relation A) `{!Symmetric R} (x y : A) :
   R x y ↔ R y x.
@@ -436,29 +486,29 @@ Definition lift_relation {A B} (R : relation A)
   (f : B → A) : relation B := λ x y, R (f x) (f y).
 Definition lift_relation_equivalence {A B} (R : relation A) (f : B → A) :
   Equivalence R → Equivalence (lift_relation R f).
-Proof. unfold lift_relation. firstorder. Qed.
+Proof. unfold lift_relation. firstorder auto. Qed.
 Hint Extern 0 (Equivalence (lift_relation _ _)) =>
   eapply @lift_relation_equivalence : typeclass_instances.
 
 Instance: ∀ A B (x : B), Commutative (=) (λ _ _ : A, x).
-Proof. easy. Qed.
+Proof. red. trivial. Qed.
 Instance: ∀ A (x : A), Associative (=) (λ _ _ : A, x).
-Proof. easy. Qed.
+Proof. red. trivial. Qed.
 Instance: ∀ A, Associative (=) (λ x _ : A, x).
-Proof. easy. Qed.
+Proof. red. trivial. Qed.
 Instance: ∀ A, Associative (=) (λ _ x : A, x).
-Proof. easy. Qed.
+Proof. red. trivial. Qed.
 Instance: ∀ A, Idempotent (=) (λ x _ : A, x).
-Proof. easy. Qed.
+Proof. red. trivial. Qed.
 Instance: ∀ A, Idempotent (=) (λ _ x : A, x).
-Proof. easy. Qed.
+Proof. red. trivial. Qed.
 
 Instance left_id_propholds {A} (R : relation A) i f :
   LeftId R i f → ∀ x, PropHolds (R (f i x) x).
-Proof. easy. Qed.
+Proof. red. trivial. Qed.
 Instance right_id_propholds {A} (R : relation A) i f :
   RightId R i f → ∀ x, PropHolds (R (f x i) x).
-Proof. easy. Qed.
+Proof. red. trivial. Qed.
 Instance idem_propholds {A} (R : relation A) f :
   Idempotent R f → ∀ x, PropHolds (R (f x x) x).
-Proof. easy. Qed.
+Proof. red. trivial. Qed.
diff --git a/theories/collections.v b/theories/collections.v
index 8cef0c32..cb90c53f 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -7,59 +7,108 @@ Require Export base tactics orders.
 
 (** * Theorems *)
 Section collection.
-  Context `{Collection A B}.
+  Context `{Collection A C}.
 
   Lemma elem_of_empty x : x ∈ ∅ ↔ False.
-  Proof. split. apply not_elem_of_empty. easy. Qed.
+  Proof. split. apply not_elem_of_empty. done. Qed.
   Lemma elem_of_union_l x X Y : x ∈ X → x ∈ X ∪ Y.
   Proof. intros. apply elem_of_union. auto. Qed.
   Lemma elem_of_union_r x X Y : x ∈ Y → x ∈ X ∪ Y.
   Proof. intros. apply elem_of_union. auto. Qed.
-  Lemma not_elem_of_singleton x y : x ∉ {[ y ]} ↔ x ≠ y.
-  Proof. now rewrite elem_of_singleton. Qed.
-  Lemma not_elem_of_union x X Y : x ∉ X ∪ Y ↔ x ∉ X ∧ x ∉ Y.
-  Proof. rewrite elem_of_union. tauto. Qed.
 
-  Global Instance collection_subseteq: SubsetEq B := λ X Y,
+  Global Instance collection_subseteq: SubsetEq C := λ X Y,
     ∀ x, x ∈ X → x ∈ Y.
-  Global Instance: BoundedJoinSemiLattice B.
-  Proof. firstorder. Qed.
-  Global Instance: MeetSemiLattice B.
-  Proof. firstorder. Qed.
+  Global Instance: LowerBoundedLattice C.
+  Proof. firstorder auto. Qed.
 
   Lemma elem_of_subseteq X Y : X ⊆ Y ↔ ∀ x, x ∈ X → x ∈ Y.
-  Proof. easy. Qed.
+  Proof. done. Qed.
   Lemma elem_of_equiv X Y : X ≡ Y ↔ ∀ x, x ∈ X ↔ x ∈ Y.
   Proof. firstorder. Qed.
   Lemma elem_of_equiv_alt X Y :
     X ≡ Y ↔ (∀ x, x ∈ X → x ∈ Y) ∧ (∀ x, x ∈ Y → x ∈ X).
   Proof. firstorder. Qed.
-
+  Lemma elem_of_subseteq_singleton x X : x ∈ X ↔ {[ x ]} ⊆ X.
+  Proof.
+    split.
+    * intros ??. rewrite elem_of_singleton. intro. by subst.
+    * intros Ex. by apply (Ex x), elem_of_singleton.
+  Qed.
   Global Instance singleton_proper : Proper ((=) ==> (≡)) singleton.
-  Proof. repeat intro. now subst. Qed.
+  Proof. repeat intro. by subst. Qed.
   Global Instance elem_of_proper: Proper ((=) ==> (≡) ==> iff) (∈).
   Proof. intros ???. subst. firstorder. Qed.
 
-  Lemma empty_ne_singleton x : ∅ ≢ {[ x ]}.
+  Lemma elem_of_union_list (x : A) (Xs : list C) :
+    x ∈ ⋃ Xs ↔ ∃ X, In X Xs ∧ x ∈ X.
+  Proof.
+    split.
+    * induction Xs; simpl; intros HXs.
+      + by apply elem_of_empty in HXs.
+      + apply elem_of_union in HXs. naive_solver.
+    * intros [X []]. induction Xs; [done | intros [?|?] ?; subst; simpl].
+      + by apply elem_of_union_l.
+      + apply elem_of_union_r; auto.
+  Qed.
+
+  Lemma non_empty_singleton x : {[ x ]} ≢ ∅.
+  Proof. intros [E _]. by apply (elem_of_empty x), E, elem_of_singleton. Qed.
+
+  Lemma intersection_twice x : {[x]} ∩ {[x]} ≡ {[x]}.
   Proof.
-    intros [_ E]. apply (elem_of_empty x).
-    apply E. now apply elem_of_singleton.
+    split; intros y; rewrite elem_of_intersection, !elem_of_singleton; tauto.
+  Qed.
+  Lemma not_elem_of_singleton x y : x ∉ {[ y ]} ↔ x ≠ y.
+  Proof. by rewrite elem_of_singleton. Qed.
+  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)}.
+
+  Global Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100.
+  Proof.
+    refine (cast_if (decide_rel (⊆) {[ x ]} X));
+      by rewrite elem_of_subseteq_singleton.
+  Defined.
+
+  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
+  | H : _ ∪ _ ≢ ∅ |- _ => apply non_empty_union in H; destruct H
+  | H : {[ _ ]} ≡ ∅ |- _ => destruct (non_empty_singleton _ H)
+  end.
+
 (** * Theorems about map *)
 Section map.
   Context `{Collection A C}.
 
   Lemma elem_of_map_1 (f : A → A) (X : C) (x : A) :
+    x ∈ map f X → ∃ y, x = f y ∧ y ∈ X.
+  Proof. intros. by apply (elem_of_map _). Qed.
+  Lemma elem_of_map_2 (f : A → A) (X : C) (x : A) :
     x ∈ X → f x ∈ map f X.
   Proof. intros. apply (elem_of_map _). eauto. Qed.
-  Lemma elem_of_map_1_alt (f : A → A) (X : C) (x : A) y :
+  Lemma elem_of_map_2_alt (f : A → A) (X : C) (x : A) y :
     x ∈ X → y = f x → y ∈ map f X.
   Proof. intros. apply (elem_of_map _). eauto. Qed.
-  Lemma elem_of_map_2 (f : A → A) (X : C) (x : A) :
-    x ∈ map f X → ∃ y, x = f y ∧ y ∈ X.
-  Proof. intros. now apply (elem_of_map _). Qed.
 End map.
 
 (** * Tactics *)
@@ -67,16 +116,19 @@ End map.
 [(∖)], [map], [∅], [{[_]}], [(≡)], and [(⊆)], by rewriting these into
 logically equivalent propositions. For example we rewrite [A → x ∈ X ∪ ∅] into
 [A → x ∈ X ∨ False]. *)
-Ltac unfold_elem_of := repeat
-  match goal with
-  | H : context [ _ ⊆ _ ] |- _ => setoid_rewrite elem_of_subseteq in H
-  | H : context [ _ ≡ _ ] |- _ => setoid_rewrite elem_of_equiv_alt in H
-  | H : context [ _ ∈ ∅ ] |- _ => setoid_rewrite elem_of_empty in H
-  | H : context [ _ ∈ {[ _ ]} ] |- _ => setoid_rewrite elem_of_singleton in H
-  | H : context [ _ ∈ _ ∪ _ ] |- _ => setoid_rewrite elem_of_union in H
-  | H : context [ _ ∈ _ ∩ _ ] |- _ => setoid_rewrite elem_of_intersection in H
-  | H : context [ _ ∈ _ ∖ _ ] |- _ => setoid_rewrite elem_of_difference in H
-  | H : context [ _ ∈ map _ _ ] |- _ => setoid_rewrite elem_of_map in H
+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 elem_of_equiv_alt in H
+    | context [ _ ∈ ∅ ] => setoid_rewrite elem_of_empty in H
+    | context [ _ ∈ {[ _ ]} ] => setoid_rewrite elem_of_singleton in H
+    | context [ _ ∈ _ ∪ _ ] => setoid_rewrite elem_of_union in H
+    | context [ _ ∈ _ ∩ _ ] => setoid_rewrite elem_of_intersection in H
+    | context [ _ ∈ _ ∖ _ ] => setoid_rewrite elem_of_difference in H
+    | context [ _ ∈ map _ _ ] => setoid_rewrite elem_of_map in H
+    end);
+  repeat match goal with
   | |- context [ _ ⊆ _ ] => setoid_rewrite elem_of_subseteq
   | |- context [ _ ≡ _ ] => setoid_rewrite elem_of_equiv_alt
   | |- context [ _ ∈ ∅ ] => setoid_rewrite elem_of_empty
@@ -90,7 +142,7 @@ Ltac unfold_elem_of := repeat
 (** The tactic [solve_elem_of tac] composes the above tactic with [intuition].
 For goals that do not involve [≡], [⊆], [map], or quantifiers this tactic is
 generally powerful enough. This tactic either fails or proves the goal. *)
-Tactic Notation "solve_elem_of" tactic(tac) :=
+Tactic Notation "solve_elem_of" tactic3(tac) :=
   simpl in *;
   unfold_elem_of;
   solve [intuition (simplify_equality; tac)].
@@ -101,19 +153,20 @@ Tactic Notation "solve_elem_of" := solve_elem_of auto.
 fails or loops on very small goals generated by [solve_elem_of] already. We
 use the [naive_solver] tactic as a substitute. This tactic either fails or
 proves the goal. *)
-Tactic Notation "esolve_elem_of" tactic(tac) :=
+Tactic Notation "esolve_elem_of" tactic3(tac) :=
   simpl in *;
   unfold_elem_of;
   naive_solver tac.
 Tactic Notation "esolve_elem_of" := esolve_elem_of eauto.
 
-(** Given an assumption [H : _ ∈ _], the tactic [destruct_elem_of H] will
+(** Given a hypothesis [H : _ ∈ _], the tactic [destruct_elem_of H] will
 recursively split [H] for [(∪)], [(∩)], [(∖)], [map], [∅], [{[_]}]. *)
-Tactic Notation "destruct_elem_of" hyp(H) :=
+Tactic Notation "decompose_elem_of" hyp(H) :=
   let rec go H :=
   lazymatch type of H with
   | _ ∈ ∅ => apply elem_of_empty in H; destruct H
-  | _ ∈ {[ ?l' ]} => apply elem_of_singleton in H; subst l'
+  | ?l ∈ {[ ?l' ]} =>
+    apply elem_of_singleton in H; first [ subst l' | subst l | idtac ]
   | _ ∈ _ ∪ _ =>
     let H1 := fresh in let H2 := fresh in apply elem_of_union in H;
     destruct H as [H1|H2]; [go H1 | go H2]
@@ -128,6 +181,8 @@ Tactic Notation "destruct_elem_of" hyp(H) :=
     destruct H as [?[? H1]]; go H1
   | _ => idtac
   end in go H.
+Tactic Notation "decompose_elem_of" :=
+  repeat_on_hyps (fun H => decompose_elem_of H).
 
 (** * Sets without duplicates up to an equivalence *)
 Section no_dup.
@@ -208,10 +263,10 @@ End quantifiers.
 Section more_quantifiers.
   Context `{Collection A B}.
 
-  Lemma cforall_weak (P Q : A → Prop) (Hweak : ∀ x, P x → Q x) X :
+  Lemma cforall_weaken (P Q : A → Prop) (Hweaken : ∀ x, P x → Q x) X :
     cforall P X → cforall Q X.
   Proof. unfold cforall. naive_solver. Qed.
-  Lemma cexists_weak (P Q : A → Prop) (Hweak : ∀ x, P x → Q x) X :
+  Lemma cexists_weaken (P Q : A → Prop) (Hweaken : ∀ x, P x → Q x) X :
     cexists P X → cexists Q X.
   Proof. unfold cexists. naive_solver. Qed.
 End more_quantifiers.
@@ -226,7 +281,7 @@ Section fresh.
     exist (∉ X) (fresh X) (is_fresh X).
 
   Global Instance fresh_proper: Proper ((≡) ==> (=)) fresh.
-  Proof. intros ???. now apply fresh_proper_alt, elem_of_equiv. Qed.
+  Proof. intros ???. by apply fresh_proper_alt, elem_of_equiv. Qed.
 
   Fixpoint fresh_list (n : nat) (X : C) : list A :=
     match n with
@@ -238,8 +293,8 @@ Section fresh.
   Proof.
     intros ? n ?. subst.
     induction n; simpl; intros ?? E; f_equal.
-    * now rewrite E.
-    * apply IHn. now rewrite E.
+    * by rewrite E.
+    * apply IHn. by rewrite E.
   Qed.
 
   Lemma fresh_list_length n X : length (fresh_list n X) = n.
@@ -248,7 +303,7 @@ Section fresh.
   Lemma fresh_list_is_fresh n X x : In x (fresh_list n X) → x ∉ X.
   Proof.
     revert X. induction n; simpl.
-    * easy.
+    * done.
     * intros X [?| Hin]. subst.
       + apply is_fresh.
       + apply IHn in Hin. solve_elem_of.
diff --git a/theories/decidable.v b/theories/decidable.v
index 3bdfbf96..e8412ab4 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -3,7 +3,10 @@
 (** This file collects theorems, definitions, tactics, related to propositions
 with a decidable equality. Such propositions are collected by the [Decision]
 type class. *)
-Require Export base.
+Require Export base tactics.
+
+Lemma dec_stable `{Decision P} : ¬¬P → P.
+Proof. firstorder. Qed.
 
 (** We introduce [decide_rel] to avoid inefficienct computation due to eager
 evaluation of propositions by [vm_compute]. This inefficiency occurs if
@@ -14,10 +17,10 @@ Definition decide_rel {A B} (R : A → B → Prop) {dec : ∀ x y, Decision (R x
   (x : A) (y : B) : Decision (R x y) := dec x y.
 Lemma decide_rel_correct {A B} (R : A → B → Prop) `{∀ x y, Decision (R x y)}
   (x : A) (y : B) : decide_rel R x y = decide (R x y).
-Proof. easy. Qed.
+Proof. done. Qed.
 
 (** The tactic [case_decide] performs case analysis on an arbitrary occurrence
-of [decide] or [decide_rel] in the conclusion or assumptions. *)
+of [decide] or [decide_rel] in the conclusion or hypotheses. *)
 Ltac case_decide :=
   match goal with
   | H : context [@decide ?P ?dec] |- _ =>
@@ -34,21 +37,21 @@ Ltac case_decide :=
 with instance resolution to automatically generate decision procedures. *)
 Ltac solve_trivial_decision :=
   match goal with
-  | [ |- Decision (?P) ] => apply _
-  | [ |- sumbool ?P (¬?P) ] => change (Decision P); apply _
+  | |- Decision (?P) => apply _
+  | |- sumbool ?P (¬?P) => change (Decision P); apply _
   end.
-Ltac solve_decision :=
-  intros; first [ solve_trivial_decision
-                | unfold Decision; decide equality; solve_trivial_decision ].
+Ltac solve_decision := intros; first
+  [ solve_trivial_decision
+  | unfold Decision; decide equality; solve_trivial_decision ].
 
 (** We can convert decidable propositions to booleans. *)
 Definition bool_decide (P : Prop) {dec : Decision P} : bool :=
   if dec then true else false.
 
 Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P → P.
-Proof. unfold bool_decide. now destruct dec. Qed.
+Proof. unfold bool_decide. by destruct dec. Qed.
 Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P → bool_decide P.
-Proof. unfold bool_decide. now destruct dec. Qed.
+Proof. unfold bool_decide. by destruct dec. Qed.
 
 (** * Decidable Sigma types *)
 (** Leibniz equality on Sigma types requires the equipped proofs to be
@@ -70,38 +73,43 @@ Proof.
   * intro. destruct x as [x Hx], y as [y Hy].
     simpl in *. subst. f_equal.
     revert Hx Hy. case (bool_decide (P y)).
-    + now intros [] [].
-    + easy.
+    + by intros [] [].
+    + done.
 Qed.
 
+(** The following combinators are useful to create Decision proofs in
+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_or S1 S2 := (if S1 then left _ else cast_if S2).
+Notation cast_if_not S := (if S then right _ else left _).
+
 (** * Instances of Decision *)
 (** Instances of [Decision] for operators of propositional logic. *)
-Program Instance True_dec: Decision True := left _.
-Program Instance False_dec: Decision False := right _.
-Program Instance and_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
-    Decision (P ∧ Q) :=
-  match P_dec with
-  | left _ => match Q_dec with left _ => left _ | right _ => right _ end
-  | right _ => right _
-  end.
-Solve Obligations using intuition.
-Program Instance or_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
-    Decision (P ∨ Q) :=
-  match P_dec with
-  | left _ => left _
-  | right _ => match Q_dec with left _ => left _ | right _ => right _ end
-  end.
-Solve Obligations using intuition.
+Instance True_dec: Decision True := left I.
+Instance False_dec: Decision False := right (False_rect False).
+
+Section prop_dec.
+  Context `(P_dec : Decision P) `(Q_dec : Decision Q).
+
+  Global Instance and_dec: Decision (P ∧ Q).
+  Proof. refine (cast_if_and P_dec Q_dec); intuition. Qed.
+  Global Instance or_dec: Decision (P ∨ Q).
+  Proof. refine (cast_if_or P_dec Q_dec); intuition. Qed.
+  Global Instance impl_dec: Decision (P → Q).
+  Proof. refine (if P_dec then cast_if Q_dec else left _); intuition. Qed.
+End prop_dec.
 
 (** Instances of [Decision] for common data types. *)
-Program 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) :=
-  match A_dec (fst x) (fst y) with
-  | left _ =>
-    match B_dec (snd x) (snd y) with
-    | left _ => left _
-    | right _ => right _
-    end
-  | right _ => right _
-  end.
-Solve Obligations using intuition (simpl;congruence).
+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).
+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).
+Proof. solve_decision. Defined.
diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index 06caeb17..3521e255 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -4,11 +4,11 @@
 importantly, it implements a fold and size function and some useful induction
 principles on finite collections . *)
 Require Import Permutation.
-Require Export collections listset.
+Require Export collections listset numbers.
 
 Instance collection_size `{Elements A C} : Size C := λ X, length (elements X).
 Definition collection_fold `{Elements A C} {B} (f : A → B → B)
-  (b : B) (X : C) : B := fold_right f b (elements X).
+  (b : B) (X : C) : B := foldr f b (elements X).
 
 Section fin_collection.
 Context `{FinCollection A C}.
@@ -18,15 +18,15 @@ Proof.
   intros ?? E. apply NoDup_Permutation.
   * apply elements_nodup.
   * apply elements_nodup.
-  * intros. now rewrite <-!elements_spec, E.
+  * intros. by rewrite <-!elements_spec, E.
 Qed.
 Global Instance collection_size_proper: Proper ((≡) ==> (=)) size.
-Proof. intros ?? E. apply Permutation_length. now rewrite E. Qed.
+Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
 
 Lemma size_empty : size ∅ = 0.
 Proof.
   unfold size, collection_size. rewrite (in_nil_inv (elements ∅)).
-  * easy.
+  * done.
   * intro. rewrite <-elements_spec. solve_elem_of.
 Qed.
 Lemma size_empty_inv X : size X = 0 → X ≡ ∅.
@@ -35,7 +35,7 @@ Proof.
   rewrite (nil_length (elements X)); intuition.
 Qed.
 Lemma size_empty_iff X : size X = 0 ↔ X ≡ ∅.
-Proof. split. apply size_empty_inv. intros E. now rewrite E, size_empty. Qed.
+Proof. split. apply size_empty_inv. intros E. by rewrite E, size_empty. Qed.
 
 Lemma size_singleton x : size {[ x ]} = 1.
 Proof.
@@ -49,56 +49,42 @@ Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y.
 Proof.
   unfold size, collection_size. rewrite !elements_spec.
   generalize (elements X). intros [|? l].
-  * discriminate.
-  * injection 1. intro. rewrite (nil_length l) by easy.
+  * done.
+  * injection 1. intro. rewrite (nil_length l) by done.
     simpl. intuition congruence.
 Qed.
 
-Lemma choose X : X ≢ ∅ → { x | x ∈ X }.
+Lemma elem_of_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅.
 Proof.
-  destruct (elements X) as [|x l] eqn:E.
-  * intros []. apply equiv_empty.
-    intros x. rewrite elements_spec, E. contradiction.
-  * exists x. rewrite elements_spec, E. now left.
+  destruct (elements X) as [|x xs] eqn:E.
+  * right. apply equiv_empty. intros x Ex.
+    by rewrite elements_spec, E in Ex.
+  * left. exists x. rewrite elements_spec, E.
+    by constructor.
 Qed.
-Lemma size_pos_choose X : 0 < size X → { x | x ∈ X }.
+
+Lemma choose X : X ≢ ∅ → ∃ x, x ∈ X.
+Proof.
+  destruct (elem_of_or_empty X) as [[x ?]|?].
+  * by exists x.
+  * done.
+Qed.
+Lemma size_pos_choose X : 0 < size X → ∃ x, x ∈ X.
 Proof.
-  intros E. apply choose.
-  intros E2. rewrite E2, size_empty in E.
-  now destruct (Lt.lt_n_0 0).
+  intros E1. apply choose.
+  intros E2. rewrite E2, size_empty in E1.
+  by apply (Lt.lt_n_0 0).
 Qed.
-Lemma size_1_choose X : size X = 1 → { x | X ≡ {[ x ]} }.
+Lemma size_1_choose X : size X = 1 → ∃ x, X ≡ {[ x ]}.
 Proof.
   intros E. destruct (size_pos_choose X).
   * rewrite E. auto with arith.
   * exists x. apply elem_of_equiv. split.
-    + intro. rewrite elem_of_singleton. eauto using size_singleton_inv.
+    + intro. rewrite elem_of_singleton.
+      eauto using size_singleton_inv.
     + solve_elem_of.
 Qed.
 
-Program Instance collection_car_eq_dec_slow (x y : A) :
-    Decision (x = y) | 100 :=
-  match Compare_dec.zerop (size ({[ x ]} ∩ {[ y ]})) with
-  | left _ => right _
-  | right _ => left _
-  end.
-Next Obligation.
-  intro. apply empty_ne_singleton with x.
-  transitivity ({[ x ]} ∩ {[ y ]}).
-  * symmetry. now apply size_empty_iff.
-  * solve_elem_of.
-Qed.
-Next Obligation. edestruct size_pos_choose; esolve_elem_of. Qed.
-
-Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100 :=
-  match decide_rel In x (elements X) with
-  | left Hx => left (proj2 (elements_spec _ _) Hx)
-  | right Hx => right (Hx ∘ proj1 (elements_spec _ _))
-  end.
-
-Lemma union_difference X Y : X ∪ Y ∖ X ≡ X ∪ Y.
-Proof. split; intros x; destruct (decide (x ∈ X)); solve_elem_of. Qed.
-
 Lemma size_union X Y : X ∩ Y ≡ ∅ → size (X ∪ Y) = size X + size Y.
 Proof.
   intros [E _]. unfold size, collection_size. rewrite <-app_length.
@@ -108,16 +94,42 @@ Proof.
     intros x. rewrite <-!elements_spec. esolve_elem_of.
   * intros. rewrite in_app_iff, <-!elements_spec. solve_elem_of.
 Qed.
+
+Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100.
+Proof.
+  refine (cast_if (decide_rel In x (elements X)));
+    by rewrite (elements_spec _).
+Defined.
+Global Program Instance collection_subseteq_dec_slow (X Y : C) :
+    Decision (X ⊆ Y) | 100 :=
+  match decide_rel (=) (size (X ∖ Y)) 0 with
+  | left E1 => left _
+  | right E1 => right _
+  end.
+Next Obligation.
+  intros x Ex; apply dec_stable; intro.
+  destruct (proj1 (elem_of_empty x)).
+  apply (size_empty_inv _ E1).
+  by rewrite elem_of_difference.
+Qed.
+Next Obligation.
+  intros E2. destruct E1.
+  apply size_empty_iff, equiv_empty. intros x.
+  rewrite elem_of_difference. intros [E3 ?].
+  by apply E2 in E3.
+Qed.
+
 Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X).
 Proof.
-  rewrite <-size_union. now rewrite union_difference. solve_elem_of.
+  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. now rewrite size_singleton. solve_elem_of.
+  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. now rewrite <-size_union_alt, subseteq_union_1. Qed.
+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).
@@ -127,7 +139,7 @@ Qed.
 
 Lemma subseteq_size X Y : X ⊆ Y → size X ≤ size Y.
 Proof.
-  intros. rewrite <-(subseteq_union_1 X Y) by easy.
+  intros. rewrite <-(subseteq_union_1 X Y) by done.
   rewrite <-(union_difference X Y), size_union by solve_elem_of.
   auto with arith.
 Qed.
@@ -139,7 +151,7 @@ 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.
-  * now destruct (Lt.lt_n_0 (size X)).
+  * by destruct (Lt.lt_n_0 (size X)).
   * apply Hind. intros. apply IHn. eauto with arith.
 Qed.
 
@@ -151,7 +163,7 @@ Lemma collection_ind (P : C → Prop) :
 Proof.
   intros ? Hemp Hadd. apply collection_wf_ind.
   intros X IH. destruct (Compare_dec.zerop (size X)).
-  * now rewrite size_empty_inv.
+  * by rewrite size_empty_inv.
   * destruct (size_pos_choose X); auto.
     rewrite <-(subseteq_union_1 {[ x ]} X) by solve_elem_of.
     rewrite <-union_difference.
@@ -166,10 +178,10 @@ Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B)
   ∀ X, P (collection_fold f b X) X.
 Proof.
   intros ? Hemp Hadd.
-  cut (∀ l, NoDup l → ∀ X, (∀ x, x ∈ X ↔ In x l) → P (fold_right f b l) X).
+  cut (∀ l, NoDup l → ∀ X, (∀ x, x ∈ X ↔ In x l) → P (foldr f b l) X).
   { intros help ?. apply help. apply elements_nodup. apply elements_spec. }
   induction 1 as [|x l ?? IHl]; simpl.
-  * intros X HX. rewrite equiv_empty. easy. intros ??. firstorder.
+  * intros X HX. rewrite equiv_empty; firstorder.
   * intros X HX.
     rewrite <-(subseteq_union_1 {[ x ]} X) by esolve_elem_of.
     rewrite <-union_difference.
@@ -182,39 +194,24 @@ Qed.
 Lemma collection_fold_proper {B} (f : A → B → B) (b : B) :
   (∀ a1 a2 b, f a1 (f a2 b) = f a2 (f a1 b)) →
   Proper ((≡) ==> (=)) (collection_fold f b).
-Proof. intros ??? E. apply fold_right_permutation. auto. now rewrite E. Qed.
+Proof. intros ??? E. apply foldr_permutation. auto. by rewrite E. Qed.
 
-Global Program Instance cforall_dec `(P : A → Prop)
-    `{∀ x, Decision (P x)} X : Decision (cforall P X) | 100 :=
-  match decide (Forall P (elements X)) with
-  | left Hall => left _
-  | right Hall => right _
-  end.
-Next Obligation.
-  red. setoid_rewrite elements_spec. now apply Forall_forall.
-Qed.
-Next Obligation.
-  intro. apply Hall, Forall_forall. setoid_rewrite <-elements_spec. auto.
-Qed.
+Global Instance cforall_dec `(P : A → Prop)
+    `{∀ x, Decision (P x)} X : Decision (cforall P X) | 100.
+Proof.
+  refine (cast_if (decide (Forall P (elements X))));
+  abstract (unfold cforall; setoid_rewrite elements_spec;
+    by rewrite <-Forall_forall).
+Defined.
 
-Global Program Instance cexists_dec `(P : A → Prop)
-    `{∀ x, Decision (P x)} X : Decision (cexists P X) | 100 :=
-  match decide (Exists P (elements X)) with
-  | left Hex => left _
-  | right Hex => right _
-  end.
-Next Obligation.
-  red. setoid_rewrite elements_spec. now apply Exists_exists.
-Qed.
-Next Obligation.
-  intro. apply Hex, Exists_exists. setoid_rewrite <-elements_spec. auto.
-Qed.
+Global Instance cexists_dec `(P : A → Prop) `{∀ x, Decision (P x)} X :
+  Decision (cexists P X) | 100.
+Proof.
+  refine (cast_if (decide (Exists P (elements X))));
+  abstract (unfold cexists; setoid_rewrite elements_spec;
+    by rewrite <-Exists_exists).
+Defined.
 
 Global Instance rel_elem_of_dec `{∀ x y, Decision (R x y)} x X :
   Decision (elem_of_upto R x X) | 100 := decide (cexists (R x) X).
-
-Lemma not_elem_of_intersection x X Y : x ∉ X ∩ Y ↔ x ∉ X ∨ x ∉ Y.
-Proof. destruct (decide (x ∈ X)); solve_elem_of. Qed.
-Lemma not_elem_of_difference x X Y : x ∉ X ∖ Y ↔ x ∉ X ∨ x ∈ Y.
-Proof. destruct (decide (x ∈ Y)); solve_elem_of. Qed.
 End fin_collection.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 073b46b0..a7796501 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -19,8 +19,9 @@ parametrized by an implementation of finite sets over the map's key type. *)
 (** Finite map implementations are required to implement the [merge] function
 which enables us to give a generic implementation of [union_with],
 [intersection_with], and [difference_with]. *)
-Class FinMap K M `{∀ A, Empty (M A)} `{Lookup K M} `{FMap M}
-    `{PartialAlter K M} `{Dom K M} `{Merge M} := {
+Class FinMap K M `{Lookup K M} `{∀ A, Empty (M A)}
+    `{∀ `(f : A → B), FMap M f} `{PartialAlter K M} `{Dom K M} `{Merge M}
+    `{∀ i j : K, Decision (i = j)} := {
   finmap_eq {A} (m1 m2 : M A) :
     (∀ i, m1 !! i = m2 !! i) → m1 = m2;
   lookup_empty {A} i :
@@ -73,32 +74,32 @@ Instance finmap_union `{Merge M} {A} : Union (M A) := union_with (λ x _ , x).
 
 (** * General theorems *)
 Section finmap.
-Context `{FinMap K M} `{∀ i j : K, Decision (i = j)} {A : Type}.
+Context `{FinMap K M} {A : Type}.
 
 Global Instance finmap_subseteq: SubsetEq (M A) := λ m n,
   ∀ i x, m !! i = Some x → n !! i = Some x.
 Global Instance: BoundedPreOrder (M A).
-Proof. split. firstorder. intros m i x. rewrite lookup_empty. discriminate. Qed.
+Proof. split; [firstorder |]. intros m i x. by rewrite lookup_empty. Qed.
 
-Lemma lookup_subseteq_Some (m1 m2 : M A) i x :
-  m1 ⊆ m2 → m1 !! i = Some x → m2 !! i = Some x.
+Lemma lookup_weaken (m1 m2 : M A) i x :
+  m1 !! i = Some x → m1 ⊆ m2 → m2 !! i = Some x.
 Proof. auto. Qed.
-Lemma lookup_subseteq_None (m1 m2 : M A) i :
-  m1 ⊆ m2 → m2 !! i = None → m1 !! i = None.
+Lemma lookup_weaken_None (m1 m2 : M A) i :
+  m2 !! i = None → m1 ⊆ m2 → m1 !! i = None.
 Proof. rewrite !eq_None_not_Some. firstorder. Qed.
 Lemma lookup_ne (m : M A) i j : m !! i ≠ m !! j → i ≠ j.
 Proof. congruence. Qed.
 
 Lemma not_elem_of_dom C `{Collection K C} (m : M A) i :
   i ∉ dom C m ↔ m !! i = None.
-Proof. now rewrite (elem_of_dom C), eq_None_not_Some. Qed.
+Proof. by rewrite (elem_of_dom C), eq_None_not_Some. Qed.
 
 Lemma finmap_empty (m : M A) : (∀ i, m !! i = None) → m = ∅.
-Proof. intros Hm. apply finmap_eq. intros. now rewrite Hm, lookup_empty. Qed.
+Proof. intros Hm. apply finmap_eq. intros. by rewrite Hm, lookup_empty. Qed.
 Lemma dom_empty C `{Collection K C} : dom C (∅ : M A) ≡ ∅.
 Proof.
   split; intro.
-  * rewrite (elem_of_dom C), lookup_empty. simplify_is_Some.
+  * rewrite (elem_of_dom C), lookup_empty. by destruct 1.
   * solve_elem_of.
 Qed.
 Lemma dom_empty_inv C `{Collection K C} (m : M A) : dom C m ≡ ∅ → m = ∅.
@@ -108,16 +109,16 @@ Proof.
 Qed.
 
 Lemma lookup_empty_not i : ¬is_Some ((∅ : M A) !! i).
-Proof. rewrite lookup_empty. simplify_is_Some. Qed.
+Proof. rewrite lookup_empty. by destruct 1. Qed.
 Lemma lookup_empty_Some i (x : A) : ¬∅ !! i = Some x.
-Proof. rewrite lookup_empty. discriminate. Qed.
+Proof. by rewrite lookup_empty. Qed.
 
 Lemma partial_alter_compose (m : M A) i f g :
   partial_alter (f ∘ g) i m = partial_alter f i (partial_alter g i m).
 Proof.
   intros. apply finmap_eq. intros ii. case (decide (i = ii)).
-  * intros. subst. now rewrite !lookup_partial_alter.
-  * intros. now rewrite !lookup_partial_alter_ne.
+  * intros. subst. by rewrite !lookup_partial_alter.
+  * intros. by rewrite !lookup_partial_alter_ne.
 Qed.
 Lemma partial_alter_comm (m : M A) i j f g :
   i ≠ j →
@@ -125,23 +126,23 @@ Lemma partial_alter_comm (m : M A) i j f g :
 Proof.
   intros. apply finmap_eq. intros jj.
   destruct (decide (jj = j)).
-  * subst. now rewrite lookup_partial_alter_ne,
+  * subst. by rewrite lookup_partial_alter_ne,
      !lookup_partial_alter, lookup_partial_alter_ne.
   * destruct (decide (jj = i)).
-    + subst. now rewrite lookup_partial_alter,
+    + subst. by rewrite lookup_partial_alter,
        !lookup_partial_alter_ne, lookup_partial_alter by congruence.
-    + now rewrite !lookup_partial_alter_ne by congruence.
+    + by rewrite !lookup_partial_alter_ne by congruence.
 Qed.
 Lemma partial_alter_self_alt (m : M A) i x :
   x = m !! i → partial_alter (λ _, x) i m = m.
 Proof.
   intros. apply finmap_eq. intros ii.
   destruct (decide (i = ii)).
-  * subst. now rewrite lookup_partial_alter.
-  * now rewrite lookup_partial_alter_ne.
+  * subst. by rewrite lookup_partial_alter.
+  * by rewrite lookup_partial_alter_ne.
 Qed.
 Lemma partial_alter_self (m : M A) i : partial_alter (λ _, m !! i) i m = m.
-Proof. now apply partial_alter_self_alt. Qed.
+Proof. by apply partial_alter_self_alt. Qed.
 
 Lemma lookup_insert (m : M A) i x : <[i:=x]>m !! i = Some x.
 Proof. unfold insert. apply lookup_partial_alter. Qed.
@@ -161,7 +162,7 @@ Proof.
       rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence.
   * intros [[??]|[??]].
     + subst. apply lookup_insert.
-    + now rewrite lookup_insert_ne.
+    + by rewrite lookup_insert_ne.
 Qed.
 Lemma lookup_insert_None (m : M A) i j x :
   <[i:=x]>m !! j = None ↔ m !! j = None ∧ i ≠ j.
@@ -169,7 +170,7 @@ Proof.
   split.
   * destruct (decide (i = j)); subst;
       rewrite ?lookup_insert, ?lookup_insert_ne; intuition congruence.
-  * intros [??]. now rewrite lookup_insert_ne.
+  * intros [??]. by rewrite lookup_insert_ne.
 Qed.
 
 Lemma lookup_singleton_Some i j (x y : A) :
@@ -185,11 +186,16 @@ Proof.
   unfold singleton, finmap_singleton.
   rewrite lookup_insert_None, lookup_empty. simpl. tauto.
 Qed.
+Lemma insert_singleton i (x y : A) : <[i:=y]>{[(i, x)]} = {[(i, y)]}.
+Proof.
+  unfold singleton, finmap_singleton, insert, finmap_insert.
+  by rewrite <-partial_alter_compose.
+Qed.
 
 Lemma lookup_singleton i (x : A) : {[(i, x)]} !! i = Some x.
-Proof. rewrite lookup_singleton_Some. tauto. Qed.
+Proof. by rewrite lookup_singleton_Some. Qed.
 Lemma lookup_singleton_ne i j (x : A) : i ≠ j → {[(i, x)]} !! j = None.
-Proof. now rewrite lookup_singleton_None. Qed.
+Proof. by rewrite lookup_singleton_None. Qed.
 
 Lemma lookup_delete (m : M A) i : delete i m !! i = None.
 Proof. apply lookup_partial_alter. Qed.
@@ -202,7 +208,7 @@ Proof.
   split.
   * destruct (decide (i = j)); subst;
       rewrite ?lookup_delete, ?lookup_delete_ne; intuition congruence.
-  * intros [??]. now rewrite lookup_delete_ne.
+  * intros [??]. by rewrite lookup_delete_ne.
 Qed.
 Lemma lookup_delete_None (m : M A) i j :
   delete i m !! j = None ↔ i = j ∨ m !! j = None.
@@ -213,21 +219,21 @@ Proof.
 Qed.
 
 Lemma delete_empty i : delete i (∅ : M A) = ∅.
-Proof. rewrite <-(partial_alter_self ∅) at 2. now rewrite lookup_empty. Qed.
+Proof. rewrite <-(partial_alter_self ∅) at 2. by rewrite lookup_empty. Qed.
 Lemma delete_singleton i (x : A) : delete i {[(i, x)]} = ∅.
 Proof. setoid_rewrite <-partial_alter_compose. apply delete_empty. Qed.
 Lemma delete_comm (m : M A) i j : delete i (delete j m) = delete j (delete i m).
-Proof. destruct (decide (i = j)). now subst. now apply partial_alter_comm. Qed.
+Proof. destruct (decide (i = j)). by subst. by apply partial_alter_comm. Qed.
 Lemma delete_insert_comm (m : M A) i j x :
   i ≠ j → delete i (<[j:=x]>m) = <[j:=x]>(delete i m).
-Proof. intro. now apply partial_alter_comm. Qed.
+Proof. intro. by apply partial_alter_comm. Qed.
 
 Lemma delete_notin (m : M A) i : m !! i = None → delete i m = m.
 Proof.
   intros. apply finmap_eq. intros j.
   destruct (decide (i = j)).
-  * subst. now rewrite lookup_delete.
-  * now apply lookup_delete_ne.
+  * subst. by rewrite lookup_delete.
+  * by apply lookup_delete_ne.
 Qed.
 
 Lemma delete_partial_alter (m : M A) i f :
@@ -248,14 +254,14 @@ Lemma insert_delete (m : M A) i x : m !! i = Some x → <[i:=x]>(delete i m) = m
 Proof.
   intros Hmi. unfold delete, finmap_delete, insert, finmap_insert.
   rewrite <-partial_alter_compose. unfold compose. rewrite <-Hmi.
-  now apply partial_alter_self_alt.
+  by apply partial_alter_self_alt.
 Qed.
 
 Lemma elem_of_dom_delete C `{Collection K C} (m : M A) i j :
   i ∈ dom C (delete j m) ↔ i ≠ j ∧ i ∈ dom C m.
 Proof.
   rewrite !(elem_of_dom C). unfold is_Some.
-  setoid_rewrite lookup_delete_Some. firstorder auto.
+  setoid_rewrite lookup_delete_Some. naive_solver.
 Qed.
 Lemma not_elem_of_dom_delete C `{Collection K C} (m : M A) i :
   i ∉ dom C (delete i m).
@@ -273,21 +279,21 @@ Proof.
   apply (collection_ind (λ X, ∀ m, dom C m ≡ X → P m)) with (dom C m).
   * solve_proper.
   * clear m. intros m Hm. rewrite finmap_empty.
-    + easy.
+    + done.
     + intros. rewrite <-(not_elem_of_dom C), Hm.
-      now solve_elem_of.
+      by solve_elem_of.
   * clear m. intros i X Hi IH m Hdom.
     assert (is_Some (m !! i)) as [x Hx].
     { apply (elem_of_dom C).
       rewrite Hdom. clear Hdom.
-      now solve_elem_of. }
-    rewrite <-(insert_delete m i x) by easy.
+      by solve_elem_of. }
+    rewrite <-(insert_delete m i x) by done.
     apply Hinsert.
-    { now apply (not_elem_of_dom_delete C). }
+    { by apply (not_elem_of_dom_delete C). }
     apply IH. apply elem_of_equiv. intros.
     rewrite (elem_of_dom_delete C).
     esolve_elem_of.
-  * easy.
+  * done.
 Qed.
 
 (** We use the [listset] implementation to prove an induction principle that
@@ -305,30 +311,30 @@ Qed.
 Lemma lookup_delete_list (m : M A) is j :
   In j is → delete_list is m !! j = None.
 Proof.
-  induction is as [|i is]; simpl; [easy |].
+  induction is as [|i is]; simpl; [done |].
   intros [?|?].
-  * subst. now rewrite lookup_delete.
+  * subst. by rewrite lookup_delete.
   * destruct (decide (i = j)).
-    + subst. now rewrite lookup_delete.
+    + subst. by rewrite lookup_delete.
     + rewrite lookup_delete_ne; auto.
 Qed.
 Lemma lookup_delete_list_notin (m : M A) is j :
   ¬In j is → delete_list is m !! j = m !! j.
 Proof.
-  induction is; simpl; [easy |].
+  induction is; simpl; [done |].
   intros. rewrite lookup_delete_ne; tauto.
 Qed.
 
 Lemma delete_list_notin (m : M A) is :
   Forall (λ i, m !! i = None) is → delete_list is m = m.
 Proof.
-  induction 1; simpl; [easy |].
+  induction 1; simpl; [done |].
   rewrite delete_notin; congruence.
 Qed.
 Lemma delete_list_insert_comm (m : M A) is j x :
   ¬In j is → delete_list is (<[j:=x]>m) = <[j:=x]>(delete_list is m).
 Proof.
-  induction is; simpl; [easy |].
+  induction is; simpl; [done |].
   intros. rewrite IHis, delete_insert_comm; tauto.
 Qed.
 
@@ -336,7 +342,7 @@ Lemma lookup_insert_list (m : M A) l1 l2 i x :
   (∀y, ¬In (i,y) l1) → insert_list (l1 ++ (i,x) :: l2) m !! i = Some x.
 Proof.
   induction l1 as [|[j y] l1 IH]; simpl.
-  * intros. now rewrite lookup_insert.
+  * intros. by rewrite lookup_insert.
   * intros Hy. rewrite lookup_insert_ne; naive_solver.
 Qed.
 
@@ -344,7 +350,7 @@ Lemma lookup_insert_list_not_in (m : M A) l i :
   (∀y, ¬In (i,y) l) → insert_list l m !! i = m !! i.
 Proof.
   induction l as [|[j y] l IH]; simpl.
-  * easy.
+  * done.
   * intros Hy. rewrite lookup_insert_ne; naive_solver.
 Qed.
 
@@ -355,15 +361,15 @@ Section merge.
   Global Instance: LeftId (=) None f → LeftId (=) ∅ (merge f).
   Proof.
     intros ??. apply finmap_eq. intros.
-    now rewrite !(merge_spec f), lookup_empty, (left_id None f).
+    by rewrite !(merge_spec f), lookup_empty, (left_id None f).
   Qed.
   Global Instance: RightId (=) None f → RightId (=) ∅ (merge f).
   Proof.
     intros ??. apply finmap_eq. intros.
-    now rewrite !(merge_spec f), lookup_empty, (right_id None f).
+    by rewrite !(merge_spec f), lookup_empty, (right_id None f).
   Qed.
   Global Instance: Idempotent (=) f → Idempotent (=) (merge f).
-  Proof. intros ??. apply finmap_eq. intros. now rewrite !(merge_spec f). Qed.
+  Proof. intros ??. apply finmap_eq. intros. by rewrite !(merge_spec f). Qed.
 
   Context `{!PropHolds (f None None = None)}.
 
@@ -378,17 +384,17 @@ Section merge.
   Lemma merge_comm m1 m2 :
     (∀ i, f (m1 !! i) (m2 !! i) = f (m2 !! i) (m1 !! i)) →
     merge f m1 m2 = merge f m2 m1.
-  Proof. intros. apply finmap_eq. intros. now rewrite !(merge_spec f). Qed.
+  Proof. intros. apply finmap_eq. intros. by rewrite !(merge_spec f). Qed.
   Global Instance: Commutative (=) f → Commutative (=) (merge f).
-  Proof. intros ???. apply merge_comm. intros. now apply (commutative f). Qed.
+  Proof. intros ???. apply merge_comm. intros. by apply (commutative f). Qed.
 
   Lemma merge_assoc m1 m2 m3 :
     (∀ i, f (m1 !! i) (f (m2 !! i) (m3 !! i)) =
           f (f (m1 !! i) (m2 !! i)) (m3 !! i)) →
     merge f m1 (merge f m2 m3) = merge f (merge f m1 m2) m3.
-  Proof. intros. apply finmap_eq. intros. now rewrite !(merge_spec f). Qed.
+  Proof. intros. apply finmap_eq. intros. by rewrite !(merge_spec f). Qed.
   Global Instance: Associative (=) f → Associative (=) (merge f).
-  Proof. intros ????. apply merge_assoc. intros. now apply (associative f). Qed.
+  Proof. intros ????. apply merge_assoc. intros. by apply (associative f). Qed.
 End merge.
 
 (** * Properties of the union and intersection operation *)
@@ -401,19 +407,19 @@ Section union_intersection.
     union_with f m1 m2 !! i = Some (f x y).
   Proof.
     intros Hx Hy. unfold union_with, finmap_union_with.
-    now rewrite (merge_spec _), Hx, Hy.
+    by rewrite (merge_spec _), Hx, Hy.
   Qed.
   Lemma finmap_union_with_l m1 m2 i x :
     m1 !! i = Some x → m2 !! i = None → union_with f m1 m2 !! i = Some x.
   Proof.
     intros Hx Hy. unfold union_with, finmap_union_with.
-    now rewrite (merge_spec _), Hx, Hy.
+    by rewrite (merge_spec _), Hx, Hy.
   Qed.
   Lemma finmap_union_with_r m1 m2 i y :
     m1 !! i = None → m2 !! i = Some y → union_with f m1 m2 !! i = Some y.
   Proof.
     intros Hx Hy. unfold union_with, finmap_union_with.
-    now rewrite (merge_spec _), Hx, Hy.
+    by rewrite (merge_spec _), Hx, Hy.
   Qed.
   Lemma finmap_union_with_None m1 m2 i :
     union_with f m1 m2 !! i = None ↔ m1 !! i = None ∧ m2 !! i = None.
@@ -447,24 +453,29 @@ End finmap.
 
 (** * The finite map tactic *)
 (** The tactic [simplify_map by tac] simplifies finite map expressions
-occuring in the conclusion and assumptions. It uses [tac] to discharge generated
+occuring in the conclusion and hypotheses. It uses [tac] to discharge generated
 inequalities. *)
-Tactic Notation "simplify_map" "by" tactic(T) := repeat
+Tactic Notation "simplify_map" "by" tactic3(tac) := repeat
   match goal with
-  | _ => progress simplify_equality
+  | H1 : ?m !! ?i = Some ?x, H2 : ?m !! ?i = Some ?y |- _ =>
+    assert (x = y) by congruence; subst y; clear H2
   | H : context[ ∅ !! _ ] |- _ => rewrite lookup_empty in H
   | H : context[ (<[_:=_]>_) !! _ ] |- _ => rewrite lookup_insert in H
-  | H : context[ (<[_:=_]>_) !! _ ] |- _ => rewrite lookup_insert_ne in H by T
+  | H : context[ (<[_:=_]>_) !! _ ] |- _ => rewrite lookup_insert_ne in H by tac
   | H : context[ (delete _ _) !! _ ] |- _ => rewrite lookup_delete in H
-  | H : context[ (delete _ _) !! _ ] |- _ => rewrite lookup_delete_ne in H by T
+  | H : context[ (delete _ _) !! _ ] |- _ => rewrite lookup_delete_ne in H by tac
   | H : context[ {[ _ ]} !! _ ] |- _ => rewrite lookup_singleton in H
-  | H : context[ {[ _ ]} !! _ ] |- _ => rewrite lookup_singleton_ne in H by T
+  | H : context[ {[ _ ]} !! _ ] |- _ => rewrite lookup_singleton_ne in H by tac
   | |- context[ ∅ !! _ ] => rewrite lookup_empty
   | |- context[ (<[_:=_]>_) !! _ ] => rewrite lookup_insert
-  | |- context[ (<[_:=_]>_) !! _ ] => rewrite lookup_insert_ne by T
+  | |- context[ (<[_:=_]>_) !! _ ] => rewrite lookup_insert_ne by tac
   | |- context[ (delete _ _) !! _ ] => rewrite lookup_delete
-  | |- context[ (delete _ _) !! _ ] => rewrite lookup_delete_ne by T
+  | |- context[ (delete _ _) !! _ ] => rewrite lookup_delete_ne by tac
   | |- context[ {[ _ ]} !! _ ] => rewrite lookup_singleton
-  | |- context[ {[ _ ]} !! _ ] => rewrite lookup_singleton_ne by T
+  | |- context[ {[ _ ]} !! _ ] => rewrite lookup_singleton_ne by tac
   end.
 Tactic Notation "simplify_map" := simplify_map by auto.
+
+Tactic Notation "simplify_map_equality" "by" tactic3(tac) :=
+  repeat first [ progress (simplify_map by tac) | progress simplify_equality ].
+Tactic Notation "simplify_map_equality" := simplify_map_equality by auto.
diff --git a/theories/fresh_numbers.v b/theories/fresh_numbers.v
new file mode 100644
index 00000000..c75cf774
--- /dev/null
+++ b/theories/fresh_numbers.v
@@ -0,0 +1,35 @@
+(* Copyright (c) 2012, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** Given a finite set of binary naturals [N], we generate a fresh element by
+taking the maximum, and adding one to it. We declare this operation as an
+instance of the type class [Fresh]. *)
+Require Export numbers fin_collections.
+
+Definition Nmax `{Elements N C} : C → N := collection_fold Nmax 0%N.
+
+Instance Nmax_proper `{FinCollection N C} : Proper ((≡) ==> (=)) Nmax.
+Proof.
+  apply collection_fold_proper. intros.
+  rewrite !N.max_assoc. f_equal. apply N.max_comm.
+Qed.
+
+Lemma Nmax_max `{FinCollection N C} X x : x ∈ X → (x ≤ Nmax X)%N.
+Proof.
+  change ((λ b X, x ∈ X → (x ≤ b)%N) (collection_fold N.max 0%N X) X).
+  apply collection_fold_ind.
+  * solve_proper.
+  * solve_elem_of.
+  * solve_elem_of (eauto using N.le_max_l, N.le_max_r, N.le_trans).
+Qed.
+
+Instance Nfresh `{FinCollection N C} : Fresh N C := λ l, (1 + Nmax l)%N.
+Instance Nfresh_spec `{FinCollection N C} : FreshSpec N C.
+Proof.
+  split.
+  * intros. unfold fresh, Nfresh.
+    setoid_replace X with Y; [done |].
+    by apply elem_of_equiv.
+  * intros X E. assert (1 ≤ 0)%N as []; [| done].
+    apply N.add_le_mono_r with (Nmax X).
+    by apply Nmax_max.
+Qed.
diff --git a/theories/list.v b/theories/list.v
index 34dc58d6..22ecc074 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2,16 +2,35 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects general purpose definitions and theorems on lists that
 are not in the Coq standard library. *)
-Require Import Permutation.
+Require Import Omega Permutation.
 Require Export base decidable option.
 
+Arguments length {_} _.
 Arguments cons {_} _ _.
 Arguments app {_} _ _.
 
+Arguments Forall_nil {_ _}.
+Arguments Forall_cons {_ _} _ _ _ _.
+Arguments Exists_nil {_ _}.
+Arguments Exists_cons {_ _} _ _.
+
 Arguments In {_} _ _.
 Arguments NoDup_nil {_}.
 Arguments Permutation {_} _ _.
 
+Notation tail := tl.
+Notation take := firstn.
+Notation drop := skipn.
+Notation foldr := fold_right.
+Notation foldl := fold_left.
+
+Arguments take {_} !_ !_ /.
+Arguments drop {_} !_ !_ /.
+
+Notation take_drop := firstn_skipn.
+Notation foldr_app := fold_right_app.
+Notation foldl_app := fold_left_app.
+
 Notation "(::)" := cons (only parsing) : C_scope.
 Notation "( x ::)" := (cons x) (only parsing) : C_scope.
 Notation "(:: l )" := (λ x, cons x l) (only parsing) : C_scope.
@@ -22,47 +41,57 @@ Notation "(++ k )" := (λ l, app l k) (only parsing) : C_scope.
 (** * General definitions *)
 (** Looking up elements and updating elements in a list. *)
 Global Instance list_lookup: Lookup nat list :=
-  fix list_lookup A (i : nat) (l : list A) {struct l} : option A :=
+  fix go A (i : nat) (l : list A) {struct l} : option A :=
   match l with
   | [] => None
   | x :: l =>
     match i with
     | 0 => Some x
-    | S i => @lookup _ _ list_lookup _ i l
+    | S i => @lookup _ _ go _ i l
     end
   end.
 
 Global Instance list_alter: Alter nat list :=
-  fix list_alter A (f : A → A) (i : nat) (l : list A) {struct l} :=
+  fix go A (f : A → A) (i : nat) (l : list A) {struct l} :=
   match l with
   | [] => []
   | x :: l =>
     match i with
     | 0 => f x :: l
-    | S i => x :: @alter _ _ list_alter _ f i l
+    | S i => x :: @alter _ _ go _ f i l
     end
   end.
 
-(** The [simpl] tactic does not simplify [list_lookup] as it is wrapped into
-an operational type class and we cannot let it unfold on a per instance basis.
-Therefore we use the [simplify_list_lookup] tactic to perform these
-simplifications. Bug: it does not unfold under binders. *)
-Ltac simplify_list_lookup := repeat
-  match goal with
-  | |- context C [@nil ?A !! _] =>
-    let X := (context C [@None A]) in change X
-  | |- context C [(?x :: _) !! 0] =>
-    let X := (context C [Some x]) in change X
-  | |- context C [(_ :: ?l) !! S ?i] =>
-    let X := (context C [l !! i]) in change X
-  | H : context C [@nil ?A !! _] |- _ =>
-    let X := (context C [@None A]) in change X in H
-  | H : context C [(?x :: _) !! 0] |- _ =>
-    let X := (context C [Some x]) in change X in H
-  | H : context C [(_ :: ?l) !! S ?i] |- _  =>
-    let X := (context C [l !! i]) in change X in H
+Global Instance list_insert: Insert nat list := λ _ i x,
+  alter (λ _, x) i.
+
+Global Instance list_delete: Delete nat list :=
+  fix go A (i : nat) (l : list A) {struct l} : list A :=
+  match l with
+  | [] => []
+  | x :: l =>
+    match i with
+    | 0 => l
+    | S i => x :: @delete _ _ go _ i l
+    end
   end.
 
+Tactic Notation "discriminate_list_equality" hyp(H) :=
+  apply (f_equal length) in H;
+  repeat (simpl in H || rewrite app_length in H);
+  exfalso; omega.
+Tactic Notation "discriminate_list_equality" :=
+  repeat_on_hyps (fun H => discriminate_list_equality H).
+
+Ltac simplify_list_equality := repeat
+  match goal with
+  | _ => progress simplify_equality
+  | H : _ ++ _ = _ ++ _ |- _ => first
+     [ apply app_inv_head in H
+     | apply app_inv_tail in H ]
+  | H : _ |- _ => discriminate_list_equality H
+  end.
+    
 (** The function [option_list] converts an element of the option type into
 a list. *)
 Definition option_list {A} : option A → list A := option_rect _ (λ x, [x]) [].
@@ -79,56 +108,127 @@ Context {A : Type}.
 Lemma list_eq (l1 l2 : list A) : (∀ i, l1 !! i = l2 !! i) → l1 = l2.
 Proof.
   revert l2. induction l1; intros [|??] H.
-  * easy.
+  * done.
   * discriminate (H 0).
   * discriminate (H 0).
-  * f_equal. now injection (H 0). apply IHl1. intro. apply (H (S _)).
+  * f_equal. by injection (H 0). apply IHl1. intro. apply (H (S _)).
 Qed.
 
 Lemma list_lookup_nil i : @nil A !! i = None.
-Proof. now destruct i. Qed.
+Proof. by destruct i. Qed.
 Lemma list_lookup_tail (l : list A) i : tail l !! i = l !! S i.
-Proof. now destruct l. Qed.
+Proof. by destruct l. Qed.
 
 Lemma list_lookup_Some_In (l : list A) i x : l !! i = Some x → In x l.
 Proof.
   revert i. induction l; intros [|i] ?;
-    simplify_list_lookup; simplify_equality; constructor (solve [eauto]).
+    simpl; simplify_equality; constructor (solve [eauto]).
 Qed.
 
 Lemma list_lookup_In_Some (l : list A) x : In x l → ∃ i, l !! i = Some x.
 Proof.
   induction l; destruct 1; subst.
-  * now exists 0.
-  * destruct IHl as [i ?]; auto. now exists (S i).
+  * by exists 0.
+  * destruct IHl as [i ?]; auto. by exists (S i).
 Qed.
 Lemma list_lookup_In (l : list A) x : In x l ↔ ∃ i, l !! i = Some x.
 Proof. firstorder eauto using list_lookup_Some_In, list_lookup_In_Some. Qed.
 
-Lemma list_lookup_app_length (l1 l2 : list A) (x : A) :
+Lemma list_lookup_middle (l1 l2 : list A) (x : A) :
   (l1 ++ x :: l2) !! length l1 = Some x.
-Proof. induction l1; simpl; now simplify_list_lookup. Qed.
+Proof. by induction l1; simpl. Qed.
 
 Lemma list_lookup_lt_length (l : list A) i : is_Some (l !! i) ↔ i < length l.
 Proof.
   revert i. induction l.
-  * split; now inversion 1.
-  * intros [|?]; simplify_list_lookup; simpl.
+  * split; by inversion 1.
+  * intros [|?]; simpl.
     + split; auto with arith.
-    + now rewrite <-NPeano.Nat.succ_lt_mono.
+    + by rewrite <-NPeano.Nat.succ_lt_mono.
 Qed.
 Lemma list_lookup_weaken (l l' : list A) i x :
   l !! i = Some x → (l ++ l') !! i = Some x.
-Proof. revert i. induction l. discriminate. now intros []. Qed.
+Proof. revert i. induction l. done. by intros []. Qed.
+
+Lemma take_lookup i j (l : list A) :
+  j < i → take i l !! j = l !! j.
+Proof.
+  revert i j. induction l; intros [|i] j ?; trivial.
+  * by destruct (le_Sn_0 j).
+  * destruct j; simpl; auto with arith.
+Qed.
 
-Lemma fold_right_permutation {B} (f : A → B → B) (b : B) :
+Lemma take_lookup_le i j (l : list A) :
+  i ≤ j → take i l !! j = None.
+Proof.
+  revert i j. induction l; intros [|i] [|j] ?; trivial.
+  * by destruct (le_Sn_0 i).
+  * simpl; auto with arith.
+Qed.
+
+Lemma drop_lookup i j (l : list A) :
+  drop i l !! j = l !! (i + j).
+Proof. revert i j. induction l; intros [|i] ?; simpl; auto. Qed.
+
+Lemma list_lookup_alter (f : A → A) i l : alter f i l !! i = f <$> l !! i.
+Proof. revert i. induction l. done. intros [|i]. done. apply (IHl i). Qed.
+Lemma list_lookup_alter_ne (f : A → A) i j l :
+  i ≠ j → alter f i l !! j = l !! j.
+Proof.
+  revert i j. induction l; [done|].
+  intros [|i] [|j] ?; try done. apply (IHl i). congruence.
+Qed.
+
+Lemma take_alter (f : A → A) i j l :
+  i ≤ j → take i (alter f j l) = take i l.
+Proof.
+  intros. apply list_eq. intros jj. destruct (le_lt_dec i jj).
+  * by rewrite !take_lookup_le.
+  * by rewrite !take_lookup, !list_lookup_alter_ne by omega.
+Qed.
+Lemma take_insert i j (x : A) l :
+  i ≤ j → take i (<[j:=x]>l) = take i l.
+Proof take_alter _ _ _ _.
+
+Lemma drop_alter (f : A → A) i j l :
+  j < i → drop i (alter f j l) = drop i l.
+Proof.
+  intros. apply list_eq. intros jj.
+  by rewrite !drop_lookup, !list_lookup_alter_ne by omega.
+Qed.
+Lemma drop_insert i j (x : A) l :
+  j < i → drop i (<[j:=x]>l) = drop i l.
+Proof drop_alter _ _ _ _.
+
+Lemma foldr_permutation {B} (f : A → B → B) (b : B) :
   (∀ a1 a2 b, f a1 (f a2 b) = f a2 (f a1 b)) →
-  Proper (Permutation ==> (=)) (fold_right f b).
+  Proper (Permutation ==> (=)) (foldr f b).
 Proof. intro. induction 1; simpl; congruence. Qed.
 
+Lemma Forall_cons_inv (P : A → Prop) x l :
+  Forall P (x :: l) → P x ∧ Forall P l.
+Proof. by inversion_clear 1. Qed.
+
+Lemma Forall_app (P : A → Prop) l1 l2 :
+  Forall P (l1 ++ l2) ↔ Forall P l1 ∧ Forall P l2.
+Proof.
+  split.
+   induction l1; inversion 1; intuition.
+  intros [H ?]. induction H; simpl; intuition.
+Qed.
+
+Lemma Forall_true (P : A → Prop) l :
+  (∀ x, P x) → Forall P l.
+Proof. induction l; auto. Qed.
 Lemma Forall_impl (P Q : A → Prop) l :
   Forall P l → (∀ x, P x → Q x) → Forall Q l.
 Proof. induction 1; auto. Qed.
+Lemma Forall_delete (P : A → Prop) l i :
+  Forall P l → Forall P (delete i l).
+Proof.
+  intros H. revert i.
+  by induction H; intros [|i]; try constructor.
+Qed.
 
 Lemma Forall2_length {B} (P : A → B → Prop) l1 l2 :
   Forall2 P l1 l2 → length l1 = length l2.
@@ -148,13 +248,13 @@ Proof.
 Qed.
 
 Lemma NoDup_singleton (x : A) : NoDup [x].
-Proof. constructor. easy. constructor. Qed.
+Proof. constructor. intros []. constructor. Qed.
 Lemma NoDup_app (l k : list A) :
   NoDup l → NoDup k → (∀ x, In x l → ¬In x k) → NoDup (l ++ k).
 Proof.
   induction 1; simpl.
-  * easy.
-  * constructor. rewrite in_app_iff. firstorder. firstorder.
+  * done.
+  * constructor; rewrite ?in_app_iff; firstorder.
 Qed.
 
 Global Instance: ∀ k : list A, Injective (=) (=) (k ++).
@@ -163,21 +263,36 @@ Global Instance: ∀ k : list A, Injective (=) (=) (++ k).
 Proof. intros ???. apply app_inv_tail. Qed.
 
 Lemma in_nil_inv (l : list A) : (∀ x, ¬In x l) → l = [].
-Proof. destruct l. easy. now edestruct 1; constructor. Qed.
+Proof. destruct l. done. by edestruct 1; constructor. Qed.
 Lemma nil_length (l : list A) : length l = 0 → l = [].
-Proof. destruct l. easy. discriminate. Qed.
+Proof. by destruct l. Qed.
 Lemma NoDup_inv_1 (x : A) (l : list A) : NoDup (x :: l) → ¬In x l.
-Proof. now inversion_clear 1. Qed.
+Proof. by inversion_clear 1. Qed.
 Lemma NoDup_inv_2 (x : A) (l : list A) : NoDup (x :: l) → NoDup l.
-Proof. now inversion_clear 1. Qed.
+Proof. by inversion_clear 1. Qed.
 Lemma Forall_inv_2 (P : A → Prop) x l : Forall P (x :: l) → Forall P l.
-Proof. now inversion 1. Qed.
+Proof. by inversion 1. Qed.
 Lemma Exists_inv (P : A → Prop) x l : Exists P (x :: l) → P x ∨ Exists P l.
-Proof. inversion 1; intuition. Qed.
+Proof. inversion 1; intuition trivial. Qed.
+
+Definition reverse (l : list A) : list A := rev_append l [].
+
+Lemma reverse_nill : reverse [] = [].
+Proof. done. Qed.
+Lemma reverse_cons x l : reverse (x :: l) = reverse l ++ [x].
+Proof. unfold reverse. by rewrite <-!rev_alt. Qed.
+Lemma reverse_snoc x l : reverse (l ++ [x]) = x :: reverse l.
+Proof. unfold reverse. by rewrite <-!rev_alt, rev_unit. Qed.
+Lemma reverse_app l1 l2 : reverse (l1 ++ l2) = reverse l2 ++ reverse l1.
+Proof. unfold reverse. rewrite <-!rev_alt. apply rev_app_distr. Qed.
+Lemma reverse_length l : length (reverse l) = length l.
+Proof. unfold reverse. rewrite <-!rev_alt. apply rev_length. Qed.
+Lemma reverse_involutive l : reverse (reverse l) = l.
+Proof. unfold reverse. rewrite <-!rev_alt. apply rev_involutive. Qed. 
 
 Global Instance list_eq_dec {dec : ∀ x y : A, Decision (x = y)} : ∀ l k,
   Decision (l = k) := list_eq_dec dec.
-Global Instance list_in_dec {dec : ∀ x y : A, Decision (x = y)} : ∀ x l,
+Global Instance In_dec {dec : ∀ x y : A, Decision (x = y)} : ∀ x l,
   Decision (In x l) := in_dec dec.
 
 Global Instance NoDup_dec {dec : ∀ x y : A, Decision (x = y)} :
@@ -186,7 +301,7 @@ Global Instance NoDup_dec {dec : ∀ x y : A, Decision (x = y)} :
   match l return Decision (NoDup l) with
   | [] => left NoDup_nil
   | x :: l =>
-    match In_dec dec x l with
+    match In_dec x l with
     | left Hin => right (λ H, NoDup_inv_1 _ _ H Hin)
     | right Hin =>
       match NoDup_dec l with
@@ -196,37 +311,53 @@ Global Instance NoDup_dec {dec : ∀ x y : A, Decision (x = y)} :
     end
   end.
 
-Global Instance Forall_dec (P : A → Prop) {dec : ∀ x, Decision (P x)} :
-    ∀ l, Decision (Forall P l) :=
-  fix go (l : list A) :=
-  match l return {Forall P l} + {¬Forall P l} with
-  | [] => left (Forall_nil _)
-  | x :: l =>
-    match dec x with
-    | left Hx =>
-      match go l with
-      | left Hl => left (Forall_cons _ Hx Hl)
-      | right Hl => right (Hl ∘ Forall_inv_2 _ _ _)
-      end
-    | right Hx => right (Hx ∘ @Forall_inv _ _ _ _)
-    end
+Section Forall_Exists.
+Context (P : A → Prop).
+
+Lemma Exists_not_Forall l : Exists (not ∘ P) l → ¬Forall P l.
+Proof. induction 1; inversion_clear 1; contradiction. Qed.
+
+Lemma Forall_not_Exists l : Forall (not ∘ P) l → ¬Exists P l.
+Proof. induction 1; inversion_clear 1; contradiction. Qed.
+
+Context {dec : ∀ x, Decision (P x)}.
+
+Fixpoint Forall_Exists_dec l : {Forall P l} + {Exists (not ∘ P) l}.
+Proof.
+ refine (
+  match l with
+  | [] => left _
+  | x :: l => cast_if_and (dec x) (Forall_Exists_dec l)
+  end); clear Forall_Exists_dec; abstract intuition.
+Defined.
+
+Lemma not_Forall_Exists l : ¬Forall P l → Exists (not ∘ P) l.
+Proof. intro. destruct (Forall_Exists_dec l); intuition. Qed.
+
+Global Instance Forall_dec l : Decision (Forall P l) :=
+  match Forall_Exists_dec l with
+  | left H => left H
+  | right H => right (Exists_not_Forall _ H)
   end.
 
-Global Instance Exists_dec (P : A → Prop) {dec : ∀ x, Decision (P x)} :
-    ∀ l, Decision (Exists P l) :=
-  fix go (l : list A) :=
-  match l return {Exists P l} + {¬Exists P l} with
-  | [] => right (proj1 (Exists_nil _))
-  | x :: l =>
-    match dec x with
-    | left Hx => left (Exists_cons_hd _ _ _ Hx)
-    | right Hx =>
-      match go l with
-      | left Hl => left (Exists_cons_tl _ Hl)
-      | right Hl => right (or_ind Hx Hl ∘ Exists_inv _ _ _)
-      end
-    end
+Fixpoint Exists_Forall_dec l : {Exists P l} + {Forall (not ∘ P) l}.
+Proof.
+ refine (
+  match l with
+  | [] => right _
+  | x :: l => cast_if_or (dec x) (Exists_Forall_dec l)
+  end); clear Exists_Forall_dec; abstract intuition.
+Defined.
+
+Lemma not_Exists_Forall l : ¬Exists P l → Forall (not ∘ P) l.
+Proof. intro. destruct (Exists_Forall_dec l); intuition. Qed.
+
+Global Instance Exists_dec l : Decision (Exists P l) :=
+  match Exists_Forall_dec l with
+  | left H => left H
+  | right H => right (Forall_not_Exists _ H)
   end.
+End Forall_Exists.
 End general_properties.
 
 (** * Theorems on the prefix and suffix predicates *)
@@ -236,30 +367,31 @@ Context {A : Type}.
 Global Instance: PreOrder (@prefix_of A).
 Proof.
   split.
-   intros ?. eexists []. now rewrite app_nil_r.
-  intros ??? [k1 ?] [k2 ?]. exists (k1 ++ k2). subst. now rewrite app_assoc.
+  * intros ?. eexists []. by rewrite app_nil_r.
+  * intros ??? [k1 ?] [k2 ?].
+    exists (k1 ++ k2). subst. by rewrite app_assoc.
 Qed.
 
 Lemma prefix_of_nil (l : list A) : prefix_of [] l.
-Proof. now exists l. Qed.
+Proof. by exists l. Qed.
 Lemma prefix_of_nil_not x (l : list A) : ¬prefix_of (x :: l) [].
-Proof. intros [k E]. discriminate. Qed.
+Proof. by intros [k E]. Qed.
 Lemma prefix_of_cons x y (l1 l2 : list A) :
   x = y → prefix_of l1 l2 → prefix_of (x :: l1) (y :: l2).
-Proof. intros ? [k E]. exists k. now subst. Qed.
+Proof. intros ? [k E]. exists k. by subst. Qed.
 Lemma prefix_of_cons_inv_1 x y (l1 l2 : list A) :
   prefix_of (x :: l1) (y :: l2) → x = y.
-Proof. intros [k E]. now injection E. Qed.
+Proof. intros [k E]. by injection E. Qed.
 Lemma prefix_of_cons_inv_2 x y (l1 l2 : list A) :
   prefix_of (x :: l1) (y :: l2) → prefix_of l1 l2.
-Proof. intros [k E]. exists k. now injection E. Qed.
+Proof. intros [k E]. exists k. by injection E. Qed.
 
 Lemma prefix_of_app_l (l1 l2 l3 : list A) :
   prefix_of (l1 ++ l3) l2 → prefix_of l1 l2.
-Proof. intros [k ?]. red. exists (l3 ++ k). subst. now rewrite <-app_assoc. Qed.
+Proof. intros [k ?]. red. exists (l3 ++ k). subst. by rewrite <-app_assoc. Qed.
 Lemma prefix_of_app_r (l1 l2 l3 : list A) :
   prefix_of l1 l2 → prefix_of l1 (l2 ++ l3).
-Proof. intros [k ?]. exists (k ++ l3). subst. now rewrite app_assoc. Qed.
+Proof. intros [k ?]. exists (k ++ l3). subst. by rewrite app_assoc. Qed.
 
 Global Instance prefix_of_dec `{∀ x y : A, Decision (x = y)} :
     ∀ l1 l2, Decision (prefix_of l1 l2) :=
@@ -281,89 +413,88 @@ Global Instance prefix_of_dec `{∀ x y : A, Decision (x = y)} :
 Global Instance: PreOrder (@suffix_of A).
 Proof.
   split.
-  * intros ?. now eexists [].
+  * intros ?. by eexists [].
   * intros ??? [k1 ?] [k2 ?].
-    exists (k2 ++ k1). subst. now rewrite app_assoc.
+    exists (k2 ++ k1). subst. by rewrite app_assoc.
 Qed.
 
-Lemma prefix_suffix_rev (l1 l2 : list A) :
-  prefix_of l1 l2 ↔ suffix_of (rev l1) (rev l2).
+Lemma prefix_suffix_reverse (l1 l2 : list A) :
+  prefix_of l1 l2 ↔ suffix_of (reverse l1) (reverse l2).
 Proof.
-  split; intros [k E]; exists (rev k).
-  * now rewrite E, rev_app_distr.
-  * now rewrite <-(rev_involutive l2), E, rev_app_distr, rev_involutive.
+  split; intros [k E]; exists (reverse k).
+  * by rewrite E, reverse_app.
+  * by rewrite <-(reverse_involutive l2), E, reverse_app, reverse_involutive.
 Qed.
-Lemma suffix_prefix_rev (l1 l2 : list A) :
-  suffix_of l1 l2 ↔ prefix_of (rev l1) (rev l2).
-Proof. now rewrite prefix_suffix_rev, !rev_involutive. Qed.
+Lemma suffix_prefix_reverse (l1 l2 : list A) :
+  suffix_of l1 l2 ↔ prefix_of (reverse l1) (reverse l2).
+Proof. by rewrite prefix_suffix_reverse, !reverse_involutive. Qed.
 
 Lemma suffix_of_nil (l : list A) : suffix_of [] l.
-Proof. exists l. now rewrite app_nil_r. Qed.
-Lemma suffix_of_nil_not x (l : list A) : ¬suffix_of (x :: l) [].
-Proof. intros [[] ?]; discriminate. Qed.
-Lemma suffix_of_cons x y (l1 l2 : list A) :
-  x = y → suffix_of l1 l2 → suffix_of (l1 ++ [x]) (l2 ++ [y]).
-Proof. intros ? [k E]. exists k. subst. now rewrite app_assoc. Qed.
+Proof. exists l. by rewrite app_nil_r. Qed.
+Lemma suffix_of_nil_inv (l : list A) : suffix_of l [] → l = [].
+Proof. by intros [[|?] ?]; simplify_list_equality. Qed.
+Lemma suffix_of_cons_nil_inv x (l : list A) : ¬suffix_of (x :: l) [].
+Proof. by intros [[] ?]. Qed.
+
+Lemma suffix_of_app (l1 l2 k : list A) :
+  suffix_of l1 l2 → suffix_of (l1 ++ k) (l2 ++ k).
+Proof. intros [k' E]. exists k'. subst. by rewrite app_assoc. Qed.
+
 Lemma suffix_of_snoc_inv_1 x y (l1 l2 : list A) :
   suffix_of (l1 ++ [x]) (l2 ++ [y]) → x = y.
 Proof.
-  rewrite suffix_prefix_rev, !rev_unit. now apply prefix_of_cons_inv_1.
+  rewrite suffix_prefix_reverse, !reverse_snoc.
+  by apply prefix_of_cons_inv_1.
 Qed.
 Lemma suffix_of_snoc_inv_2 x y (l1 l2 : list A) :
   suffix_of (l1 ++ [x]) (l2 ++ [y]) → suffix_of l1 l2.
 Proof.
-  rewrite !suffix_prefix_rev, !rev_unit. now apply prefix_of_cons_inv_2.
+  rewrite !suffix_prefix_reverse, !reverse_snoc.
+  by apply prefix_of_cons_inv_2.
 Qed.
 
 Lemma suffix_of_cons_l (l1 l2 : list A) x :
   suffix_of (x :: l1) l2 → suffix_of l1 l2.
-Proof. intros [k ?]. exists (k ++ [x]). subst. now rewrite <-app_assoc. Qed.
+Proof. intros [k ?]. exists (k ++ [x]). subst. by rewrite <-app_assoc. Qed.
 Lemma suffix_of_app_l (l1 l2 l3 : list A) :
   suffix_of (l3 ++ l1) l2 → suffix_of l1 l2.
-Proof. intros [k ?]. exists (k ++ l3). subst. now rewrite <-app_assoc. Qed.
+Proof. intros [k ?]. exists (k ++ l3). subst. by rewrite <-app_assoc. Qed.
 Lemma suffix_of_cons_r (l1 l2 : list A) x :
   suffix_of l1 l2 → suffix_of l1 (x :: l2).
-Proof. intros [k ?]. exists (x :: k). now subst. Qed.
+Proof. intros [k ?]. exists (x :: k). by subst. Qed.
 Lemma suffix_of_app_r (l1 l2 l3 : list A) :
   suffix_of l1 l2 → suffix_of l1 (l3 ++ l2).
-Proof. intros [k ?]. exists (l3 ++ k). subst. now rewrite app_assoc. Qed.
+Proof. intros [k ?]. exists (l3 ++ k). subst. by rewrite app_assoc. Qed.
 
 Lemma suffix_of_cons_inv (l1 l2 : list A) x y :
-  suffix_of (x :: l1) (y :: l2) → x :: l1 = y :: l2 ∨ suffix_of (x :: l1) l2.
+  suffix_of (x :: l1) (y :: l2) →
+    x :: l1 = y :: l2 ∨ suffix_of (x :: l1) l2.
 Proof.
   intros [[|? k] E].
-   now left.
-  right. simplify_equality. now apply suffix_of_app_r.
+  * by left.
+  * right. simplify_equality. by apply suffix_of_app_r.
 Qed.
+
 Lemma suffix_of_cons_not x (l : list A) : ¬suffix_of (x :: l) l.
-Proof.
-  intros [k E]. change ([] ++ l = k ++ [x] ++ l) in E.
-  rewrite app_assoc in E. apply app_inv_tail in E.
-  destruct k; simplify_equality.
-Qed.
+Proof. intros [??]. discriminate_list_equality. Qed.
 
-Global Program Instance suffix_of_dec `{∀ x y : A, Decision (x = y)} l1 l2 :
-    Decision (suffix_of l1 l2) :=
-  match decide_rel prefix_of (rev_append l1 []) (rev_append l2 []) with
-  | left Hpre => left _
-  | right Hpre => right _
-  end.
-Next Obligation. apply suffix_prefix_rev. now rewrite !rev_alt. Qed.
-Next Obligation.
-  intro. destruct Hpre. rewrite <-!rev_alt.
-  now apply suffix_prefix_rev.
-Qed.
+Global Instance suffix_of_dec `{∀ x y : A, Decision (x = y)} (l1 l2 : list A) :
+  Decision (suffix_of l1 l2).
+Proof.
+  refine (cast_if (decide_rel prefix_of (reverse l1) (reverse l2)));
+   abstract (by rewrite suffix_prefix_reverse).
+Defined.
 End prefix_postfix.
 
-(** The [simplify_suffix_of] removes [suffix_of] assumptions that are
-tautologies, and simplifies [suffix_of] assumptions involving [(::)] and
+(** The [simplify_suffix_of] removes [suffix_of] hypotheses that are
+tautologies, and simplifies [suffix_of] hypotheses involving [(::)] and
 [(++)]. *)
 Ltac simplify_suffix_of := repeat
   match goal with
   | H : suffix_of (_ :: _) _ |- _ =>
     destruct (suffix_of_cons_not _ _ H)
   | H : suffix_of (_ :: _) [] |- _ =>
-    destruct (suffix_of_nil_not _ _ H)
+    apply suffix_of_nil_inv in H
   | H : suffix_of (_ :: _) (_ :: _) |- _ =>
     destruct (suffix_of_cons_inv _ _ _ _ H); clear H
   | H : suffix_of ?x ?x |- _ => clear H
@@ -373,65 +504,82 @@ Ltac simplify_suffix_of := repeat
   end.
 
 (** The [solve_suffix_of] tries to solve goals involving [suffix_of]. It uses
-[simplify_suffix_of] to simplify assumptions, tries to solve [suffix_of]
-conclusions, and adds transitive consequences of assumptions to the context. 
-This tactic either fails or proves the goal. *)
-Ltac solve_suffix_of :=
-  let rec go :=
+[simplify_suffix_of] to simplify hypotheses and tries to solve [suffix_of]
+conclusions. This tactic either fails or proves the goal. *)
+Ltac solve_suffix_of := solve [intuition (repeat
   match goal with
-  | _ => progress simplify_suffix_of; go
+  | _ => done
+  | _ => progress simplify_suffix_of
   | |- suffix_of [] _ => apply suffix_of_nil
   | |- suffix_of _ _ => reflexivity
-  | |- suffix_of _ _ => solve [auto]
-  | |- suffix_of _ (_ :: _) => apply suffix_of_cons_r; go
-  | |- suffix_of _ (_ ++ _) => apply suffix_of_app_r; go
-  | H : ¬suffix_of _ _ |- _ => destruct H; go
-  | H1 : suffix_of ?x ?y, H2 : suffix_of ?y ?z |- _ =>
-     match goal with
-     | _ : suffix_of x z |- _ => fail 1
-     | _ => assert (suffix_of x z) by (transitivity y; assumption);
-            clear H1; clear H2; go (**i clear to avoid loops *)
-     end
-  end in go.
+  | |- suffix_of _ (_ :: _) => apply suffix_of_cons_r
+  | |- suffix_of _ (_ ++ _) => apply suffix_of_app_r
+  | H : suffix_of _ _ → False |- _ => destruct H
+  end)].
 Hint Extern 0 (PropHolds (suffix_of _ _)) =>
   unfold PropHolds; solve_suffix_of : typeclass_instances.
 
 (** * Monadic operations *)
-Global Instance list_ret: MRet list := λ A a, [a].
-Global Instance list_fmap: FMap list :=
-  fix go A B (f : A → B) (l : list A) :=
+Global Instance list_fmap {A B} (f : A → B) : FMap list f :=
+  fix go (l : list A) :=
   match l with
   | [] => []
-  | x :: l => f x :: @fmap _ go _ _ f l
+  | x :: l => f x :: @fmap _ _ _ f go l
   end.
-Global Instance list_join: MJoin list :=
-  fix go A (l : list (list A)) : list A :=
+Global Instance list_join {A} : MJoin list :=
+  fix go (l : list (list A)) : list A :=
   match l with
   | [] =>  []
-  | x :: l => x ++ @mjoin _ go _ l
+  | x :: l => x ++ @mjoin _ _ go l
   end.
-Global Instance list_bind: MBind list := λ A B f l, mjoin (f <$> l).
+Global Instance list_bind {A B} (f : A → list B) : MBind list f := λ l,
+  mjoin (f <$> l).
 
 Section list_fmap.
   Context {A B : Type} (f : A → B).
 
-  Local Arguments fmap _ _ _ _ _ !_ /.
+  Global Instance: Injective (=) (=) f → Injective (=) (=) (fmap f).
+  Proof.
+    intros ? l1. induction l1 as [|x l1 IH].
+    * by intros [|??].
+    * intros [|??]; [done |]; simpl; intros; simplify_equality.
+      by f_equal; [apply (injective f) | auto].
+  Qed.
+  Lemma fmap_app l1 l2 : f <$> l1 ++ l2 = (f <$> l1) ++ (f <$> l2).
+  Proof. induction l1; simpl; by f_equal. Qed.
+  Lemma fmap_cons_inv y l k :
+    f <$> l = y :: k → ∃ x l', y = f x ∧ l = x :: l'.
+  Proof. intros. destruct l; simpl; simplify_equality; eauto. Qed.
+  Lemma fmap_app_inv l k1 k2 :
+    f <$> l = k1 ++ k2 → ∃ l1 l2, k1 = f <$> l1 ∧ k2 = f <$> l2 ∧ l = l1 ++ l2.
+  Proof.
+    revert l. induction k1 as [|y k1 IH]; simpl.
+    * intros l ?. by eexists [], l.
+    * intros [|x l] ?; simpl; simplify_equality.
+      destruct (IH l) as [l1 [l2 [? [??]]]]; subst; [done |].
+      by exists (x :: l1) l2.
+  Qed.
 
   Lemma fmap_length l : length (f <$> l) = length l.
-  Proof. induction l; simpl; auto. Qed.
+  Proof. induction l; simpl; by f_equal. Qed.
+  Lemma fmap_reverse l : f <$> reverse l = reverse (f <$> l).
+  Proof.
+    induction l; simpl; [done |].
+    by rewrite !reverse_cons, fmap_app, IHl.
+  Qed.
 
   Lemma list_lookup_fmap l i : (f <$> l) !! i = f <$> (l !! i).
-  Proof. revert i. induction l; now intros [|]. Qed.
+  Proof. revert i. induction l; by intros [|]. Qed.
 
   Lemma in_fmap_1 l x : In x l → In (f x) (f <$> l).
   Proof. induction l; destruct 1; subst; constructor (solve [auto]). Qed.
   Lemma in_fmap_1_alt l x y : In x l → y = f x → In y (f <$> l).
-  Proof. intros. subst. now apply in_fmap_1. Qed.
+  Proof. intros. subst. by apply in_fmap_1. Qed.
   Lemma in_fmap_2 l x : In x (f <$> l) → ∃ y, x = f y ∧ In y l.
   Proof.
     induction l as [|y l]; destruct 1; subst.
-    * exists y; now intuition.
-    * destruct IHl as [y' [??]]. easy. exists y'; now intuition.
+    * exists y; by intuition.
+    * destruct IHl as [y' [??]]. done. exists y'; intuition.
   Qed.
   Lemma in_fmap l x : In x (f <$> l) ↔ ∃ y, x = f y ∧ In y l.
   Proof.
@@ -439,14 +587,22 @@ Section list_fmap.
     * apply in_fmap_2.
     * intros [? [??]]. eauto using in_fmap_1_alt.
   Qed.
+
+  Lemma Forall_fmap (l : list A) (P : B → Prop) :
+    Forall (P ∘ f) l ↔ Forall P (f <$> l).
+  Proof. induction l; split; inversion_clear 1; constructor; firstorder auto. Qed.
 End list_fmap.
 
-Lemma Forall_fst {A B} (l : list (A * B)) (P : A → Prop) :
-  Forall (P ∘ fst) l ↔ Forall P (fst <$> l).
-Proof. induction l; split; inversion 1; subst; constructor; firstorder auto. Qed.
-Lemma Forall_snd {A B} (l : list (A * B)) (P : B → Prop) :
-  Forall (P ∘ snd) l ↔ Forall P (snd <$> l).
-Proof. induction l; split; inversion 1; subst; constructor; firstorder auto. Qed.
+Ltac simplify_list_fmap_equality := repeat
+  match goal with
+  | _ => progress simplify_equality
+  | H : _ <$> _ = _ :: _ |- _ =>
+    apply fmap_cons_inv in H; destruct H as [? [? [??]]]
+  | H : _ :: _ = _ <$> _ |- _ => symmetry in H
+  | H : _ <$> _ = _ ++ _ |- _ =>
+    apply fmap_app_inv in H; destruct H as [? [? [? [??]]]]
+  | H : _ ++ _ = _ <$> _ |- _ => symmetry in H
+  end.
 
 (** * Indexed folds and maps *)
 (** We define stronger variants of map and fold that also take the index of the
@@ -459,7 +615,7 @@ Definition imap_go {A B} (f : nat → A → B) : nat → list A → list B :=
   end.
 Definition imap {A B} (f : nat → A → B) : list A → list B := imap_go f 0.
 
-Definition ifold_right {A B} (f : nat → B → A → A)
+Definition ifoldr {A B} (f : nat → B → A → A)
     (a : nat → A) : nat → list B → A :=
   fix go (n : nat) (l : list B) : A :=
   match l with
@@ -467,9 +623,9 @@ Definition ifold_right {A B} (f : nat → B → A → A)
   | b :: l => f n b (go (S n) l)
   end.
 
-Lemma ifold_right_app {A B} (f : nat → B → A → A) (a : nat → A)
+Lemma ifoldr_app {A B} (f : nat → B → A → A) (a : nat → A)
     (l1 l2 : list B) n :
-  ifold_right f a n (l1 ++ l2) = ifold_right f (λ n, ifold_right f a n l2) n l1.
+  ifoldr f a n (l1 ++ l2) = ifoldr f (λ n, ifoldr f a n l2) n l1.
 Proof.
   revert n a. induction l1 as [| b l1 IH ]; intros; simpl; f_equal; auto.
 Qed.
@@ -499,20 +655,31 @@ Section same_length.
   Proof.
     rewrite same_length_length.
     setoid_rewrite list_lookup_lt_length.
-    intros E. now rewrite E.
+    intros E. by rewrite E.
   Qed.
+
+  Lemma Forall2_app_inv (P : A → B → Prop) l1 l2 k1 k2 :
+    same_length l1 k1 →
+    Forall2 P (l1 ++ l2) (k1 ++ k2) → Forall2 P l2 k2.
+  Proof. induction 1. done. inversion 1; subst; auto. Qed.
 End same_length.
 
+Instance: ∀ A, Reflexive (@same_length A A).
+Proof. intros A l. induction l; try constructor; auto. Qed.
+
 (** * Zipping lists *)
-(** Since we prefer Haskell style naming, we rename the standard library's
-implementation [combine] into [zip] using a notation. *)
-Notation zip := combine.
+Definition zip_with {A B C} (f : A → B → C) : list A → list B → list C :=
+  fix go l1 l2 :=
+  match l1, l2 with
+  | x1 :: l1, x2 :: l2 => f x1 x2 :: go l1 l2
+  | _ , _ => []
+  end.
+
+Notation zip := (zip_with pair).
 
 Section zip.
   Context {A B : Type}.
 
-  Local Arguments fmap _ _ _ _ _ !_ /.
-
   Lemma zip_fst_le (l1 : list A) (l2 : list B) :
     length l1 ≤ length l2 → fst <$> zip l1 l2 = l1.
   Proof.
@@ -524,7 +691,7 @@ Section zip.
     same_length l1 l2 → fst <$> zip l1 l2 = l1.
   Proof.
     rewrite same_length_length. intros H.
-    apply zip_fst_le. now rewrite H.
+    apply zip_fst_le. by rewrite H.
   Qed.
 
   Lemma zip_snd_le (l1 : list A) (l2 : list B) :
@@ -538,6 +705,60 @@ Section zip.
     same_length l1 l2 → snd <$> zip l1 l2 = l2.
   Proof.
     rewrite same_length_length. intros H.
-    apply zip_snd_le. now rewrite H.
+    apply zip_snd_le. by rewrite H.
   Qed.
 End zip.
+
+Definition zipped_map {A B} (f : list A → list A → A → B) :
+    list A → list A → list B :=
+  fix go l k :=
+  match k with
+  | [] => []
+  | x :: k => f l k x :: go (x :: l) k
+  end.
+
+Lemma In_zipped_map {A B} (f : list A → list A → A → B) l k x :
+  In x (zipped_map f l k) ↔
+    ∃ k' k'' y, k = k' ++ [y] ++ k'' ∧ x = f (reverse k' ++ l) k'' y.
+Proof.
+  split.
+  * revert l. induction k as [|z k IH]; [done | intros l [?|?]]; subst.
+    + by eexists [], k, z.
+    + destruct (IH (z :: l)) as [k' [k'' [y [??]]]]; [done |]; subst.
+      eexists (z :: k'), k'', y. split; [done |].
+      by rewrite reverse_cons, <-app_assoc.
+  * intros [k' [k'' [y [??]]]]; subst.
+    revert l. induction k' as [|z k' IH]; intros l.
+    + by left.
+    + right. by rewrite reverse_cons, <-!app_assoc.
+Qed.
+
+Section zipped_list_ind.
+  Context {A} (P : list A → list A → Prop).
+  Context (Pnil : ∀ l, P l []).
+  Context (Pcons : ∀ l k x, P (x :: l) k → P l (x :: k)).
+
+  Fixpoint zipped_list_ind l k : P l k :=
+    match k with
+    | [] => Pnil _
+    | x :: k => Pcons _ _ _ (zipped_list_ind (x :: l) k)
+    end.
+End zipped_list_ind.
+
+Inductive zipped_Forall {A} (P : list A → list A → A → Prop) :
+    list A → list A → Prop :=
+  | zipped_Forall_nil l : zipped_Forall P l []
+  | zipped_Forall_cons l k x :
+     P l k x →
+     zipped_Forall P (x :: l) k →
+     zipped_Forall P l (x :: k).
+Arguments zipped_Forall_nil {_ _} _.
+Arguments zipped_Forall_cons {_ _} _ _ _ _ _.
+
+Lemma zipped_Forall_app {A} (P : list A → list A → A → Prop) l k k' :
+  zipped_Forall P l (k ++ k') → zipped_Forall P (reverse k ++ l) k'.
+Proof.
+  revert l. induction k as [|x k IH]; simpl; [done |].
+  inversion_clear 1. rewrite reverse_cons, <-app_assoc.
+  by apply IH.
+Qed.
diff --git a/theories/listset.v b/theories/listset.v
index 682319f0..4405464c 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -3,7 +3,7 @@
 (** 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 list collections.
+Require Export base decidable collections list.
 
 Definition listset A := sig (@NoDup A).
 
@@ -33,8 +33,8 @@ Lemma listset_difference_raw_nodup l k :
 Proof.
   induction 1; simpl; try case_decide.
   * constructor.
-  * easy.
-  * constructor. rewrite listset_difference_raw_in; intuition. easy.
+  * done.
+  * constructor. rewrite listset_difference_raw_in; intuition. done.
 Qed.
 Global Instance listset_difference: Difference (listset A) := λ l k,
   listset_difference_raw (`l) (`k)↾
@@ -51,8 +51,8 @@ Lemma listset_union_raw_nodup l k :
   NoDup l → NoDup k → NoDup (listset_union_raw l k).
 Proof.
   intros. apply NoDup_app.
-  * now apply listset_difference_raw_nodup.
-  * easy.
+  * by apply listset_difference_raw_nodup.
+  * done.
   * intro. rewrite listset_difference_raw_in. intuition.
 Qed.
 Global Instance listset_union: Union (listset A) := λ l k,
@@ -77,8 +77,8 @@ Lemma listset_intersection_raw_nodup l k :
 Proof.
   induction 1; simpl; try case_decide.
   * constructor.
-  * constructor. rewrite listset_intersection_raw_in; intuition. easy.
-  * easy.
+  * constructor. rewrite listset_intersection_raw_in; intuition. done.
+  * done.
 Qed.
 Global Instance listset_intersection: Intersection (listset A) := λ l k,
   listset_intersection_raw (`l) (`k)↾
@@ -99,14 +99,14 @@ Fixpoint listset_map_raw (f : A → A) (l : list A) :=
   | x :: l => listset_add_raw (f x) (listset_map_raw f l)
   end.
 Lemma listset_map_raw_nodup f l : NoDup (listset_map_raw f l).
-Proof. induction l; simpl. constructor. now apply listset_add_raw_nodup. Qed.
+Proof. induction l; simpl. constructor. by apply listset_add_raw_nodup. Qed.
 Lemma listset_map_raw_in f l x :
   In x (listset_map_raw f l) ↔ ∃ y, x = f y ∧ In y l.
 Proof.
   split.
-  * induction l; simpl; [easy |].
+  * induction l; simpl; [done |].
     rewrite listset_add_raw_in. firstorder.
-  * intros [?[??]]. subst. induction l; simpl in *; [easy |].
+  * intros [?[??]]. subst. induction l; simpl in *; [done |].
     rewrite listset_add_raw_in. firstorder congruence.
 Qed.
 Global Instance listset_map: Map A (listset A) := λ f l,
@@ -115,7 +115,7 @@ Global Instance listset_map: Map A (listset A) := λ f l,
 Global Instance: Collection A (listset A).
 Proof.
   split.
-  * easy.
+  * intros ? [].
   * compute. intuition.
   * intros. apply listset_union_raw_in.
   * intros. apply listset_intersection_raw_in.
@@ -126,5 +126,5 @@ Qed.
 Global Instance listset_elems: Elements A (listset A) := @proj1_sig _ _.
 
 Global Instance: FinCollection A (listset A).
-Proof. split. apply _. easy. now intros [??]. Qed.
+Proof. split. apply _. done. by intros [??]. Qed.
 End list_collection.
diff --git a/theories/nmap.v b/theories/nmap.v
index 1ee586ee..2fbf85f3 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -35,7 +35,7 @@ Global Instance Nmerge: Merge Nmap := λ A f t1 t2,
   match t1, t2 with
   | Build_Nmap o1 t1, Build_Nmap o2 t2 => Build_Nmap (f o1 o2) (merge f t1 t2)
   end.
-Global Instance Nfmap: FMap Nmap := λ A B f t,
+Global Instance Nfmap {A B} (f : A → B) : FMap Nmap f := λ t,
   match t with
   | Build_Nmap o t => Build_Nmap (fmap f o) (fmap f t)
   end.
@@ -44,19 +44,19 @@ Global Instance: FinMap N Nmap.
 Proof.
   split.
   * intros ? [??] [??] H. f_equal.
-    + now apply (H 0).
-    + apply finmap_eq. intros i. now apply (H (Npos i)).
-  * now intros ? [|?].
-  * intros ? f [? t] [|i].
-    + easy.
-    + now apply (lookup_partial_alter f t i).
-  * intros ? f [? t] [|i] [|j]; try intuition congruence.
-    intros. apply (lookup_partial_alter_ne f t i j). congruence.
-  * intros ??? [??] []. easy. apply lookup_fmap.
-  * intros ?? ???????? [o t] n; unfold dom, lookup, Ndom, Nlookup; simpl.
+    + apply (H 0).
+    + apply finmap_eq. intros i. apply (H (Npos i)).
+  * by intros ? [|?].
+  * intros ? f [? t] [|i]; simpl.
+    + done.
+    + apply lookup_partial_alter.
+  * 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 (simplify_is_Some; eauto).
-  * intros ? f ? [o1 t1] [o2 t2] [|?].
-    + easy.
+  * intros ? f ? [o1 t1] [o2 t2] [|?]; simpl.
+    + done.
     + apply (merge_spec f t1 t2).
 Qed.
diff --git a/theories/numbers.v b/theories/numbers.v
index dbf29a5b..4d09c4f8 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -1,19 +1,26 @@
 (* Copyright (c) 2012, Robbert Krebbers. *)
 (* This file is distributed under the terms of the BSD license. *)
-(** This file collects some trivial facts on Coq's number data types [nat],
-[N], and [Z], and introduces some useful notations. *)
+(** This file collects some trivial facts on the Coq types [nat] and [N] for
+natural numbers, and the type [Z] for integers. It also declares some useful
+notations. *)
 Require Export PArith NArith ZArith.
-Require Export base decidable fin_collections.
+Require Export base decidable.
 
 Infix "≤" := le : nat_scope.
-
 Instance nat_eq_dec: ∀ x y : nat, Decision (x = y) := eq_nat_dec.
+
+Lemma lt_n_SS n : n < S (S n).
+Proof. auto with arith. Qed.
+Lemma lt_n_SSS n : n < S (S (S n)).
+Proof. auto with arith. Qed.
+
 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.
 
 Infix "≤" := N.le : N_scope.
 Notation "(≤)" := N.le (only parsing) : N_scope.
+Notation "(<)" := N.lt (only parsing) : N_scope.
 
 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 :=
@@ -22,15 +29,23 @@ Program Instance N_le_dec (x y : N) : Decision (x ≤ y)%N :=
   | _ => left _
   end.
 Next Obligation. congruence. Qed.
+Program Instance N_lt_dec (x y : N) : Decision (x < y)%N :=
+  match Ncompare x y with
+  | Lt => left _
+  | _ => right _
+  end.
+Next Obligation. congruence. Qed.
 
 Infix "≤" := Z.le : Z_scope.
 Notation "(≤)" := Z.le (only parsing) : Z_scope.
+Notation "(<)" := Z.lt (only parsing) : Z_scope.
 Instance Z_eq_dec: ∀ x y : Z, Decision (x = y) := Z.eq_dec.
 Instance Z_le_dec: ∀ x y : Z, Decision (x ≤ y)%Z := Z_le_dec.
+Instance Z_lt_dec: ∀ x y : Z, Decision (x < y)%Z := Z_lt_dec.
 
 (** * Conversions *)
-(** Converts an integer [x] into a natural number by giving [None] in case [x]
-is negative. *)
+(** The function [Z_to_option_N] converts an integer [x] into a natural number
+by giving [None] in case [x] is negative. *)
 Definition Z_to_option_N (x : Z) : option N :=
   match x with
   | Z0 => Some N0
@@ -43,40 +58,8 @@ by yielding one if [P] holds and zero if [P] does not. *)
 Definition Z_decide (P : Prop) {dec : Decision P} : Z :=
   (if dec then 1 else 0)%Z.
 
-(** The function [Z_decide_rel] is the more efficient variant of [Z_decide] for
-decidable binary relations. It yields one if [R x y] and zero if not [R x y]. *)
+(** The function [Z_decide_rel] is the more efficient variant of [Z_decide] when
+used for binary relations. It yields one if [R x y] and zero if not [R x y]. *)
 Definition Z_decide_rel {A B} (R : A → B → Prop)
     {dec : ∀ x y, Decision (R x y)} (x : A) (y : B) : Z :=
   (if dec x y then 1 else 0)%Z.
-
-(** * Fresh binary naturals *)
-(** Given a finite set of binary naturals [N], we generate a fresh element by
-taking the maximum, and adding one to it. *)
-Definition Nmax `{Elements N C} : C → N := collection_fold Nmax 0%N.
-
-Instance Nmax_proper `{FinCollection N C} : Proper ((≡) ==> (=)) Nmax.
-Proof.
-  apply collection_fold_proper. intros.
-  rewrite !N.max_assoc. f_equal. apply N.max_comm.
-Qed.
-
-Lemma Nmax_max `{FinCollection N C} X x : x ∈ X → (x ≤ Nmax X)%N.
-Proof.
-  change ((λ b X, x ∈ X → (x ≤ b)%N) (collection_fold N.max 0%N X) X).
-  apply collection_fold_ind.
-  * solve_proper.
-  * solve_elem_of.
-  * solve_elem_of (eauto using N.le_max_l, N.le_max_r, N.le_trans).
-Qed.
-
-Instance Nfresh `{FinCollection N C} : Fresh N C := λ l, (1 + Nmax l)%N.
-Instance Nfresh_spec `{FinCollection N C} : FreshSpec N C.
-Proof.
-  split.
-  * intros. unfold fresh, Nfresh.
-    setoid_replace X with Y; [easy |].
-    now apply elem_of_equiv.
-  * intros X E. assert (1 ≤ 0)%N as []; [| easy].
-    apply N.add_le_mono_r with (Nmax X).
-    now apply Nmax_max.
-Qed.
diff --git a/theories/option.v b/theories/option.v
index 09beb718..517b0d0a 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -2,7 +2,7 @@
 (* This file is distributed under the terms of the BSD license. *)
 (** This file collects general purpose definitions and theorems on the option
 data type that are not in the Coq standard library. *)
-Require Export base tactics decidable orders.
+Require Export base tactics decidable.
 
 (** * General definitions and theorems *)
 (** Basic properties about equality. *)
@@ -36,12 +36,12 @@ Lemma option_eq {A} (x y : option A) :
   x = y ↔ ∀ a, x = Some a ↔ y = Some a.
 Proof.
   split.
-  { intros. now subst. }
+  { intros. by subst. }
   intros E. destruct x, y.
-  + now apply E.
-  + symmetry. now apply E.
-  + now apply E.
-  + easy.
+  + by apply E.
+  + symmetry. by apply E.
+  + by apply E.
+  + done.
 Qed.
 
 (** We define [is_Some] as a [sig] instead of a [sigT] as extraction of
@@ -97,44 +97,46 @@ Instance option_eq_dec `{dec : ∀ x y : A, Decision (x = y)}
   end.
 
 (** * Monadic operations *)
-Instance option_ret: MRet option := @Some.
-Instance option_bind: MBind option := λ A B f x,
+Instance option_bind {A B} (f : A → option B) : MBind option f := λ x,
   match x with
   | Some a => f a
   | None => None
   end.
-Instance option_join: MJoin option := λ A x,
+Instance option_join {A} : MJoin option := λ x : option (option A),
   match x with
   | Some x => x
   | None => None
   end.
-Instance option_fmap: FMap option := @option_map.
+Instance option_fmap {A B} (f : A → B) : FMap option f := option_map f.
 
 Lemma option_fmap_is_Some {A B} (f : A → B) (x : option A) :
   is_Some x ↔ is_Some (f <$> x).
-Proof. destruct x; split; intros [??]; subst; compute; eauto; discriminate. Qed.
+Proof. destruct x; split; intros [??]; subst; compute; by eauto. Qed.
 Lemma option_fmap_is_None {A B} (f : A → B) (x : option A) :
   x = None ↔ f <$> x = None.
 Proof. unfold fmap, option_fmap. destruct x; simpl; split; congruence. Qed.
 
-Ltac simplify_option_bind := repeat
+Tactic Notation "simplify_option_bind" "by" tactic3(tac) := repeat
   match goal with
-  | |- context C [mbind (M:=option) ?f None] =>
-    let X := (context C [ None ]) in change X
-  | H : context C [mbind (M:=option) ?f None] |- _ =>
-    let X := (context C [ None ]) in change X in H
-  | |- context C [mbind (M:=option) ?f (Some ?a)] =>
-    let X := (context C [ f a ]) in
-    let X' := eval simpl in X in change X'
-  | H : context C [mbind (M:=option) ?f (Some ?a)] |- _ =>
-    let X := context C [ f a ] in
-    let X' := eval simpl in X in change X' in H
-  | _ => progress simplify_equality
+  | _ => 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;
+    let Hx := fresh in
+    assert (o = Some x') as Hx by tac;
+    rewrite Hx in H; clear Hx
   | 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:?
-  | H : context [ ?o = _ ] |- mbind (M:=option) ?f ?o = ?x =>
-    erewrite H by eauto
+  | |- 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;
+    let Hx := fresh in
+    assert (o = Some x') as Hx by tac;
+    rewrite Hx; clear Hx
   end.
+Tactic Notation "simplify_option_bind" := simplify_option_bind by eauto.
 
 (** * Union, intersection and difference *)
 Instance option_union: UnionWith option := λ A f x y,
@@ -160,39 +162,39 @@ Section option_union_intersection.
   Context {A} (f : A → A → A).
 
   Global Instance: LeftId (=) None (union_with f).
-  Proof. now intros [?|]. Qed.
+  Proof. by intros [?|]. Qed.
   Global Instance: RightId (=) None (union_with f).
-  Proof. now intros [?|]. Qed.
+  Proof. by intros [?|]. Qed.
   Global Instance: Commutative (=) f → Commutative (=) (union_with f).
   Proof.
     intros ? [?|] [?|]; compute; try reflexivity.
-    now rewrite (commutative f).
+    by rewrite (commutative f).
   Qed.
   Global Instance: Associative (=) f → Associative (=) (union_with f).
   Proof.
     intros ? [?|] [?|] [?|]; compute; try reflexivity.
-    now rewrite (associative f).
+    by rewrite (associative f).
   Qed.
   Global Instance: Idempotent (=) f → Idempotent (=) (union_with f).
   Proof.
     intros ? [?|]; compute; try reflexivity.
-    now rewrite (idempotent f).
+    by rewrite (idempotent f).
   Qed.
 
   Global Instance: Commutative (=) f → Commutative (=) (intersection_with f).
   Proof.
     intros ? [?|] [?|]; compute; try reflexivity.
-    now rewrite (commutative f).
+    by rewrite (commutative f).
   Qed.
   Global Instance: Associative (=) f → Associative (=) (intersection_with f).
   Proof.
     intros ? [?|] [?|] [?|]; compute; try reflexivity.
-    now rewrite (associative f).
+    by rewrite (associative f).
   Qed.
   Global Instance: Idempotent (=) f → Idempotent (=) (intersection_with f).
   Proof.
     intros ? [?|]; compute; try reflexivity.
-    now rewrite (idempotent f).
+    by rewrite (idempotent f).
   Qed.
 End option_union_intersection.
 
@@ -200,5 +202,5 @@ Section option_difference.
   Context {A} (f : A → A → option A).
 
   Global Instance: RightId (=) None (difference_with f).
-  Proof. now intros [?|]. Qed.
+  Proof. by intros [?|]. Qed.
 End option_difference.
diff --git a/theories/orders.v b/theories/orders.v
index a763f908..db32b3a2 100644
--- a/theories/orders.v
+++ b/theories/orders.v
@@ -2,7 +2,8 @@
 (* 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 base.
+Require Import SetoidList.
+Require Export base decidable tactics list.
 
 (** * Pre-orders *)
 (** We extend a pre-order to a partial order by defining equality as
@@ -26,8 +27,12 @@ Section preorder.
     * transitivity x1. tauto. transitivity x2; tauto.
     * transitivity y1. tauto. transitivity y2; tauto.
   Qed.
-End preorder.
 
+  Context `{∀ X Y : A, Decision (X ⊆ Y)}.
+  Global Instance preorder_equiv_dec_slow (X Y : A) :
+    Decision (X ≡ Y) | 100 := _.
+End preorder.
+Typeclasses Opaque preorder_equiv.
 Hint Extern 0 (@Equivalence _ (≡)) =>
   class_apply preorder_equivalence : typeclass_instances.
 
@@ -47,7 +52,7 @@ Section bounded_join_sl.
   Lemma union_compat x1 x2 y1 y2 : x1 ⊆ x2 → y1 ⊆ y2 → x1 ∪ y1 ⊆ x2 ∪ y2.
   Proof. auto. Qed.
   Lemma union_empty x : x ∪ ∅ ⊆ x.
-  Proof. apply union_least. easy. auto. Qed.
+  Proof. by apply union_least. Qed.
   Lemma union_comm x y : x ∪ y ⊆ y ∪ x.
   Proof. auto. Qed.
   Lemma union_assoc_1 x y z : (x ∪ y) ∪ z ⊆ x ∪ (y ∪ z).
@@ -55,7 +60,7 @@ Section bounded_join_sl.
   Lemma union_assoc_2 x y z : x ∪ (y ∪ z) ⊆ (x ∪ y) ∪ z.
   Proof. auto. Qed.
 
-  Global Instance: Proper ((≡) ==> (≡) ==> (≡)) (∪).
+  Global Instance union_proper: Proper ((≡) ==> (≡) ==> (≡)) (∪).
   Proof.
     unfold equiv, preorder_equiv. split; apply union_compat; simpl in *; tauto.
   Qed.
@@ -79,6 +84,33 @@ Section bounded_join_sl.
 
   Lemma equiv_empty X : X ⊆ ∅ → X ≡ ∅.
   Proof. split; eauto. Qed.
+
+  Global Instance: Proper (eqlistA (≡) ==> (≡)) union_list.
+  Proof.
+    induction 1; simpl.
+    * done.
+    * by apply union_proper.
+  Qed.
+
+  Lemma empty_union X Y : X ∪ Y ≡ ∅ ↔ X ≡ ∅ ∧ Y ≡ ∅.
+  Proof.
+    split.
+    * intros E. split; apply equiv_empty;
+        by transitivity (X ∪ Y); [auto | rewrite E].
+    * intros [E1 E2]. by rewrite E1, E2, (left_id _ _).
+  Qed.
+  Lemma empty_list_union Xs : ⋃ Xs ≡ ∅ ↔ Forall (≡ ∅) Xs.
+  Proof.
+    split.
+    * induction Xs; simpl; rewrite ?empty_union; intuition.
+    * induction 1 as [|?? E1 ? E2]; simpl. done. by apply empty_union.
+  Qed.
+
+  Context `{∀ X Y : A, Decision (X ⊆ Y)}.
+  Lemma non_empty_union X Y : X ∪ Y ≢ ∅ → X ≢ ∅ ∨ Y ≢ ∅.
+  Proof. rewrite empty_union. destruct (decide (X ≡ ∅)); intuition. Qed.
+  Lemma non_empty_list_union Xs : ⋃ Xs ≢ ∅ → Exists (≢ ∅) Xs.
+  Proof. rewrite empty_list_union. apply (not_Forall_Exists _). Qed.
 End bounded_join_sl.
 
 (** * Meet semi lattices *)
@@ -123,3 +155,17 @@ Section meet_sl.
   Lemma subseteq_intersection_2 X Y : X ∩ Y ≡ X → X ⊆ Y.
   Proof. apply subseteq_intersection. Qed.
 End meet_sl.
+
+(** * Lower bounded lattices *)
+Section lower_bounded_lattice.
+  Context `{LowerBoundedLattice A}.
+
+  Global Instance: LeftAbsorb (≡) ∅ (∩).
+  Proof.
+    split.
+    * by apply subseteq_intersection_l.
+    * by apply subseteq_empty.
+  Qed.
+  Global Instance: RightAbsorb (≡) ∅ (∩).
+  Proof. intros ?. by rewrite (commutative _), (left_absorb _ _). Qed.
+End lower_bounded_lattice.
diff --git a/theories/pmap.v b/theories/pmap.v
index b8a35bb7..d6a54ad0 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -14,13 +14,6 @@ Local Open Scope positive_scope.
 Local Hint Extern 0 (@eq positive _ _) => congruence.
 Local Hint Extern 0 (¬@eq positive _ _) => congruence.
 
-(** Enable unfolding of the finite map operations in this file. *)
-Local Arguments lookup _ _ _ _ _ !_ /.
-Local Arguments partial_alter _ _ _ _ _ _ !_ /.
-Local Arguments fmap _ _ _ _ _ !_ /.
-Local Arguments merge _ _ _ _ !_ _ /.
-Local Arguments mbind _ _ _ _ _ !_/.
-
 (** * The tree data structure *)
 (** The data type [Pmap_raw] specifies radix-2 search trees. These trees do
 not ensure canonical representations of maps. For example the empty map can
@@ -46,10 +39,9 @@ Local Hint Constructors Pmap_ne.
 Instance Pmap_ne_dec `(t : Pmap_raw A) : Decision (Pmap_ne t).
 Proof.
   red. induction t as [|? IHl [?|] ? IHr].
-  * right. now inversion 1.
-  * now intuition.
-  * destruct IHl, IHr; try solve [left; auto]; right;
-      inversion_clear 1; contradiction.
+  * right. by inversion 1.
+  * intuition.
+  * destruct IHl, IHr; try (by left; auto); right; by inversion_clear 1.
 Qed.
 
 (** The following predicate describes well well formed trees. A tree is well
@@ -65,10 +57,11 @@ Instance Pmap_wf_dec `(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; inversion_clear 1; intuition.
+  * destruct IHl, IHr; try solve [left; intuition auto];
+      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.
+      try solve [left; intuition auto];
+      right; inversion_clear 1; intuition.
 Qed.
 
 (** Now we restrict the data type of trees to those that are well formed. *)
@@ -100,14 +93,14 @@ Instance Plookup_raw: Lookup positive Pmap_raw :=
 Global Instance Plookup: Lookup positive Pmap := λ A i t, `t !! i.
 
 Lemma Plookup_raw_empty {A} i : (∅ : Pmap_raw A) !! i = None.
-Proof. now destruct i. Qed.
+Proof. by destruct i. Qed.
 
 Lemma Pmap_ne_lookup `(t : Pmap_raw A) : Pmap_ne t → ∃ i x, t !! i = Some x.
 Proof.
   induction 1 as [? x ?| l r ? IHl | l r ? IHr].
-  * intros. now exists 1 x.
-  * destruct IHl as [i [x ?]]. now exists (i~0) x.
-  * destruct IHr as [i [x ?]]. now exists (i~1) x.
+  * intros. by exists 1 x.
+  * destruct IHl as [i [x ?]]. by exists (i~0) x.
+  * destruct IHr as [i [x ?]]. by exists (i~1) x.
 Qed.
 
 Lemma Pmap_wf_eq_get {A} (t1 t2 : Pmap_raw A) :
@@ -116,29 +109,29 @@ Proof.
   intros t1wf. revert t2.
   induction t1wf as [| ? x ? ? IHl ? IHr | l r ? IHl ? IHr Hne1 ].
   * destruct 1 as [| | ???? [?|?]]; intros Hget.
-    + easy.
+    + done.
     + discriminate (Hget 1).
-    + destruct (Pmap_ne_lookup l) as [i [??]]; auto.
+    + destruct (Pmap_ne_lookup l) as [i [??]]; trivial.
       specialize (Hget (i~0)). simpl in *. congruence.
-    + destruct (Pmap_ne_lookup r) as [i [??]]; auto.
+    + destruct (Pmap_ne_lookup r) as [i [??]]; trivial.
       specialize (Hget (i~1)). simpl in *. congruence.
   * destruct 1; intros Hget.
     + discriminate (Hget xH).
     + f_equal.
-      - apply IHl; auto. intros i. now apply (Hget (i~0)).
-      - now apply (Hget 1).
-      - apply IHr; auto. intros i. now apply (Hget (i~1)).
+      - apply IHl; trivial. intros i. apply (Hget (i~0)).
+      - apply (Hget 1).
+      - apply IHr; trivial. intros i. apply (Hget (i~1)).
     + specialize (Hget 1). simpl in *. congruence.
   * destruct 1; intros Hget.
     + destruct Hne1.
-      destruct (Pmap_ne_lookup l) as [i [??]]; auto.
+      destruct (Pmap_ne_lookup l) as [i [??]]; trivial.
       - specialize (Hget (i~0)). simpl in *. congruence.
-      - destruct (Pmap_ne_lookup r) as [i [??]]; auto.
+      - destruct (Pmap_ne_lookup r) as [i [??]]; trivial.
         specialize (Hget (i~1)). simpl in *. congruence.
     + specialize (Hget 1). simpl in *. congruence.
     + f_equal.
-      - apply IHl; auto. intros i. now apply (Hget (i~0)).
-      - apply IHr; auto. intros i. now apply (Hget (i~1)).
+      - apply IHl; trivial. intros i. apply (Hget (i~0)).
+      - apply IHr; trivial. intros i. apply (Hget (i~1)).
 Qed.
 
 Fixpoint Psingleton_raw {A} (i : positive) (x : A) : Pmap_raw A :=
@@ -156,7 +149,7 @@ Proof. induction i; simpl; intuition. Qed.
 Local Hint Resolve Psingleton_raw_wf.
 
 Lemma Plookup_raw_singleton {A} i (x : A) : Psingleton_raw i x !! i = Some x.
-Proof. now induction i. Qed.
+Proof. by induction i. Qed.
 Lemma Plookup_raw_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.
@@ -174,13 +167,13 @@ 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.
-Proof. now destruct l,o,r. Qed.
+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.
-Proof. now destruct l,o,r. Qed.
+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.
-Proof. now destruct l,o,r. Qed.
+Proof. by destruct l,o,r. Qed.
 Ltac Pnode_canon_rewrite := repeat (
   rewrite Pnode_canon_lookup_xH ||
   rewrite Pnode_canon_lookup_xO ||
@@ -219,43 +212,43 @@ Lemma Plookup_raw_alter {A} f i (t : Pmap_raw A) :
   partial_alter f i t !! i = f (t !! i).
 Proof.
   revert i. induction t.
-  * simpl. case (f None).
-    + intros. now apply Plookup_raw_singleton.
-    + now destruct i.
-  * intros [?|?|]; simpl; Pnode_canon_rewrite; auto.
+  * intros i. unfold partial_alter, lookup. simpl. case (f None).
+    + intros. apply Plookup_raw_singleton.
+    + by destruct i.
+  * intros [?|?|]; simpl; by Pnode_canon_rewrite.
 Qed.
 Lemma Plookup_raw_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].
-  * simpl. intros. case (f None).
-    + intros. now apply Plookup_raw_singleton_ne.
-    + easy.
+  * intros. unfold partial_alter, lookup. simpl. case (f None).
+    + intros. by apply Plookup_raw_singleton_ne.
+    + done.
   * intros [?|?|] [?|?|]; simpl; Pnode_canon_rewrite; auto; congruence.
 Qed.
 
-Instance Pfmap_raw: FMap Pmap_raw :=
-  fix Pfmap_raw A B f (t : Pmap_raw A) : Pmap_raw B :=
+Instance Pfmap_raw {A B} (f : A → B) : FMap Pmap_raw f :=
+  fix Pfmap_raw (t : Pmap_raw A) : Pmap_raw B :=
   match t with
   | Pleaf => Pleaf
   | Pnode l x r =>
-    Pnode (@fmap _ Pfmap_raw _ _ f l) (fmap f x) (@fmap _ Pfmap_raw _ _ f r)
+    Pnode (@fmap _ _ _ f Pfmap_raw l) (fmap f x) (@fmap _ _ _ f Pfmap_raw r)
   end.
 
 Lemma Pfmap_raw_ne `(f : A → B) (t : Pmap_raw A) :
   Pmap_ne t → Pmap_ne (fmap f t).
-Proof. induction 1; simpl; auto. Qed.
+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).
 Proof. induction 1; simpl; intuition auto. Qed.
 
-Global Instance Pfmap: FMap Pmap := λ A B f t,
+Global Instance Pfmap {A B} (f : A → B) : FMap Pmap f := λ t,
   dexist _ (Pfmap_raw_wf f _ (proj2_dsig t)).
 
 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. easy. intros [?|?|]; simpl; auto. Qed.
+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. *)
@@ -276,8 +269,8 @@ Section dom.
     * 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 (now apply (IHl (f ∘ (~0)))
-        || now apply (IHr (f ∘ (~1))) || simplify_is_Some).
+        solve_elem_of (by apply (IHl (f ∘ (~0)))
+        || by apply (IHr (f ∘ (~1))) || simplify_is_Some).
   Qed.
 End dom.
 
@@ -299,7 +292,7 @@ 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).
 Proof.
-  revert i. induction t as [| l IHl o r IHr ]; [easy |].
+  revert i. induction t as [| l IHl o r IHr ]; [done |].
   intros [?|?|]; simpl; Pnode_canon_rewrite; auto.
 Qed.
 
@@ -325,24 +318,24 @@ Lemma Pmerge_raw_spec {A} f (Hf : f None None = None) (t1 t2 : Pmap_raw A) i :
   merge f t1 t2 !! i = f (t1 !! i) (t2 !! i).
 Proof.
   revert t2 i. induction t1 as [| l1 IHl1 o1 r1 IHr1 ].
-  * simpl. now apply Pmerge_aux_spec.
+  * intros. unfold merge. simpl. by rewrite Pmerge_aux_spec.
   * destruct t2 as [| l2 o2 r2 ].
-    + unfold merge, Pmerge_raw. intros. now rewrite Pmerge_aux_spec.
-    + intros [?|?|]; simpl; Pnode_canon_rewrite; auto.
+    + unfold merge, Pmerge_raw. intros. by rewrite Pmerge_aux_spec.
+    + intros [?|?|]; simpl; by Pnode_canon_rewrite.
 Qed.
 
 Global Instance: FinMap positive Pmap.
 Proof.
   split.
   * intros ? [t1?] [t2?]. intros. apply dsig_eq. simpl.
-    apply Pmap_wf_eq_get; auto; now apply (bool_decide_unpack _).
-  * now destruct i.
-  * intros ?? [??] ?. now apply Plookup_raw_alter.
-  * intros ?? [??] ??. now apply Plookup_raw_alter_ne.
-  * intros ??? [??]. now apply Plookup_raw_fmap.
+    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 ?????????? [??] i. unfold dom, Pdom.
     rewrite Plookup_raw_dom. unfold id. split.
-    + intros [? [??]]. now subst.
-    + firstorder.
-  * intros ??? [??] [??] ?. now apply Pmerge_raw_spec.
+    + intros [? [??]]. by subst.
+    + naive_solver.
+  * intros ??? [??] [??] ?. by apply Pmerge_raw_spec.
 Qed.
diff --git a/theories/prelude.v b/theories/prelude.v
index 39beaa8d..3712495c 100644
--- a/theories/prelude.v
+++ b/theories/prelude.v
@@ -7,8 +7,10 @@ Require Export
   orders
   option
   list
+  vector
+  numbers
   collections
   fin_collections
   listset
   subset
-  numbers.
+  fresh_numbers.
diff --git a/theories/subset.v b/theories/subset.v
index 00a45e95..b75ecc95 100644
--- a/theories/subset.v
+++ b/theories/subset.v
@@ -16,4 +16,4 @@ Instance subset_difference {A} : Difference (subset A) := λ P Q x, P x ∧ ¬Q
 Instance subset_map {A} : Map A (subset A) := λ f P x, ∃ y, f y = x ∧ P y.
 
 Instance subset_container: Collection A (subset A) | 100.
-Proof. firstorder try congruence. Qed.
+Proof. firstorder congruence. Qed.
diff --git a/theories/tactics.v b/theories/tactics.v
index ea2b9ce0..f29ec03f 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -4,18 +4,104 @@
 the development. *)
 Require Export base.
 
+(** A slightly modified version of Ssreflect's finishing tactic [done]. It
+also performs [reflexivity] and does not compute the goal's [hnf] so as to
+avoid unfolding setoid equalities. Note that this tactic performs much better
+than Coq's [easy] as it does not perform [inversion]. *)
+Ltac done :=
+  trivial; intros; solve
+    [ repeat first
+      [ solve [trivial]
+      | solve [symmetry; trivial]
+      | reflexivity
+      | discriminate
+      | contradiction
+      | split ]
+    | match goal with
+      H : ¬_ |- _ => solve [destruct H; trivial]
+      end ].
+Tactic Notation "by" tactic(tac) :=
+  tac; done.
+
+(** The tactic [clear dependent H1 ... Hn] clears the hypotheses [Hi] and
+their dependencies. *)
+Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) :=
+  clear dependent H1; clear dependent H2.
+Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) hyp(H3) :=
+  clear dependent H1 H2; clear dependent H3.
+Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) hyp(H3) hyp(H4) :=
+  clear dependent H1 H2 H3; clear dependent H4.
+Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) hyp(H3) hyp(H4)
+  hyp(H5) := clear dependent H1 H2 H3 H4; clear dependent H5.
+Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) hyp(H3) hyp(H4) hyp(H5)
+  hyp (H6) := clear dependent H1 H2 H3 H4 H5; clear dependent H6.
+Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) hyp(H3) hyp(H4) hyp(H5)
+  hyp (H6) hyp(H7) := clear dependent H1 H2 H3 H4 H5 H6; clear dependent H7.
+Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) hyp(H3) hyp(H4) hyp(H5)
+  hyp (H6) hyp(H7) hyp(H8) :=
+  clear dependent H1 H2 H3 H4 H5 H6 H7; clear dependent H8.
+Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) hyp(H3) hyp(H4) hyp(H5)
+  hyp (H6) hyp(H7) hyp(H8) hyp(H9) :=
+  clear dependent H1 H2 H3 H4 H5 H6 H7 H8; clear dependent H9.
+Tactic Notation "clear" "dependent" hyp(H1) hyp(H2) hyp(H3) hyp(H4) hyp(H5)
+  hyp (H6) hyp(H7) hyp(H8) hyp(H9) hyp(H10) :=
+  clear dependent H1 H2 H3 H4 H5 H6 H7 H8 H9; clear dependent H10.
+
+(** The tactic [first_of tac1 tac2] calls [tac1] and then calls [tac2] on the
+first subgoal generated by [tac1] *)
+Tactic Notation "first_of" tactic3(tac1) "by" tactic3(tac2) :=
+     (tac1; [ tac2 ])
+  || (tac1; [ tac2 |])
+  || (tac1; [ tac2 | | ])
+  || (tac1; [ tac2 | | | ])
+  || (tac1; [ tac2 | | | | ])
+  || (tac1; [ tac2 | | | | | ])
+  || (tac1; [ tac2 | | | | | |])
+  || (tac1; [ tac2 | | | | | | |])
+  || (tac1; [ tac2 | | | | | | | |])
+  || (tac1; [ tac2 | | | | | | | | |])
+  || (tac1; [ tac2 | | | | | | | | | |])
+  || (tac1; [ tac2 | | | | | | | | | | |])
+  || (tac1; [ tac2 | | | | | | | | | | | |]).
+
+(** The tactic [is_non_dependent H] determines whether the goal's conclusion or
+assumptions depend on [H]. *)
+Tactic Notation "is_non_dependent" constr(H) :=
+  match goal with
+  | _ : context [ H ] |- _ => fail 1
+  | |- context [ H ] => fail 1
+  | _ => idtac
+  end.
+
+(* The tactic [var_eq x y] fails if [x] and [y] are unequal. *)
+Ltac var_eq x1 x2 := match x1 with x2 => idtac | _ => fail 1 end.
+Ltac var_neq x1 x2 := match x1 with x2 => fail 1 | _ => idtac end.
+
+Tactic Notation "repeat_on_hyps" tactic3(tac) :=
+  repeat match goal with H : _ |- _ => progress tac H end.
+
+Ltac block_hyps := repeat_on_hyps (fun H =>
+  match type of H with
+  | block _ => idtac
+  | ?T => change (block T) in H
+  end).
+Ltac unblock_hyps := unfold block in * |-.
+
+(** The tactic [injection' H] is a variant of injection that introduces the
+generated equalities. *)
+Ltac injection' H :=
+  block_goal; injection H; clear H; intros; unblock_goal.
+
 (** The tactic [simplify_equality] repeatedly substitutes, discriminates,
 and injects equalities, and tries to contradict impossible inequalities. *)
 Ltac simplify_equality := repeat
   match goal with
-  | |- _ => progress subst
-  | |- _ = _ => reflexivity
-  | H : _ ≠ _ |- _ => now destruct H
-  | H : _ = _ → False |- _ => now destruct H
+  | H : _ ≠ _ |- _ => by destruct H
+  | H : _ = _ → False |- _ => by destruct H
+  | H : ?x = _ |- _ => subst x
+  | H : _ = ?x |- _ => subst x
   | H : _ = _ |- _ => discriminate H
-  | H : _ = _ |-  ?G =>
-    (* avoid introducing additional equalities *)
-    change (id G); injection H; clear H; intros; unfold id at 1
+  | H : _ = _ |- _ => injection' H
   end.
 
 (** Coq's default [remember] tactic does have an option to name the generated
@@ -26,13 +112,12 @@ Tactic Notation "remember" constr(t) "as" "(" ident(x) "," ident(E) ")" :=
   | E' : x = _ |- _ => rename E' into E
   end.
 
-(** Given a list [l], the tactic [map tac l] runs [tac x] for each element [x]
-of the list [l]. It will succeed for the first element [x] of [l] for which 
-[tac x] succeeds. *)
-Tactic Notation "map" tactic(tac) tactic(l) :=
+(** Given a tactic [tac2] generating a list of terms, [iter tac1 tac2]
+runs [tac x] for each element [x] until [tac x] succeeds. If it does not
+suceed for any element of the generated list, the whole tactic wil fail. *)
+Tactic Notation "iter" tactic(tac) tactic(l) :=
   let rec go l :=
   match l with
-  | nil => idtac
   | ?x :: ?l => tac x || go l
   end in go l.
 
@@ -97,15 +182,6 @@ Tactic Notation "feed" "destruct" constr(H) :=
 Tactic Notation "feed" "destruct" constr(H) "as" simple_intropattern(IP) :=
   feed (fun p => let H':=fresh in pose proof p as H'; destruct H' as IP) H.
 
-(** The tactic [is_non_dependent H] determines whether the goal's conclusion or
-assumptions depend on [H]. *)
-Tactic Notation "is_non_dependent" constr(H) :=
-  match goal with
-  | _ : context [ H ] |- _ => fail 1
-  | |- context [ H ] => fail 1
-  | _ => idtac
-  end.
-
 (** Coq's [firstorder] tactic fails or loops on rather small goals already. In 
 particular, on those generated by the tactic [unfold_elem_ofs] to solve
 propositions on collections. The [naive_solver] tactic implements an ad-hoc
@@ -134,9 +210,7 @@ Tactic Notation "naive_solver" tactic(tac) :=
   | |- _ => progress simpl in *
   | |- _ => progress simplify_equality
   (**i solve the goal *)
-  | |- _ => eassumption
-  | |- _ => now constructor
-  | |- _ => now symmetry
+  | |- _ => solve [ eassumption | symmetry; eassumption | reflexivity ]
   (**i operations that generate more subgoals *)
   | |- _ ∧ _ => split
   | H : _ ∨ _ |- _ => destruct H
diff --git a/theories/vector.v b/theories/vector.v
new file mode 100644
index 00000000..101bfaab
--- /dev/null
+++ b/theories/vector.v
@@ -0,0 +1,341 @@
+(* Copyright (c) 2012, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** This file collects general purpose definitions and theorems on vectors
+(lists of fixed length) and the fin type (bounded naturals). It uses the
+definitions from the standard library, but renames or changes their notations,
+so that it becomes more consistent with the naming conventions in this
+development. *)
+Require Import list.
+Open Scope vector_scope.
+
+(** * The fin type *)
+(** The type [fin n] represents natural numbers [i] with [0 ≤ i < n]. We
+define a scope [fin], in which we declare notations for small literals of the
+[fin] type. Whereas the standard library starts counting at [1], we start
+counting at [0]. This way, the embedding [fin_to_nat] preserves [0], and allows
+us to define [fin_to_nat] as a coercion without introducing notational
+ambiguity. *)
+Notation fin := Fin.t.
+Notation FS := Fin.FS.
+
+Delimit Scope fin_scope with fin.
+Arguments Fin.FS _ _%fin.
+
+Notation "0" := Fin.F1 : fin_scope.
+Notation "1" := (FS 0) : fin_scope.
+Notation "2" := (FS 1) : fin_scope.
+Notation "3" := (FS 2) : fin_scope.
+Notation "4" := (FS 3) : fin_scope.
+Notation "5" := (FS 4) : fin_scope.
+Notation "6" := (FS 5) : fin_scope.
+Notation "7" := (FS 6) : fin_scope.
+Notation "8" := (FS 7) : fin_scope.
+Notation "9" := (FS 8) : fin_scope.
+Notation "10" := (FS 9) : fin_scope.
+
+Fixpoint fin_to_nat {n} (i : fin n) : nat :=
+  match i with
+  | 0%fin => 0
+  | FS _ i => S (fin_to_nat i)
+  end.
+Coercion fin_to_nat : fin >-> nat.
+
+Notation fin_rect2 := Fin.rect2.
+Notation FS_inj := Fin.FS_inj.
+
+Instance fin_dec {n} : ∀ i j : fin n, Decision (i = j).
+Proof.
+ refine (fin_rect2
+  (λ n (i j : fin n), { i = j } + { i ≠ j })
+  (λ _, left _)
+  (λ _ _, right _)
+  (λ _ _, right _)
+  (λ _ _ _ H, cast_if H));
+  abstract (f_equal; by auto using FS_inj).
+Defined.
+
+(** The inversion principle [fin_S_inv] is more convenient than its variant
+[Fin.caseS] in the standard library, as we keep the parameter [n] fixed.
+In the tactic [inv_fin i] to perform dependent case analysis on [i], we
+therefore do not have to generalize over the index [n] and all assumptions
+depending on it. Notice that contrary to [dependent destruction], which uses
+the [JMeq_eq] axiom, the tactic [inv_fin] produces axiom free proofs.*)
+Notation fin_0_inv := Fin.case0.
+
+Definition fin_S_inv {n} (P : fin (S n) → Type)
+  (H0 : P 0%fin) (HS : ∀ i, P (FS i)) (i : fin (S n)) : P i.
+Proof.
+ revert P H0 HS. refine (
+  match i with
+  | 0%fin => λ _ H0 _, H0
+  | FS _ i => λ _ _ HS, HS i
+  end).
+Defined.
+
+Ltac inv_fin i :=
+  match type of i with
+  | fin 0 =>
+    revert dependent i;
+    match goal with
+    |- ∀ i, @?P i => apply (fin_0_inv P)
+    end
+  | fin (S ?n) =>
+    revert dependent i;
+    match goal with
+    |- ∀ i, @?P i => apply (fin_S_inv P)
+    end
+  end.
+
+(** * Vectors *)
+(** The type [vec n] represents lists of consisting of exactly [n] elements.
+Whereas the standard library declares exactly the same notations for vectors as
+used for lists, we use slightly different notations so it becomes easier to use
+lists and vectors together. *)
+Notation vec := Vector.t.
+Notation vnil := Vector.nil.
+Arguments vnil {_}.
+Notation vcons := Vector.cons.
+Notation vapp := Vector.append.
+Arguments vcons {_} _ {_} _.
+
+Infix ":::" := vcons (at level 60, right associativity) : vector_scope.
+Notation "[# ] " := vnil : vector_scope.
+Notation "[# x ] " := (vcons x vnil) : vector_scope.
+Notation "[# x ; .. ; y ] " := (vcons x .. (vcons y vnil) ..) : vector_scope.
+
+Infix "+++" := vapp (at level 60, right associativity) : vector_scope.
+
+(** Notice that we cannot define [Vector.nth] as an instance of our [Lookup]
+type class, as it has a dependent type. *)
+Arguments Vector.nth {_ _} !_ !_%fin /.
+Infix "!!!" := Vector.nth (at level 20) : vector_scope.
+
+(** The tactic [vec_double_ind v1 v2] performs double induction on [v1] and [v2]
+provided that they have the same length. *)
+Notation vec_rect2 := Vector.rect2.
+Ltac vec_double_ind v1 v2 :=
+  match type of v1 with
+  | vec _ ?n =>
+    repeat match goal with
+    | H' : context [ n ] |- _ =>
+      var_neq v1 H'; var_neq v2 H'; revert H'
+    end;
+    revert n v1 v2;
+    match goal with
+    | |- ∀ n v1 v2, @?P n v1 v2 => apply (vec_rect2 P)
+    end
+  end.
+
+Notation vcons_inj := VectorSpec.cons_inj.
+Lemma vcons_inj_1 {A n} x y (v w : vec A n) : x ::: v = y ::: w → x = y.
+Proof. apply vcons_inj. Qed.
+Lemma vcons_inj_2 {A n} x y (v w : vec A n) : x ::: v = y ::: w → v = w.
+Proof. apply vcons_inj. Qed.
+
+Instance vec_dec {A} {dec : ∀ x y : A, Decision (x = y)} {n} :
+  ∀ v w : vec A n, Decision (v = w).
+Proof.
+ refine (vec_rect2
+  (λ n (v w : vec A n), { v = w } + { v ≠ w })
+  (left _)
+  (λ _ _ _ H x y, cast_if_and (dec x y) H));
+  f_equal; eauto using vcons_inj_1, vcons_inj_2.
+Defined.
+
+(** Similar to [fin], we provide an inversion principle that keeps the length
+fixed. We define a tactic [inv_vec v] to perform case analysis on [v], using
+this inversion principle. *)
+Notation vec_0_inv := Vector.case0.
+Definition vec_S_inv {A n} (P : vec A (S n) → Type)
+  (Hcons : ∀ x v, P (x ::: v)) v : P v.
+Proof.
+ revert P Hcons. refine (
+  match v with
+  | [#] => tt
+  | x ::: v => λ P Hcons, Hcons x v
+  end).
+Defined.
+
+Ltac inv_vec v :=
+  match type of v with
+  | vec _ 0 =>
+    revert dependent v;
+    match goal with
+    |- ∀ v, @?P v => apply (vec_0_inv P)
+    end
+  | vec _ (S ?n) =>
+    revert dependent v;
+    match goal with
+    |- ∀ v, @?P v => apply (vec_S_inv P)
+    end
+  end.
+
+(** The following tactic performs case analysis on all hypotheses of the shape
+[fin 0], [fin (S n)], [vec A 0] and [vec A (S n)] until no further case
+analyses are possible. *)
+Ltac inv_all_vec_fin :=
+  block_goal;
+  repeat match goal with
+  | v : vec _ _ |- _ => inv_vec v; intros
+  | i : fin _ |- _ => inv_fin i; intros
+  end;
+  unblock_goal.
+
+(** We define a coercion from [vec] to [list] and show that it preserves the
+operations on vectors. We also define a function to go in the other way, but
+do not define it as a coercion, as it would otherwise introduce ambiguity. *)
+Fixpoint vec_to_list {A n} (v : vec A n) : list A :=
+  match v with
+  | [#] => []
+  | x ::: v => x :: vec_to_list v
+  end.
+Coercion vec_to_list : vec >-> list.
+Notation list_to_vec := Vector.of_list.
+
+Lemma vec_to_list_cons {A n} x (v : vec A n) :
+  vec_to_list (x ::: v) = x :: vec_to_list v.
+Proof. done. Qed.
+Lemma vec_to_list_app {A n m} (v : vec A n) (w : vec A m) :
+  vec_to_list (v +++ w) = vec_to_list v ++ vec_to_list w.
+Proof. by induction v; simpl; f_equal. Qed.
+
+Lemma vec_to_list_of_list {A} (l : list A): vec_to_list (list_to_vec l) = l.
+Proof. by induction l; simpl; f_equal. Qed.
+
+Lemma vec_to_list_length {A n} (v : vec A n) : length (vec_to_list v) = n.
+Proof. induction v; simpl; by f_equal. Qed.
+
+Lemma vec_to_list_inj1 {A n m} (v : vec A n) (w : vec A m) :
+  vec_to_list v = vec_to_list w → n = m.
+Proof.
+  revert m w. induction v; intros ? [|???] ?;
+   simpl in *; simplify_equality; f_equal; eauto.
+Qed.
+Lemma vec_to_list_inj2 {A n} (v : vec A n) (w : vec A n) :
+  vec_to_list v = vec_to_list w → v = w.
+Proof.
+  revert w. induction v; intros w; inv_vec w; intros;
+    simpl in *; simplify_equality; f_equal; eauto.
+Qed.
+
+Lemma vlookup_middle {A n m} (v : vec A n) (w : vec A m) x :
+  ∃ i : fin (n + S m), x = (v +++ x ::: w) !!! i.
+Proof.
+  induction v; simpl.
+  * by eexists 0%fin.
+  * destruct IHv as [i ?]. by exists (FS i).
+Qed.
+
+Lemma vec_to_list_lookup_middle {A n} (v : vec A n) (l k : list A) x :
+  vec_to_list v = l ++ x :: k →
+    ∃ i : fin n, l = take i v ∧ x = v !!! i ∧ k = drop (S i) v.
+Proof.
+  intros H.
+  rewrite <-(vec_to_list_of_list l), <-(vec_to_list_of_list k) in H.
+  rewrite <-vec_to_list_cons, <-vec_to_list_app in H.
+  pose proof (vec_to_list_inj1 _ _ H); subst.
+  apply vec_to_list_inj2 in H; subst.
+  induction l. simpl.
+  * eexists 0%fin. simpl. by rewrite vec_to_list_of_list.
+  * destruct IHl as [i ?]. exists (FS i). simpl. intuition congruence.
+Qed.
+
+Lemma vec_to_list_drop_lookup {A n} (v : vec A n) (i : fin n) :
+  drop i v = v !!! i :: drop (S i) v.
+Proof. induction i; inv_vec v; simpl; intros; [done | by rewrite IHi]. Qed.
+
+Lemma vec_to_list_take_drop_lookup {A n} (v : vec A n) (i : fin n) :
+  vec_to_list v = take i v ++ v !!! i :: drop (S i) v.
+Proof.
+  rewrite <-(take_drop i v) at 1. f_equal.
+  apply vec_to_list_drop_lookup.
+Qed. 
+
+Lemma In_vlookup {A n} (v : vec A n) x :
+  In x (vec_to_list v) ↔ ∃ i, v !!! i = x.
+Proof.
+  split.
+  * induction v; simpl; [done | intros [?|?]; subst].
+    + by eexists 0%fin.
+    + destruct IHv as [i ?]; trivial. by exists (FS i).
+  * intros [i ?]; subst. induction v; inv_fin i.
+    + by left.
+    + right. apply IHv.
+Qed.
+
+Lemma Forall_vlookup {A} (P : A → Prop) {n} (v : vec A n) :
+  Forall P (vec_to_list v) ↔ ∀ i, P (v !!! i).
+Proof.
+  rewrite Forall_forall.
+  setoid_rewrite In_vlookup. naive_solver.
+Qed.
+Lemma Forall_vlookup_1 {A} (P : A → Prop) {n} (v : vec A n) i :
+  Forall P (vec_to_list v) → P (v !!! i).
+Proof. by rewrite Forall_vlookup. Qed.
+Lemma Forall_vlookup_2 {A} (P : A → Prop) {n} (v : vec A n) :
+  (∀ i, P (v !!! i)) → Forall P (vec_to_list v).
+Proof. by rewrite Forall_vlookup. Qed.
+
+Lemma Exists_vlookup {A} (P : A → Prop) {n} (v : vec A n) :
+  Exists P (vec_to_list v) ↔ ∃ i, P (v !!! i).
+Proof.
+  rewrite Exists_exists.
+  setoid_rewrite In_vlookup. naive_solver.
+Qed.
+
+Lemma Forall2_vlookup {A B} (P : A → B → Prop)
+    {n} (v1 : vec A n) (v2 : vec B n) :
+  Forall2 P (vec_to_list v1) (vec_to_list v2) ↔
+    ∀ i, P (v1 !!! i) (v2 !!! i).
+Proof.
+  split.
+  * vec_double_ind v1 v2.
+    + intros _ i. inv_fin i.
+    + intros n v1 v2 IH a b; simpl. inversion_clear 1.
+      intros i. inv_fin i; simpl; auto.
+  * vec_double_ind v1 v2.
+    + constructor.
+    + intros ??? IH ?? H.
+      constructor. apply (H 0%fin). apply IH, (λ i, H (FS i)).
+Qed.
+
+(** The function [vmap f v] applies a function [f] element wise to [v]. *)
+Notation vmap := Vector.map.
+
+Lemma vlookup_map `(f : A → B) {n} (v : vec A n) i :
+  vmap f v !!! i = f (v !!! i).
+Proof. by apply Vector.nth_map. Qed.
+
+Lemma vec_to_list_map `(f : A → B) {n} (v : vec A n) :
+  vec_to_list (vmap f v) = f <$> vec_to_list v.
+Proof. induction v; simpl. done. by rewrite IHv. Qed.
+
+(** The function [vzip_with f v w] combines the vectors [v] and [w] element
+wise using the function [f]. *)
+Notation vzip_with := Vector.map2.
+
+Lemma vzip_with_lookup `(f : A → B → C) {n} (v1 : vec A n) (v2 : vec B n) i :
+  vzip_with f v1 v2 !!! i = f (v1 !!! i) (v2 !!! i).
+Proof. by apply Vector.nth_map2. Qed.
+
+(** Similar to vlookup, we cannot define [vinsert] as an instance of the
+[Insert] type class, as it has a dependent type. *)
+Fixpoint vinsert {A n} (i : fin n) (x : A) : vec A n → vec A n :=
+  match i with
+  | 0%fin => vec_S_inv _ (λ _ v, x ::: v)
+  | FS _ i => vec_S_inv _ (λ y v, y ::: vinsert i x v)
+  end.
+
+Lemma vec_to_list_insert {A n} i x (v : vec A n) :
+  vec_to_list (vinsert i x v) = insert (fin_to_nat i) x (vec_to_list v).
+Proof. induction v; inv_fin i. done. simpl. intros. by rewrite IHv. Qed.
+
+Lemma vlookup_insert {A n} i x (v : vec A n) : vinsert i x v !!! i = x.
+Proof. by induction i; inv_vec v. Qed.
+
+Lemma vlookup_insert_ne {A n} i j x (v : vec A n) :
+  i ≠ j → vinsert i x v !!! j = v !!! j.
+Proof.
+  induction i; inv_fin j; inv_vec v; simpl; try done.
+  intros. apply IHi. congruence.
+Qed.
-- 
GitLab