Initial commit

theories/base.v

+Global Generalizable All Variables.
+Global Set Automatic Coercions Import.
+Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid NArith.
+
+Arguments existT {_ _} _ _.
+Arguments existT2 {_ _ _} _ _ _.
+
+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.
+
+(*  Common notations *)
+Delimit Scope C_scope with C.
+Global Open Scope C_scope.
+
+Notation "(=)" := eq (only parsing) : C_scope.
+Notation "( x =)" := (eq x) (only parsing) : C_scope.
+Notation "(= x )" := (λ y, eq y x) (only parsing) : C_scope.
+Notation "(≠)" := (λ x y, x ≠ y) (only parsing) : C_scope.
+Notation "( x ≠)" := (λ y, x ≠ y) (only parsing) : C_scope.
+Notation "(≠ x )" := (λ y, y ≠ x) (only parsing) : C_scope.
+
+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.
+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.
+Notation "x ↾ p" := (exist _ x p) (at level 20) : C_scope.
+Notation "` x" := (proj1_sig x) : C_scope.
+
+(* Provable propositions *)
+Class PropHolds (P : Prop) := prop_holds: P.
+
+(* Decidable propositions *)
+Class Decision (P : Prop) := decide : {P} + {¬P}.
+Arguments decide _ {_}.
+
+(* Common relations & operations *)
+Class Equiv A := equiv: relation A.
+Infix "≡" := equiv (at level 70, no associativity) : C_scope.
+Notation "(≡)" := equiv (only parsing) : C_scope.
+Notation "( x ≡)" := (equiv x) (only parsing) : C_scope.
+Notation "(≡ x )" := (λ y, y ≡ x) (only parsing) : C_scope.
+Notation "(≢)" := (λ x y, ¬x ≡ y) (only parsing) : C_scope.
+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.
+
+Instance equiv_default_relation `{Equiv A} : DefaultRelation (≡) | 3.
+Hint Extern 0 (?x ≡ ?x) => reflexivity.
+
+Class Empty A := empty: A.
+Notation "∅" := empty : C_scope.
+
+Class Union A := union: A → A → A.
+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.
+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.
+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 SubsetEq A := subseteq: A → A → Prop.
+Infix "⊆" := subseteq (at level 70) : C_scope.
+Notation "(⊆)" := subseteq (only parsing) : C_scope.
+Notation "( X ⊆ )" := (subseteq X) (only parsing) : C_scope.
+Notation "( ⊆ X )" := (λ Y, subseteq Y X) (only parsing) : C_scope.
+Notation "X ⊈ Y" := (¬X ⊆ Y) (at level 70) : C_scope.
+Notation "(⊈)" := (λ X Y, X ⊈ Y) (only parsing) : C_scope.
+Notation "( X ⊈ )" := (λ Y, X ⊈ Y) (only parsing) : C_scope.
+Notation "( ⊈ X )" := (λ Y, Y ⊈ X) (only parsing) : C_scope.
+
+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.
+Infix "∈" := elem_of (at level 70) : C_scope.
+Notation "(∈)" := elem_of (only parsing) : C_scope.
+Notation "( x ∈)" := (elem_of x) (only parsing) : C_scope.
+Notation "(∈ X )" := (λ x, elem_of x X) (only parsing) : C_scope.
+Notation "x ∉ X" := (¬x ∈ X) (at level 80) : C_scope.
+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.
+
+(* 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).
+
+Arguments injective {_ _ _ _} _ {_} _ _ _.
+Arguments idempotent {_ _} _ {_} _.
+Arguments commutative {_ _ _} _ {_} _ _.
+Arguments left_id {_ _} _ _ {_} _.
+Arguments right_id {_ _} _ _ {_} _.
+Arguments associative {_ _} _ {_} _ _ _.
+
+(* Monadic operations *)
+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.
+
+(* Ordered structures *)
+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 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;
+  subseteq_union_r x y : y ⊆ x ∪ y;
+  union_least x y z : x ⊆ z → y ⊆ z → x ∪ y ⊆ z
+}.
+Class MeetSemiLattice A `{Empty A} `{SubsetEq A} `{Intersection A} := {
+  msl_preorder :>> BoundedPreOrder A;
+  subseteq_intersection_l x y : x ∩ y ⊆ x;
+  subseteq_intersection_r x y : x ∩ y ⊆ y;
+  intersection_greatest x y z : z ⊆ x → z ⊆ y → z ⊆ x ∩ y
+}.
+
+(* Containers *)
+Class Size C := size: C → nat.
+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_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;
+  elem_of_map f X (x : A) : x ∈ map f X ↔ ∃ y, x = f y ∧ y ∈ X
+}.
+
+Class Elements A C := elements: C → list A.
+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 Fresh A C := fresh: C → A.
+Class FreshSpec A C `{!Fresh A C} `{!ElemOf A C} := {
+  fresh_proper 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.
+
+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.
+
+(* Misc *)
+Instance pointwise_reflexive {A} `{R : relation B} :
+  Reflexive R → Reflexive (pointwise_relation A R) | 9.
+Proof. firstorder. Qed.
+Instance pointwise_symmetric {A} `{R : relation B} :
+  Symmetric R → Symmetric (pointwise_relation A R) | 9.
+Proof. firstorder. Qed.
+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).
+
+Section prod_relation.
+  Context `{R1 : relation A} `{R2 : relation B}.
+  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).
+  Proof. firstorder eauto. Qed.
+  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).
+  Proof. split; apply _. Qed.
+  Global Instance: Proper (R1 ==> R2 ==> prod_relation R1 R2) pair.
+  Proof. firstorder eauto. Qed.
+  Global Instance: Proper (prod_relation R1 R2 ==> R1) fst.
+  Proof. firstorder eauto. Qed.
+  Global Instance: Proper (prod_relation R1 R2 ==> R2) snd.
+  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_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.
+
+Instance: ∀ A B (x : B), Commutative (=) (λ _ _ : A, x).
+Proof. easy. Qed.
+Instance: ∀ A (x : A), Associative (=) (λ _ _ : A, x).
+Proof. easy. Qed.
+Instance: ∀ A, Associative (=) (λ x _ : A, x).
+Proof. easy. Qed.
+Instance: ∀ A, Associative (=) (λ _ x : A, x).
+Proof. easy. Qed.
+Instance: ∀ A, Idempotent (=) (λ x _ : A, x).
+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).
+Proof. easy. Qed.
+Instance right_id_propholds {A} (R : relation A) i f : RightId R i f → ∀ x, PropHolds (R (f x i) x).
+Proof. easy. Qed.
+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.

theories/collections.v

+Require Export base orders.
+
+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_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.
+
+  Global Instance collection_subseteq: SubsetEq B := λ X Y, ∀ x, x ∈ X → x ∈ Y.
+  Global Instance: BoundedJoinSemiLattice B.
+  Proof. firstorder. Qed.
+  Global Instance: MeetSemiLattice B.
+  Proof. firstorder. Qed.
+
+  Lemma elem_of_subseteq X Y : X ⊆ Y ↔ ∀ x, x ∈ X → x ∈ Y.
+  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).
+  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. 
+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.
+  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.
+  Proof. intros. apply (elem_of_map _). eauto. Qed.
+  Lemma elem_of_map_2 (f : A → A) (X : C) (x : A) : x ∈ map f X → ∃ y, x = f y ∧ y ∈ X.
+  Proof. intros. now apply (elem_of_map _). Qed.
+End 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
+  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_singleton in H
+  | H : context [ _ ∈ _ ∪ _ ] |- _ => setoid_rewrite elem_of_union in H
+  | H : context [ _ ∈ _ ∩ _ ] |- _ => setoid_rewrite elem_of_intersection in H
+  | H : context [ _ ∈ _ ∖ _ ] |- _ => setoid_rewrite elem_of_difference in H
+  | H : context [ _ ∈ map _ _ ] |- _ => setoid_rewrite elem_of_map in H
+  | |- 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_union
+  | |- context [ _ ∈ _ ∩ _ ] => setoid_rewrite elem_of_intersection
+  | |- context [ _ ∈ _ ∖ _ ] => setoid_rewrite elem_of_difference
+  | |- 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 *)
+  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 [ _ ∧ _ ] |- _ => 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
+  (* 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).
+
+Section no_dup.
+  Context `{Collection A B} (R : relation A) `{!Equivalence R}.
+
+  Definition elem_of_upto (x : A) (X : B) := ∃ y, y ∈ X ∧ R x y.
+  Definition no_dup (X : B) := ∀ x y, x ∈ X → y ∈ X → R x y → x = y.
+
+  Global Instance: Proper ((≡) ==> iff) (elem_of_upto x).
+  Proof. firstorder. Qed.
+  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.
+  Qed.
+  Global Instance: Proper ((≡) ==> iff) 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.
+  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.
+  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.
+  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).
+  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_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.
+  Proof. unfold no_dup. simplify_elem_of. Qed.
+End no_dup.
+
+Section quantifiers.
+  Context `{Collection A B} (P : A → Prop).
+
+  Definition cforall X := ∀ x, x ∈ X → P x.
+  Definition cexists X := ∃ x, x ∈ X ∧ P x.
+
+  Lemma cforall_empty : cforall ∅.
+  Proof. unfold cforall. simplify_elem_of. Qed.
+  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.
+  Lemma cforall_union_inv_1 X Y : cforall (X ∪ Y) → cforall X.
+  Proof. unfold cforall. simplify_elem_of. Qed.
+  Lemma cforall_union_inv_2 X Y : cforall (X ∪ Y) → cforall Y.
+  Proof. unfold cforall. simplify_elem_of. Qed.
+
+  Lemma cexists_empty : ¬cexists ∅.
+  Proof. unfold cexists. esimplify_elem_of. Qed.
+  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.
+  Lemma cexists_union_2 X Y : cexists Y → cexists (X ∪ Y).
+  Proof. unfold cexists. esimplify_elem_of. Qed.
+  Lemma cexists_union_inv X Y : cexists (X ∪ Y) → cexists X ∨ cexists Y.
+  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.

theories/decidable.v

+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.
+
+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 *
+  | |- context [@decide ?P ?dec] => case (@decide P dec) in *
+  | |- context [@decide_rel _ _ ?R ?x ?y ?dec] => case (@decide_rel _ _ R x y dec) in *
+  end.
+
+Ltac solve_trivial_decision :=