Move fresh element generator to infinite.

Also make the instances non-global, to prevent multiple instance
problems.

theories/fin_collections.v

@@ -283,76 +283,5 @@ Proof.
  refine (cast_if (decide (Exists P (elements X))));
    by rewrite set_Exists_elements.
 Defined.
-
-(** * Fresh elements *)
-Section Fresh.
-  Context `{Infinite A, ∀ (x: A) (s: C), Decision (x ∈ s)}.
-
-  Lemma subset_difference_in {x: A} {s: C} (inx: x ∈ s): s ∖ {[ x ]} ⊂ s.
-  Proof. set_solver. Qed.
-
-  Definition fresh_generic_body (s: C) (rec: ∀ s', s' ⊂ s → nat → A) (n: nat) :=
-    let cand := inject n in
-    match decide (cand ∈ s) with
-    | left H => rec _ (subset_difference_in H) (S n)
-    | right _ => cand
-    end.
-  Lemma fresh_generic_body_proper s (f g: ∀ y, y ⊂ s → nat → A):
-    (∀ y Hy Hy', pointwise_relation nat eq (f y Hy) (g y Hy')) →
-    pointwise_relation nat eq (fresh_generic_body s f) (fresh_generic_body s g).
-  Proof.
-    intros relfg i.
-    unfold fresh_generic_body.
-    destruct decide.
-    2: done.
-    apply relfg.
-  Qed.
-
-  Definition fresh_generic_fix := Fix collection_wf (const (nat → A)) fresh_generic_body.
-
-  Lemma fresh_generic_fixpoint_unfold s n:
-    fresh_generic_fix s n = fresh_generic_body s (λ s' _ n, fresh_generic_fix s' n) n.
-  Proof.
-    apply (Fix_unfold_rel collection_wf (const (nat → A)) (const (pointwise_relation nat (=)))
-                          fresh_generic_body fresh_generic_body_proper s n).
-  Qed.
-
-  Lemma fresh_generic_fixpoint_spec s n:
-    ∃ m, n ≤ m ∧ fresh_generic_fix s n = inject m ∧ inject m ∉ s ∧ ∀ i, n ≤ i < m → inject i ∈ s.
-  Proof.
-    revert n.
-    induction s as [s IH] using (well_founded_ind collection_wf); intro.
-    setoid_rewrite fresh_generic_fixpoint_unfold; unfold fresh_generic_body.
-    destruct decide as [case|case].
-    - destruct (IH _ (subset_difference_in case) (S n)) as [m [mbound [eqfix [notin inbelow]]]].
-      exists m; repeat split; auto.
-      + omega.
-      + rewrite not_elem_of_difference, elem_of_singleton in notin.
-        destruct notin as [?|?%inject_injective]; auto; omega.
-      + intros i ibound.
-        destruct (decide (i = n)) as [<-|neq]; auto.
-        enough (inject i ∈ s ∖ {[inject n]}) by set_solver.
-        apply inbelow; omega.
-    - exists n; repeat split; auto.
-      intros; omega.
-  Qed.
-
-  Global Instance fresh_generic: Fresh A C | 20 := λ s, fresh_generic_fix s 0.
-
-  Global Instance fresh_generic_spec: FreshSpec A C.
-  Proof.
-    split.
-    - apply _.
-    - intros * eqXY.
-      unfold fresh, fresh_generic.
-      destruct (fresh_generic_fixpoint_spec X 0) as [mX [_ [-> [notinX belowinX]]]].
-      destruct (fresh_generic_fixpoint_spec Y 0) as [mY [_ [-> [notinY belowinY]]]].
-      destruct (Nat.lt_trichotomy mX mY) as [case|[->|case]]; auto.
-      + contradict notinX; rewrite eqXY; apply belowinY; omega.
-      + contradict notinY; rewrite <- eqXY; apply belowinX; omega.
-    - intro.
-      unfold fresh, fresh_generic.
-      destruct (fresh_generic_fixpoint_spec X 0) as [m [_ [-> [notinX belowinX]]]]; auto.
-  Qed.
-End Fresh.
 End fin_collection.
+

theories/infinite.v

@@ -23,6 +23,78 @@ Proof.
   rewrite !replicate_length in eqrep; done.
 Qed.
 
+(** * Fresh elements *)
+Section Fresh.
+  Context `{Infinite A, ∀ (x: A) (s: C), Decision (x ∈ s)}.
+
+  Lemma subset_difference_in {x: A} {s: C} (inx: x ∈ s): s ∖ {[ x ]} ⊂ s.
+  Proof. set_solver. Qed.
+
+  Definition fresh_generic_body (s: C) (rec: ∀ s', s' ⊂ s → nat → A) (n: nat) :=
+    let cand := inject n in
+    match decide (cand ∈ s) with
+    | left H => rec _ (subset_difference_in H) (S n)
+    | right _ => cand
+    end.
+  Lemma fresh_generic_body_proper s (f g: ∀ y, y ⊂ s → nat → A):
+    (∀ y Hy Hy', pointwise_relation nat eq (f y Hy) (g y Hy')) →
+    pointwise_relation nat eq (fresh_generic_body s f) (fresh_generic_body s g).
+  Proof.
+    intros relfg i.
+    unfold fresh_generic_body.
+    destruct decide.
+    2: done.
+    apply relfg.
+  Qed.
+
+  Definition fresh_generic_fix := Fix collection_wf (const (nat → A)) fresh_generic_body.
+
+  Lemma fresh_generic_fixpoint_unfold s n:
+    fresh_generic_fix s n = fresh_generic_body s (λ s' _ n, fresh_generic_fix s' n) n.
+  Proof.
+    apply (Fix_unfold_rel collection_wf (const (nat → A)) (const (pointwise_relation nat (=)))
+                          fresh_generic_body fresh_generic_body_proper s n).
+  Qed.
+
+  Lemma fresh_generic_fixpoint_spec s n:
+    ∃ m, n ≤ m ∧ fresh_generic_fix s n = inject m ∧ inject m ∉ s ∧ ∀ i, n ≤ i < m → inject i ∈ s.
+  Proof.
+    revert n.
+    induction s as [s IH] using (well_founded_ind collection_wf); intro.
+    setoid_rewrite fresh_generic_fixpoint_unfold; unfold fresh_generic_body.
+    destruct decide as [case|case].
+    - destruct (IH _ (subset_difference_in case) (S n)) as [m [mbound [eqfix [notin inbelow]]]].
+      exists m; repeat split; auto.
+      + omega.
+      + rewrite not_elem_of_difference, elem_of_singleton in notin.
+        destruct notin as [?|?%inject_injective]; auto; omega.
+      + intros i ibound.
+        destruct (decide (i = n)) as [<-|neq]; auto.
+        enough (inject i ∈ s ∖ {[inject n]}) by set_solver.
+        apply inbelow; omega.
+    - exists n; repeat split; auto.
+      intros; omega.
+  Qed.
+
+  Instance fresh_generic: Fresh A C | 20 := λ s, fresh_generic_fix s 0.
+
+  Instance fresh_generic_spec: FreshSpec A C.
+  Proof.
+    split.
+    - apply _.
+    - intros * eqXY.
+      unfold fresh, fresh_generic.
+      destruct (fresh_generic_fixpoint_spec X 0) as [mX [_ [-> [notinX belowinX]]]].
+      destruct (fresh_generic_fixpoint_spec Y 0) as [mY [_ [-> [notinY belowinY]]]].
+      destruct (Nat.lt_trichotomy mX mY) as [case|[->|case]]; auto.
+      + contradict notinX; rewrite eqXY; apply belowinY; omega.
+      + contradict notinY; rewrite <- eqXY; apply belowinX; omega.
+    - intro.
+      unfold fresh, fresh_generic.
+      destruct (fresh_generic_fixpoint_spec X 0) as [m [_ [-> [notinX belowinX]]]]; auto.
+  Qed.
+End Fresh.
+
 (** Derive fresh instances. *)
 Section StringFresh.
   Context `{FinCollection string C, ∀ (x: string) (s: C), Decision (x ∈ s)}.