diff --git a/theories/ars.v b/theories/ars.v
new file mode 100644
index 0000000000000000000000000000000000000000..9a4fb2241c948fe322d0c2a3aff8a6c4141eded3
--- /dev/null
+++ b/theories/ars.v
@@ -0,0 +1,159 @@
+(* Copyright (c) 2012, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** This file collects definitions and theorems on abstract rewriting systems.
+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 Export tactics base.
+
+(** * Definitions *)
+Section definitions.
+  Context `(R : relation A).
+
+  (** An element is reducible if a step is possible. *)
+  Definition red (x : A) := âˆƒ y, R x y.
+
+  (** An element is in normal form if no further steps are possible. *)
+  Definition nf (x : A) := Â¬red x.
+
+  (** The reflexive transitive closure. *)
+  Inductive rtc : relation A :=
+    | rtc_refl x : rtc x x
+    | rtc_l x y z : R x y â†’ rtc y z â†’ rtc x z.
+
+  (** Reductions of exactly [n] steps. *)
+  Inductive nsteps : nat â†’ relation A :=
+    | nsteps_O x : nsteps 0 x x
+    | nsteps_l n x y z : R x y â†’ nsteps n y z â†’ nsteps (S n) x z.
+
+  (** Reduction of at most [n] steps. *)
+  Inductive bsteps : nat â†’ relation A :=
+    | bsteps_refl n x : bsteps n x x
+    | bsteps_l n x y z : R x y â†’ bsteps n y z â†’ bsteps (S n) x z.
+
+  (** The transitive closure. *)
+  Inductive tc : relation A :=
+    | tc_once x y : R x y â†’ tc x y
+    | tc_l x y z : R x y â†’ tc y z â†’ tc x z.
+
+  (** An element [x] is looping if all paths starting at [x] are infinite. *)
+  CoInductive looping : A â†’ Prop :=
+    | looping_do_step x : red x â†’ (âˆ€ y, R x y â†’ looping y) â†’ looping x.
+End definitions.
+
+Hint Constructors rtc nsteps bsteps tc : ars.
+
+(** * General theorems *)
+Section rtc.
+  Context `{R : relation A}.
+
+  Global Instance: Reflexive (rtc R).
+  Proof rtc_refl R.
+  Global Instance rtc_trans: Transitive (rtc R).
+  Proof. red; induction 1; eauto with ars. Qed.
+  Lemma rtc_once x y : R x y â†’ rtc R x y.
+  Proof. eauto with ars. Qed.
+  Global Instance: subrelation R (rtc R).
+  Proof. exact @rtc_once. Qed.
+  Lemma rtc_r x y z : rtc R x y â†’ R y z â†’ rtc R x z.
+  Proof. intros. etransitivity; eauto with ars. Qed.
+
+  Lemma rtc_inv x z : rtc R x z â†’ x = z âˆ¨ âˆƒ y, R x y âˆ§ rtc R y z.
+  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.
+  Proof.
+    cut (âˆ€ y z, rtc R y z â†’ âˆ€ x, rtc R x y â†’ P x y â†’ P x z).
+    { eauto using rtc_refl. }
+    induction 1; eauto using rtc_r.
+  Qed.
+
+  Lemma rtc_inv_r x z : rtc R x z â†’ x = z âˆ¨ âˆƒ y, rtc R x y âˆ§ R y z.
+  Proof. revert x z. apply rtc_ind_r; eauto. Qed.
+
+  Lemma nsteps_once x y : R x y â†’ nsteps R 1 x y.
+  Proof. eauto with ars. Qed.
+  Lemma nsteps_trans n m x y z :
+    nsteps R n x y â†’ nsteps R m y z â†’ nsteps R (n + m) x z.
+  Proof. induction 1; simpl; eauto with ars. Qed.
+  Lemma nsteps_r n x y z : nsteps R n x y â†’ R y z â†’ nsteps R (S n) x z.
+  Proof. induction 1; eauto with ars. Qed.
+  Lemma nsteps_rtc n x y : nsteps R n x y â†’ rtc R x y.
+  Proof. induction 1; eauto with ars. Qed.
+  Lemma rtc_nsteps x y : rtc R x y â†’ âˆƒ n, nsteps R n x y.
+  Proof. induction 1; firstorder eauto with ars. Qed.
+
+  Lemma bsteps_once n x y : R x y â†’ bsteps R (S n) x y.
+  Proof. eauto with ars. Qed.
+  Lemma bsteps_plus_r n m x y :
+    bsteps R n x y â†’ bsteps R (n + m) x y.
+  Proof. induction 1; simpl; eauto with ars. Qed.
+  Lemma bsteps_weaken n m x y :
+    n â‰¤ m â†’ bsteps R n x y â†’ bsteps R m x y.
+  Proof.
+    intros. rewrite (Minus.le_plus_minus n m); auto using bsteps_plus_r.
+  Qed.
+  Lemma bsteps_plus_l n m x y :
+    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.
+  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.
+  Lemma bsteps_r n x y z : bsteps R n x y â†’ R y z â†’ bsteps R (S n) x z.
+  Proof. induction 1; eauto with ars. Qed.
+  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.
+
+  Global Instance tc_trans: Transitive (tc R).
+  Proof. red; induction 1; eauto with ars. Qed.
+  Lemma tc_r x y z : tc R x y â†’ R y z â†’ tc R x z.
+  Proof. intros. etransitivity; eauto with ars. Qed.
+  Lemma tc_rtc x y : tc R x y â†’ rtc R x y.
+  Proof. induction 1; eauto with ars. Qed.
+  Global Instance: subrelation (tc R) (rtc R).
+  Proof. exact @tc_rtc. Qed.
+
+  Lemma looping_red x : looping R x â†’ red R x.
+  Proof. destruct 1; auto. Qed.
+  Lemma looping_step x y : looping R x â†’ R x y â†’ looping R y.
+  Proof. destruct 1; auto. Qed.
+  Lemma looping_rtc x y : looping R x â†’ rtc R x y â†’ looping R y.
+  Proof. induction 2; eauto using looping_step. Qed.
+
+  Lemma looping_alt x :
+    looping R x â†” âˆ€ y, rtc R x y â†’ red R y.
+  Proof.
+    split.
+    * eauto using looping_red, looping_rtc.
+    * intros H. cut (âˆ€ z, rtc R x z â†’ looping R z).
+      { eauto with ars. }
+      cofix FIX. constructor; eauto using rtc_r with ars.
+  Qed.
+End rtc.
+
+Hint Resolve rtc_once rtc_r tc_r : 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.
+  Lemma nf_subrel x : nf R2 x â†’ nf R1 x.
+  Proof. intros H1 H2. destruct H1. now apply red_subrel. Qed.
+
+  Global Instance rtc_subrel: subrelation (rtc R1) (rtc R2).
+  Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed.
+  Global Instance nsteps_subrel: subrelation (nsteps R1 n) (nsteps R2 n).
+  Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed.
+  Global Instance bsteps_subrel: subrelation (bsteps R1 n) (bsteps R2 n).
+  Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed.
+  Global Instance tc_subrel: subrelation (tc R1) (tc R2).
+  Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed.
+End subrel.
diff --git a/theories/base.v b/theories/base.v
index b021a29870abbba8ad8b133a06261c983b46b99c..06a1a94d166f90f9e7a8ae739ad03eb63dd75666 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1,20 +1,34 @@
+(* Copyright (c) 2012, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** This file collects type class interfaces, notations, and general theorems
+that are used throughout the whole development. Most importantly it contains
+abstract interfaces for ordered structures, collections, and various other data
+structures. *)
 Global Generalizable All Variables.
 Global Set Automatic Coercions Import.
 Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid NArith.
 
+(** * General *)
+(** The following coercion allows us to use Booleans as propositions. *)
+Coercion Is_true : bool >-> Sortclass.
+
+(** Ensure that [simpl] unfolds [id] and [compose] when fully applied. *)
 Arguments id _ _/.
 Arguments compose _ _ _ _ _ _ /.
 
-(* Change True and False into notations so we can overload them *)
+(** Change [True] and [False] into notations in order to enable overloading.
+We will use this in the file [assertions] to give [True] and [False] a
+different interpretation in [assert_scope] used for assertions of our axiomatic
+semantics. *)
 Notation "'True'" := True : type_scope.
 Notation "'False'" := False : type_scope.
 
-Arguments existT {_ _} _ _.
-
-(*  Common notations *)
+(** Throughout this development we use [C_scope] for all general purpose
+notations that do not belong to a more specific scope. *)
 Delimit Scope C_scope with C.
 Global Open Scope C_scope.
 
+(** Introduce some Haskell style like notations. *)
 Notation "(=)" := eq (only parsing) : C_scope.
 Notation "( x =)" := (eq x) (only parsing) : C_scope.
 Notation "(= x )" := (Î» y, eq y x) (only parsing) : C_scope.
@@ -33,17 +47,39 @@ Infix "âˆ˜" := compose : C_scope.
 Notation "(âˆ˜)" := compose (only parsing) : C_scope.
 Notation "( f âˆ˜)" := (compose f) (only parsing) : C_scope.
 Notation "(âˆ˜ f )" := (Î» g, compose g f) (only parsing) : C_scope.
+
+(** Set convenient implicit arguments for [existT] and introduce notations. *)
+Arguments existT {_ _} _ _.
 Notation "x â†¾ p" := (exist _ x p) (at level 20) : C_scope.
 Notation "` x" := (proj1_sig x) : C_scope.
 
-(* Provable propositions *)
+(** * Type classes *)
+(** ** Provable propositions *)
+(** This type class collects provable propositions. It is useful to constraint
+type classes by arbitrary propositions. *)
 Class PropHolds (P : Prop) := prop_holds: P.
 
-(* Decidable propositions *)
+Hint Extern 0 (PropHolds _) => assumption : typeclass_instances.
+Instance: Proper (iff ==> iff) PropHolds.
+Proof. now repeat intro. Qed.
+
+Ltac solve_propholds :=
+  match goal with
+  | [ |- PropHolds (?P) ] => apply _
+  | [ |- ?P ] => change (PropHolds P); apply _
+  end.
+
+(** ** Decidable propositions *)
+(** This type class by (Spitters/van der Weegen, 2011) collects decidable
+propositions. For example to declare a parameter expressing decidable equality
+on a type [A] we write [`{âˆ€ x y : A, Decision (x = y)}] and use it by writing
+[decide (x = y)]. *)
 Class Decision (P : Prop) := decide : {P} + {Â¬P}.
 Arguments decide _ {_}.
 
-(* Common relations & operations *)
+(** ** Setoid equality *)
+(** We define an operational type class for setoid equality. This is based on
+(Spitters/van der Weegen, 2011). *)
 Class Equiv A := equiv: relation A.
 Infix "â‰¡" := equiv (at level 70, no associativity) : C_scope.
 Notation "(â‰¡)" := equiv (only parsing) : C_scope.
@@ -54,31 +90,54 @@ Notation "x â‰¢ y":= (Â¬x â‰¡ y) (at level 70, no associativity) : C_scope.
 Notation "( x â‰¢)" := (Î» y, x â‰¢ y) (only parsing) : C_scope.
 Notation "(â‰¢ x )" := (Î» y, y â‰¢ x) (only parsing) : C_scope.
 
+(** A [Params f n] instance forces the setoid rewriting mechanism not to
+rewrite in the first [n] arguments of the function [f]. We will declare such
+instances for all operational type classes in this development. *)
+Instance: Params (@equiv) 2.
+
+(** The following instance forces [setoid_replace] to use setoid equality
+(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.
 
+(** ** Operations on collections *)
+(** We define operational type classes for the standard operations and
+relations on collections: the empty collection [âˆ…], the union [(âˆª)],
+intersection [(âˆ©)], difference [(âˆ–)], and the singleton [{[_]}]
+operation, and the subset [(âŠ†)] and element of [(âˆˆ)] relation. *)
 Class Empty A := empty: A.
 Notation "âˆ…" := empty : C_scope.
 
 Class Union A := union: A â†’ A â†’ A.
+Instance: Params (@union) 2.
 Infix "âˆª" := union (at level 50, left associativity) : C_scope.
 Notation "(âˆª)" := union (only parsing) : C_scope.
 Notation "( x âˆª)" := (union x) (only parsing) : C_scope.
 Notation "(âˆª x )" := (Î» y, union y x) (only parsing) : C_scope.
 
 Class Intersection A := intersection: A â†’ A â†’ A.
+Instance: Params (@intersection) 2.
 Infix "âˆ©" := intersection (at level 40) : C_scope.
 Notation "(âˆ©)" := intersection (only parsing) : C_scope.
 Notation "( x âˆ©)" := (intersection x) (only parsing) : C_scope.
 Notation "(âˆ© x )" := (Î» y, intersection y x) (only parsing) : C_scope.
 
 Class Difference A := difference: A â†’ A â†’ A.
+Instance: Params (@difference) 2.
 Infix "âˆ–" := difference (at level 40) : C_scope.
 Notation "(âˆ–)" := difference (only parsing) : C_scope.
 Notation "( x âˆ–)" := (difference x) (only parsing) : C_scope.
 Notation "(âˆ– x )" := (Î» y, difference y x) (only parsing) : C_scope.
 
+Class Singleton A B := singleton: A â†’ B.
+Instance: Params (@singleton) 3.
+Notation "{[ x ]}" := (singleton x) : C_scope.
+Notation "{[ x ; y ; .. ; z ]}" :=
+  (union .. (union (singleton x) (singleton y)) .. (singleton z)) : C_scope.
+
 Class SubsetEq A := subseteq: A â†’ A â†’ Prop.
+Instance: Params (@subseteq) 2.
 Infix "âŠ†" := subseteq (at level 70) : C_scope.
 Notation "(âŠ†)" := subseteq (only parsing) : C_scope.
 Notation "( X âŠ† )" := (subseteq X) (only parsing) : C_scope.
@@ -90,12 +149,8 @@ Notation "( âŠˆ X )" := (Î» Y, Y âŠˆ X) (only parsing) : C_scope.
 
 Hint Extern 0 (?x âŠ† ?x) => reflexivity.
 
-Class Singleton A B := singleton: A â†’ B.
-Notation "{[ x ]}" := (singleton x) : C_scope.
-Notation "{[ x ; y ; .. ; z ]}" :=
-  (union .. (union (singleton x) (singleton y)) .. (singleton z)) : C_scope.
-
 Class ElemOf A B := elem_of: A â†’ B â†’ Prop.
+Instance: Params (@elem_of) 3.
 Infix "âˆˆ" := elem_of (at level 70) : C_scope.
 Notation "(âˆˆ)" := elem_of (only parsing) : C_scope.
 Notation "( x âˆˆ)" := (elem_of x) (only parsing) : C_scope.
@@ -105,14 +160,87 @@ Notation "(âˆ‰)" := (Î» x X, x âˆ‰ X) (only parsing) : C_scope.
 Notation "( x âˆ‰)" := (Î» X, x âˆ‰ X) (only parsing) : C_scope.
 Notation "(âˆ‰ X )" := (Î» x, x âˆ‰ X) (only parsing) : C_scope.
 
+(** ** Operations on maps *)
+(** In this file we will only define operational type classes for the
+operations on maps. In the file [fin_maps] we will axiomatize finite maps.
+The function lookup [m !! k] should yield the element at key [k] in [m]. *)
+Class Lookup K M := lookup: âˆ€ {A}, K â†’ M A â†’ option A.
+Instance: Params (@lookup) 4.
+
+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.
+
+(** The function insert [<[k:=a]>m] should update the element at key [k] with
+value [a] in [m]. *)
+Class Insert K M :=
+  insert: âˆ€ {A}, K â†’ A â†’ M A â†’ M A.
+Instance: Params (@insert) 4.
+Notation "<[ k := a ]>" := (insert k a)
+  (at level 5, right associativity, format "<[ k := a ]>") : C_scope.
+
+(** The function delete [delete k m] should deletes the value at key [k] in
+[m]. *)
+Class Delete K M :=
+  delete: K â†’ M â†’ M.
+Instance: Params (@delete) 3.
+
+(** 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]. When [k] is
+not a member of [m], the original map should be returned. *)
+Class Alter K M :=
+  alter: âˆ€ {A}, (A â†’ A) â†’ K â†’ M A â†’ M A.
+Instance: Params (@alter) 4.
+
+(** 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] if
+[k] is not a member of [m]. The value at [k] should be deleted if [f] yields
+[None]. *)
+Class PartialAlter K M :=
+  partial_alter: âˆ€ {A}, (option A â†’ option A) â†’ K â†’ M A â†’ M A.
+Instance: Params (@partial_alter) 4.
+
+(** 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 M :=
+  dom: âˆ€ C `{Empty C} `{Union C} `{Singleton K C}, M â†’ C.
+Instance: Params (@dom) 7.
+
+(** The function [merge f m1 m2] should merge the maps [m1] and [m2] by
+constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)]
+provided that [k] is a member of either [m1] or [m2].*)
+Class Merge M :=
+  merge: âˆ€ {A}, (option A â†’ option A â†’ option A) â†’ M A â†’ M A â†’ M A.
+Instance: Params (@merge) 3.
+
+(** 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 :=
+  fold_right (Î» p, <[ fst p := snd p ]>) m l.
+Instance: Params (@insert_list) 4.
+Definition delete_list `{Delete K M} (l : list K) (m : M) : M :=
+  fold_right delete m l.
+Instance: Params (@delete_list) 3.
+
+(** The function [union_with f m1 m2] should yield the union of [m1] and [m2]
+using the function [f] to combine values of members that are in both [m1] and
+[m2]. *)
 Class UnionWith M :=
   union_with: âˆ€ {A}, (A â†’ A â†’ A) â†’ M A â†’ M A â†’ M A.
+Instance: Params (@union_with) 3.
+
+(** Similarly for the intersection and difference. *)
 Class IntersectionWith M :=
   intersection_with: âˆ€ {A}, (A â†’ A â†’ A) â†’ M A â†’ M A â†’ M A.
+Instance: Params (@intersection_with) 3.
 Class DifferenceWith M :=
   difference_with: âˆ€ {A}, (A â†’ A â†’ option A) â†’ M A â†’ M A â†’ M A.
+Instance: Params (@difference_with) 3.
 
-(* Common properties *)
+(** ** Common properties *)
+(** These operational type classes allow us to refer to common mathematical
+properties in a generic way. For example, for injectivity of [(k ++)] it
+allows us to write [injective (k ++)] instead of [app_inv_head k]. *)
 Class Injective {A B} R S (f : A â†’ B) :=
   injective: âˆ€ x y : A, S (f x) (f y) â†’ R x y.
 Class Idempotent {A} R (f : A â†’ A â†’ A) :=
@@ -133,7 +261,9 @@ Arguments left_id {_ _} _ _ {_} _.
 Arguments right_id {_ _} _ _ {_} _.
 Arguments associative {_ _} _ {_} _ _ _.
 
-(* Using idempotent_eq we can force Coq to not use the setoid mechanism *)
+(** 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
+rewriting mechanism. *)
 Lemma idempotent_eq {A} (f : A â†’ A â†’ A) `{!Idempotent (=) f} x :
   f x x = x.
 Proof. auto. Qed.
@@ -150,7 +280,10 @@ 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.
 
-(* Monadic operations *)
+(** ** 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). *)
 Section monad_ops.
   Context (M : Type â†’ Type).
 
@@ -160,9 +293,13 @@ Section monad_ops.
   Class FMap := fmap: âˆ€ {A B}, (A â†’ B) â†’ 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} _ _.
+Instance: Params (@mjoin) 3.
 Arguments mjoin {M MJoin A} _.
+Instance: Params (@fmap) 4.
 Arguments fmap {M FMap A B} _ _.
 
 Notation "m â‰«= f" := (mbind f m) (at level 60, right associativity) : C_scope.
@@ -170,14 +307,17 @@ Notation "x â† y ; z" := (y â‰«= (Î» x : _, z))
   (at level 65, next at level 35, right associativity) : C_scope.
 Infix "<$>" := fmap (at level 65, right associativity, only parsing) : C_scope.
 
-(* Ordered structures *)
+(** ** Axiomatization of ordered structures *)
+(** A pre-order equiped with a smallest element. *)
 Class BoundedPreOrder A `{Empty A} `{SubsetEq A} := {
   bounded_preorder :>> PreOrder (âŠ†);
   subseteq_empty x : âˆ… âŠ† x
 }.
 
-(* Note: no equality to avoid the need for setoids. We define setoid 
-equality in a generic way. *)
+(** We do not include equality in the following interfaces so as to avoid the
+need for proofs that the  relations and operations respect setoid equality.
+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;
   subseteq_union_l x y : x âŠ† x âˆª y;
@@ -191,13 +331,15 @@ Class MeetSemiLattice A `{Empty A} `{SubsetEq A} `{Intersection A} := {
   intersection_greatest x y z : z âŠ† x â†’ z âŠ† y â†’ z âŠ† x âˆ© y
 }.
 
-(* Containers *)
-Class Size C := size: C â†’ nat.
+(** ** 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
+[Map] type class instead of the polymorphic [FMap]. *)
 Class Map A C := map: (A â†’ A) â†’ (C â†’ C).
-
-Class Collection A C `{ElemOf A C} `{Empty C} `{Union C} 
+Instance: Params (@map) 3.
+Class Collection A C `{ElemOf A C} `{Empty C} `{Union C}
     `{Intersection C} `{Difference C} `{Singleton A C} `{Map A C} := {
-  elem_of_empty (x : A) : x âˆ‰ âˆ…;
+  not_elem_of_empty (x : A) : x âˆ‰ âˆ…;
   elem_of_singleton (x y : A) : x âˆˆ {[ y ]} â†” x = y;
   elem_of_union X Y (x : A) : x âˆˆ X âˆª Y â†” x âˆˆ X âˆ¨ x âˆˆ Y;
   elem_of_intersection X Y (x : A) : x âˆˆ X âˆ© Y â†” x âˆˆ X âˆ§ x âˆˆ Y;
@@ -205,52 +347,42 @@ Class Collection A C `{ElemOf A C} `{Empty C} `{Union C}
   elem_of_map f X (x : A) : x âˆˆ map f X â†” âˆƒ y, x = f y âˆ§ y âˆˆ X
 }.
 
+(** We axiomative a finite collection as a collection whose elements can be
+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.
-Class FinCollection A C `{Empty C} `{Union C} `{Intersection C} `{Difference C} 
+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} := {
   fin_collection :>> Collection A C;
   elements_spec X x : x âˆˆ X â†” In x (elements X);
   elements_nodup X : NoDup (elements X)
-}. 
+}.
+Class Size C := size: C â†’ nat.
+Instance: Params (@size) 2.
 
+(** The function [fresh X] yields an element that is not contained in [X]. We
+will later prove that [fresh] is [Proper] with respect to the induced setoid
+equality on collections. *)
 Class Fresh A C := fresh: C â†’ A.
+Instance: Params (@fresh) 3.
 Class FreshSpec A C `{!Fresh A C} `{!ElemOf A C} := {
-  fresh_proper X Y : (âˆ€ x, x âˆˆ X â†” x âˆˆ Y) â†’ fresh X = fresh Y;
+  fresh_proper_alt X Y : (âˆ€ x, x âˆˆ X â†” x âˆˆ Y) â†’ fresh X = fresh Y;
   is_fresh (X : C) : fresh X âˆ‰ X
 }.
 
-(* Maps *)
-Class Lookup K M := lookup: âˆ€ {A}, K â†’ M A â†’ option A.
-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.
+(** * 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.
 
-Class PartialAlter K M :=
-  partial_alter: âˆ€ {A}, (option A â†’ option A) â†’ K â†’ M A â†’ M A.
-Class Alter K M :=
-  alter: âˆ€ {A}, (A â†’ A) â†’ K â†’ M A â†’ M A.
-Class Dom K M :=
-  dom: âˆ€ C `{Empty C} `{Union C} `{Singleton K C}, M â†’ C.
-Class Merge M :=
-  merge: âˆ€ {A}, (option A â†’ option A â†’ option A) â†’ M A â†’ M A â†’ M A.
-Class Insert K M :=
-  insert: âˆ€ {A}, K â†’ A â†’ M A â†’ M A.
-Notation "<[ k := a ]>" := (insert k a) 
-  (at level 5, right associativity, format "<[ k := a ]>") : C_scope.
-Class Delete K M :=
-  delete: K â†’ M â†’ M.
-
-Definition insert_list `{Insert K M} {A} (l : list (K * A)) (m : M A) : M A :=
-  fold_right (Î» p, <[ fst p := snd p ]>) m l.
-Definition delete_list `{Delete K M} (l : list K) (m : M) : M := 
-  fold_right delete m l.
-
-(* Misc *)
 Lemma symmetry_iff `(R : relation A) `{!Symmetric R} (x y : A) :
   R x y â†” R y x.
 Proof. intuition. Qed.
 
+(** ** Pointwise relations *)
+(** These instances are in Coq trunk since revision 15455, but are not in Coq
+8.4 yet. *)
 Instance pointwise_reflexive {A} `{R : relation B} :
   Reflexive R â†’ Reflexive (pointwise_relation A R) | 9.
 Proof. firstorder. Qed.
@@ -261,6 +393,7 @@ Instance pointwise_transitive {A} `{R : relation B} :
   Transitive R â†’ Transitive (pointwise_relation A R) | 9.
 Proof. firstorder. Qed.
 
+(** ** Products *)
 Definition fst_map {A A' B} (f : A â†’ A') (p : A * B) : A' * B :=
   (f (fst p), snd p).
 Definition snd_map {A B B'} (f : B â†’ B') (p : A * B) : A * B' :=
@@ -290,6 +423,7 @@ Section prod_relation.
   Proof. firstorder eauto. Qed.
 End prod_relation.
 
+(** ** Other *)
 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) :
@@ -320,80 +454,3 @@ Proof. easy. Qed.
 Instance idem_propholds {A} (R : relation A) f :
   Idempotent R f â†’ âˆ€ x, PropHolds (R (f x x) x).
 Proof. easy. Qed.
-
-Ltac simplify_eqs := repeat
-  match goal with
-  | |- _ => progress subst
-  | |- _ = _ => reflexivity
-  | H : _ â‰  _ |- _ => now destruct H
-  | H : _ = _ â†’ False |- _ => now destruct H
-  | H : _ = _ |- _ => discriminate H
-  | H : _ = _ |-  ?G =>
-    change (id G); injection H; clear H; intros; unfold id at 1
-  | H : ?f _ = ?f _ |- _ => apply (injective f) in H
-  | H : ?f _ ?x = ?f _ ?x |- _ => apply (injective (Î» y, f y x)) in H
-  end.
-
-Hint Extern 0 (PropHolds _) => assumption : typeclass_instances.
-Instance: Proper (iff ==> iff) PropHolds.
-Proof. now repeat intro. Qed.
-
-Ltac solve_propholds :=
-  match goal with
-  | [ |- PropHolds (?P) ] => apply _
-  | [ |- ?P ] => change (PropHolds P); apply _
-  end.
-
-Tactic Notation "remember" constr(t) "as" "(" ident(x) "," ident(E) ")" :=
-  remember t as x;
-  match goal with
-  | E' : x = _ |- _ => rename E' into E
-  end.
-
-Ltac feed tac H :=
-  let H' := type of H in
-  match eval hnf in H' with
-  | ?T1 â†’ ?T2 =>
-    let HT1 := fresh in assert T1 as HT1;
-    [| feed tac (H HT1); clear HT1 ]
-  | _ => tac H
-  end.
-Tactic Notation "feed" tactic(tac) constr(H) := feed tac H.
-
-Ltac efeed tac H :=
-  let H' := type of H in
-  match eval hnf in H' with
-  | ?T1 â†’ ?T2 =>
-    let HT1 := fresh in assert T1 as HT1; [| efeed tac (H HT1); clear HT1 ]
-  | ?T1 â†’ _ =>
-    let e := fresh in evar (e:T1);
-    let e' := eval unfold e in e in
-    clear e; efeed tac (H e')
-  | _ => tac H
-  end.
-Tactic Notation "efeed" tactic(tac) constr(H) := efeed tac H.
-
-Tactic Notation "feed" "pose" "proof" constr(H) "as" ident(H') :=
-  feed (fun H => pose proof H as H') H.
-Tactic Notation "feed" "pose" "proof" constr(H) :=
-  feed (fun H => pose proof H) H.
-
-Tactic Notation "efeed" "pose" "proof" constr(H) "as" ident(H') :=
-  efeed (fun H => pose proof H as H') H.
-Tactic Notation "efeed" "pose" "proof" constr(H) :=
-  efeed (fun H => pose proof H) H.
-
-Tactic Notation "feed" "specialize" ident(H) :=
-  feed (fun H => specialize H) H.
-Tactic Notation "efeed" "specialize" ident(H) :=
-  efeed (fun H => specialize H) H.
-
-Tactic Notation "feed" "inversion" constr(H) :=
-  feed (fun H => let H':=fresh in pose proof H as H'; inversion H') H.
-Tactic Notation "feed" "inversion" constr(H) "as" simple_intropattern(IP) :=
-  feed (fun H => let H':=fresh in pose proof H as H'; inversion H' as IP) H.
-
-Tactic Notation "feed" "destruct" constr(H) :=
-  feed (fun H => let H':=fresh in pose proof H as H'; destruct H') H.
-Tactic Notation "feed" "destruct" constr(H) "as" simple_intropattern(IP) :=
-  feed (fun H => let H':=fresh in pose proof H as H'; destruct H' as IP) H.
diff --git a/theories/collections.v b/theories/collections.v
index d7e107ef91b1d30fca19daa2c7d1be6b1d2ff40a..8cef0c32b6f07cb99ac6b82487ca4a1db7d9917d 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -1,17 +1,27 @@
-Require Export base orders.
-
+(* Copyright (c) 2012, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** This file collects definitions and theorems on collections. Most
+importantly, it implements some tactics to automatically solve goals involving
+collections. *)
+Require Export base tactics orders.
+
+(** * Theorems *)
 Section collection.
   Context `{Collection A B}.
 
-  Lemma elem_of_empty_iff x : x âˆˆ âˆ… â†” False.
-  Proof. split. apply elem_of_empty. easy. Qed.
-
+  Lemma elem_of_empty x : x âˆˆ âˆ… â†” False.
+  Proof. split. apply not_elem_of_empty. easy. 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, âˆ€ x, x âˆˆ X â†’ x âˆˆ Y.
+  Global Instance collection_subseteq: SubsetEq B := Î» X Y,
+    âˆ€ x, x âˆˆ X â†’ x âˆˆ Y.
   Global Instance: BoundedJoinSemiLattice B.
   Proof. firstorder. Qed.
   Global Instance: MeetSemiLattice B.
@@ -25,17 +35,20 @@ Section collection.
     X â‰¡ Y â†” (âˆ€ x, x âˆˆ X â†’ x âˆˆ Y) âˆ§ (âˆ€ x, x âˆˆ Y â†’ x âˆˆ X).
   Proof. firstorder. Qed.
 
-  Global Instance: Proper ((=) ==> (â‰¡) ==> iff) (âˆˆ).
+  Global Instance singleton_proper : Proper ((=) ==> (â‰¡)) singleton.
+  Proof. repeat intro. now subst. Qed.
+  Global Instance elem_of_proper: Proper ((=) ==> (â‰¡) ==> iff) (âˆˆ).
   Proof. intros ???. subst. firstorder. Qed.
 
-  Lemma empty_ne_singleton x :  âˆ… â‰¢ {[ x ]}.
+  Lemma empty_ne_singleton x : âˆ… â‰¢ {[ x ]}.
   Proof.
-    intros [_ E]. destruct (elem_of_empty x).
+    intros [_ E]. apply (elem_of_empty x).
     apply E. now apply elem_of_singleton.
-  Qed. 
+  Qed.
 End collection.
 
-Section cmap.
+(** * Theorems about map *)
+Section map.
   Context `{Collection A C}.
 
   Lemma elem_of_map_1 (f : A â†’ A) (X : C) (x : A) :
@@ -47,19 +60,18 @@ Section cmap.
   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 cmap.
-
-Definition fresh_sig `{FreshSpec A C} (X : C) : { x : A | x âˆ‰ X } :=
-  exist (âˆ‰ X) (fresh X) (is_fresh X).
-
-Lemma elem_of_fresh_iff `{FreshSpec A C} (X : C) : fresh X âˆˆ X â†” False.
-Proof. split. apply is_fresh. easy. Qed.
-
-Ltac split_elem_ofs := repeat
+End map.
+
+(** * Tactics *)
+(** The first pass consists of eliminating all occurrences of [(âˆª)], [(âˆ©)],
+[(âˆ–)], [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_iff 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
@@ -67,7 +79,7 @@ Ltac split_elem_ofs := repeat
   | H : context [ _ âˆˆ map _ _ ] |- _ => setoid_rewrite elem_of_map in H
   | |- context [ _ âŠ† _ ] => setoid_rewrite elem_of_subseteq
   | |- context [ _ â‰¡ _ ] => setoid_rewrite elem_of_equiv_alt
-  | |- context [ _ âˆˆ âˆ… ] => setoid_rewrite elem_of_empty_iff
+  | |- context [ _ âˆˆ âˆ… ] => setoid_rewrite elem_of_empty
   | |- context [ _ âˆˆ {[ _ ]} ] => setoid_rewrite elem_of_singleton
   | |- context [ _ âˆˆ _ âˆª _ ] => setoid_rewrite elem_of_union
   | |- context [ _ âˆˆ _ âˆ© _ ] => setoid_rewrite elem_of_intersection
@@ -75,56 +87,49 @@ Ltac split_elem_ofs := repeat
   | |- context [ _ âˆˆ map _ _ ] => setoid_rewrite elem_of_map
   end.
 
-Ltac destruct_elem_ofs := repeat
-  match goal with
-  | H : context [ @elem_of (_ * _) _ _ ?x _ ] |- _ => is_var x; destruct x
-  | H : context [ @elem_of (_ + _) _ _ ?x _] |- _ => is_var x; destruct x
-  end.
-
-Tactic Notation "simplify_elem_of" tactic(t) :=
-  intros; (* due to bug #2790 *)
+(** 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) :=
   simpl in *;
-  split_elem_ofs;
-  destruct_elem_ofs;
-  intuition (simplify_eqs; t).
-Tactic Notation "simplify_elem_of" := simplify_elem_of auto.
-
-Ltac naive_firstorder t :=
-  match goal with
-  (* intros *)
-  | |- âˆ€ _, _ => intro; naive_firstorder t
-  (* destructs without information loss *)
-  | H : False |- _ => destruct H
-  | H : ?X, Hneg : Â¬?X|- _ => now destruct Hneg
-  | H : _ âˆ§ _ |- _ => destruct H; naive_firstorder t
-  | H : âˆƒ _, _  |- _ => destruct H; naive_firstorder t
-  (* simplification *)
-  | |- _ => progress (simplify_eqs; simpl in *); naive_firstorder t
-  (* constructs *)
-  | |- _ âˆ§ _ => split; naive_firstorder t
-  (* solve *)
-  | |- _ => solve [t]
-  (* dirty destructs *)
-  | H : context [ âˆƒ _, _ ] |- _ =>
-    edestruct H; clear H;naive_firstorder t || clear H; naive_firstorder t
-  | H : context [ _ âˆ§ _ ] |- _ => 
-    destruct H; clear H; naive_firstorder t || clear H; naive_firstorder t
-  | H : context [ _ âˆ¨ _ ] |- _ =>
-    edestruct H; clear H; naive_firstorder t || clear H; naive_firstorder t
-  (* dirty constructs *)
-  | |- âˆƒ x, _ => eexists; naive_firstorder t
-  | |- _ âˆ¨ _ => left; naive_firstorder t || right; naive_firstorder t
-  | H : _ â†’ False |- _ => destruct H; naive_firstorder t
-  end.
-Tactic Notation "naive_firstorder" tactic(t) :=
-  unfold iff, not in *; 
-  naive_firstorder t.
-
-Tactic Notation "esimplify_elem_of" tactic(t) := 
-  (simplify_elem_of t); 
-  try naive_firstorder t.
-Tactic Notation "esimplify_elem_of" := esimplify_elem_of (eauto 5).
-
+  unfold_elem_of;
+  solve [intuition (simplify_equality; tac)].
+Tactic Notation "solve_elem_of" := solve_elem_of auto.
+
+(** For goals with quantifiers we could use the above tactic but with
+[firstorder] instead of [intuition] as finishing tactic. However, [firstorder]
+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) :=
+  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
+recursively split [H] for [(âˆª)], [(âˆ©)], [(âˆ–)], [map], [âˆ…], [{[_]}]. *)
+Tactic Notation "destruct_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'
+  | _ âˆˆ _ âˆª _ =>
+    let H1 := fresh in let H2 := fresh in apply elem_of_union in H;
+    destruct H as [H1|H2]; [go H1 | go H2]
+  | _ âˆˆ _ âˆ© _ =>
+    let H1 := fresh in let H2 := fresh in apply elem_of_intersection in H;
+    destruct H as [H1 H2]; go H1; go H2
+  | _ âˆˆ _ âˆ– _ =>
+    let H1 := fresh in let H2 := fresh in apply elem_of_difference in H;
+    destruct H as [H1 H2]; go H1; go H2
+  | _ âˆˆ map _ _ =>
+    let H1 := fresh in apply elem_of_map in H;
+    destruct H as [?[? H1]]; go H1
+  | _ => idtac
+  end in go H.
+
+(** * Sets without duplicates up to an equivalence *)
 Section no_dup.
   Context `{Collection A B} (R : relation A) `{!Equivalence R}.
 
@@ -143,33 +148,34 @@ Section no_dup.
   Proof. firstorder. Qed.
 
   Lemma elem_of_upto_elem_of x X : x âˆˆ X â†’ elem_of_upto x X.
-  Proof. unfold elem_of_upto. esimplify_elem_of. Qed.
+  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
   Lemma elem_of_upto_empty x : Â¬elem_of_upto x âˆ….
-  Proof. unfold elem_of_upto. esimplify_elem_of. Qed.
+  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
   Lemma elem_of_upto_singleton x y : elem_of_upto x {[ y ]} â†” R x y.
-  Proof. unfold elem_of_upto. esimplify_elem_of. Qed.
+  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
 
   Lemma elem_of_upto_union X Y x :
     elem_of_upto x (X âˆª Y) â†” elem_of_upto x X âˆ¨ elem_of_upto x Y.
-  Proof. unfold elem_of_upto. esimplify_elem_of. Qed.
+  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
   Lemma not_elem_of_upto x X : Â¬elem_of_upto x X â†’ âˆ€ y, y âˆˆ X â†’ Â¬R x y.
-  Proof. unfold elem_of_upto. esimplify_elem_of. Qed.
+  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
 
   Lemma no_dup_empty: no_dup âˆ….
-  Proof. unfold no_dup. simplify_elem_of. Qed.
+  Proof. unfold no_dup. solve_elem_of. Qed.
   Lemma no_dup_add x X : Â¬elem_of_upto x X â†’ no_dup X â†’ no_dup ({[ x ]} âˆª X).
-  Proof. unfold no_dup, elem_of_upto. esimplify_elem_of. Qed.
+  Proof. unfold no_dup, elem_of_upto. esolve_elem_of. Qed.
   Lemma no_dup_inv_add x X : x âˆ‰ X â†’ no_dup ({[ x ]} âˆª X) â†’ Â¬elem_of_upto x X.
   Proof.
     intros Hin Hnodup [y [??]].
-    rewrite (Hnodup x y) in Hin; simplify_elem_of.
+    rewrite (Hnodup x y) in Hin; solve_elem_of.
   Qed.
   Lemma no_dup_inv_union_l X Y : no_dup (X âˆª Y) â†’ no_dup X.
-  Proof. unfold no_dup. simplify_elem_of. Qed.
+  Proof. unfold no_dup. solve_elem_of. Qed.
   Lemma no_dup_inv_union_r X Y : no_dup (X âˆª Y) â†’ no_dup Y.
-  Proof. unfold no_dup. simplify_elem_of. Qed.
+  Proof. unfold no_dup. solve_elem_of. Qed.
 End no_dup.
 
+(** * Quantifiers *)
 Section quantifiers.
   Context `{Collection A B} (P : A â†’ Prop).
 
@@ -177,48 +183,65 @@ Section quantifiers.
   Definition cexists X := âˆƒ x, x âˆˆ X âˆ§ P x.
 
   Lemma cforall_empty : cforall âˆ….
-  Proof. unfold cforall. simplify_elem_of. Qed.
+  Proof. unfold cforall. solve_elem_of. Qed.
   Lemma cforall_singleton x : cforall {[ x ]} â†” P x.
-  Proof. unfold cforall. simplify_elem_of. Qed.
+  Proof. unfold cforall. solve_elem_of. Qed.
   Lemma cforall_union X Y : cforall X â†’ cforall Y â†’ cforall (X âˆª Y).
-  Proof. unfold cforall. simplify_elem_of. Qed.
+  Proof. unfold cforall. solve_elem_of. Qed.
   Lemma cforall_union_inv_1 X Y : cforall (X âˆª Y) â†’ cforall X.
-  Proof. unfold cforall. simplify_elem_of. Qed.
+  Proof. unfold cforall. solve_elem_of. Qed.
   Lemma cforall_union_inv_2 X Y : cforall (X âˆª Y) â†’ cforall Y.
-  Proof. unfold cforall. simplify_elem_of. Qed.
+  Proof. unfold cforall. solve_elem_of. Qed.
 
   Lemma cexists_empty : Â¬cexists âˆ….
-  Proof. unfold cexists. esimplify_elem_of. Qed.
+  Proof. unfold cexists. esolve_elem_of. Qed.
   Lemma cexists_singleton x : cexists {[ x ]} â†” P x.
-  Proof. unfold cexists. esimplify_elem_of. Qed.
+  Proof. unfold cexists. esolve_elem_of. Qed.
   Lemma cexists_union_1 X Y : cexists X â†’ cexists (X âˆª Y).
-  Proof. unfold cexists. esimplify_elem_of. Qed.
+  Proof. unfold cexists. esolve_elem_of. Qed.
   Lemma cexists_union_2 X Y : cexists Y â†’ cexists (X âˆª Y).
-  Proof. unfold cexists. esimplify_elem_of. Qed.
+  Proof. unfold cexists. esolve_elem_of. Qed.
   Lemma cexists_union_inv X Y : cexists (X âˆª Y) â†’ cexists X âˆ¨ cexists Y.
-  Proof. unfold cexists. esimplify_elem_of. Qed.
+  Proof. unfold cexists. esolve_elem_of. Qed.
 End quantifiers.
 
 Section more_quantifiers.
   Context `{Collection A B}.
-  
+
   Lemma cforall_weak (P Q : A â†’ Prop) (Hweak : âˆ€ x, P x â†’ Q x) X :
     cforall P X â†’ cforall Q X.
-  Proof. firstorder. Qed.
+  Proof. unfold cforall. naive_solver. Qed.
   Lemma cexists_weak (P Q : A â†’ Prop) (Hweak : âˆ€ x, P x â†’ Q x) X :
     cexists P X â†’ cexists Q X.
-  Proof. firstorder. Qed.
+  Proof. unfold cexists. naive_solver. Qed.
 End more_quantifiers.
 
+(** * Fresh elements *)
+(** We collect some properties on the [fresh] operation. In particular we
+generalize [fresh] to generate lists of fresh elements. *)
 Section fresh.
   Context `{Collection A C} `{Fresh A C} `{!FreshSpec A C} .
 
+  Definition fresh_sig (X : C) : { x : A | x âˆ‰ X } :=
+    exist (âˆ‰ X) (fresh X) (is_fresh X).
+
+  Global Instance fresh_proper: Proper ((â‰¡) ==> (=)) fresh.
+  Proof. intros ???. now apply fresh_proper_alt, elem_of_equiv. Qed.
+
   Fixpoint fresh_list (n : nat) (X : C) : list A :=
     match n with
     | 0 => []
     | S n => let x := fresh X in x :: fresh_list n ({[ x ]} âˆª X)
     end.
 
+  Global Instance fresh_list_proper: Proper ((=) ==> (â‰¡) ==> (=)) fresh_list.
+  Proof.
+    intros ? n ?. subst.
+    induction n; simpl; intros ?? E; f_equal.
+    * now rewrite E.
+    * apply IHn. now rewrite E.
+  Qed.
+
   Lemma fresh_list_length n X : length (fresh_list n X) = n.
   Proof. revert X. induction n; simpl; auto. Qed.
 
@@ -228,7 +251,7 @@ Section fresh.
     * easy.
     * intros X [?| Hin]. subst.
       + apply is_fresh.
-      + apply IHn in Hin. simplify_elem_of.
+      + apply IHn in Hin. solve_elem_of.
   Qed.
 
   Lemma fresh_list_nodup n X : NoDup (fresh_list n X).
@@ -236,6 +259,6 @@ Section fresh.
     revert X.
     induction n; simpl; constructor; auto.
     intros Hin. apply fresh_list_is_fresh in Hin.
-    simplify_elem_of.
+    solve_elem_of.
   Qed.
 End fresh.
diff --git a/theories/decidable.v b/theories/decidable.v
index 3cbb71240d3fbba45d802d8551555064b42aeb0f..3bdfbf967dd79a1e01bc9e5b9a08974153fec38c 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -1,58 +1,60 @@
+(* Copyright (c) 2012, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** 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.
 
-Definition decide_rel {A B} (R : A â†’ B â†’ Prop) 
-  {dec : âˆ€ x y, Decision (R x y)} (x : A) (y : B) : Decision (R x y) := dec x y.
+(** We introduce [decide_rel] to avoid inefficienct computation due to eager
+evaluation of propositions by [vm_compute]. This inefficiency occurs if
+[(x = y) := (f x = f y)] as [decide (x = y)] evaluates to [decide (f x = f y)]
+which then might lead to evaluation of [f x] and [f y]. Using [decide_rel]
+we hide [f] under a lambda abstraction to avoid this unnecessary evaluation. *)
+Definition decide_rel {A B} (R : A â†’ B â†’ Prop) {dec : âˆ€ x y, Decision (R x y)}
+  (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.
 
-Ltac case_decide := 
+(** The tactic [case_decide] performs case analysis on an arbitrary occurrence
+of [decide] or [decide_rel] in the conclusion or assumptions. *)
+Ltac case_decide :=
   match goal with
-  | H : context [@decide ?P ?dec] |- _ => case (@decide P dec) in *
+  | H : context [@decide ?P ?dec] |- _ =>
+    destruct (@decide P dec)
   | H : context [@decide_rel _ _ ?R ?x ?y ?dec] |- _ =>
-     case (@decide_rel _ _ R x y dec) in *
-  | |- context [@decide ?P ?dec] => case (@decide P dec) in *
+    destruct (@decide_rel _ _ R x y dec)
+  | |- context [@decide ?P ?dec] =>
+    destruct (@decide P dec)
   | |- context [@decide_rel _ _ ?R ?x ?y ?dec] =>
-     case (@decide_rel _ _ R x y dec) in *
+    destruct (@decide_rel _ _ R x y dec)
   end.
 
+(** The tactic [solve_decision] uses Coq's [decide equality] tactic together
+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 _
   end.
-Ltac solve_decision := 
+Ltac solve_decision :=
   intros; first [ solve_trivial_decision
                 | unfold Decision; decide equality; solve_trivial_decision ].
 
-Program Instance True_dec: Decision True := left _.
-Program Instance False_dec: Decision False := right _.
-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) := Î» 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 (program_simpl; f_equal; firstorder).
-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 (program_simpl; tauto).
-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 (program_simpl; firstorder).
+(** We can convert decidable propositions to booleans. *)
+Definition bool_decide (P : Prop) {dec : Decision P} : bool :=
+  if dec then true else false.
 
-Definition bool_decide (P : Prop) {dec : Decision P} : bool := if dec then true else false.
-Coercion Is_true : bool >-> Sortclass.
 Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P â†’ P.
 Proof. unfold bool_decide. now destruct dec. Qed.
 Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P â†’ bool_decide P.
 Proof. unfold bool_decide. now destruct dec. Qed.
 
+(** * Decidable Sigma types *)
+(** Leibniz equality on Sigma types requires the equipped proofs to be
+equal as Coq does not support proof irrelevance. For decidable we
+propositions we define the type [dsig P] whose Leibniz equality is proof
+irrelevant. That is [âˆ€ x y : dsig P, x = y â†” `x = `y]. *)
 Definition dsig `(P : A â†’ Prop) `{âˆ€ x : A, Decision (P x)} :=
   { x | bool_decide (P x) }.
 Definition proj2_dsig `{âˆ€ x : A, Decision (P x)} (x : dsig P) : P (`x) :=
@@ -60,15 +62,46 @@ Definition proj2_dsig `{âˆ€ x : A, Decision (P x)} (x : dsig P) : P (`x) :=
 Definition dexist `{âˆ€ x : A, Decision (P x)} (x : A) (p : P x) : dsig P :=
   xâ†¾bool_decide_pack _ p.
 
-Lemma proj1_dsig_inj {A} (P : A â†’ Prop) x (Px : P x) y (Py : P y) :
-  xâ†¾Px = yâ†¾Py â†’ x = y.
-Proof. now injection 1. Qed.
 Lemma dsig_eq {A} (P : A â†’ Prop) {dec : âˆ€ x, Decision (P x)}
-  (x y : { x | bool_decide (P x) }) : `x = `y â†’ x = y.
+  (x y : dsig P) : x = y â†” `x = `y.
 Proof.
-  intros H1. 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.
+  split.
+  * destruct x, y. apply proj1_sig_inj.
+  * 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.
 Qed.
+
+(** * 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.
+
+(** 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).
diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index f823d7c506297f002de628c29d2846aef44f1d5b..06caeb1784d064725ee799ae937d5928b400152b 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -1,9 +1,14 @@
+(* Copyright (c) 2012, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** This file collects definitions and theorems on finite collections. Most
+importantly, it implements a fold and size function and some useful induction
+principles on finite collections . *)
 Require Import Permutation.
 Require Export collections listset.
 
 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).
+Definition collection_fold `{Elements A C} {B} (f : A â†’ B â†’ B)
+  (b : B) (X : C) : B := fold_right f b (elements X).
 
 Section fin_collection.
 Context `{FinCollection A C}.
@@ -22,7 +27,7 @@ Lemma size_empty : size âˆ… = 0.
 Proof.
   unfold size, collection_size. rewrite (in_nil_inv (elements âˆ…)).
   * easy.
-  * intro. rewrite <-elements_spec. simplify_elem_of.
+  * intro. rewrite <-elements_spec. solve_elem_of.
 Qed.
 Lemma size_empty_inv X : size X = 0 â†’ X â‰¡ âˆ….
 Proof.
@@ -38,7 +43,7 @@ Proof.
   apply Permutation_length, NoDup_Permutation.
   * apply elements_nodup.
   * apply NoDup_singleton.
-  * intros. rewrite <-elements_spec. esimplify_elem_of firstorder.
+  * intros. rewrite <-elements_spec. esolve_elem_of firstorder.
 Qed.
 Lemma size_singleton_inv X x y : size X = 1 â†’ x âˆˆ X â†’ y âˆˆ X â†’ x = y.
 Proof.
@@ -51,14 +56,13 @@ Qed.
 
 Lemma choose X : X â‰¢ âˆ… â†’ { x | x âˆˆ X }.
 Proof.
-  case_eq (elements X).
-  * intros E. intros []. apply equiv_empty.
+  destruct (elements X) as [|x l] eqn:E.
+  * intros []. apply equiv_empty.
     intros x. rewrite elements_spec, E. contradiction.
-  * intros x l E. exists x.
-    rewrite elements_spec, E. now left.
+  * exists x. rewrite elements_spec, E. now left.
 Qed.
 Lemma size_pos_choose X : 0 < size X â†’ { x | x âˆˆ X }.
-Proof. 
+Proof.
   intros E. apply choose.
   intros E2. rewrite E2, size_empty in E.
   now destruct (Lt.lt_n_0 0).
@@ -67,10 +71,13 @@ 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. simplify_elem_of. eapply size_singleton_inv; eauto.
+  * exists x. apply elem_of_equiv. split.
+    + 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 :=
+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 _
@@ -79,9 +86,9 @@ Next Obligation.
   intro. apply empty_ne_singleton with x.
   transitivity ({[ x ]} âˆ© {[ y ]}).
   * symmetry. now apply size_empty_iff.
-  * simplify_elem_of.
+  * solve_elem_of.
 Qed.
-Next Obligation. edestruct size_pos_choose; esimplify_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
@@ -90,40 +97,44 @@ Instance elem_of_dec_slow (x : A) (X : C) : Decision (x âˆˆ X) | 100 :=
   end.
 
 Lemma union_difference X Y : X âˆª Y âˆ– X â‰¡ X âˆª Y.
-Proof. split; intros x; destruct (decide (x âˆˆ X)); simplify_elem_of. Qed.
+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.
   apply Permutation_length, NoDup_Permutation.
-    apply elements_nodup.
-   apply NoDup_app; try apply elements_nodup.
-   intros x. rewrite <-!elements_spec.
-   intros ??. apply (elem_of_empty x), E. simplify_elem_of.
-  intros. rewrite in_app_iff, <-!elements_spec. simplify_elem_of.
+  * apply elements_nodup.
+  * apply NoDup_app; try apply elements_nodup.
+    intros x. rewrite <-!elements_spec. esolve_elem_of.
+  * intros. rewrite in_app_iff, <-!elements_spec. solve_elem_of.
 Qed.
 Lemma size_union_alt X Y : size (X âˆª Y) = size X + size (Y âˆ– X).
-Proof. rewrite <-size_union. now rewrite union_difference. simplify_elem_of. Qed.
+Proof.
+  rewrite <-size_union. now 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. simplify_elem_of. Qed.
+Proof.
+  intros. rewrite size_union. now 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.
 Lemma size_remove X x : x âˆˆ X â†’ S (size (X âˆ– {[ x ]})) = size X.
 Proof.
   intros. rewrite <-(size_difference {[ x ]} X).
   * rewrite size_singleton. auto with arith.
-  * simplify_elem_of.
+  * solve_elem_of.
 Qed.
 
 Lemma subseteq_size X Y : X âŠ† Y â†’ size X â‰¤ size Y.
 Proof.
   intros. rewrite <-(subseteq_union_1 X Y) by easy.
-  rewrite <-(union_difference X Y), size_union by simplify_elem_of.
+  rewrite <-(union_difference X Y), size_union by solve_elem_of.
   auto with arith.
-Qed. 
+Qed.
 
 Lemma collection_wf_ind (P : C â†’ Prop) :
-  (âˆ€ X, (âˆ€ Y, size Y < size X â†’ P Y) â†’ P X) â†’ âˆ€ X, P X.
+  (âˆ€ X, (âˆ€ Y, size Y < size X â†’ P Y) â†’ P X) â†’
+  âˆ€ X, P X.
 Proof.
   intros Hind. cut (âˆ€ n X, size X < n â†’ P X).
   { intros help X. apply help with (S (size X)). auto with arith. }
@@ -133,15 +144,18 @@ Proof.
 Qed.
 
 Lemma collection_ind (P : C â†’ Prop) :
-  Proper ((â‰¡) ==> iff) P â†’ P âˆ… â†’ (âˆ€ x X, x âˆ‰ X â†’ P X â†’ P ({[ x ]} âˆª X)) â†’ âˆ€ X, P X.
+  Proper ((â‰¡) ==> iff) P â†’
+  P âˆ… â†’
+  (âˆ€ x X, x âˆ‰ X â†’ P X â†’ P ({[ x ]} âˆª X)) â†’
+  âˆ€ X, P X.
 Proof.
   intros ? Hemp Hadd. apply collection_wf_ind.
   intros X IH. destruct (Compare_dec.zerop (size X)).
   * now rewrite size_empty_inv.
   * destruct (size_pos_choose X); auto.
-    rewrite <-(subseteq_union_1 {[ x ]} X) by simplify_elem_of.
+    rewrite <-(subseteq_union_1 {[ x ]} X) by solve_elem_of.
     rewrite <-union_difference.
-    apply Hadd; simplify_elem_of. apply IH.
+    apply Hadd; [solve_elem_of |]. apply IH.
     rewrite <-(size_remove X x); auto with arith.
 Qed.
 
@@ -157,17 +171,18 @@ Proof.
   induction 1 as [|x l ?? IHl]; simpl.
   * intros X HX. rewrite equiv_empty. easy. intros ??. firstorder.
   * intros X HX.
-    rewrite <-(subseteq_union_1 {[ x ]} X) by esimplify_elem_of.
+    rewrite <-(subseteq_union_1 {[ x ]} X) by esolve_elem_of.
     rewrite <-union_difference.
-    apply Hadd. simplify_elem_of. apply IHl.
+    apply Hadd. solve_elem_of. apply IHl.
     intros y. split.
-    + intros. destruct (proj1 (HX y)); simplify_elem_of.
-    + esimplify_elem_of.
+    + intros. destruct (proj1 (HX y)); solve_elem_of.
+    + esolve_elem_of.
 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. 
+  (âˆ€ 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.
 
 Global Program Instance cforall_dec `(P : A â†’ Prop)
     `{âˆ€ x, Decision (P x)} X : Decision (cforall P X) | 100 :=
@@ -177,7 +192,7 @@ Global Program Instance cforall_dec `(P : A â†’ Prop)
   end.
 Next Obligation.
   red. setoid_rewrite elements_spec. now apply Forall_forall.
-Qed. 
+Qed.
 Next Obligation.
   intro. apply Hall, Forall_forall. setoid_rewrite <-elements_spec. auto.
 Qed.
@@ -189,12 +204,17 @@ Global Program Instance cexists_dec `(P : A â†’ Prop)
   | right Hex => right _
   end.
 Next Obligation.
-  red. setoid_rewrite elements_spec. now apply Exists_exists. 
-Qed. 
+  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 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 f9a755a8373f2979da5034023577c3699178c60b..f023e46cfdc2389b4d609ac0b96f948f671d1178 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1,6 +1,25 @@
+(* Copyright (c) 2012, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** Finite maps associate data to keys. This file defines an interface for
+finite maps and collects some theory on it. Most importantly, it proves useful
+induction principles for finite maps and implements the tactic [simplify_map]
+to simplify goals involving finite maps. *)
 Require Export prelude.
 
-Class FinMap K M `{âˆ€ A, Empty (M A)} `{Lookup K M} `{FMap M} 
+(** * Axiomatization of finite maps *)
+(** We require Leibniz equality to be extensional on finite maps. This of
+course limits the class of finite map implementations, but since we are mainly
+interested in finite maps with numbers or paths as indexes, we do not consider
+this a serious limitation. The main application of finite maps is to implement
+the memory, where extensionality of Leibniz equality becomes very important for
+a convenient use in assertions of our axiomatic semantics. *)
+(** Finiteness is axiomatized by requiring each map to have a finite domain.
+Since we may have multiple implementations of finite sets, the [dom] function is
+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} `{âˆ€ A, Dom K (M A)} `{Merge M} := {
   finmap_eq {A} (m1 m2 : M A) :
     (âˆ€ i, m1 !! i = m2 !! i) â†’ m1 = m2;
@@ -14,21 +33,26 @@ Class FinMap K M `{âˆ€ A, Empty (M A)} `{Lookup K M} `{FMap M}
     (f <$> m) !! i = f <$> m !! i;
   elem_of_dom C {A} `{Collection K C} (m : M A) i :
     i âˆˆ dom C m â†” is_Some (m !! i);
-  merge_spec {A} f `{!PropHolds (f None None = None)} 
+  merge_spec {A} f `{!PropHolds (f None None = None)}
     (m1 m2 : M A) i : merge f m1 m2 !! i = f (m1 !! i) (m2 !! i)
 }.
 
+(** * Derived operations *)
+(** All of the following functions are defined in a generic way for arbitrary
+finite map implementations. These generic implementations do not cause a
+significant enough performance loss to make including them in the finite map
+axiomatization worthwhile. *)
 Instance finmap_alter `{PartialAlter K M} : Alter K M := Î» A f,
   partial_alter (fmap f).
 Instance finmap_insert `{PartialAlter K M} : Insert K M := Î» A k x,
   partial_alter (Î» _, Some x) k.
 Instance finmap_delete `{PartialAlter K M} {A} : Delete K (M A) :=
   partial_alter (Î» _, None).
-Instance finmap_singleton `{PartialAlter K M} {A} 
+Instance finmap_singleton `{PartialAlter K M} {A}
   `{Empty (M A)} : Singleton (K * A) (M A) := Î» p, <[fst p:=snd p]>âˆ….
 
-Definition list_to_map `{Insert K M} {A} `{Empty (M A)} (l : list (K * A)) : M A :=
-  insert_list l âˆ….
+Definition list_to_map `{Insert K M} {A} `{Empty (M A)}
+  (l : list (K * A)) : M A := insert_list l âˆ….
 
 Instance finmap_union `{Merge M} : UnionWith M := Î» A f,
   merge (union_with f).
@@ -37,6 +61,7 @@ Instance finmap_intersection `{Merge M} : IntersectionWith M := Î» A f,
 Instance finmap_difference `{Merge M} : DifferenceWith M := Î» A f,
   merge (difference_with f).
 
+(** * General theorems *)
 Section finmap.
 Context `{FinMap K M} `{âˆ€ i j : K, Decision (i = j)} {A : Type}.
 
@@ -64,12 +89,12 @@ Lemma dom_empty C `{Collection K C} : dom C (âˆ… : M A) â‰¡ âˆ….
 Proof.
   split; intro.
   * rewrite (elem_of_dom C), lookup_empty. simplify_is_Some.
-  * simplify_elem_of.
+  * solve_elem_of.
 Qed.
 Lemma dom_empty_inv C `{Collection K C} (m : M A) : dom C m â‰¡ âˆ… â†’ m = âˆ….
 Proof.
   intros E. apply finmap_empty. intros. apply (not_elem_of_dom C).
-  rewrite E. simplify_elem_of.
+  rewrite E. solve_elem_of.
 Qed.
 
 Lemma lookup_empty_not i : Â¬is_Some ((âˆ… : M A) !! i).
@@ -198,10 +223,10 @@ Qed.
 Lemma delete_partial_alter (m : M A) i f :
   m !! i = None â†’ delete i (partial_alter f i m) = m.
 Proof.
-  intros. unfold delete, finmap_delete. rewrite <-partial_alter_compose. 
+  intros. unfold delete, finmap_delete. rewrite <-partial_alter_compose.
   rapply partial_alter_self_alt. congruence.
 Qed.
-Lemma delete_partial_alter_dom C `{Collection K C} (m : M A) i f : 
+Lemma delete_partial_alter_dom C `{Collection K C} (m : M A) i f :
   i âˆ‰ dom C m â†’ delete i (partial_alter f i m) = m.
 Proof. rewrite (not_elem_of_dom C). apply delete_partial_alter. Qed.
 Lemma delete_insert (m : M A) i x : m !! i = None â†’ delete i (<[i:=x]>m) = m.
@@ -226,6 +251,47 @@ Lemma not_elem_of_dom_delete C `{Collection K C} (m : M A) i :
   i âˆ‰ dom C (delete i m).
 Proof. apply (not_elem_of_dom C), lookup_delete. Qed.
 
+(** * Induction principles *)
+(** We use the induction principle on finite collections to prove the
+following induction principle on finite maps. *)
+Lemma finmap_ind_alt C (P : M A â†’ Prop) `{FinCollection K C} :
+  P âˆ… â†’
+  (âˆ€ i x m, i âˆ‰ dom C m â†’ P m â†’ P (<[i:=x]>m)) â†’
+  âˆ€ m, P m.
+Proof.
+  intros Hemp Hinsert m.
+  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.
+    + intros. rewrite <-(not_elem_of_dom C), Hm.
+      now 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.
+    apply Hinsert.
+    { now apply (not_elem_of_dom_delete C). }
+    apply IH. apply elem_of_equiv. intros.
+    rewrite (elem_of_dom_delete C).
+    esolve_elem_of.
+  * easy.
+Qed.
+
+(** We use the [listset] implementation to prove an induction principle that
+does not mention the map's domain. *)
+Lemma finmap_ind (P : M A â†’ Prop) :
+  P âˆ… â†’
+  (âˆ€ i x m, m !! i = None â†’ P m â†’ P (<[i:=x]>m)) â†’
+  âˆ€ m, P m.
+Proof.
+  setoid_rewrite <-(not_elem_of_dom (listset _)).
+  apply (finmap_ind_alt (listset _) P).
+Qed.
+
+(** * Deleting and inserting multiple elements *)
 Lemma lookup_delete_list (m : M A) is j :
   In j is â†’ delete_list is m !! j = None.
 Proof.
@@ -256,30 +322,23 @@ Proof.
   intros. rewrite IHis, delete_insert_comm; tauto.
 Qed.
 
-Lemma finmap_ind C (P : M A â†’ Prop) `{FinCollection K C} :
-  P âˆ… â†’ (âˆ€ i x m, i âˆ‰ dom C m â†’ P m â†’ P (<[i:=x]>m)) â†’ âˆ€ m, P m.
+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.
-  intros Hemp Hinsert.
-  intros m. 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.
-    + intros. rewrite <-(not_elem_of_dom C), Hm.
-      now simplify_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 simplify_elem_of. }
-    rewrite <-(insert_delete m i x) by easy.
-    apply Hinsert.
-    { now apply (not_elem_of_dom_delete C). }
-    apply IH. apply elem_of_equiv. intros.
-    rewrite (elem_of_dom_delete C). rewrite Hdom.
-    clear Hdom. simplify_elem_of.
+  induction l1 as [|[j y] l1 IH]; simpl.
+  * intros. now rewrite lookup_insert.
+  * intros Hy. rewrite lookup_insert_ne; naive_solver.
+Qed.
+
+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.
+  * intros Hy. rewrite lookup_insert_ne; naive_solver.
 Qed.
 
+(** * Properties of the merge operation *)
 Section merge.
   Context (f : option A â†’ option A â†’ option A).
 
@@ -314,22 +373,26 @@ Section merge.
   Proof. intros ???. apply merge_comm. intros. now 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)) â†’ 
+    (âˆ€ 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.
   Global Instance: Associative (=) f â†’ Associative (=) (merge f).
   Proof. intros ????. apply merge_assoc. intros. now apply (associative f). Qed.
 End merge.
 
+(** * Properties of the union and intersection operation *)
 Section union_intersection.
   Context (f : A â†’ A â†’ A).
 
   Lemma finmap_union_merge m1 m2 i x y :
-    m1 !! i = Some x â†’ m2 !! i = Some y â†’ union_with f m1 m2 !! i = Some (f x y).
+    m1 !! i = Some x â†’
+    m2 !! i = Some y â†’
+    union_with f m1 m2 !! i = Some (f x y).
   Proof.
     intros Hx Hy. unfold union_with, finmap_union.
     now rewrite (merge_spec _), Hx, Hy.
-  Qed.   
+  Qed.
   Lemma finmap_union_l m1 m2 i x :
     m1 !! i = Some x â†’ m2 !! i = None â†’ union_with f m1 m2 !! i = Some x.
   Proof.
@@ -358,31 +421,15 @@ Section union_intersection.
   Global Instance:
     Idempotent (=) f â†’ Idempotent (=) (union_with f : M A â†’ M A â†’ M A) := _.
 End union_intersection.
-
-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 Hy. rewrite lookup_insert_ne. apply IH.
-   firstorder.
-  intro. apply (Hy y). left. congruence.
-Qed.
-
-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.
-  intros Hy. rewrite lookup_insert_ne.
-   firstorder.
-  intro. apply (Hy y). left. congruence.
-Qed.
 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
+inequalities. *)
 Tactic Notation "simplify_map" "by" tactic(T) := repeat
   match goal with
-  | _ => progress simplify_eqs
+  | _ => progress simplify_equality
   | H : context[ âˆ… !! _ ] |- _ => rewrite lookup_empty in H
   | H : context[ (<[_:=_]>_) !! _ ] |- _ => rewrite lookup_insert in H
   | H : context[ (<[_:=_]>_) !! _ ] |- _ => rewrite lookup_insert_ne in H by T
diff --git a/theories/list.v b/theories/list.v
index 975e2078172d47b6711bf3684235de4b96707117..34dc58d6e5c19389775e0cb64bc56671ca5602b1 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1,4 +1,8 @@
-Require Import Permutation. 
+(* 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 lists that
+are not in the Coq standard library. *)
+Require Import Permutation.
 Require Export base decidable option.
 
 Arguments cons {_} _ _.
@@ -15,6 +19,8 @@ Notation "(++)" := app (only parsing) : C_scope.
 Notation "( l ++)" := (app l) (only parsing) : C_scope.
 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 :=
   match l with
@@ -26,20 +32,6 @@ Global Instance list_lookup: Lookup nat list :=
     end
   end.
 
-(* The [simpl] tactic does not unfold [list_lookup] as it is wrapped into
-a type class. Therefore we use the following tactic. Bug: does not simplify
-under binders.
-*)
-Ltac simplify_list_lookup := repeat
-  match goal with
-  | |- context f [@nil ?A !! _] => let X := (context f [@None A]) in change X
-  | |- context f [(?x :: _) !! 0] => let X := (context f [Some x]) in change X
-  | |- context f [(_ :: ?l) !! S ?i] => let X := (context f [l !! i]) in change X
-  | H : context f [@nil ?A !! _] |- _ => let X := (context f [@None A]) in change X in H
-  | H : context f [(?x :: _) !! 0] |- _ => let X := (context f [Some x]) in change X in H
-  | H : context f [(_ :: ?l) !! S ?i] |- _  => let X := (context f [l !! i]) in change X in H
-  end.
-
 Global Instance list_alter: Alter nat list :=
   fix list_alter A (f : A â†’ A) (i : nat) (l : list A) {struct l} :=
   match l with
@@ -51,11 +43,37 @@ Global Instance list_alter: Alter nat list :=
     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
+  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]) [].
+
+(** The predicate [prefix_of] holds if the first list is a prefix of the second.
+The predicate [suffix_of] holds if the first list is a suffix of the second. *)
 Definition prefix_of {A} (l1 l2 : list A) : Prop := âˆƒ k, l2 = l1 ++ k.
 Definition suffix_of {A} (l1 l2 : list A) : Prop := âˆƒ k, l2 = k ++ l1.
 
-Section list_properties.
+(** * General theorems *)
+Section general_properties.
 Context {A : Type}.
 
 Lemma list_eq (l1 l2 : list A) : (âˆ€ i, l1 !! i = l2 !! i) â†’ l1 = l2.
@@ -75,7 +93,7 @@ Proof. now 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_eqs; constructor (solve [eauto]).
+    simplify_list_lookup; simplify_equality; constructor (solve [eauto]).
 Qed.
 
 Lemma list_lookup_In_Some (l : list A) x : In x l â†’ âˆƒ i, l !! i = Some x.
@@ -103,6 +121,11 @@ 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.
 
+Lemma fold_right_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).
+Proof. intro. induction 1; simpl; congruence. 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.
@@ -116,8 +139,13 @@ Lemma Forall2_impl {B} (P Q : A â†’ B â†’ Prop) l1 l2 :
 Proof. induction 1; auto. Qed.
 
 Lemma Forall2_unique {B} (P : A â†’ B â†’ Prop) l k1 k2 :
-  Forall2 P l k1 â†’ Forall2 P l k2 â†’ (âˆ€ x y1 y2, P x y1 â†’ P x y2 â†’ y1 = y2) â†’ k1 = k2.
-Proof. intros H. revert k2. induction H; inversion_clear 1; intros; f_equal; eauto. Qed.
+  Forall2 P l k1 â†’
+  Forall2 P l k2 â†’
+  (âˆ€ x y1 y2, P x y1 â†’ P x y2 â†’ y1 = y2) â†’
+  k1 = k2.
+Proof.
+  intros H. revert k2. induction H; inversion_clear 1; intros; f_equal; eauto.
+Qed.
 
 Lemma NoDup_singleton (x : A) : NoDup [x].
 Proof. constructor. easy. constructor. Qed.
@@ -199,6 +227,11 @@ Global Instance Exists_dec (P : A â†’ Prop) {dec : âˆ€ x, Decision (P x)} :
       end
     end
   end.
+End general_properties.
+
+(** * Theorems on the prefix and suffix predicates *)
+Section prefix_postfix.
+Context {A : Type}.
 
 Global Instance: PreOrder (@prefix_of A).
 Proof.
@@ -273,10 +306,14 @@ Lemma suffix_of_cons x y (l1 l2 : list A) :
 Proof. intros ? [k E]. exists k. subst. now 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. Qed.
+Proof.
+  rewrite suffix_prefix_rev, !rev_unit. now 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. Qed.
+Proof.
+  rewrite !suffix_prefix_rev, !rev_unit. now 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.
@@ -291,18 +328,18 @@ 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.
 
-Lemma suffix_of_cons_inv (l1 l2 : list A) x y : 
+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.
 Proof.
   intros [[|? k] E].
    now left.
-  right. simplify_eqs. now apply suffix_of_app_r.
+  right. simplify_equality. now 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_eqs.
+  destruct k; simplify_equality.
 Qed.
 
 Global Program Instance suffix_of_dec `{âˆ€ x y : A, Decision (x = y)} l1 l2 :
@@ -312,41 +349,54 @@ Global Program Instance suffix_of_dec `{âˆ€ x y : A, Decision (x = y)} l1 l2 :
   | right Hpre => right _
   end.
 Next Obligation. apply suffix_prefix_rev. now rewrite !rev_alt. Qed.
-Next Obligation. 
-  intro. destruct Hpre. rewrite <-!rev_alt. 
+Next Obligation.
+  intro. destruct Hpre. rewrite <-!rev_alt.
   now apply suffix_prefix_rev.
 Qed.
-End list_properties.
-
-Hint Resolve suffix_of_nil suffix_of_cons_r suffix_of_app_r : list.
-Hint Extern 0 (prefix_of _ _) => reflexivity : list.
-Hint Extern 0 (suffix_of _ _) => reflexivity: list.
-Hint Extern 0 (PropHolds (suffix_of _ _)) => red; auto with list : typeclass_instances.
+End prefix_postfix.
 
+(** The [simplify_suffix_of] removes [suffix_of] assumptions that are
+tautologies, and simplifies [suffix_of] assumptions 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)
+  | H : suffix_of (_ :: _) _ |- _ =>
+    destruct (suffix_of_cons_not _ _ H)
+  | H : suffix_of (_ :: _) [] |- _ =>
+    destruct (suffix_of_nil_not _ _ H)
   | H : suffix_of (_ :: _) (_ :: _) |- _ =>
     destruct (suffix_of_cons_inv _ _ _ _ H); clear H
   | H : suffix_of ?x ?x |- _ => clear H
   | H : suffix_of ?x (_ :: ?x) |- _ => clear H
   | H : suffix_of ?x (_ ++ ?x) |- _ => clear H
-  | _ => progress simplify_eqs
+  | _ => progress simplify_equality
   end.
 
-(* Extremely dirty way to discrimate inconsistent suffix_of assumptions *)
-Ltac discriminate_suffix_of := solve [repeat
+(** 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 :=
   match goal with
-  | _ => progress simplify_suffix_of
+  | _ => progress simplify_suffix_of; go
+  | |- 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 2
+     | _ : suffix_of x z |- _ => fail 1
      | _ => assert (suffix_of x z) by (transitivity y; assumption);
-                 clear H1; clear H2 (* to avoid loops *)
+            clear H1; clear H2; go (**i clear to avoid loops *)
      end
-  end].
+  end in go.
+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) :=
@@ -354,7 +404,7 @@ Global Instance list_fmap: FMap list :=
   | [] => []
   | x :: l => f x :: @fmap _ go _ _ f l
   end.
-Global Instance list_join: MJoin list := 
+Global Instance list_join: MJoin list :=
   fix go A (l : list (list A)) : list A :=
   match l with
   | [] =>  []
@@ -362,11 +412,11 @@ Global Instance list_join: MJoin list :=
   end.
 Global Instance list_bind: MBind list := Î» A B f l, mjoin (f <$> l).
 
-Local Arguments fmap _ _ _ _ _ !_ /.
-
 Section list_fmap.
   Context {A B : Type} (f : A â†’ B).
 
+  Local Arguments fmap _ _ _ _ _ !_ /.
+
   Lemma fmap_length l : length (f <$> l) = length l.
   Proof. induction l; simpl; auto. Qed.
 
@@ -398,6 +448,9 @@ 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.
 
+(** * Indexed folds and maps *)
+(** We define stronger variants of map and fold that also take the index of the
+element into account. *)
 Definition imap_go {A B} (f : nat â†’ A â†’ B) : nat â†’ list A â†’ list B :=
   fix go (n : nat) (l : list A) :=
   match l with
@@ -406,22 +459,24 @@ 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.
 
-Lemma fold_right_permutation `(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).
-Proof. intro. induction 1; simpl; congruence. Qed.
-
-Definition ifold_right {A B} (f : nat â†’ B â†’ A â†’ A) (a : nat â†’ A) : nat â†’ list B â†’ A :=
+Definition ifold_right {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
   | nil => a n
   | b :: l => f n b (go (S n) l)
   end.
 
-Lemma ifold_right_app {A B} (f : nat â†’ B â†’ A â†’ A) (a : nat â†’ A) (l1 l2 : list B) n :
+Lemma ifold_right_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.
-Proof. revert n a. induction l1 as [| b l1 IH ]; intros; simpl; f_equal; auto. Qed.
+Proof.
+  revert n a. induction l1 as [| b l1 IH ]; intros; simpl; f_equal; auto.
+Qed.
 
+(** * Lists of the same length *)
+(** The [same_length] view allows convenient induction over two lists with the
+same length. *)
 Section same_length.
   Context {A B : Type}.
 
@@ -448,11 +503,16 @@ Section same_length.
   Qed.
 End same_length.
 
+(** * Zipping lists *)
+(** Since we prefer Haskell style naming, we rename the standard library's
+implementation [combine] into [zip] using a notation. *)
 Notation zip := combine.
 
 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.
diff --git a/theories/listset.v b/theories/listset.v
index 2af31ad9e77aefc90bb53bfd0ce048561662a5b6..682319f0fddbf80043c36fe0360266e204e0bd1e 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -1,3 +1,8 @@
+(* Copyright (c) 2012, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** This file implements finite as unordered lists without duplicates.
+Although this implementation is slow, it is very useful as decidable equality
+is the only constraint on the carrier set. *)
 Require Export base decidable list collections.
 
 Definition listset A := sig (@NoDup A).
@@ -18,25 +23,32 @@ Fixpoint listset_difference_raw (l k : list A) :=
     then listset_difference_raw l k
     else x :: listset_difference_raw l k
   end.
-Lemma listset_difference_raw_in l k x : In x (listset_difference_raw l k) â†” In x l âˆ§ Â¬In x k.
-Proof. split; induction l; simpl; try case_decide; simpl; intuition congruence. Qed.
-Lemma listset_difference_raw_nodup l k : NoDup l â†’ NoDup (listset_difference_raw l k).
-Proof. 
+Lemma listset_difference_raw_in l k x :
+  In x (listset_difference_raw l k) â†” In x l âˆ§ Â¬In x k.
+Proof.
+  split; induction l; simpl; try case_decide; simpl; intuition congruence.
+Qed.
+Lemma listset_difference_raw_nodup l k :
+  NoDup l â†’ NoDup (listset_difference_raw l k).
+Proof.
   induction 1; simpl; try case_decide.
   * constructor.
   * easy.
   * constructor. rewrite listset_difference_raw_in; intuition. easy.
 Qed.
 Global Instance listset_difference: Difference (listset A) := Î» l k,
-  listset_difference_raw (`l) (`k)â†¾listset_difference_raw_nodup (`l) (`k) (proj2_sig l).
+  listset_difference_raw (`l) (`k)â†¾
+    listset_difference_raw_nodup (`l) (`k) (proj2_sig l).
 
 Definition listset_union_raw (l k : list A) := listset_difference_raw l k ++ k.
-Lemma listset_union_raw_in l k x : In x (listset_union_raw l k) â†” In x l âˆ¨ In x k.
-Proof. 
+Lemma listset_union_raw_in l k x :
+  In x (listset_union_raw l k) â†” In x l âˆ¨ In x k.
+Proof.
   unfold listset_union_raw. rewrite in_app_iff, listset_difference_raw_in.
   intuition. case (decide (In x k)); intuition.
 Qed.
-Lemma listset_union_raw_nodup l k : NoDup l â†’ NoDup k â†’ NoDup (listset_union_raw l k).
+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.
@@ -44,7 +56,8 @@ Proof.
   * intro. rewrite listset_difference_raw_in. intuition.
 Qed.
 Global Instance listset_union: Union (listset A) := Î» l k,
-  listset_union_raw (`l) (`k)â†¾listset_union_raw_nodup (`l) (`k) (proj2_sig l) (proj2_sig k).
+  listset_union_raw (`l) (`k)â†¾
+    listset_union_raw_nodup (`l) (`k) (proj2_sig l) (proj2_sig k).
 
 Fixpoint listset_intersection_raw (l k : list A) :=
   match l with
@@ -68,14 +81,17 @@ Proof.
   * easy.
 Qed.
 Global Instance listset_intersection: Intersection (listset A) := Î» l k,
-  listset_intersection_raw (`l) (`k)â†¾listset_intersection_raw_nodup (`l) (`k) (proj2_sig l).
+  listset_intersection_raw (`l) (`k)â†¾
+    listset_intersection_raw_nodup (`l) (`k) (proj2_sig l).
 
 Definition listset_add_raw x (l : list A) : list A :=
   if decide_rel In x l then l else x :: l.
 Lemma listset_add_raw_in x l y : In y (listset_add_raw x l) â†” y = x âˆ¨ In y l.
-Proof. unfold listset_add_raw. case (decide_rel _); firstorder congruence. Qed.
+Proof. unfold listset_add_raw. case_decide; firstorder congruence. Qed.
 Lemma listset_add_raw_nodup x l : NoDup l â†’ NoDup (listset_add_raw x l).
-Proof. unfold listset_add_raw. case (decide_rel _); try constructor; firstorder. Qed. 
+Proof.
+  unfold listset_add_raw. case_decide; try constructor; firstorder.
+Qed.
 
 Fixpoint listset_map_raw (f : A â†’ A) (l : list A) :=
   match l with
@@ -84,7 +100,8 @@ Fixpoint listset_map_raw (f : A â†’ A) (l : list A) :=
   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.
-Lemma listset_map_raw_in f l x : In x (listset_map_raw f l) â†” âˆƒ y, x = f y âˆ§ In y l.
+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 |].
diff --git a/theories/monads.v b/theories/monads.v
deleted file mode 100644
index 62d6b392550e634e9e062688282c048289607e6c..0000000000000000000000000000000000000000
--- a/theories/monads.v
+++ /dev/null
@@ -1,20 +0,0 @@
-Require Import base.
-
-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.
-End monad_ops.
-
-Arguments mret {M MRet A} _.
-Arguments mbind {M MBind A B} _ _.
-Arguments mjoin {M MJoin A} _.
-Arguments fmap {M FMap A B} _ _.
-
-Notation "m â‰«= f" := (mbind f m) (at level 60, right associativity) : C_scope.
-Notation "x â† y ; z" := (y â‰«= (Î» x : _, z))
-  (at level 65, next at level 35, right associativity) : C_scope.
-Infix "<$>" := fmap (at level 65, right associativity, only parsing) : C_scope.
diff --git a/theories/nmap.v b/theories/nmap.v
index 03791529e53c1baad78761c3178938ab7c0b4690..8e6fe722136c8231833bc8291b80fb460b70eeb9 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -1,3 +1,7 @@
+(* Copyright (c) 2012, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** This files extends the implementation of finite over [positive] to finite
+maps whose keys range over Coq's data type of binary naturals [N]. *)
 Require Import pmap.
 Require Export prelude fin_maps.
 
@@ -8,8 +12,10 @@ Arguments Nmap_0 {_} _.
 Arguments Nmap_pos {_} _.
 Arguments Build_Nmap {_} _ _.
 
-Global Instance Pmap_dec `{âˆ€ x y : A, Decision (x = y)} : âˆ€ x y : Nmap A, Decision (x = y).
+Global Instance Pmap_dec `{âˆ€ x y : A, Decision (x = y)} :
+  âˆ€ x y : Nmap A, Decision (x = y).
 Proof. solve_decision. Defined.
+
 Global Instance Nempty {A} : Empty (Nmap A) := Build_Nmap None âˆ….
 Global Instance Nlookup: Lookup N Nmap := Î» A i t,
   match i with
@@ -49,7 +55,7 @@ Proof.
   * intros ??? [??] []. easy. apply lookup_fmap.
   * intros ?? ???????? [o t] n; unfold dom, lookup, Ndom, Nlookup; simpl.
     rewrite elem_of_union, Plookup_raw_dom.
-    destruct o, n; esimplify_elem_of (simplify_is_Some; eauto).
+    destruct o, n; esolve_elem_of (simplify_is_Some; eauto).
   * intros ? f ? [o1 t1] [o2 t2] [|?].
     + easy.
     + apply (merge_spec f t1 t2).
diff --git a/theories/numbers.v b/theories/numbers.v
index a3df40efe0254e10420b2ad441d17dcea64f1cea..dbf29a5b00bb81f12a1cd71395b25836674093a3 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -1,3 +1,7 @@
+(* 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. *)
 Require Export PArith NArith ZArith.
 Require Export base decidable fin_collections.
 
@@ -24,13 +28,30 @@ Notation "(â‰¤)" := Z.le (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.
 
-Definition Z_to_option_N (x : Z) :=
+(** * Conversions *)
+(** 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
   | Zpos p => Some (Npos p)
   | Zneg _ => None
   end.
 
+(** The function [Z_decide] converts a decidable proposition [P] into an integer
+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]. *)
+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.
@@ -44,8 +65,8 @@ Proof.
   change ((Î» b X, x âˆˆ X â†’ (x â‰¤ b)%N) (collection_fold N.max 0%N X) X).
   apply collection_fold_ind.
   * solve_proper.
-  * simplify_elem_of.
-  * simplify_elem_of. apply N.le_max_l. apply N.max_le_iff; auto.
+  * 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.
diff --git a/theories/option.v b/theories/option.v
index 7b7f7c0c4eea93c7ddbd1aae7efe5ca81aee77a6..09beb718e6e3b4ee55705cf6c0c0f5388af42dbb 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -1,5 +1,11 @@
-Require Export base decidable orders.
-
+(* 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 the option
+data type that are not in the Coq standard library. *)
+Require Export base tactics decidable orders.
+
+(** * General definitions and theorems *)
+(** Basic properties about equality. *)
 Lemma None_ne_Some `(a : A) : None â‰  Some a.
 Proof. congruence. Qed.
 Lemma Some_ne_None `(a : A) : Some a â‰  None.
@@ -9,36 +15,43 @@ Proof. congruence. Qed.
 Instance Some_inj {A} : Injective (=) (=) (@Some A).
 Proof. congruence. Qed.
 
-Definition option_case {A B} (f : A â†’ B) (b : B) (x : option A) :=
+(** The non dependent elimination principle on the option type. *)
+Definition option_case {A B} (f : A â†’ B) (b : B) (x : option A) : B :=
   match x with
   | None => b
   | Some a => f a
   end.
 
-Definition maybe {A} (a : A) (x : option A) :=
+(** The [maybe] function allows us to get the value out of the option type
+by specifying a default value. *)
+Definition maybe {A} (a : A) (x : option A) : A :=
   match x with
   | None => a
-  | Some a => a
+  | Some b => b
   end.
 
+(** An alternative, but equivalent, definition of equality on the option
+data type. This theorem is useful to prove that two options are the same. *)
 Lemma option_eq {A} (x y : option A) :
   x = y â†” âˆ€ a, x = Some a â†” y = Some a.
 Proof.
   split.
-  * intros. now subst.
-  * intros E. destruct x, y.
-    + now apply E.
-    + symmetry. now apply E.
-    + now apply E.
-    + easy.
+  { intros. now subst. }
+  intros E. destruct x, y.
+  + now apply E.
+  + symmetry. now apply E.
+  + now apply E.
+  + easy.
 Qed.
 
-Definition is_Some `(x : option A) := âˆƒ a, x = Some a.
+(** We define [is_Some] as a [sig] instead of a [sigT] as extraction of
+witnesses can be derived (see [is_Some_sigT] below). *)
+Definition is_Some `(x : option A) : Prop := âˆƒ a, x = Some a.
 Hint Extern 10 (is_Some _) => solve [eexists; eauto].
 
 Ltac simplify_is_Some := repeat intro; repeat
   match goal with
-  | _ => progress simplify_eqs
+  | _ => progress simplify_equality
   | H : is_Some _ |- _ => destruct H as [??]
   | |- is_Some _ => eauto
   end.
@@ -48,23 +61,24 @@ Proof. simplify_is_Some. Qed.
 Lemma None_not_is_Some {A} : Â¬is_Some (@None A).
 Proof. simplify_is_Some. Qed.
 
-Definition is_Some_1 `(x : option A) : is_Some x â†’ { a | x = Some a } :=
+Definition is_Some_sigT `(x : option A) : is_Some x â†’ { a | x = Some a } :=
   match x with
   | None => False_rect _ âˆ˜ ex_ind None_ne_Some
   | Some a => Î» _, aâ†¾eq_refl
   end.
-Lemma is_Some_2 `(x : option A) a : x = Some a â†’ is_Some x.
+Lemma eq_Some_is_Some `(x : option A) a : x = Some a â†’ is_Some x.
 Proof. simplify_is_Some. Qed.
 
 Lemma eq_None_not_Some `(x : option A) : x = None â†” Â¬is_Some x.
 Proof. destruct x; simpl; firstorder congruence. Qed.
 
-Lemma make_eq_Some {A} (x : option A) a : 
+Lemma make_eq_Some {A} (x : option A) a :
   is_Some x â†’ (âˆ€ b, x = Some b â†’ b = a) â†’ x = Some a.
 Proof. intros [??] H. subst. f_equal. auto. Qed.
 
-Instance option_eq_dec `{dec : âˆ€ x y : A, Decision (x = y)} (x y : option A) :
-    Decision (x = y) :=
+(** Equality on [option] is decidable. *)
+Instance option_eq_dec `{dec : âˆ€ x y : A, Decision (x = y)}
+    (x y : option A) : Decision (x = y) :=
   match x with
   | Some a =>
     match y with
@@ -82,49 +96,7 @@ Instance option_eq_dec `{dec : âˆ€ x y : A, Decision (x = y)} (x y : option A) :
     end
   end.
 
-Inductive option_lift `(P : A â†’ Prop) : option A â†’ Prop :=
-  | option_lift_some x : P x â†’ option_lift P (Some x)
-  | option_lift_None : option_lift P None.
-
-Ltac option_lift_inv := repeat
-  match goal with
-  | H : option_lift _ (Some _) |- _ => inversion H; clear H; subst
-  | H : option_lift _ None |- _ => inversion H
-  end.
-
-Lemma option_lift_inv_Some `(P : A â†’ Prop) x : option_lift P (Some x) â†’ P x.
-Proof. intros. now option_lift_inv. Qed.
-
-Definition option_lift_sig `(P : A â†’ Prop) (x : option A) :
-    option_lift P x â†’ option (sig P) :=
-  match x with
-  | Some a => Î» p, Some (exist _ a (option_lift_inv_Some P a p))
-  | None => Î» _, None
-  end.
-
-Definition option_lift_dsig `(P : A â†’ Prop) `{âˆ€ x : A, Decision (P x)} 
-    (x : option A) : option_lift P x â†’ option (dsig P) :=
-  match x with
-  | Some a => Î» p, Some (dexist a (option_lift_inv_Some P a p))
-  | None => Î» _, None
-  end.
-
-Lemma option_lift_dsig_Some `(P : A â†’ Prop) `{âˆ€ x : A, Decision (P x)} x y px py :
-  option_lift_dsig P x px = Some (yâ†¾py) â†” x = Some y.
-Proof.
-  split.
-  * destruct x; simpl; intros; now simplify_eqs.
-  * intros. subst. simpl. f_equal. now apply dsig_eq.
-Qed.
-
-Lemma option_lift_dsig_is_Some `(P : A â†’ Prop) `{âˆ€ x : A, Decision (P x)} x px :
-  is_Some (option_lift_dsig P x px) â†” is_Some x.
-Proof.
-  split.
-  * intros [[??] ?]. eapply is_Some_2, option_lift_dsig_Some; eauto.
-  * intros [??]. subst. eapply is_Some_2. reflexivity.
-Qed.
-
+(** * Monadic operations *)
 Instance option_ret: MRet option := @Some.
 Instance option_bind: MBind option := Î» A B f x,
   match x with
@@ -138,18 +110,6 @@ Instance option_join: MJoin option := Î» A x,
   end.
 Instance option_fmap: FMap option := @option_map.
 
-Ltac simplify_options := repeat
-  match goal with
-  | _ => progress simplify_eqs
-  | H : mbind (M:=option) ?f ?o = ?x |- _ =>
-    change (option_bind _ _ f o = x) in H;
-    destruct o; simpl in H; try discriminate
-  | H : context [ ?o = _ ] |- mbind (M:=option) ?f ?o = ?x =>
-    change (option_bind _ _ f o = x);
-    erewrite H by eauto;
-    simpl
-  end.
-
 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.
@@ -157,6 +117,26 @@ 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
+  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
+  | H : mbind (M:=option) ?f ?o = ?x |- _ =>
+    destruct o eqn:?
+  | H : context [ ?o = _ ] |- mbind (M:=option) ?f ?o = ?x =>
+    erewrite H by eauto
+  end.
+
+(** * Union, intersection and difference *)
 Instance option_union: UnionWith option := Î» A f x y,
   match x, y with
   | Some a, Some b => Some (f a b)
@@ -184,11 +164,36 @@ Section option_union_intersection.
   Global Instance: RightId (=) None (union_with f).
   Proof. now intros [?|]. Qed.
   Global Instance: Commutative (=) f â†’ Commutative (=) (union_with f).
-  Proof. intros ? [?|] [?|]; compute; try reflexivity. now rewrite (commutative f). Qed.
+  Proof.
+    intros ? [?|] [?|]; compute; try reflexivity.
+    now rewrite (commutative f).
+  Qed.
   Global Instance: Associative (=) f â†’ Associative (=) (union_with f).
-  Proof. intros ? [?|] [?|] [?|]; compute; try reflexivity. now rewrite (associative f). Qed.
+  Proof.
+    intros ? [?|] [?|] [?|]; compute; try reflexivity.
+    now rewrite (associative f).
+  Qed.
   Global Instance: Idempotent (=) f â†’ Idempotent (=) (union_with f).
-  Proof. intros ? [?|]; compute; try reflexivity. now rewrite (idempotent f). Qed.
+  Proof.
+    intros ? [?|]; compute; try reflexivity.
+    now rewrite (idempotent f).
+  Qed.
+
+  Global Instance: Commutative (=) f â†’ Commutative (=) (intersection_with f).
+  Proof.
+    intros ? [?|] [?|]; compute; try reflexivity.
+    now rewrite (commutative f).
+  Qed.
+  Global Instance: Associative (=) f â†’ Associative (=) (intersection_with f).
+  Proof.
+    intros ? [?|] [?|] [?|]; compute; try reflexivity.
+    now rewrite (associative f).
+  Qed.
+  Global Instance: Idempotent (=) f â†’ Idempotent (=) (intersection_with f).
+  Proof.
+    intros ? [?|]; compute; try reflexivity.
+    now rewrite (idempotent f).
+  Qed.
 End option_union_intersection.
 
 Section option_difference.
diff --git a/theories/orders.v b/theories/orders.v
index 9d164b9c7ffef9f3d768e1bdf933ec07dd8c7880..a763f908cf51a4743b8c16ae50386c59f2ff74ee 100644
--- a/theories/orders.v
+++ b/theories/orders.v
@@ -1,5 +1,12 @@
+(* Copyright (c) 2012, Robbert Krebbers. *)
+(* 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.
 
+(** * Pre-orders *)
+(** We extend a pre-order to a partial order by defining equality as
+[Î» X Y, X âŠ† Y âˆ§ Y âŠ† X]. We prove that this indeed gives rise to a setoid. *)
 Section preorder.
   Context `{SubsetEq A} `{!PreOrder (âŠ†)}.
 
@@ -24,6 +31,8 @@ End preorder.
 Hint Extern 0 (@Equivalence _ (â‰¡)) =>
   class_apply preorder_equivalence : typeclass_instances.
 
+(** * Join semi lattices *)
+(** General purpose theorems on join semi lattices. *)
 Section bounded_join_sl.
   Context `{BoundedJoinSemiLattice A}.
 
@@ -72,6 +81,8 @@ Section bounded_join_sl.
   Proof. split; eauto. Qed.
 End bounded_join_sl.
 
+(** * Meet semi lattices *)
+(** The dual of the above section, but now for meet semi lattices. *)
 Section meet_sl.
   Context `{MeetSemiLattice A}.
 
diff --git a/theories/pmap.v b/theories/pmap.v
index 65897410bc17602df70e7f86522a61a1b33e9d63..d760798ee2976581afa9bc308dabd6d92526e880 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -1,3 +1,12 @@
+(* Copyright (c) 2012, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** This files implements an efficient implementation of finite maps whose keys
+range over Coq's data type of positive binary naturals [positive]. The
+implementation is based on Xavier Leroy's implementation of radix-2 search
+trees (uncompressed Patricia trees) and guarantees logarithmic-time operations.
+However, we extend Leroy's implementation by packing the trees into a Sigma
+type such that canonicity of representation is ensured. This is necesarry for
+Leibniz equality to become extensional. *)
 Require Import PArith.
 Require Export prelude fin_maps.
 
@@ -5,12 +14,18 @@ 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
+be represented as a binary tree of an arbitrary size that contains [None] at
+all nodes. *)
 Inductive Pmap_raw A :=
   | Pleaf: Pmap_raw A
   | Pnode: Pmap_raw A â†’ option A â†’ Pmap_raw A â†’ Pmap_raw A.
@@ -21,6 +36,7 @@ Instance Pmap_raw_eq_dec `{âˆ€ x y : A, Decision (x = y)} (x y : Pmap_raw A) :
   Decision (x = y).
 Proof. solve_decision. Defined.
 
+(** The following predicate describes non empty trees. *)
 Inductive Pmap_ne {A} : Pmap_raw A â†’ Prop :=
   | Pmap_ne_val l x r : Pmap_ne (Pnode l (Some x) r)
   | Pmap_ne_l l r : Pmap_ne l â†’ Pmap_ne (Pnode l None r)
@@ -36,6 +52,8 @@ Proof.
       inversion_clear 1; contradiction.
 Qed.
 
+(** The following predicate describes well well formed trees. A tree is well
+formed if it is empty or if all nodes at the bottom contain a value. *)
 Inductive Pmap_wf {A} : Pmap_raw A â†’ Prop :=
   | Pmap_wf_leaf : Pmap_wf Pleaf
   | Pmap_wf_node l x r : Pmap_wf l â†’ Pmap_wf r â†’ Pmap_wf (Pnode l (Some x) r)
@@ -49,17 +67,19 @@ Proof.
   * intuition.
   * destruct IHl, IHr; try solve [left; intuition];
       right; inversion_clear 1; intuition.
-  * destruct IHl, IHr, (decide (Pmap_ne l)), (decide (Pmap_ne r)); 
+  * destruct IHl, IHr, (decide (Pmap_ne l)), (decide (Pmap_ne r));
       try solve [left; intuition]; right; inversion_clear 1; intuition.
 Qed.
 
+(** Now we restrict the data type of trees to those that are well formed. *)
 Definition Pmap A := @dsig (Pmap_raw A) Pmap_wf _.
 
+(** * Operations on the data structure *)
 Global Instance Pmap_dec `{âˆ€ x y : A, Decision (x = y)} (t1 t2 : Pmap A) :
     Decision (t1 = t2) :=
   match Pmap_raw_eq_dec (`t1) (`t2) with
-  | left H => left (dsig_eq _ t1 t2 H)
-  | right H => right (H âˆ˜ eq_ind _ (Î» x, `t1 = `x) eq_refl _)
+  | left H => left (proj2 (dsig_eq _ t1 t2) H)
+  | right H => right (H âˆ˜ proj1 (dsig_eq _ t1 t2))
   end.
 
 Instance Pempty_raw {A} : Empty (Pmap_raw A) := Pleaf.
@@ -152,13 +172,13 @@ Lemma Pnode_canon_wf `(l : Pmap_raw A) (o : option A) (r : Pmap_raw A) :
 Proof. intros H1 H2. destruct H1, o, H2; simpl; intuition. Qed.
 Local Hint Resolve Pnode_canon_wf.
 
-Lemma Pnode_canon_lookup_xH `(l : Pmap_raw A) (o : option A) (r : Pmap_raw A) :
+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.
-Lemma Pnode_canon_lookup_xO `(l : Pmap_raw A) (o : option A) (r : Pmap_raw A) i :
+Lemma Pnode_canon_lookup_xO `(l : Pmap_raw A) o (r : Pmap_raw A) i :
   Pnode_canon l o r !! i~0 = l !! i.
 Proof. now destruct l,o,r. Qed.
-Lemma Pnode_canon_lookup_xI `(l : Pmap_raw A) (o : option A) (r : Pmap_raw A) i :
+Lemma Pnode_canon_lookup_xI `(l : Pmap_raw A) o (r : Pmap_raw A) i :
   Pnode_canon l o r !! i~1 = r !! i.
 Proof. now destruct l,o,r. Qed.
 Ltac Pnode_canon_rewrite := repeat (
@@ -222,11 +242,13 @@ Instance Pfmap_raw: FMap Pmap_raw :=
     Pnode (@fmap _ Pfmap_raw _ _ f l) (fmap f x) (@fmap _ Pfmap_raw _ _ f 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. 
+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.
 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. 
+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,
   dexist _ (Pfmap_raw_wf f _ (proj2_dsig t)).
@@ -235,6 +257,8 @@ 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.
 
+(** The [dom] function is rather inefficient, but since we do not intend to
+use it for computation it does not really matter to us. *)
 Section dom.
   Context `{Collection B D}.
 
@@ -249,22 +273,22 @@ Section dom.
     x âˆˆ Pdom_raw f t â†” âˆƒ i, x = f i âˆ§ is_Some (t !! i).
   Proof.
     split.
-    * revert f. induction t as [|? IHl [?|] ? IHr]; esimplify_elem_of.
+    * 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 [?|?|];
-        simplify_elem_of (now apply (IHl (f âˆ˜ (~0))) 
+        solve_elem_of (now apply (IHl (f âˆ˜ (~0)))
         || now apply (IHr (f âˆ˜ (~1))) || simplify_is_Some).
   Qed.
 End dom.
 
-Global Instance Pdom {A} : Dom positive (Pmap A) := Î» C _ _ _ t, Pdom_raw id (`t).
+Global Instance Pdom {A} : Dom positive (Pmap A) := Î» C _ _ _ t,
+  Pdom_raw id (`t).
 
 Fixpoint Pmerge_aux `(f : option A â†’ option B) (t : Pmap_raw A) : Pmap_raw B :=
   match t with
   | Pleaf => Pleaf
   | Pnode l o r => Pnode_canon (Pmerge_aux f l) (f o) (Pmerge_aux f r)
   end.
-Local Hint Constructors option_lift.
 
 Lemma Pmerge_aux_wf `(f : option A â†’ option B) (t : Pmap_raw A) :
   Pmap_wf t â†’ Pmap_wf (Pmerge_aux f t).
@@ -284,7 +308,8 @@ Global Instance Pmerge_raw: Merge Pmap_raw :=
   match t1, t2 with
   | Pleaf, t2 => Pmerge_aux (f None) t2
   | t1, Pleaf => Pmerge_aux (flip f None) t1
-  | Pnode l1 o1 r1, Pnode l2 o2 r2 => Pnode_canon (@merge _ Pmerge_raw _ f l1 l2)
+  | Pnode l1 o1 r1, Pnode l2 o2 r2 =>
+     Pnode_canon (@merge _ Pmerge_raw _ f l1 l2)
       (f o1 o2) (@merge _ Pmerge_raw _ f r1 r2)
   end.
 Local Arguments Pmerge_aux _ _ _ _ : simpl never.
@@ -293,7 +318,8 @@ Lemma Pmerge_wf {A} f (t1 t2 : Pmap_raw A) :
   Pmap_wf t1 â†’ Pmap_wf t2 â†’ Pmap_wf (merge f t1 t2).
 Proof. intros t1wf. revert t2. induction t1wf; destruct 1; simpl; auto. Qed.
 Global Instance Pmerge: Merge Pmap := Î» A f t1 t2,
-  dexist (merge f (`t1) (`t2)) (Pmerge_wf _ _ _ (proj2_dsig t1) (proj2_dsig t2)).
+  dexist (merge f (`t1) (`t2))
+    (Pmerge_wf _ _ _ (proj2_dsig t1) (proj2_dsig t2)).
 
 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).
diff --git a/theories/prelude.v b/theories/prelude.v
index 86fe754c144d2ec36cded163891a11364dbcd1cf..39beaa8d556a2dc5aee8b828094681bb250bbb2a 100644
--- a/theories/prelude.v
+++ b/theories/prelude.v
@@ -1,10 +1,14 @@
+(* Copyright (c) 2012, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
 Require Export
-  base 
+  base
+  tactics
   decidable
   orders
-  collections
-  fin_collections
   option
   list
+  collections
+  fin_collections
+  listset
   subset
-  numbers.
\ No newline at end of file
+  numbers.
diff --git a/theories/subset.v b/theories/subset.v
index 27662375b256e4a73057b7445793d55324fbe41c..00a45e9586b9e8f867a3e743db06d33fcd0af5b9 100644
--- a/theories/subset.v
+++ b/theories/subset.v
@@ -1,3 +1,7 @@
+(* Copyright (c) 2012, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** This file implements the operations on non computable subsets [A â†’ Prop]
+over some carrier [A]. *)
 Require Export base.
 
 Definition subset A := A â†’ Prop.
@@ -6,7 +10,8 @@ Instance subset_elem_of {A} : ElemOf A (subset A) | 100 := Î» x P, P x.
 Instance subset_empty {A} : Empty (subset A) := Î» _, False.
 Instance subset_singleton {A} : Singleton A (subset A) := (=).
 Instance subset_union {A} : Union (subset A) := Î» P Q x, P x âˆ¨ Q x.
-Instance subset_intersection {A} : Intersection (subset A) := Î» P Q x, P x âˆ§ Q x.
+Instance subset_intersection {A} : Intersection (subset A) := Î» P Q x,
+  P x âˆ§ Q x.
 Instance subset_difference {A} : Difference (subset A) := Î» P Q x, P x âˆ§ Â¬Q x.
 Instance subset_map {A} : Map A (subset A) := Î» f P x, âˆƒ y, f y = x âˆ§ P y.
 
diff --git a/theories/tactics.v b/theories/tactics.v
new file mode 100644
index 0000000000000000000000000000000000000000..ea2b9ce066648b293e5edf80d1a2fe2c66cfc75d
--- /dev/null
+++ b/theories/tactics.v
@@ -0,0 +1,171 @@
+(* Copyright (c) 2012, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** This file collects some general purpose tactics that are used throughout
+the development. *)
+Require Export base.
+
+(** 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 : _ = _ |- _ => discriminate H
+  | H : _ = _ |-  ?G =>
+    (* avoid introducing additional equalities *)
+    change (id G); injection H; clear H; intros; unfold id at 1
+  end.
+
+(** Coq's default [remember] tactic does have an option to name the generated
+equality. The following tactic extends [remember] to do so. *)
+Tactic Notation "remember" constr(t) "as" "(" ident(x) "," ident(E) ")" :=
+  remember t as x;
+  match goal with
+  | 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) :=
+  let rec go l :=
+  match l with
+  | nil => idtac
+  | ?x :: ?l => tac x || go l
+  end in go l.
+
+(** Given H : [A_1 â†’ ... â†’ A_n â†’ B] (where each [A_i] is non-dependent), the
+tactic [feed tac H tac_by] creates a subgoal for each [A_i] and calls [tac p]
+with the generated proof [p] of [B]. *)
+Tactic Notation "feed" tactic(tac) constr(H) :=
+  let rec go H :=
+  let T := type of H in
+  lazymatch eval hnf in T with
+  | ?T1 â†’ ?T2 =>
+    (* Use a separate counter for fresh names to make it more likely that
+    the generated name is "fresh" with respect to those generated before
+    calling the [feed] tactic. In particular, this hack makes sure that
+    tactics like [let H' := fresh in feed (fun p => pose proof p as H') H] do
+    not break. *)
+    let HT1 := fresh "feed" in assert T1 as HT1;
+      [| go (H HT1); clear HT1 ]
+  | ?T1 => tac H
+  end in go H.
+
+(** The tactic [efeed tac H] is similar to [feed], but it also instantiates
+dependent premises of [H] with evars. *)
+Tactic Notation "efeed" tactic(tac) constr(H) :=
+  let rec go H :=
+  let T := type of H in
+  lazymatch eval hnf in T with
+  | ?T1 â†’ ?T2 =>
+    let HT1 := fresh "feed" in assert T1 as HT1;
+      [| go (H HT1); clear HT1 ]
+  | ?T1 â†’ _ =>
+    let e := fresh "feed" in evar (e:T1);
+    let e' := eval unfold e in e in
+    clear e; go (H e')
+  | ?T1 => tac H
+  end in go H.
+
+(** The following variants of [pose proof], [specialize], [inversion], and
+[destruct], use the [feed] tactic before invoking the actual tactic. *)
+Tactic Notation "feed" "pose" "proof" constr(H) "as" ident(H') :=
+  feed (fun p => pose proof p as H') H.
+Tactic Notation "feed" "pose" "proof" constr(H) :=
+  feed (fun p => pose proof p) H.
+
+Tactic Notation "efeed" "pose" "proof" constr(H) "as" ident(H') :=
+  efeed (fun p => pose proof p as H') H.
+Tactic Notation "efeed" "pose" "proof" constr(H) :=
+  efeed (fun p => pose proof p) H.
+
+Tactic Notation "feed" "specialize" hyp(H) :=
+  feed (fun p => specialize p) H.
+Tactic Notation "efeed" "specialize" hyp(H) :=
+  efeed (fun p => specialize p) H.
+
+Tactic Notation "feed" "inversion" constr(H) :=
+  feed (fun p => let H':=fresh in pose proof p as H'; inversion H') H.
+Tactic Notation "feed" "inversion" constr(H) "as" simple_intropattern(IP) :=
+  feed (fun p => let H':=fresh in pose proof p as H'; inversion H' as IP) H.
+
+Tactic Notation "feed" "destruct" constr(H) :=
+  feed (fun p => let H':=fresh in pose proof p as H'; destruct H') 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
+and incomplete [firstorder]-like solver using Ltac's backtracking mechanism.
+The tactic suffers from the following limitations:
+- It might leave unresolved evars as Ltac provides no way to detect that.
+- To avoid the tactic going into pointless loops, it just does not allow a
+  universally quantified hypothesis to be used more than once.
+- It does not perform backtracking on instantiation of universally quantified
+  assumptions.
+
+Despite these limitations, it works much better than Coq's [firstorder] tactic
+for the purposes of this development. This tactic either fails or proves the
+goal. *)
+Tactic Notation "naive_solver" tactic(tac) :=
+  unfold iff, not in *;
+  let rec go :=
+  repeat match goal with
+  (**i intros *)
+  | |- âˆ€ _, _ => intro
+  (**i simplification of assumptions *)
+  | H : False |- _ => destruct H
+  | H : _ âˆ§ _ |- _ => destruct H
+  | H : âˆƒ _, _  |- _ => destruct H
+  (**i simplify and solve equalities *)
+  | |- _ => progress simpl in *
+  | |- _ => progress simplify_equality
+  (**i solve the goal *)
+  | |- _ => eassumption
+  | |- _ => now constructor
+  | |- _ => now symmetry
+  (**i operations that generate more subgoals *)
+  | |- _ âˆ§ _ => split
+  | H : _ âˆ¨ _ |- _ => destruct H
+  (**i solve the goal using the user supplied tactic *)
+  | |- _ => solve [tac]
+  end;
+  (**i use recursion to enable backtracking on the following clauses *)
+  match goal with
+  (**i instantiations of assumptions *)
+  | H : _ â†’ _ |- _ =>
+    is_non_dependent H; eapply H; clear H; go
+  | H : _ â†’ _ |- _ =>
+    is_non_dependent H;
+    (**i create subgoals for all premises *)
+    efeed (fun p =>
+      match type of p with
+      | _ âˆ§ _ =>
+        let H' := fresh in pose proof p as H'; destruct H'
+      | âˆƒ _, _ =>
+        let H' := fresh in pose proof p as H'; destruct H'
+      | _ âˆ¨ _ =>
+        let H' := fresh in pose proof p as H'; destruct H'
+      | False =>
+        let H' := fresh in pose proof p as H'; destruct H'
+      end) H;
+    (**i solve these subgoals, but clear [H] to avoid loops *)
+    clear H; go
+  (**i instantiation of the conclusion *)
+  | |- âˆƒ x, _ => eexists; go
+  | |- _ âˆ¨ _ => first [left; go | right; go]
+  end in go.
+Tactic Notation "naive_solver" := naive_solver eauto.
diff --git a/theories/trs.v b/theories/trs.v
deleted file mode 100644
index 17f79db56e67f42a31610db1afc7230046c674af..0000000000000000000000000000000000000000
--- a/theories/trs.v
+++ /dev/null
@@ -1,141 +0,0 @@
-Require Export base.
-
-Definition red `(R : relation A) (x : A) := âˆƒ y, R x y.
-Definition nf `(R : relation A) (x : A) := Â¬red R x.
-
-(* The reflexive transitive closure *)
-Inductive rtc `(R : relation A) : relation A :=
-  | rtc_refl x : rtc R x x
-  | rtc_l x y z : R x y â†’ rtc R y z â†’ rtc R x z.
-(* A reduction of exactly n steps *)
-Inductive nsteps `(R : relation A) : nat â†’ relation A :=
-  | nsteps_O x : nsteps R 0 x x
-  | nsteps_l n x y z : R x y â†’ nsteps R n y z â†’ nsteps R (S n) x z.
-(* A reduction whose length is bounded by n *)
-Inductive bsteps `(R : relation A) : nat â†’ relation A :=
-  | bsteps_refl n x : bsteps R n x x
-  | bsteps_l n x y z : R x y â†’ bsteps R n y z â†’ bsteps R (S n) x z.
-(* The transitive closure *)
-Inductive tc `(R : relation A) : relation A :=
-  | tc_once x y : R x y â†’ tc R x y
-  | tc_l x y z : R x y â†’ tc R y z â†’ tc R x z.
-
-Hint Constructors rtc nsteps bsteps tc : trs.
-
-Arguments rtc_l {_ _ _ _ _} _ _.
-Arguments nsteps_l {_ _ _ _ _ _} _ _.
-Arguments bsteps_refl {_ _} _ _.
-Arguments bsteps_l {_ _ _ _ _ _} _ _.
-Arguments tc_once {_ _ _} _ _.
-Arguments tc_l {_ _ _ _ _} _ _.
-
-Ltac generalize_rtc H :=
-  match type of H with
-  | rtc ?R ?x ?y =>
-    let Hx := fresh in let Hy := fresh in
-    let Heqx := fresh in let Heqy := fresh in
-    remember x as (Hx,Heqx); remember y as (Hy,Heqy);
-    revert Heqx Heqy; repeat
-      match x with
-      | context [ ?z ] => revert z
-      end; repeat
-      match y with
-      | context [ ?z ] => revert z
-      end
-  end.
-
-Section rtc.
-  Context `{R : relation A}.
-
-  Global Instance: Reflexive (rtc R).
-  Proof rtc_refl R.
-  Global Instance rtc_trans: Transitive (rtc R).
-  Proof. red; induction 1; eauto with trs. Qed.
-  Lemma rtc_once {x y} : R x y â†’ rtc R x y.
-  Proof. eauto with trs. Qed.
-  Global Instance: subrelation R (rtc R).
-  Proof. exact @rtc_once. Qed.
-  Lemma rtc_r {x y z} : rtc R x y â†’ R y z â†’ rtc R x z.
-  Proof. intros. etransitivity; eauto with trs. Qed.
-
-  Lemma rtc_inv {x z} : rtc R x z â†’ x = z âˆ¨ âˆƒ y, R x y âˆ§ rtc R y z.
-  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.
-  Proof.
-    cut (âˆ€ y z, rtc R y z â†’ âˆ€ x, rtc R x y â†’ P x y â†’ P x z).
-    { eauto using rtc_refl. }
-    induction 1; eauto using rtc_r.
-  Qed.
-
-  Lemma rtc_inv_r {x z} : rtc R x z â†’ x = z âˆ¨ âˆƒ y, rtc R x y âˆ§ R y z.
-  Proof. revert x z. apply rtc_ind_r; eauto. Qed.
-
-  Lemma nsteps_once {x y} : R x y â†’ nsteps R 1 x y.
-  Proof. eauto with trs. Qed.
-  Lemma nsteps_trans {n m x y z} :
-    nsteps R n x y â†’ nsteps R m y z â†’ nsteps R (n + m) x z.
-  Proof. induction 1; simpl; eauto with trs. Qed.
-  Lemma nsteps_r {n x y z} : nsteps R n x y â†’ R y z â†’ nsteps R (S n) x z.
-  Proof. induction 1; eauto with trs. Qed.
-  Lemma nsteps_rtc {n x y} : nsteps R n x y â†’ rtc R x y.
-  Proof. induction 1; eauto with trs. Qed.
-  Lemma rtc_nsteps {x y} : rtc R x y â†’ âˆƒ n, nsteps R n x y.
-  Proof. induction 1; firstorder eauto with trs. Qed.
-
-  Lemma bsteps_once {n x y} : R x y â†’ bsteps R (S n) x y.
-  Proof. eauto with trs. Qed.
-  Lemma bsteps_plus_r {n m x y} :
-    bsteps R n x y â†’ bsteps R (n + m) x y.
-  Proof. induction 1; simpl; eauto with trs. Qed.
-  Lemma bsteps_weaken {n m x y} :
-    n â‰¤ m â†’ bsteps R n x y â†’ bsteps R m x y.
-  Proof.
-    intros. rewrite (Minus.le_plus_minus n m); auto using bsteps_plus_r.
-  Qed.
-  Lemma bsteps_plus_l {n m x y} :
-    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.
-  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 trs. Qed.
-  Lemma bsteps_r {n x y z} : bsteps R n x y â†’ R y z â†’ bsteps R (S n) x z.
-  Proof. induction 1; eauto with trs. Qed.
-  Lemma bsteps_rtc {n x y} : bsteps R n x y â†’ rtc R x y.
-  Proof. induction 1; eauto with trs. Qed.
-  Lemma rtc_bsteps {x y} : rtc R x y â†’ âˆƒ n, bsteps R n x y.
-  Proof. induction 1. exists 0. auto with trs. firstorder eauto with trs. Qed.
-
-  Global Instance tc_trans: Transitive (tc R).
-  Proof. red; induction 1; eauto with trs. Qed.
-  Lemma tc_r {x y z} : tc R x y â†’ R y z â†’ tc R x z.
-  Proof. intros. etransitivity; eauto with trs. Qed.
-  Lemma tc_rtc {x y} : tc R x y â†’ rtc R x y.
-  Proof. induction 1; eauto with trs. Qed.
-  Global Instance: subrelation (tc R) (rtc R).
-  Proof. exact @tc_rtc. Qed.
-End rtc.
-
-Hint Resolve rtc_once rtc_r tc_r : trs.
-
-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.
-  Lemma nf_subrel x : nf R2 x â†’ nf R1 x.
-  Proof. intros H1 H2. destruct H1. now apply red_subrel. Qed.
-
-  Global Instance rtc_subrel: subrelation (rtc R1) (rtc R2).
-  Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed.
-  Global Instance nsteps_subrel: subrelation (nsteps R1 n) (nsteps R2 n).
-  Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed.
-  Global Instance bsteps_subrel: subrelation (bsteps R1 n) (bsteps R2 n).
-  Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed.
-  Global Instance tc_subrel: subrelation (tc R1) (tc R2).
-  Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed.
-End subrel.