Major revision of the whole development.

The main changes are:

* Function calls in the operational semantics
* Mutually recursive function calls in the axiomatic semantics
* A general definition of the interpretation of the axiomatic semantics  so as
  to improve reusability (useful for function calls, and also for expressions
  in future versions)
* Type classes for stack independent, memory independent, and memory extensible
  assertions, and a lot of instances to automatically derive these properties.
* Many additional lemmas on the memory and more robust tactics to simplify
  goals involving is_free and mem_disjoint
* Proof of preservation of statements in the smallstep semantics

* Some new tactics: feed, feed destruct, feed inversion, etc...
* More robust tactic scripts using bullets and structured scripts
* Truncate most lines at 80 characters

theories/base.v

@@ -2,15 +2,14 @@ Global Generalizable All Variables.
 Global Set Automatic Coercions Import.
 Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid NArith.
 
-Arguments existT {_ _} _ _.
-Arguments existT2 {_ _ _} _ _ _.
+Arguments id _ _/.
+Arguments compose _ _ _ _ _ _ /.
+
+(* Change True and False into notations so we can overload them *)
+Notation "'True'" := True : type_scope.
+Notation "'False'" := False : type_scope.
 
-Definition proj1_T2 {A} {P Q : A → Type} (x : sigT2 P Q) : A :=
-  match x with existT2 a _ _ => a end.
-Definition proj2_T2 {A} {P Q : A → Type} (x : sigT2 P Q) : P (proj1_T2 x) :=
-  match x with existT2 _ p _ => p end.
-Definition proj3_T2 {A} {P Q : A → Type} (x : sigT2 P Q) : Q (proj1_T2 x) :=
-  match x with existT2 _ _ q => q end.
+Arguments existT {_ _} _ _.
 
 (*  Common notations *)
 Delimit Scope C_scope with C.
@@ -28,7 +27,8 @@ Hint Extern 0 (?x = ?x) => reflexivity.
 Notation "(→)" := (λ x y, x → y) : C_scope.
 Notation "( T →)" := (λ y, T → y) : C_scope.
 Notation "(→ T )" := (λ y, y → T) : C_scope.
-Notation "t $ r" := (t r) (at level 65, right associativity, only parsing) : C_scope.
+Notation "t $ r" := (t r)
+  (at level 65, right associativity,only parsing) : C_scope.
 Infix "∘" := compose : C_scope.
 Notation "(∘)" := compose (only parsing) : C_scope.
 Notation "( f ∘)" := (compose f) (only parsing) : C_scope.
@@ -91,8 +91,9 @@ 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.
+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.
 Infix "∈" := elem_of (at level 70) : C_scope.
@@ -104,16 +105,26 @@ 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.
 
-Class UnionWith M := union_with: ∀ {A}, (A → A → A) → M A → M A → M A.
-Class IntersectWith M := intersect_with: ∀ {A}, (A → A → A) → M A → M A → M A.
+Class UnionWith M :=
+  union_with: ∀ {A}, (A → A → A) → M A → M A → M A.
+Class IntersectionWith M :=
+  intersection_with: ∀ {A}, (A → A → A) → M A → M A → M A.
+Class DifferenceWith M :=
+  difference_with: ∀ {A}, (A → A → option A) → M A → M A → M A.
 
 (* Common properties *)
-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) := idempotent: ∀ x, R (f x x) x.
-Class Commutative {A B} R (f : B → B → A) := commutative: ∀ x y, R (f x y) (f y x).
-Class LeftId {A} R (i : A) (f : A → A → A) := left_id: ∀ x, R (f i x) x.
-Class RightId {A} R (i : A) (f : A → A → A) := right_id: ∀ x, R (f x i) x.
-Class Associative {A} R (f : A → A → A) := associative: ∀ x y z, R (f x (f y z)) (f (f x y) z).
+Class 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) :=
+  idempotent: ∀ x, R (f x x) x.
+Class Commutative {A B} R (f : B → B → A) :=
+  commutative: ∀ x y, R (f x y) (f y x).
+Class LeftId {A} R (i : A) (f : A → A → A) :=
+  left_id: ∀ x, R (f i x) x.
+Class RightId {A} R (i : A) (f : A → A → A) :=
+  right_id: ∀ x, R (f x i) x.
+Class Associative {A} R (f : A → A → A) :=
+  associative: ∀ x y z, R (f x (f y z)) (f (f x y) z).
 
 Arguments injective {_ _ _ _} _ {_} _ _ _.
 Arguments idempotent {_ _} _ {_} _.
@@ -123,15 +134,20 @@ Arguments right_id {_ _} _ _ {_} _.
 Arguments associative {_ _} _ {_} _ _ _.
 
 (* Using idempotent_eq we can force Coq to not use the setoid mechanism *)
-Lemma idempotent_eq {A} (f : A → A → A) `{!Idempotent (=) f} x : f x x = x.
+Lemma idempotent_eq {A} (f : A → A → A) `{!Idempotent (=) f} x :
+  f x x = x.
 Proof. auto. Qed.
-Lemma commutative_eq {A B} (f : B → B → A) `{!Commutative (=) f} x y : f x y = f y x.
+Lemma commutative_eq {A B} (f : B → B → A) `{!Commutative (=) f} x y :
+  f x y = f y x.
 Proof. auto. Qed.
-Lemma left_id_eq {A} (i : A) (f : A → A → A) `{!LeftId (=) i f} x : f i x = x.
+Lemma left_id_eq {A} (i : A) (f : A → A → A) `{!LeftId (=) i f} x :
+  f i x = x.
 Proof. auto. Qed.
-Lemma right_id_eq {A} (i : A) (f : A → A → A) `{!RightId (=) i f} x : f x i = x.
+Lemma right_id_eq {A} (i : A) (f : A → A → A) `{!RightId (=) i f} x :
+  f x i = x.
 Proof. auto. Qed.
-Lemma associative_eq {A} (f : A → A → A) `{!Associative (=) f} x y z : f x (f y z) = f (f x y) z.
+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 *)
@@ -150,7 +166,8 @@ 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.
+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 *)
@@ -159,7 +176,8 @@ Class BoundedPreOrder A `{Empty A} `{SubsetEq A} := {
   subseteq_empty x : ∅ ⊆ x
 }.
 
-(* Note: no equality to avoid the need for setoids. We define equality in a generic way. *)
+(* Note: no equality to avoid the need for setoids. We define setoid 
+equality in a generic way. *)
 Class BoundedJoinSemiLattice A `{Empty A} `{SubsetEq A} `{Union A} := {
   jsl_preorder :>> BoundedPreOrder A;
   subseteq_union_l x y : x ⊆ x ∪ y;
@@ -180,7 +198,7 @@ Class Map A C := map: (A → A) → (C → C).
 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 ∉ ∅;
-  elem_of_singleton (x y : A) : x ∈ {{ y }} ↔ x = y;
+  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;
   elem_of_difference X Y (x : A) : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y;
@@ -208,15 +226,31 @@ Notation "(!!)" := lookup (only parsing) : C_scope.
 Notation "( m !!)" := (λ i, lookup i m) (only parsing) : C_scope.
 Notation "(!! i )" := (lookup i) (only parsing) : C_scope.
 
-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) : C_scope.
-Class Delete K M := delete: K → M → M.
+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.
+
 Instance pointwise_reflexive {A} `{R : relation B} :
   Reflexive R → Reflexive (pointwise_relation A R) | 9.
 Proof. firstorder. Qed.
@@ -227,20 +261,26 @@ Instance pointwise_transitive {A} `{R : relation B} :
   Transitive R → Transitive (pointwise_relation A R) | 9.
 Proof. firstorder. Qed.
 
-Definition fst_map {A A' B} (f : A → A') (p : A * B) : A' * B := (f (fst p), snd p).
-Definition snd_map {A B B'} (f : B → B') (p : A * B) : A * B' := (fst p, f (snd p)).
-Definition prod_relation {A B} (R1 : relation A) (R2 : relation B) : relation (A * B) := λ x y,
-  R1 (fst x) (fst y) ∧ R2 (snd x) (snd y).
+Definition fst_map {A A' B} (f : A → A') (p : A * B) : A' * B :=
+  (f (fst p), snd p).
+Definition snd_map {A B B'} (f : B → B') (p : A * B) : A * B' :=
+  (fst p, f (snd p)).
+Definition prod_relation {A B} (R1 : relation A) (R2 : relation B) :
+  relation (A * B) := λ x y, R1 (fst x) (fst y) ∧ R2 (snd x) (snd y).
 
 Section prod_relation.
   Context `{R1 : relation A} `{R2 : relation B}.
-  Global Instance: Reflexive R1 → Reflexive R2 → Reflexive (prod_relation R1 R2).
+  Global Instance:
+    Reflexive R1 → Reflexive R2 → Reflexive (prod_relation R1 R2).
   Proof. firstorder eauto. Qed.
-  Global Instance: Symmetric R1 → Symmetric R2 → Symmetric (prod_relation R1 R2).
+  Global Instance:
+    Symmetric R1 → Symmetric R2 → Symmetric (prod_relation R1 R2).
   Proof. firstorder eauto. Qed.
-  Global Instance: Transitive R1 → Transitive R2 → Transitive (prod_relation R1 R2).
+  Global Instance:
+    Transitive R1 → Transitive R2 → Transitive (prod_relation R1 R2).
   Proof. firstorder eauto. Qed.
-  Global Instance: Equivalence R1 → Equivalence R2 → Equivalence (prod_relation R1 R2).
+  Global Instance:
+    Equivalence R1 → Equivalence R2 → Equivalence (prod_relation R1 R2).
   Proof. split; apply _. Qed.
   Global Instance: Proper (R1 ==> R2 ==> prod_relation R1 R2) pair.
   Proof. firstorder eauto. Qed.
@@ -250,11 +290,13 @@ Section prod_relation.
   Proof. firstorder eauto. Qed.
 End prod_relation.
 
-Definition lift_relation {A B} (R : relation A) (f : B → A) : relation B := λ x y, R (f x) (f y).
+Definition lift_relation {A B} (R : relation A)
+  (f : B → A) : relation B := λ x y, R (f x) (f y).
 Definition lift_relation_equivalence {A B} (R : relation A) (f : B → A) :
   Equivalence R → Equivalence (lift_relation R f).
 Proof. unfold lift_relation. firstorder. Qed.
-Hint Extern 0 (Equivalence (lift_relation _ _)) => eapply @lift_relation_equivalence : typeclass_instances.
+Hint Extern 0 (Equivalence (lift_relation _ _)) =>
+  eapply @lift_relation_equivalence : typeclass_instances.
 
 Instance: ∀ A B (x : B), Commutative (=) (λ _ _ : A, x).
 Proof. easy. Qed.
@@ -269,11 +311,14 @@ Proof. easy. Qed.
 Instance: ∀ A, Idempotent (=) (λ _ x : A, x).
 Proof. easy. Qed.
 
-Instance left_id_propholds {A} (R : relation A) i f : LeftId R i f → ∀ x, PropHolds (R (f i x) x).
+Instance left_id_propholds {A} (R : relation A) i f :
+  LeftId R i f → ∀ x, PropHolds (R (f i x) x).
 Proof. easy. Qed.
-Instance right_id_propholds {A} (R : relation A) i f : RightId R i f → ∀ x, PropHolds (R (f x i) x).
+Instance right_id_propholds {A} (R : relation A) i f :
+  RightId R i f → ∀ x, PropHolds (R (f x i) x).
 Proof. easy. Qed.
-Instance idem_propholds {A} (R : relation A) f : Idempotent R f → ∀ x, PropHolds (R (f x x) x).
+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
@@ -283,7 +328,8 @@ Ltac simplify_eqs := repeat
   | 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 : _ = _ |-  ?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.
@@ -303,3 +349,51 @@ Tactic Notation "remember" constr(t) "as" "(" ident(x) "," ident(E) ")" :=
   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.

theories/collections.v

@@ -21,28 +21,36 @@ Section collection.
   Proof. easy. Qed.
   Lemma elem_of_equiv X Y : X ≡ Y ↔ ∀ x, x ∈ X ↔ x ∈ Y.
   Proof. firstorder. Qed.
-  Lemma elem_of_equiv_alt X Y : X ≡ Y ↔ (∀ x, x ∈ X → x ∈ Y) ∧ (∀ x, x ∈ Y → x ∈ X).
+  Lemma elem_of_equiv_alt X Y :
+    X ≡ Y ↔ (∀ x, x ∈ X → x ∈ Y) ∧ (∀ x, x ∈ Y → x ∈ X).
   Proof. firstorder. Qed.
 
   Global Instance: Proper ((=) ==> (≡) ==> iff) (∈).
   Proof. intros ???. subst. firstorder. Qed.
 
-  Lemma empty_ne_singleton x :  ∅ ≢ {{ x }}.
-  Proof. intros [_ E]. destruct (elem_of_empty x). apply E. now apply elem_of_singleton. Qed. 
+  Lemma empty_ne_singleton x :  ∅ ≢ {[ x ]}.
+  Proof.
+    intros [_ E]. destruct (elem_of_empty x).
+    apply E. now apply elem_of_singleton.
+  Qed. 
 End collection.
 
 Section cmap.
   Context `{Collection A C}.
 
-  Lemma elem_of_map_1 (f : A → A) (X : C) (x : A) : x ∈ X → f x ∈ map f X.
+  Lemma elem_of_map_1 (f : A → A) (X : C) (x : A) :
+    x ∈ X → f x ∈ map f X.
   Proof. intros. apply (elem_of_map _). eauto. Qed.
-  Lemma elem_of_map_1_alt (f : A → A) (X : C) (x : A) y : x ∈ X → y = f x → y ∈ map f X.
+  Lemma elem_of_map_1_alt (f : A → A) (X : C) (x : A) y :
+    x ∈ X → y = f x → y ∈ map f X.
   Proof. intros. apply (elem_of_map _). eauto. Qed.
-  Lemma elem_of_map_2 (f : A → A) (X : C) (x : A) : x ∈ map f X → ∃ y, x = f y ∧ y ∈ X.
+  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).
+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.
@@ -52,7 +60,7 @@ Ltac split_elem_ofs := repeat
   | 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_singleton in H
+  | H : context [ _ ∈ {[ _ ]} ] |- _ => setoid_rewrite elem_of_singleton in H
   | H : context [ _ ∈ _ ∪ _ ] |- _ => setoid_rewrite elem_of_union in H
   | H : context [ _ ∈ _ ∩ _ ] |- _ => setoid_rewrite elem_of_intersection in H
   | H : context [ _ ∈ _ ∖ _ ] |- _ => setoid_rewrite elem_of_difference in H
@@ -60,7 +68,7 @@ Ltac split_elem_ofs := repeat
   | |- 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_singleton
+  | |- context [ _ ∈ {[ _ ]} ] => setoid_rewrite elem_of_singleton
   | |- context [ _ ∈ _ ∪ _ ] => setoid_rewrite elem_of_union
   | |- context [ _ ∈ _ ∩ _ ] => setoid_rewrite elem_of_intersection
   | |- context [ _ ∈ _ ∖ _ ] => setoid_rewrite elem_of_difference
@@ -97,9 +105,12 @@ Ltac naive_firstorder t :=
   (* solve *)
   | |- _ => solve [t]
   (* dirty destructs *)
-  | H : context [ ∃ _, _ ] |- _ => edestruct 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
-  | H : context [ _ ∨ _ ] |- _ => edestruct 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
+  | 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
@@ -125,8 +136,8 @@ Section no_dup.
   Global Instance: Proper (R ==> (≡) ==> iff) elem_of_upto.
   Proof.
     intros ?? E1 ?? E2. split; intros [z [??]]; exists z.
-     rewrite <-E1, <-E2; intuition.
-    rewrite E1, E2; intuition.
+    * rewrite <-E1, <-E2; intuition.
+    * rewrite E1, E2; intuition.
   Qed.
   Global Instance: Proper ((≡) ==> iff) no_dup.
   Proof. firstorder. Qed.
@@ -135,20 +146,24 @@ Section no_dup.
   Proof. unfold elem_of_upto. esimplify_elem_of. Qed.
   Lemma elem_of_upto_empty x : ¬elem_of_upto x ∅.
   Proof. unfold elem_of_upto. esimplify_elem_of. Qed.
-  Lemma elem_of_upto_singleton x y : elem_of_upto x {{ y }} ↔ R x y.
+  Lemma elem_of_upto_singleton x y : elem_of_upto x {[ y ]} ↔ R x y.
   Proof. unfold elem_of_upto. esimplify_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.
+  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.
   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.
 
   Lemma no_dup_empty: no_dup ∅.
   Proof. unfold no_dup. simplify_elem_of. Qed.
-  Lemma no_dup_add x X : ¬elem_of_upto x X → no_dup X → no_dup ({{ x }} ∪ X).
+  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.
-  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. 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.
+  Qed.
   Lemma no_dup_inv_union_l X Y : no_dup (X ∪ Y) → no_dup X.
   Proof. unfold no_dup. simplify_elem_of. Qed.
   Lemma no_dup_inv_union_r X Y : no_dup (X ∪ Y) → no_dup Y.
@@ -163,7 +178,7 @@ Section quantifiers.
 
   Lemma cforall_empty : cforall ∅.
   Proof. unfold cforall. simplify_elem_of. Qed.
-  Lemma cforall_singleton x : cforall {{ x }} ↔ P x.
+  Lemma cforall_singleton x : cforall {[ x ]} ↔ P x.
   Proof. unfold cforall. simplify_elem_of. Qed.
   Lemma cforall_union X Y : cforall X → cforall Y → cforall (X ∪ Y).
   Proof. unfold cforall. simplify_elem_of. Qed.
@@ -174,7 +189,7 @@ Section quantifiers.
 
   Lemma cexists_empty : ¬cexists ∅.
   Proof. unfold cexists. esimplify_elem_of. Qed.
-  Lemma cexists_singleton x : cexists {{ x }} ↔ P x.
+  Lemma cexists_singleton x : cexists {[ x ]} ↔ P x.
   Proof. unfold cexists. esimplify_elem_of. Qed.
   Lemma cexists_union_1 X Y : cexists X → cexists (X ∪ Y).
   Proof. unfold cexists. esimplify_elem_of. Qed.
@@ -184,9 +199,43 @@ Section quantifiers.
   Proof. unfold cexists. esimplify_elem_of. Qed.
 End quantifiers.
 
-Lemma cforall_weak `{Collection A B} (P Q : A → Prop) (Hweak : ∀ x, P x → Q x) X :
-  cforall P X → cforall Q X.
-Proof. firstorder. Qed.
-Lemma cexists_weak `{Collection A B} (P Q : A → Prop) (Hweak : ∀ x, P x → Q x) X :
-  cexists P X → cexists Q X.
-Proof. firstorder. Qed.
+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.
+  Lemma cexists_weak (P Q : A → Prop) (Hweak : ∀ x, P x → Q x) X :
+    cexists P X → cexists Q X.
+  Proof. firstorder. Qed.
+End more_quantifiers.
+
+Section fresh.
+  Context `{Collection A C} `{Fresh A C} `{!FreshSpec A C} .
+
+  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.
+
+  Lemma fresh_list_length n X : length (fresh_list n X) = n.
+  Proof. revert X. induction n; simpl; auto. Qed.
+
+  Lemma fresh_list_is_fresh n X x : In x (fresh_list n X) → x ∉ X.
+  Proof.
+    revert X. induction n; simpl.
+    * easy.
+    * intros X [?| Hin]. subst.
+      + apply is_fresh.
+      + apply IHn in Hin. simplify_elem_of.
+  Qed.
+
+  Lemma fresh_list_nodup n X : NoDup (fresh_list n X).
+  Proof.
+    revert X.
+    induction n; simpl; constructor; auto.
+    intros Hin. apply fresh_list_is_fresh in Hin.
+    simplify_elem_of.
+  Qed.
+End fresh.

theories/decidable.v

@@ -6,9 +6,11 @@ Definition decide_rel {A B} (R : A → B → Prop)
 Ltac case_decide := 
   match goal with
   | H : context [@decide ?P ?dec] |- _ => case (@decide P dec) in *
-  | H : context [@decide_rel _ _ ?R ?x ?y ?dec] |- _ => case (@decide_rel _ _ R x y dec) in *
+  | 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 *
-  | |- context [@decide_rel _ _ ?R ?x ?y ?dec] => case (@decide_rel _ _ R x y dec) in *
+  | |- context [@decide_rel _ _ ?R ?x ?y ?dec] =>
+     case (@decide_rel _ _ R x y dec) in *
   end.
 
 Ltac solve_trivial_decision :=
@@ -16,25 +18,28 @@ Ltac solve_trivial_decision :=
   | [ |- Decision (?P) ] => apply _
   | [ |- sumbool ?P (¬?P) ] => change (Decision P); apply _
   end.
-Ltac solve_decision :=
-  first [solve_trivial_decision | unfold Decision; decide equality; solve_trivial_decision].
+Ltac solve_decision := 
+  intros; first [ solve_trivial_decision
+                | unfold Decision; decide equality; solve_trivial_decision ].
 
 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,
+    `(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) :=
+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) :=
+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
@@ -48,15 +53,22 @@ 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.
 
-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) := bool_decide_unpack _ (proj2_sig x).
-Definition dexist `{∀ x : A, Decision (P x)} (x : A) (p : P x) : dsig P := x↾bool_decide_pack _ p.
+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) :=
+  bool_decide_unpack _ (proj2_sig 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.
+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.
+Lemma dsig_eq {A} (P : A → Prop) {dec : ∀ x, Decision (P x)}
+  (x y : { x | bool_decide (P x) }) : `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)). simpl. now intros [] []. easy.
+  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.
 Qed.

theories/fin_collections.v

@@ -11,9 +11,9 @@ Context `{FinCollection A C}.
 Global Instance elements_proper: Proper ((≡) ==> Permutation) elements.
 Proof.
   intros ?? E. apply NoDup_Permutation.
-    apply elements_nodup.
-   apply elements_nodup.
-  intros. now rewrite <-!elements_spec, E.
+  * apply elements_nodup.
+  * apply elements_nodup.
+  * intros. now rewrite <-!elements_spec, E.
 Qed.
 Global Instance collection_size_proper: Proper ((≡) ==> (=)) size.
 Proof. intros ?? E. apply Permutation_length. now rewrite E. Qed.
@@ -21,8 +21,8 @@ Proof. intros ?? E. apply Permutation_length. now rewrite E. Qed.
 Lemma size_empty : size ∅ = 0.
 Proof.
   unfold size, collection_size. rewrite (in_nil_inv (elements ∅)).
-   easy.
-  intro. rewrite <-elements_spec. simplify_elem_of.
+  * easy.
+  * intro. rewrite <-elements_spec. simplify_elem_of.
 Qed.
 Lemma size_empty_inv X : size X = 0 → X ≡ ∅.
 Proof.
@@ -32,52 +32,54 @@ Qed.
 Lemma size_empty_iff X : size X = 0 ↔ X ≡ ∅.
 Proof. split. apply size_empty_inv. intros E. now rewrite E, size_empty. Qed.
 
-Lemma size_singleton x : size {{ x }} = 1.
+Lemma size_singleton x : size {[ x ]} = 1.
 Proof.
-  change (length (elements {{x}}) = length [x]).
+  change (length (elements {[ x ]}) = length [x]).
   apply Permutation_length, NoDup_Permutation.
-    apply elements_nodup.
-   apply NoDup_singleton.
-  intros. rewrite <-elements_spec. esimplify_elem_of firstorder.
+  * apply elements_nodup.
+  * apply NoDup_singleton.
+  * intros. rewrite <-elements_spec. esimplify_elem_of firstorder.
 Qed.
 Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y.
 Proof.
   unfold size, collection_size. rewrite !elements_spec.
   generalize (elements X). intros [|? l].
-   discriminate.
-  injection 1. intro. rewrite (nil_length l) by easy.
-  simpl. intuition congruence.
+  * discriminate.
+  * injection 1. intro. rewrite (nil_length l) by easy.
+    simpl. intuition congruence.
 Qed.
 
 Lemma choose X : X ≢ ∅ → { x | x ∈ X }.
 Proof.
   case_eq (elements X).
-   intros E. intros []. apply equiv_empty.
-   intros x. rewrite elements_spec, E. contradiction.
-  intros x l E. exists x. rewrite elements_spec, E. now left.
+  * intros E. intros []. apply equiv_empty.
+    intros x. rewrite elements_spec, E. contradiction.
+  * intros x l E. exists x.
+    rewrite elements_spec, E. now left.
 Qed.
 Lemma size_pos_choose X : 0 < size X → { x | x ∈ X }.
 Proof. 
   intros E. apply choose.
-  intros E2. rewrite E2, size_empty in E. now destruct (Lt.lt_n_0 0).
+  intros E2. rewrite E2, size_empty in E.
+  now destruct (Lt.lt_n_0 0).
 Qed.
-Lemma size_1_choose X : size X = 1 → { x | X ≡ {{ x }} }.
+Lemma size_1_choose X : size X = 1 → { x | X ≡ {[ x ]} }.
 Proof.
   intros E. destruct (size_pos_choose X).
-   rewrite E. auto with arith.
-  exists x. simplify_elem_of. eapply size_singleton_inv; eauto.
+  * rewrite E. auto with arith.
+  * exists x. simplify_elem_of. eapply size_singleton_inv; eauto.
 Qed.
 
 Program Instance collection_car_eq_dec_slow (x y : A) : Decision (x = y) | 100 :=
-  match Compare_dec.zerop (size ({{ x }} ∩ {{ y }})) with
+  match Compare_dec.zerop (size ({[ x ]} ∩ {[ y ]})) with
   | left _ => right _
   | right _ => left _
   end.
 Next Obligation.
   intro. apply empty_ne_singleton with x.
-  transitivity ({{ x }} ∩ {{ y }}).
-   symmetry. now apply size_empty_iff.
-  simplify_elem_of.
+  transitivity ({[ x ]} ∩ {[ y ]}).
+  * symmetry. now apply size_empty_iff.
+  * simplify_elem_of.
 Qed.
 Next Obligation. edestruct size_pos_choose; esimplify_elem_of. Qed.
 
@@ -87,9 +89,7 @@ Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100 :=
   | right Hx => right (Hx ∘ proj1 (elements_spec _ _))
   end.
 
-Lemma union_diff_1 X Y : X ⊆ Y → X ∪ Y ∖ X ≡ Y.
-Proof. split; intros x; destruct (decide (x ∈ X)); simplify_elem_of. Qed.
-Lemma union_diff_2 X Y : X ∪ Y ≡ X ∪ Y ∖ X.
+Lemma union_difference X Y : X ∪ Y ∖ X ≡ X ∪ Y.
 Proof. split; intros x; destruct (decide (x ∈ X)); simplify_elem_of. Qed.
 
 Lemma size_union X Y : X ∩ Y ≡ ∅ → size (X ∪ Y) = size X + size Y.
@@ -103,80 +103,98 @@ Proof.
   intros. rewrite in_app_iff, <-!elements_spec. simplify_elem_of.
 Qed.
 Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X).
-Proof. rewrite <-size_union. now rewrite union_diff_2. simplify_elem_of. Qed.
-Lemma size_add X x : x ∉ X → size ({{ x }} ∪ X) = S (size X).
+Proof. rewrite <-size_union. now rewrite union_difference. simplify_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.
-Lemma size_diff X Y : X ⊆ Y → size X + size (Y ∖ X) = size Y.
+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.
+Lemma size_remove X x : x ∈ X → S (size (X ∖ {[ x ]})) = size X.
 Proof.
-  intros. rewrite <-(size_diff {{ x }} X).
-   rewrite size_singleton. auto with arith.
-  simplify_elem_of.
+  intros. rewrite <-(size_difference {[ x ]} X).
+  * rewrite size_singleton. auto with arith.
+  * simplify_elem_of.
 Qed.
 
 Lemma subseteq_size X Y : X ⊆ Y → size X ≤ size Y.
-Proof. intros. rewrite <-(union_diff_1 X Y), size_union by simplify_elem_of. auto with arith. Qed. 
+Proof.
+  intros. rewrite <-(subseteq_union_1 X Y) by easy.
+  rewrite <-(union_difference X Y), size_union by simplify_elem_of.
+  auto with arith.
+Qed. 
 
 Lemma collection_wf_ind (P : C → Prop) :
   (∀ X, (∀ Y, size Y < size X → P Y) → P X) → ∀ X, P X.
 Proof.
-  intros Hind. assert (∀ n X, size X < n → P X) as help.
-   induction n.
-    intros. now destruct (Lt.lt_n_0 (size X)).
-   intros. apply Hind. intros. apply IHn. eauto with arith.
-  intros. apply help with (S (size X)). auto with arith.
+  intros Hind. cut (∀ n X, size X < n → P X).
+  { intros help X. apply help with (S (size X)). auto with arith. }
+  induction n; intros.
+  * now destruct (Lt.lt_n_0 (size X)).
+  * apply Hind. intros. apply IHn. eauto with arith.
 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 <-(union_diff_1 {{ x }} X); simplify_elem_of.
-  apply Hadd; simplify_elem_of. apply IH.
-  rewrite <-(size_remove X x); auto with arith.
+  * now rewrite size_empty_inv.
+  * destruct (size_pos_choose X); auto.
+    rewrite <-(subseteq_union_1 {[ x ]} X) by simplify_elem_of.
+    rewrite <-union_difference.
+    apply Hadd; simplify_elem_of. apply IH.
+    rewrite <-(size_remove X x); auto with arith.
 Qed.
 
 Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
   Proper ((=) ==> (≡) ==> iff) P →
-  P b ∅ → (∀ x X r, x ∉ X → P r X → P (f x r) ({{ x }} ∪ X)) → ∀ X, P (collection_fold f b X) X.
+  P b ∅ →
+  (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) →
+  ∀ X, P (collection_fold f b X) X.
 Proof.
   intros ? Hemp Hadd.
-  assert (∀ l, NoDup l → ∀ X, (∀ x, x ∈ X ↔ In x l) → P (fold_right f b l) X) as help.
-   induction 1 as [|x l ?? IHl]; simpl.
-    intros X HX. rewrite equiv_empty; esimplify_elem_of.
-   intros X HX. rewrite <-(union_diff_1 {{ x }} X).
+  cut (∀ l, NoDup l → ∀ X, (∀ x, x ∈ X ↔ In x l) → P (fold_right f b l) X).
+  { intros help ?. apply help. apply elements_nodup. apply elements_spec. }
+  induction 1 as [|x l ?? IHl]; simpl.
+  * intros X HX. rewrite equiv_empty. easy. intros ??. firstorder.
+  * intros X HX.
+    rewrite <-(subseteq_union_1 {[ x ]} X) by esimplify_elem_of.
+    rewrite <-union_difference.
     apply Hadd. simplify_elem_of. apply IHl.
     intros y. split.
-     intros. destruct (proj1 (HX y)); simplify_elem_of.
-    esimplify_elem_of.
-   esimplify_elem_of.
-  intros. apply help. apply elements_nodup. apply elements_spec.
+    + intros. destruct (proj1 (HX y)); simplify_elem_of.
+    + esimplify_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. 
 
-Global Program Instance cforall_dec `(P : A → Prop) `{∀ x, Decision (P x)} X : Decision (cforall P X) | 100 :=
+Global Program Instance cforall_dec `(P : A → Prop)
+    `{∀ x, Decision (P x)} X : Decision (cforall P X) | 100 :=
   match decide (Forall P (elements X)) with
   | left Hall => left _
   | right Hall => right _
   end.
-Next Obligation. red. setoid_rewrite elements_spec. now apply Forall_forall. Qed. 
-Next Obligation. intro. apply Hall, Forall_forall. setoid_rewrite <-elements_spec. auto. Qed.
+Next Obligation.
+  red. setoid_rewrite elements_spec. now apply Forall_forall.
+Qed. 
+Next Obligation.
+  intro. apply Hall, Forall_forall. setoid_rewrite <-elements_spec. auto.
+Qed.
 
-Global Program Instance cexists_dec `(P : A → Prop) `{∀ x, Decision (P x)} X : Decision (cexists P X) | 100 :=
+Global Program Instance cexists_dec `(P : A → Prop)
+    `{∀ x, Decision (P x)} X : Decision (cexists P X) | 100 :=
   match decide (Exists P (elements X)) with
   | left Hex => left _
   | right Hex => right _
   end.
-Next Obligation. red. setoid_rewrite elements_spec. now apply Exists_exists. Qed. 
-Next Obligation. intro. apply Hex, Exists_exists. setoid_rewrite <-elements_spec. auto. Qed.
+Next Obligation.
+  red. setoid_rewrite elements_spec. now apply Exists_exists. 
+Qed. 
+Next Obligation.
+  intro. apply Hex, Exists_exists. setoid_rewrite <-elements_spec. auto.
+Qed.
 
-Global Instance 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).
+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).
 End fin_collection.

theories/listset.v

@@ -7,59 +7,71 @@ Context {A : Type} `{∀ x y : A, Decision (x = y)}.
 
 Global Instance listset_elem_of: ElemOf A (listset A) := λ x l, In x (`l).
 Global Instance listset_empty: Empty (listset A) := []↾@NoDup_nil _.
-Global Instance listset_singleton: Singleton A (listset A) := λ x, [x]↾NoDup_singleton x.
+Global Instance listset_singleton: Singleton A (listset A) := λ x,
+  [x]↾NoDup_singleton x.
 
-Fixpoint listset_diff_raw (l k : list A) :=
+Fixpoint listset_difference_raw (l k : list A) :=
   match l with
   | [] => []
-  | x :: l => if decide_rel In x k then listset_diff_raw l k else x :: listset_diff_raw l k
+  | x :: l =>
+    if decide_rel In x k
+    then listset_difference_raw l k
+    else x :: listset_difference_raw l k
   end.
-Lemma listset_diff_raw_in l k x : In x (listset_diff_raw l k) ↔ In x l ∧ ¬In x k.
+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_diff_raw_nodup l k : NoDup l → NoDup (listset_diff_raw l k).
+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_diff_raw_in; intuition. easy.
+  * constructor.
+  * easy.
+  * constructor. rewrite listset_difference_raw_in; intuition. easy.
 Qed.
-Global Instance listset_diff: Difference (listset A) := λ l k,
-  listset_diff_raw (`l) (`k)↾listset_diff_raw_nodup (`l) (`k) (proj2_sig l).
+Global Instance listset_difference: Difference (listset A) := λ l k,
+  listset_difference_raw (`l) (`k)↾listset_difference_raw_nodup (`l) (`k) (proj2_sig l).
 
-Definition listset_union_raw (l k : list A) := listset_diff_raw l k ++ k.
+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. 
-  unfold listset_union_raw. rewrite in_app_iff, listset_diff_raw_in.
+  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).
 Proof.
   intros. apply NoDup_app.
-    now apply listset_diff_raw_nodup.
-   easy.
-  intro. rewrite listset_diff_raw_in. intuition.
+  * now apply listset_difference_raw_nodup.
+  * easy.
+  * 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).
 
-Fixpoint listset_inter_raw (l k : list A) :=
+Fixpoint listset_intersection_raw (l k : list A) :=
   match l with
   | [] => []
-  | x :: l => if decide_rel In x k then x :: listset_inter_raw l k else listset_inter_raw l k
+  | x :: l =>
+    if decide_rel In x k
+    then x :: listset_intersection_raw l k
+    else listset_intersection_raw l k
   end.
-Lemma listset_inter_raw_in l k x : In x (listset_inter_raw l k) ↔ In x l ∧ In x k.
-Proof. split; induction l; simpl; try case_decide; simpl; intuition congruence. Qed.
-Lemma listset_inter_raw_nodup l k : NoDup l → NoDup (listset_inter_raw l k).
+Lemma listset_intersection_raw_in l k x :
+  In x (listset_intersection_raw l k) ↔ In x l ∧ In x k.
+Proof.
+  split; induction l; simpl; try case_decide; simpl; intuition congruence.
+Qed.
+Lemma listset_intersection_raw_nodup l k :
+  NoDup l → NoDup (listset_intersection_raw l k).
 Proof.
   induction 1; simpl; try case_decide.
-    constructor.
-   constructor. rewrite listset_inter_raw_in; intuition. easy.
-  easy.
+  * constructor.
+  * constructor. rewrite listset_intersection_raw_in; intuition. easy.
+  * easy.
 Qed.
-Global Instance listset_inter: Intersection (listset A) := λ l k,
-  listset_inter_raw (`l) (`k)↾listset_inter_raw_nodup (`l) (`k) (proj2_sig l).
+Global Instance listset_intersection: Intersection (listset A) := λ l k,
+  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.
+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.
 Lemma listset_add_raw_nodup x l : NoDup l → NoDup (listset_add_raw x l).
@@ -75,9 +87,10 @@ 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.
 Proof.
   split.
-   induction l; simpl. easy. rewrite listset_add_raw_in. firstorder.
-  intros [?[??]]. subst. induction l; simpl in *. easy.
-  rewrite listset_add_raw_in. firstorder congruence.
+  * induction l; simpl; [easy |].
+    rewrite listset_add_raw_in. firstorder.
+  * intros [?[??]]. subst. induction l; simpl in *; [easy |].
+    rewrite listset_add_raw_in. firstorder congruence.
 Qed.
 Global Instance listset_map: Map A (listset A) := λ f l,
   listset_map_raw f (`l)↾listset_map_raw_nodup f (`l).
@@ -85,12 +98,12 @@ Global Instance listset_map: Map A (listset A) := λ f l,
 Global Instance: Collection A (listset A).
 Proof.
   split.
-       easy.
-      compute. intuition.
-     intros. apply listset_union_raw_in.
-    intros. apply listset_inter_raw_in.
-   intros. apply listset_diff_raw_in.
-  intros. apply listset_map_raw_in.
+  * easy.
+  * compute. intuition.
+  * intros. apply listset_union_raw_in.
+  * intros. apply listset_intersection_raw_in.
+  * intros. apply listset_difference_raw_in.
+  * intros. apply listset_map_raw_in.
 Qed.
 
 Global Instance listset_elems: Elements A (listset A) := @proj1_sig _ _.

theories/monads.v

@@ -15,5 +15,6 @@ 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.
+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.

theories/nmap.v

@@ -23,7 +23,7 @@ Global Instance Npartial_alter: PartialAlter N Nmap := λ A f i t,
   end.
 Global Instance Ndom {A} : Dom N (Nmap A) := λ A _ _ _ t,
   match t with
-  | Build_Nmap o t => option_case (λ _, {{ 0 }}) ∅ o ∪ (Pdom_raw Npos (`t))
+  | Build_Nmap o t => option_case (λ _, {[ 0 ]}) ∅ o ∪ (Pdom_raw Npos (`t))
   end.
 Global Instance Nmerge: Merge Nmap := λ A f t1 t2,
   match t1, t2 with
@@ -37,16 +37,20 @@ Global Instance Nfmap: FMap Nmap := λ A B f t,
 Global Instance: FinMap N Nmap.
 Proof.
   split.
-        intros ? [??] [??] H. f_equal.
-         now apply (H 0).
-        apply finmap_eq. intros i. now apply (H (Npos i)).
-       now intros ? [|?].
-      intros ? f [? t] [|i]. easy. now apply (lookup_partial_alter f t i).
-     intros ? f [? t] [|i] [|j]; try intuition congruence.
-     intros. apply (lookup_partial_alter_ne f t i j). congruence.
-    intros ??? [??] []. easy. apply lookup_fmap.
-   intros ?? ???????? [o t] n; unfold dom, lookup, Ndom, Nlookup; simpl.
-   rewrite elem_of_union, Plookup_raw_dom.
-   destruct o, n; esimplify_elem_of (simplify_is_Some; eauto).
-  intros ? f ? [o1 t1] [o2 t2] [|?]. easy. apply (merge_spec f t1 t2).
+  * intros ? [??] [??] H. f_equal.
+    + now apply (H 0).
+    + apply finmap_eq. intros i. now apply (H (Npos i)).
+  * now intros ? [|?].
+  * intros ? f [? t] [|i].
+    + easy.
+    + now apply (lookup_partial_alter f t i).
+  * intros ? f [? t] [|i] [|j]; try intuition congruence.
+    intros. apply (lookup_partial_alter_ne f t i j). congruence.
+  * intros ??? [??] []. easy. apply lookup_fmap.
+  * intros ?? ???????? [o t] n; unfold dom, lookup, Ndom, Nlookup; simpl.
+    rewrite elem_of_union, Plookup_raw_dom.
+    destruct o, n; esimplify_elem_of (simplify_is_Some; eauto).
+  * intros ? f ? [o1 t1] [o2 t2] [|?].
+    + easy.
+    + apply (merge_spec f t1 t2).
 Qed.

theories/numbers.v

 Require Export PArith NArith ZArith.
 Require Export base decidable fin_collections.
 
+Infix "≤" := le : nat_scope.
+
 Instance nat_eq_dec: ∀ x y : nat, Decision (x = y) := eq_nat_dec.
 Instance positive_eq_dec: ∀ x y : positive, Decision (x = y) := Pos.eq_dec.
 Notation "(~0)" := xO (only parsing) : positive_scope.
@@ -41,18 +43,19 @@ Lemma Nmax_max `{FinCollection N C} X x : x ∈ X → (x ≤ Nmax X)%N.
 Proof.
   change ((λ b X, x ∈ X → (x ≤ b)%N) (collection_fold N.max 0%N X) X).
   apply collection_fold_ind.
-    solve_proper.
-   simplify_elem_of.
-  simplify_elem_of. apply N.le_max_l. apply N.max_le_iff; auto.
+  * solve_proper.
+  * simplify_elem_of.
+  * simplify_elem_of. apply N.le_max_l. apply N.max_le_iff; auto.
 Qed.
 
 Instance Nfresh `{FinCollection N C} : Fresh N C := λ l, (1 + Nmax l)%N.
 Instance Nfresh_spec `{FinCollection N C} : FreshSpec N C.
 Proof.
   split.
-   intros. unfold fresh, Nfresh.
-   setoid_replace X with Y; esimplify_elem_of.
-  intros X E. assert (1 ≤ 0)%N as []; [| easy].
-  apply N.add_le_mono_r with (Nmax X).
-  now apply Nmax_max.
+  * intros. unfold fresh, Nfresh.
+    setoid_replace X with Y; [easy |].
+    now apply elem_of_equiv.
+  * intros X E. assert (1 ≤ 0)%N as []; [| easy].
+    apply N.add_le_mono_r with (Nmax X).
+    now apply Nmax_max.
 Qed.

theories/option.v

@@ -6,7 +6,7 @@ Lemma Some_ne_None `(a : A) : Some a ≠ None.
 Proof. congruence. Qed.
 Lemma eq_None_ne_Some `(x : option A) a : x = None → x ≠ Some a.
 Proof. congruence. Qed.
-Lemma Some_inj {A} (a b : A) : Some a = Some b → a = b.
+Instance Some_inj {A} : Injective (=) (=) (@Some A).
 Proof. congruence. Qed.
 
 Definition option_case {A B} (f : A → B) (b : B) (x : option A) :=
@@ -15,26 +15,33 @@ Definition option_case {A B} (f : A → B) (b : B) (x : option A) :=
   | Some a => f a
   end.
 
+Definition maybe {A} (a : A) (x : option A) :=
+  match x with
+  | None => a
+  | Some a => a
+  end.
+
 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.
 Hint Extern 10 (is_Some _) => solve [eexists; eauto].
 
-Ltac simplify_is_Some := repeat intro; repeat (
+Ltac simplify_is_Some := repeat intro; repeat
   match goal with
+  | _ => progress simplify_eqs
   | H : is_Some _ |- _ => destruct H as [??]
   | |- is_Some _ => eauto
-  end || simplify_eqs).
+  end.
 
 Lemma Some_is_Some `(a : A) : is_Some (Some a).
 Proof. simplify_is_Some. Qed.
@@ -56,14 +63,15 @@ 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) :=
+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
     | Some b =>
       match dec a b with
       | left H => left (f_equal _ H)
-      | right H => right (H ∘ Some_inj _ _)
+      | right H => right (H ∘ injective Some _ _)
       end
     | None => right (Some_ne_None _)
     end
@@ -87,7 +95,8 @@ Ltac option_lift_inv := repeat
 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) :=
+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
@@ -104,16 +113,16 @@ Lemma option_lift_dsig_Some `(P : A → Prop) `{∀ x : A, Decision (P x)} x y p
   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.
+  * 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.
+  * intros [[??] ?]. eapply is_Some_2, option_lift_dsig_Some; eauto.
+  * intros [??]. subst. eapply is_Some_2. reflexivity.
 Qed.
 
 Instance option_ret: MRet option := @Some.
@@ -141,9 +150,11 @@ Ltac simplify_options := repeat
     simpl
   end.
 
-Lemma option_fmap_is_Some {A B} (f : A → B) (x : option A) : is_Some x ↔ is_Some (f <$> x).
+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.
-Lemma option_fmap_is_None {A B} (f : A → B) (x : option A) : x = None ↔ f <$> x = None.
+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.
 
 Instance option_union: UnionWith option := λ A f x y,
@@ -153,13 +164,19 @@ Instance option_union: UnionWith option := λ A f x y,
   | None, Some b => Some b
   | None, None => None
   end.
-Instance option_intersect: IntersectWith option := λ A f x y,
+Instance option_intersection: IntersectionWith option := λ A f x y,
   match x, y with
   | Some a, Some b => Some (f a b)
   | _, _ => None
   end.
+Instance option_difference: DifferenceWith option := λ A f x y,
+  match x, y with
+  | Some a, Some b => f a b
+  | Some a, None => Some a
+  | None, _ => None
+  end.
 
-Section option_union_intersect.
+Section option_union_intersection.
   Context {A} (f : A → A → A).
 
   Global Instance: LeftId (=) None (union_with f).
@@ -172,4 +189,11 @@ Section option_union_intersect.
   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.
-End option_union_intersect.
+End option_union_intersection.
+
+Section option_difference.
+  Context {A} (f : A → A → option A).
+
+  Global Instance: RightId (=) None (difference_with f).
+  Proof. now intros [?|]. Qed.
+End option_difference.

theories/orders.v

@@ -5,17 +5,24 @@ Section preorder.
 
   Global Instance preorder_equiv: Equiv A := λ X Y, X ⊆ Y ∧ Y ⊆ X.
   Instance preorder_equivalence: @Equivalence A (≡).
-  Proof. split. firstorder. firstorder. intros x y z; split; transitivity y; firstorder. Qed.
+  Proof.
+    split.
+    * firstorder.
+    * firstorder.
+    * intros x y z; split; transitivity y; firstorder.
+  Qed.
 
   Global Instance: Proper ((≡) ==> (≡) ==> iff) (⊆).
   Proof.
-    unfold equiv, preorder_equiv. intros x1 y1 ? x2 y2 ?. split; intro.
-     transitivity x1. tauto. transitivity x2; tauto.
-    transitivity y1. tauto. transitivity y2; tauto.
+    unfold equiv, preorder_equiv.
+    intros x1 y1 ? x2 y2 ?. split; intro.
+    * transitivity x1. tauto. transitivity x2; tauto.
+    * transitivity y1. tauto. transitivity y2; tauto.
   Qed.
 End preorder.
 
-Hint Extern 0 (@Equivalence _ (≡)) => class_apply preorder_equivalence : typeclass_instances.
+Hint Extern 0 (@Equivalence _ (≡)) =>
+  class_apply preorder_equivalence : typeclass_instances.
 
 Section bounded_join_sl.
   Context `{BoundedJoinSemiLattice A}.
@@ -40,7 +47,9 @@ Section bounded_join_sl.
   Proof. auto. Qed.
 
   Global Instance: Proper ((≡) ==> (≡) ==> (≡)) (∪).
-  Proof. unfold equiv, preorder_equiv. split; apply union_compat; simpl in *; tauto. Qed.
+  Proof.
+    unfold equiv, preorder_equiv. split; apply union_compat; simpl in *; tauto.
+  Qed.
   Global Instance: Idempotent (≡) (∪).
   Proof. split; eauto. Qed.
   Global Instance: LeftId (≡) ∅ (∪).
@@ -66,7 +75,8 @@ End bounded_join_sl.
 Section meet_sl.
   Context `{MeetSemiLattice A}.
 
-  Hint Resolve subseteq_intersection_l subseteq_intersection_r intersection_greatest.
+  Hint Resolve subseteq_intersection_l subseteq_intersection_r
+    intersection_greatest.
 
   Lemma intersection_compat_l x1 x2 y : x1 ⊆ x2 → x1 ∩ y ⊆ x2.
   Proof. intros. transitivity x1; auto. Qed.
@@ -84,7 +94,10 @@ Section meet_sl.
   Proof. auto. Qed.
 
   Global Instance: Proper ((≡) ==> (≡) ==> (≡)) (∩).
-  Proof. unfold equiv, preorder_equiv. split; apply intersection_compat; simpl in *; tauto. Qed.
+  Proof.
+    unfold equiv, preorder_equiv. split;
+      apply intersection_compat; simpl in *; tauto.
+  Qed.
   Global Instance: Idempotent (≡) (∩).
   Proof. split; eauto. Qed.
   Global Instance: Commutative (≡) (∩).

theories/pmap.v

@@ -17,7 +17,8 @@ Inductive Pmap_raw A :=
 Arguments Pleaf {_}.
 Arguments Pnode {_} _ _ _.
 
-Instance Pmap_raw_eq_dec `{∀ x y : A, Decision (x = y)} : ∀ x y : Pmap_raw A, Decision (x = y).
+Instance Pmap_raw_eq_dec `{∀ x y : A, Decision (x = y)} (x y : Pmap_raw A) :
+  Decision (x = y).
 Proof. solve_decision. Defined.
 
 Inductive Pmap_ne {A} : Pmap_raw A → Prop :=
@@ -29,36 +30,41 @@ Local Hint Constructors Pmap_ne.
 Instance Pmap_ne_dec `(t : Pmap_raw A) : Decision (Pmap_ne t).
 Proof.
   red. induction t as [|? IHl [?|] ? IHr].
-    right. now inversion 1.
-   now intuition.
-  destruct IHl, IHr; try solve [left; auto]; right; inversion_clear 1; contradiction.
+  * right. now inversion 1.
+  * now intuition.
+  * destruct IHl, IHr; try solve [left; auto]; right;
+      inversion_clear 1; contradiction.
 Qed.
 
 Inductive Pmap_wf {A} : Pmap_raw A → Prop :=
   | Pmap_wf_leaf : Pmap_wf Pleaf
   | Pmap_wf_node l x r : Pmap_wf l → Pmap_wf r → Pmap_wf (Pnode l (Some x) r)
-  | Pmap_wf_empty l r : Pmap_wf l → Pmap_wf r → (Pmap_ne l ∨ Pmap_ne r) → Pmap_wf (Pnode l None r).
+  | Pmap_wf_empty l r :
+     Pmap_wf l → Pmap_wf r → (Pmap_ne l ∨ Pmap_ne r) → Pmap_wf (Pnode l None r).
 Local Hint Constructors Pmap_wf.
 
 Instance Pmap_wf_dec `(t : Pmap_raw A) : Decision (Pmap_wf t).
 Proof.
   red. induction t as [|l IHl [?|] r IHr]; simpl.
-    intuition.
-   destruct IHl, IHr; try solve [left; intuition]; right; inversion_clear 1; intuition.
-  destruct IHl, IHr, (decide (Pmap_ne l)), (decide (Pmap_ne r)); 
-    try solve [left; intuition]; right; inversion_clear 1; intuition.
+  * intuition.
+  * destruct IHl, IHr; try solve [left; intuition];
+      right; inversion_clear 1; intuition.
+  * destruct IHl, IHr, (decide (Pmap_ne l)), (decide (Pmap_ne r)); 
+      try solve [left; intuition]; right; inversion_clear 1; intuition.
 Qed.
 
 Definition Pmap A := @dsig (Pmap_raw A) Pmap_wf _.
 
-Global Instance Pmap_dec `{∀ x y : A, Decision (x = y)} (t1 t2 : Pmap A) : Decision (t1 = t2) :=
+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 _)
   end.
 
 Instance Pempty_raw {A} : Empty (Pmap_raw A) := Pleaf.
-Global Instance Pempty {A} : Empty (Pmap A) := (∅ : Pmap_raw A)↾bool_decide_pack _ Pmap_wf_leaf.
+Global Instance Pempty {A} : Empty (Pmap A) :=
+  (∅ : Pmap_raw A)↾bool_decide_pack _ Pmap_wf_leaf.
 
 Instance Plookup_raw: Lookup positive Pmap_raw :=
   fix Plookup_raw A (i : positive) (t : Pmap_raw A) {struct t} : option A :=
@@ -79,39 +85,40 @@ Proof. now destruct i. Qed.
 Lemma Pmap_ne_lookup `(t : Pmap_raw A) : Pmap_ne t → ∃ i x, t !! i = Some x.
 Proof.
   induction 1 as [? x ?| l r ? IHl | l r ? IHr].
-    intros. now exists 1 x.
-   destruct IHl as [i [x ?]]. now exists (i~0) x.
-  destruct IHr as [i [x ?]]. now exists (i~1) x.
+  * intros. now exists 1 x.
+  * destruct IHl as [i [x ?]]. now exists (i~0) x.
+  * destruct IHr as [i [x ?]]. now exists (i~1) x.
 Qed.
 
 Lemma Pmap_wf_eq_get {A} (t1 t2 : Pmap_raw A) :
   Pmap_wf t1 → Pmap_wf t2 → (∀ i, t1 !! i = t2 !! i) → t1 = t2.
 Proof.
-  intros t1wf. revert t2. induction t1wf as [| ? x ? ? IHl ? IHr | l r ? IHl ? IHr Hne1 ].
-    destruct 1 as [| | ???? [?|?]]; intros Hget.
-       easy.
-      discriminate (Hget 1).
-     destruct (Pmap_ne_lookup l) as [i [??]]; auto.
-     specialize (Hget (i~0)). simpl in *. congruence.
-    destruct (Pmap_ne_lookup r) as [i [??]]; auto.
-    specialize (Hget (i~1)). simpl in *. congruence.
-   destruct 1; intros Hget.
-     discriminate (Hget xH).
-    f_equal.
-      apply IHl; auto. intros i. now apply (Hget (i~0)).
-     now apply (Hget 1).
-    apply IHr; auto. intros i. now apply (Hget (i~1)).
-   specialize (Hget 1). simpl in *. congruence.
-  destruct 1; intros Hget.
-    destruct Hne1.
-     destruct (Pmap_ne_lookup l) as [i [??]]; auto.
-     specialize (Hget (i~0)). simpl in *. congruence.
-    destruct (Pmap_ne_lookup r) as [i [??]]; auto.
-    specialize (Hget (i~1)). simpl in *. congruence.
-   specialize (Hget 1). simpl in *. congruence.
-  f_equal.
-   apply IHl; auto. intros i. now apply (Hget (i~0)).
-  apply IHr; auto. intros i. now apply (Hget (i~1)).
+  intros t1wf. revert t2.
+  induction t1wf as [| ? x ? ? IHl ? IHr | l r ? IHl ? IHr Hne1 ].
+  * destruct 1 as [| | ???? [?|?]]; intros Hget.
+    + easy.
+    + discriminate (Hget 1).
+    + destruct (Pmap_ne_lookup l) as [i [??]]; auto.
+      specialize (Hget (i~0)). simpl in *. congruence.
+    + destruct (Pmap_ne_lookup r) as [i [??]]; auto.
+      specialize (Hget (i~1)). simpl in *. congruence.
+  * destruct 1; intros Hget.
+    + discriminate (Hget xH).
+    + f_equal.
+      - apply IHl; auto. intros i. now apply (Hget (i~0)).
+      - now apply (Hget 1).
+      - apply IHr; auto. intros i. now apply (Hget (i~1)).
+    + specialize (Hget 1). simpl in *. congruence.
+  * destruct 1; intros Hget.
+    + destruct Hne1.
+      destruct (Pmap_ne_lookup l) as [i [??]]; auto.
+      - specialize (Hget (i~0)). simpl in *. congruence.
+      - destruct (Pmap_ne_lookup r) as [i [??]]; auto.
+        specialize (Hget (i~1)). simpl in *. congruence.
+    + specialize (Hget 1). simpl in *. congruence.
+    + f_equal.
+      - apply IHl; auto. intros i. now apply (Hget (i~0)).
+      - apply IHr; auto. intros i. now apply (Hget (i~1)).
 Qed.
 
 Fixpoint Psingleton_raw {A} (i : positive) (x : A) : Pmap_raw A :=
@@ -130,7 +137,8 @@ Local Hint Resolve Psingleton_raw_wf.
 
 Lemma Plookup_raw_singleton {A} i (x : A) : Psingleton_raw i x !! i = Some x.
 Proof. now induction i. Qed.
-Lemma Plookup_raw_singleton_ne {A} i j (x : A) : i ≠ j → Psingleton_raw i x !! j = None.
+Lemma Plookup_raw_singleton_ne {A} i j (x : A) :
+  i ≠ j → Psingleton_raw i x !! j = None.
 Proof. revert j. induction i; intros [?|?|]; simpl; auto. congruence. Qed.
 
 Definition Pnode_canon `(l : Pmap_raw A) (o : option A) (r : Pmap_raw A) :=
@@ -154,10 +162,13 @@ Lemma Pnode_canon_lookup_xI `(l : Pmap_raw A) (o : option A) (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 (
-  rewrite Pnode_canon_lookup_xH || rewrite Pnode_canon_lookup_xO || rewrite Pnode_canon_lookup_xI).
+  rewrite Pnode_canon_lookup_xH ||
+  rewrite Pnode_canon_lookup_xO ||
+  rewrite Pnode_canon_lookup_xI).
 
 Instance Ppartial_alter_raw: PartialAlter positive Pmap_raw :=
-  fix Ppartial_alter_raw A (f : option A → option A) (i : positive) (t : Pmap_raw A) {struct t} : Pmap_raw A :=
+  fix Ppartial_alter_raw A (f : option A → option A) (i : positive)
+    (t : Pmap_raw A) {struct t} : Pmap_raw A :=
   match t with
   | Pleaf =>
     match f None with
@@ -172,39 +183,43 @@ Instance Ppartial_alter_raw: PartialAlter positive Pmap_raw :=
     end
   end.
 
-Lemma Ppartial_alter_raw_wf {A} f i (t : Pmap_raw A) : Pmap_wf t → Pmap_wf (partial_alter f i t).
+Lemma Ppartial_alter_raw_wf {A} f i (t : Pmap_raw A) :
+  Pmap_wf t → Pmap_wf (partial_alter f i t).
 Proof.
   intros twf. revert i. induction twf.
-    unfold partial_alter. simpl. case (f None); intuition.
-   intros [?|?|]; simpl; intuition.
-  intros [?|?|]; simpl; intuition.
+  * unfold partial_alter. simpl. case (f None); intuition.
+  * intros [?|?|]; simpl; intuition.
+  * intros [?|?|]; simpl; intuition.
 Qed.
 
 Global Instance Ppartial_alter: PartialAlter positive Pmap := λ A f i t,
   dexist (partial_alter f i (`t)) (Ppartial_alter_raw_wf f i _ (proj2_dsig t)).
 
-Lemma Plookup_raw_alter {A} f i (t : Pmap_raw A) : partial_alter f i t !! i = f (t !! i).
+Lemma Plookup_raw_alter {A} f i (t : Pmap_raw A) :
+  partial_alter f i t !! i = f (t !! i).
 Proof.
   revert i. induction t.
-   simpl. case (f None).
-    intros. now apply Plookup_raw_singleton.
-   now destruct i.
-  intros [?|?|]; simpl; Pnode_canon_rewrite; auto.
+  * simpl. case (f None).
+    + intros. now apply Plookup_raw_singleton.
+    + now destruct i.
+  * intros [?|?|]; simpl; Pnode_canon_rewrite; auto.
 Qed.
-Lemma Plookup_raw_alter_ne {A} f i j (t : Pmap_raw A) : i ≠ j → partial_alter f i t !! j = t !! j.
+Lemma Plookup_raw_alter_ne {A} f i j (t : Pmap_raw A) :
+  i ≠ j → partial_alter f i t !! j = t !! j.
 Proof.
   revert i j. induction t as [|l IHl ? r IHr].
-   simpl. intros. case (f None).
-    intros. now apply Plookup_raw_singleton_ne.
-   easy.
-  intros [?|?|] [?|?|]; simpl; Pnode_canon_rewrite; auto; congruence.
+  * simpl. intros. case (f None).
+    + intros. now apply Plookup_raw_singleton_ne.
+    + easy.
+  * intros [?|?|] [?|?|]; simpl; Pnode_canon_rewrite; auto; congruence.
 Qed.
 
 Instance Pfmap_raw: FMap Pmap_raw :=
   fix Pfmap_raw A B f (t : Pmap_raw A) : Pmap_raw B :=
   match t with
   | Pleaf => Pleaf
-  | Pnode l x r => Pnode (@fmap _ Pfmap_raw _ _ f l) (fmap f x) (@fmap _ Pfmap_raw _ _ f r)
+  | Pnode l x r =>
+    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).
@@ -213,9 +228,11 @@ Local Hint Resolve Pfmap_raw_ne.
 Lemma Pfmap_raw_wf `(f : A → B) (t : Pmap_raw A) : Pmap_wf t → Pmap_wf (fmap f t).
 Proof. induction 1; simpl; intuition auto. Qed. 
 
-Global Instance Pfmap: FMap Pmap := λ A B f t, dexist _ (Pfmap_raw_wf f _ (proj2_dsig t)).
+Global Instance Pfmap: FMap Pmap := λ A B f t,
+  dexist _ (Pfmap_raw_wf f _ (proj2_dsig t)).
 
-Lemma Plookup_raw_fmap `(f : A → B) (t : Pmap_raw A) i : fmap f t !! i = fmap f (t !! i).
+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.
 
 Section dom.
@@ -224,16 +241,19 @@ Section dom.
   Fixpoint Pdom_raw (f : positive → B) `(t : Pmap_raw A) : D :=
     match t with
     | Pleaf => ∅
-    | Pnode l o r => option_case (λ _, {{ f 1 }}) ∅ o ∪ Pdom_raw (f ∘ (~0)) l ∪ Pdom_raw (f ∘ (~1)) r
+    | Pnode l o r => option_case (λ _, {[ f 1 ]}) ∅ o
+                       ∪ Pdom_raw (f ∘ (~0)) l ∪ Pdom_raw (f ∘ (~1)) r
     end.
 
-  Lemma Plookup_raw_dom f `(t : Pmap_raw A) x : x ∈ Pdom_raw f t ↔ ∃ i, x = f i ∧ is_Some (t !! i).
+  Lemma Plookup_raw_dom f `(t : Pmap_raw A) x :
+    x ∈ Pdom_raw f t ↔ ∃ i, x = f i ∧ is_Some (t !! i).
   Proof.
     split.
-     revert f. induction t as [|? IHl [?|] ? IHr]; esimplify_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))) || now apply (IHr (f ∘ (~1))) || simplify_is_Some).
+    * revert f. induction t as [|? IHl [?|] ? IHr]; esimplify_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))) 
+        || now apply (IHr (f ∘ (~1))) || simplify_is_Some).
   Qed.
 End dom.
 
@@ -246,14 +266,16 @@ Fixpoint Pmerge_aux `(f : option A → option B) (t : Pmap_raw A) : Pmap_raw B :
   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).
+Lemma Pmerge_aux_wf `(f : option A → option B) (t : Pmap_raw A) :
+  Pmap_wf t → Pmap_wf (Pmerge_aux f t).
 Proof. induction 1; simpl; auto. Qed.
 Local Hint Resolve Pmerge_aux_wf.
 
-Lemma Pmerge_aux_spec `(f : option A → option B) (Hf : f None = None) (t : Pmap_raw A) i :
+Lemma Pmerge_aux_spec `(f : option A → option B) (Hf : f None = None)
+    (t : Pmap_raw A) i :
   Pmerge_aux f t !! i = f (t !! i).
 Proof.
-  revert i. induction t as [| l IHl o r IHr ]; auto.
+  revert i. induction t as [| l IHl o r IHr ]; [easy |].
   intros [?|?|]; simpl; Pnode_canon_rewrite; auto.
 Qed.
 
@@ -267,7 +289,8 @@ Global Instance Pmerge_raw: Merge Pmap_raw :=
   end.
 Local Arguments Pmerge_aux _ _ _ _ : simpl never.
 
-Lemma Pmerge_wf {A} f (t1 t2 : Pmap_raw A) : Pmap_wf t1 → Pmap_wf t2 → Pmap_wf (merge f t1 t2).
+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)).
@@ -276,24 +299,24 @@ Lemma Pmerge_raw_spec {A} f (Hf : f None None = None) (t1 t2 : Pmap_raw A) i :
   merge f t1 t2 !! i = f (t1 !! i) (t2 !! i).
 Proof.
   revert t2 i. induction t1 as [| l1 IHl1 o1 r1 IHr1 ].
-   simpl. now apply Pmerge_aux_spec.
-  destruct t2 as [| l2 o2 r2 ].
-   unfold merge, Pmerge_raw. intros. now rewrite Pmerge_aux_spec.
-  intros [?|?|]; simpl; Pnode_canon_rewrite; auto.
+  * simpl. now apply Pmerge_aux_spec.
+  * destruct t2 as [| l2 o2 r2 ].
+    + unfold merge, Pmerge_raw. intros. now rewrite Pmerge_aux_spec.
+    + intros [?|?|]; simpl; Pnode_canon_rewrite; auto.
 Qed.
 
 Global Instance: FinMap positive Pmap.
 Proof.
   split.
-        intros ? [t1?] [t2?]. intros. apply dsig_eq. simpl.
-        apply Pmap_wf_eq_get; auto; now apply (bool_decide_unpack _).
-       now destruct i.
-      intros ?? [??] ?. now apply Plookup_raw_alter.
-     intros ?? [??] ??. now apply Plookup_raw_alter_ne.
-    intros ??? [??]. now apply Plookup_raw_fmap.
-   intros ?????????? [??] i. unfold dom, Pdom.
-   rewrite Plookup_raw_dom. unfold id. split.
-    intros [? [??]]. now subst.
-   firstorder.
-  intros ??? [??] [??] ?. now apply Pmerge_raw_spec.
+  * intros ? [t1?] [t2?]. intros. apply dsig_eq. simpl.
+    apply Pmap_wf_eq_get; auto; now apply (bool_decide_unpack _).
+  * now destruct i.
+  * intros ?? [??] ?. now apply Plookup_raw_alter.
+  * intros ?? [??] ??. now apply Plookup_raw_alter_ne.
+  * intros ??? [??]. now apply Plookup_raw_fmap.
+  * intros ?????????? [??] i. unfold dom, Pdom.
+    rewrite Plookup_raw_dom. unfold id. split.
+    + intros [? [??]]. now subst.
+    + firstorder.
+  * intros ??? [??] [??] ?. now apply Pmerge_raw_spec.
 Qed.

theories/subset.v

@@ -6,8 +6,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_inter {A} : Intersection (subset A) := λ P Q x, P x ∧ Q x.
-Instance subset_diff {A} : Difference (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.
 
 Instance subset_container: Collection A (subset A) | 100.

theories/trs.v

@@ -3,19 +3,29 @@ 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 tc : trs.
+
+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 {_ _ _ _ _} _ _.
 
@@ -55,9 +65,9 @@ Section rtc.
     (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.
-    assert (∀ y z, rtc R y z → ∀ x, rtc R x y → P x y → P x z).
-     induction 1; eauto using rtc_r.
-    eauto using rtc_refl.
+    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.
@@ -75,6 +85,31 @@ Section rtc.
   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.
@@ -96,14 +131,11 @@ Section subrel.
   Proof. intros H1 H2. destruct H1. now apply red_subrel. Qed.
 
   Global Instance rtc_subrel: subrelation (rtc R1) (rtc R2).
-  Proof.
-    induction 1; [easy |].
-    eapply rtc_l; [eapply Hsub|]; eauto.
-  Qed.
+  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.
-     now apply tc_once, Hsub.
-    eapply tc_l; [eapply Hsub|]; eauto.
-  Qed.
+  Proof. induction 1; [left|eright]; eauto; now apply Hsub. Qed.
 End subrel.