Overhaul of the `Infinite`/`Fresh` infrastructure.

- The class `Infinite A` is now defined as having a function
  `fresh : list A → A`, that given a list `xs`, gives an element `x ∉ xs`.
- For most types this `fresh` function has a sensible computable behavior,
  for example:
  + For numbers, it yields one added to the maximal element in `xs`.
  + For strings, it yields the first string representation of a number that is
    not in `xs`.
- For any type `C` of finite sets with elements of infinite type `A`, we lift
  the fresh function to `C → A`.

As a consequence:

- It is now possible to pick fresh elements from _any_ finite set and from
  _any_ list with elements of an infinite type. Before it was only possible
  for specific finite sets, e.g. `gset`, `pset`, ...
- It makes the code more uniform. There was a lot of overlap between having a
  `Fresh` and an `Infinite` instance. This got unified.

theories/base.v

@@ -6,6 +6,7 @@ abstract interfaces for ordered structures, sets, and various other data
 structures. *)
 
 From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
+From Coq Require Import Permutation.
 Set Default Proof Using "Type".
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
@@ -1210,17 +1211,26 @@ Class MonadSet M `{∀ A, ElemOf A (M A),
   elem_of_join {A} (X : M (M A)) (x : A) : x ∈ mjoin X ↔ ∃ Y, x ∈ Y ∧ Y ∈ X
 }.
 
-(** The function [fresh X] yields an element that is not contained in [X]. We
-will later prove that [fresh] is [Proper] with respect to the induced setoid
-equality on sets. *)
+(** The [Infinite A] class axiomatizes types [A] with infinitely many elements.
+It contains a function [fresh : list A → A] that given a list [xs] gives an
+element [fresh xs ∉ xs].
+
+We do not directly make [fresh] a field of the [Infinite] class, but use a
+separate operational type class [Fresh] for it. That way we can overload [fresh]
+to pick fresh elements from other data structure like sets. See the file
+[fin_sets], where we define [fresh : C → A] for any finite set implementation
+[FinSet C A].
+
+Note: we require [fresh] to respect permutations, which is needed to define the
+aforementioned [fresh] function on finite sets that respects set equality. *)
 Class Fresh A C := fresh: C → A.
 Hint Mode Fresh - ! : typeclass_instances.
 Instance: Params (@fresh) 3 := {}.
-Class FreshSpec A C `{ElemOf A C,
-    Empty C, Singleton A C, Union C, Fresh A C} : Prop := {
-  fresh_set_semi_set :>> SemiSet A C;
-  fresh_proper_alt X Y : (∀ x, x ∈ X ↔ x ∈ Y) → fresh X = fresh Y;
-  is_fresh (X : C) : fresh X ∉ X
+
+Class Infinite A := {
+  infinite_fresh :> Fresh A (list A);
+  infinite_is_fresh (xs : list A) : fresh xs ∉ xs;
+  infinite_fresh_Permutation :> Proper (@Permutation A ==> (=)) fresh;
 }.
 
 (** * Miscellaneous *)

theories/fin_sets.v

@@ -7,7 +7,9 @@ From stdpp Require Import relations.
 From stdpp Require Export numbers sets.
 Set Default Proof Using "Type*".
 
+(** Operations *)
 Instance set_size `{Elements A C} : Size C := length ∘ elements.
+
 Definition set_fold `{Elements A C} {B}
   (f : A → B → B) (b : B) : C → B := foldr f b ∘ elements.
 
@@ -21,6 +23,28 @@ Definition set_map `{Elements A C, Singleton B D, Empty D, Union D}
   list_to_set (f <$> elements X).
 Typeclasses Opaque set_map.
 
+Instance set_fresh `{Elements A C, Fresh A (list A)} : Fresh A C :=
+  fresh ∘ elements.
+Typeclasses Opaque set_filter.
+
+(** We generalize the [fresh] operation on sets to generate lists of fresh
+elements w.r.t. a set [X]. *)
+Fixpoint fresh_list `{Fresh A C, Union C, Singleton A C}
+    (n : nat) (X : C) : list A :=
+  match n with
+  | 0 => []
+  | S n => let x := fresh X in x :: fresh_list n ({[ x ]} ∪ X)
+  end.
+Instance: Params (@fresh_list) 6 := {}.
+
+(** The following inductive predicate classifies that a list of elements is
+in fact fresh w.r.t. a set [X]. *)
+Inductive Forall_fresh `{ElemOf A C} (X : C) : list A → Prop :=
+  | Forall_fresh_nil : Forall_fresh X []
+  | Forall_fresh_cons x xs :
+     x ∉ xs → x ∉ X → Forall_fresh X xs → Forall_fresh X (x :: xs).
+
+(** Properties **)
 Section fin_set.
 Context `{FinSet A C}.
 Implicit Types X Y : C.
@@ -342,4 +366,58 @@ Proof.
   - intros Hinf X. destruct (Hinf (elements X)). set_solver.
   - intros Hinf xs. destruct (Hinf (list_to_set xs)). set_solver.
 Qed.
+
+Section infinite.
+  Context `{Infinite A}.
+
+  (** Properties about the [fresh] operation on finite sets *)
+  Global Instance fresh_proper: Proper ((≡@{C}) ==> (=)) fresh.
+  Proof. unfold fresh, set_fresh. solve_proper. Qed.
+
+  Lemma is_fresh X : fresh X ∉ X.
+  Proof.
+    unfold fresh, set_fresh. rewrite <-elem_of_elements. apply infinite_is_fresh.
+  Qed.
+  Lemma exist_fresh X : ∃ x, x ∉ X.
+  Proof. exists (fresh X). apply is_fresh. Qed.
+
+  (** Properties about the [fresh_list] operation on finite sets *)
+  Global Instance fresh_list_proper n : Proper ((≡@{C}) ==> (=)) (fresh_list n).
+  Proof. induction n as [|n IH]; intros ?? E; by setoid_subst. Qed.
+
+  Lemma Forall_fresh_NoDup X xs : Forall_fresh X xs → NoDup xs.
+  Proof. induction 1; by constructor. Qed.
+  Lemma Forall_fresh_elem_of X xs x : Forall_fresh X xs → x ∈ xs → x ∉ X.
+  Proof.
+    intros HX; revert x; rewrite <-Forall_forall. by induction HX; constructor.
+  Qed.
+  Lemma Forall_fresh_alt X xs :
+    Forall_fresh X xs ↔ NoDup xs ∧ ∀ x, x ∈ xs → x ∉ X.
+  Proof.
+    split; eauto using Forall_fresh_NoDup, Forall_fresh_elem_of.
+    rewrite <-Forall_forall.
+    intros [Hxs Hxs']. induction Hxs; decompose_Forall_hyps; constructor; auto.
+  Qed.
+  Lemma Forall_fresh_subseteq X Y xs :
+    Forall_fresh X xs → Y ⊆ X → Forall_fresh Y xs.
+  Proof. rewrite !Forall_fresh_alt; set_solver. Qed.
+
+  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 : x ∈ fresh_list n X → x ∉ X.
+  Proof.
+    revert X. induction n as [|n IH]; intros X; simpl;[by rewrite elem_of_nil|].
+    rewrite elem_of_cons; intros [->| Hin]; [apply is_fresh|].
+    apply IH in Hin; set_solver.
+  Qed.
+  Lemma NoDup_fresh_list n X : NoDup (fresh_list n X).
+  Proof.
+    revert X. induction n; simpl; constructor; auto.
+    intros Hin; apply fresh_list_is_fresh in Hin; set_solver.
+  Qed.
+  Lemma Forall_fresh_list X n : Forall_fresh X (fresh_list n X).
+  Proof.
+    rewrite Forall_fresh_alt; eauto using NoDup_fresh_list, fresh_list_is_fresh.
+  Qed.
+End infinite.
 End fin_set.

theories/gmap.v

@@ -264,9 +264,3 @@ Proof.
   - by rewrite option_guard_True by (rewrite elem_of_dom; eauto).
   - by rewrite option_guard_False by (rewrite not_elem_of_dom; eauto).
 Qed.
-
-(** * Fresh elements *)
-Instance gset_fresh `{Countable A, Infinite A} : Fresh A (gset A) :=
-  fresh_generic.
-Instance gset_fresh_spec `{Countable A, Infinite A} : FreshSpec A (gset A) :=
-  fresh_generic_spec.

theories/infinite.v

 (* Copyright (c) 2012-2019, Coq-std++ developers. *)
 (* This file is distributed under the terms of the BSD license. *)
-From stdpp Require Export fin_sets.
-From stdpp Require Import pretty relations.
-
-(** The class [Infinite] axiomatizes types with infinitely many elements
-by giving an injection from the natural numbers into the type. It is mostly
-used to provide a generic [fresh] algorithm. *)
-Class Infinite A := {
-  inject: nat → A;
-  inject_injective :> Inj (=) (=) inject;
-}.
-
-(** Instances *)
-Program Definition inj_infinite `{Infinite A} {B} (f : A → B) `{!Inj (=) (=) f} :
-  Infinite B := {| inject := f ∘ inject |}.
-
-Instance string_infinite: Infinite string := {| inject := λ x, "~" +:+ pretty x |}.
-Instance nat_infinite: Infinite nat := {| inject := id |}.
-Instance N_infinite: Infinite N := {| inject_injective := Nat2N.inj |}.
-Instance positive_infinite: Infinite positive := {| inject_injective := SuccNat2Pos.inj |}.
-Instance Z_infinite: Infinite Z := {| inject_injective := Nat2Z.inj |}.
-
-Instance option_infinite `{Infinite A} : Infinite (option A) := inj_infinite Some.
-Instance sum_infinite_l `{Infinite A} {B} : Infinite (A + B) := inj_infinite inl.
-Instance sum_infinite_r {A} `{Infinite B} : Infinite (A + B) := inj_infinite inr.
-Instance prod_infinite_l `{Infinite A, Inhabited B} : Infinite (A * B) :=
-  inj_infinite (,inhabitant).
-Instance prod_infinite_r `{Inhabited A, Infinite B} : Infinite (A * B) :=
-  inj_infinite (inhabitant,).
+From stdpp Require Export list.
+From stdpp Require Import relations pretty.
 
-Program Instance list_infinite `{Inhabited A}: Infinite (list A) :=
-  {| inject := λ i, replicate i inhabitant |}.
+(** * Generic constructions *)
+(** If [A] is infinite, and there is an injection from [A] to [B], then [B] is
+also infinite. Note that due to constructivity we need a rather strong notion of
+being injective, we also need a partial function [B → option A] back. *)
+Program Definition inj_infinite `{Infinite A} {B}
+    (f : A → B) (g : B → option A) (Hgf : ∀ x, g (f x) = Some x) :
+  Infinite B := {| infinite_fresh := f ∘ fresh ∘ omap g |}.
 Next Obligation.
-  intros A * i j Heqrep%(f_equal length).
-  rewrite !replicate_length in Heqrep; done.
+  intros A ? B f g Hfg xs Hxs; simpl in *.
+  apply (infinite_is_fresh (omap g xs)), elem_of_list_omap; eauto.
 Qed.
+Next Obligation. solve_proper. Qed.
 
-(** * Fresh elements *)
-(** We do not make [fresh_generic] an instance because it leads to overlap. For
-various set implementations, e.g. [Pset] and [natset], we have an efficient
-implementation of [Fresh], which should always be used. Only for specific set
-implementations like [gset], which are not meant to be computationally
-efficient in the first place, we make [fresh_generic] an instance.
-
-Since [fresh_generic] is too inefficient for all practical purposes, we seal
-off its definition. That way, Coq will not accidentally unfold it during
-unification or other tactics. *)
-Section fresh_generic.
-  Context `{FinSet A C, Infinite A, !RelDecision (∈@{C})}.
-
-  Definition fresh_generic_body (s : C) (rec : ∀ s', s' ⊂ s → nat → A) (n : nat) : A :=
-    let cand := inject n in
-    match decide (cand ∈ s) with
-    | left H => rec _ (subset_difference_elem_of H) (S n)
-    | right _ => cand
-    end.
+(** If there is an injective function [f : nat → B], then [B] is infinite. This
+construction works as follows: to obtain an element not in [xs], we return the
+first element [f 0], [f 1], [f 2], ... that is not in [xs].
 
-  Definition fresh_generic_fix_aux :
-    seal (Fix set_wf (const (nat → A)) fresh_generic_body). by eexists. Qed.
-  Definition fresh_generic_fix := fresh_generic_fix_aux.(unseal).
+This construction has a nice computational behavior to e.g. find fresh strings.
+Given some prefix [s], we use [f n := if n is S n' then s +:+ pretty n else s].
+The construction then finds the first string starting with [s] followed by a
+number that's not in the input list. For example, given [["H", "H1", "H4"]] and
+[s := "H"], it would find ["H2"]. *)
+Section search_infinite.
+  Context {B} (f : nat → B) `{!Inj (=) (=) f, !EqDecision B}.
 
-  Lemma fresh_generic_fixpoint_unfold s n:
-    fresh_generic_fix s n = fresh_generic_body s (λ s' _, fresh_generic_fix s') n.
+  Let R (xs : list B) (n1 n2 : nat) :=
+    n2 < n1 ∧ (f (n1 - 1)) ∈ xs.
+  Lemma search_infinite_step xs n : f n ∈ xs → R xs (1 + n) n.
+  Proof. split; [lia|]. replace (1 + n - 1) with n by lia; eauto. Qed.
+  Lemma search_infinite_R_wf xs : wf (R xs).
   Proof.
-    unfold fresh_generic_fix. rewrite fresh_generic_fix_aux.(seal_eq).
-    refine (Fix_unfold_rel _ _ (const (pointwise_relation nat (=))) _ _ s n).
-    intros s' f g Hfg i. unfold fresh_generic_body. case_decide; naive_solver.
+    revert xs. assert (help : ∀ xs n n',
+      Acc (R (filter (≠ f n') xs)) n → n' < n → Acc (R xs) n).
+    { induction 1 as [n _ IH]. constructor; intros n2 [??]. apply IH; [|lia].
+      split; [done|]. apply elem_of_list_filter; naive_solver lia. }
+    intros xs. induction (well_founded_ltof _ length xs) as [xs _ IH].
+    intros n1; constructor; intros n2 [Hn Hs].
+    apply help with (n2 - 1); [|lia]. apply IH. eapply filter_length_lt; eauto.
   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 set_wf); intros n.
-    setoid_rewrite fresh_generic_fixpoint_unfold; unfold fresh_generic_body.
-    destruct decide as [Hcase|Hcase]; [|by eauto with lia].
-    destruct (IH _ (subset_difference_elem_of Hcase) (S n))
-      as (m & Hmbound & Heqfix & Hnotin & Hinbelow).
-    exists m; repeat split; auto with lia.
-    - rewrite not_elem_of_difference, elem_of_singleton in Hnotin.
-      destruct Hnotin as [?|?%inject_injective]; auto with lia.
-    - intros i Hibound.
-      destruct (decide (i = n)) as [<-|Hneq]; [by auto|].
-      assert (inject i ∈ s ∖ {[inject n]}) by auto with lia.
-      set_solver.
+  Definition search_infinite_go (xs : list B) (n : nat)
+      (go : ∀ n', R xs n' n → B) : B :=
+    let x := f n in
+    match decide (x ∈ xs) with
+    | left Hx => go (S n) (search_infinite_step xs n Hx)
+    | right _ => x
+    end.
+
+  Program Definition search_infinite : Infinite B := {|
+    infinite_fresh xs :=
+      Fix_F _ (search_infinite_go xs) (wf_guard 32 (search_infinite_R_wf xs) 0)
+  |}.
+  Next Obligation.
+    intros xs. unfold fresh.
+    generalize 0 (wf_guard 32 (search_infinite_R_wf xs) 0). revert xs.
+    fix FIX 3; intros xs n [?]; simpl; unfold search_infinite_go at 1; simpl.
+    destruct (decide _); auto.
   Qed.
+  Next Obligation.
+    intros xs1 xs2 Hxs. unfold fresh.
+    generalize (wf_guard 32 (search_infinite_R_wf xs1) 0).
+    generalize (wf_guard 32 (search_infinite_R_wf xs2) 0). generalize 0.
+    fix FIX 2. intros n [acc1] [acc2]; simpl; unfold search_infinite_go.
+    destruct (decide ( _ ∈ xs1)) as [H1|H1], (decide (_ ∈ xs2)) as [H2|H2]; auto.
+    - destruct H2. by rewrite <-Hxs.
+    - destruct H1. by rewrite Hxs.
+  Qed.
+End search_infinite.
 
-  Instance fresh_generic : Fresh A C := λ s, fresh_generic_fix s 0.
+(** To select a fresh number from a given list [x₀ ... xₙ], a possible approach
+is to compute [(S x₀) `max` ... `max` (S xₙ) `max` 0]. For non-empty lists of
+non-negative numbers this is equal to taking the maximal element [xᵢ] and adding
+one.
 
-  Instance fresh_generic_spec : FreshSpec A C.
-  Proof.
-    split.
-    - apply _.
-    - intros X Y HeqXY. unfold fresh, fresh_generic.
-      destruct (fresh_generic_fixpoint_spec X 0)
-        as (mX & _ & -> & HnotinX & HbelowinX).
-      destruct (fresh_generic_fixpoint_spec Y 0)
-        as (mY & _ & -> & HnotinY & HbelowinY).
-      destruct (Nat.lt_trichotomy mX mY) as [case|[->|case]]; auto.
-      + contradict HnotinX. rewrite HeqXY. apply HbelowinY; lia.
-      + contradict HnotinY. rewrite <-HeqXY. apply HbelowinX; lia.
-    - intros X. unfold fresh, fresh_generic.
-      destruct (fresh_generic_fixpoint_spec X 0)
-        as (m & _ & -> & HnotinX & HbelowinX); auto.
+The construction below generalizes this construction to any type [A], function
+[f : A → A → A]. and initial value [a]. The fresh element is computed as
+[x₀ `f` ... `f` xₙ `f` a]. For numbers, the prototypical instance is
+[f x y := S x `max` y] and [a:=0], which gives the behavior described before.
+Note that this gives [a] (i.e. [0] for numbers) for the empty list. *)
+Section max_infinite.
+  Context {A} (f : A → A → A) (a : A) (lt : relation A).
+  Context (HR : ∀ x, ¬lt x x).
+  Context (HR1 : ∀ x y, lt x (f x y)).
+  Context (HR2 : ∀ x x' y, lt x x' → lt x (f y x')).
+  Context (Hf : ∀ x x' y, f x (f x' y) = f x' (f x y)).
+
+  Program Definition max_infinite: Infinite A := {|
+    infinite_fresh := foldr f a
+  |}.
+  Next Obligation.
+    cut (∀ xs x, x ∈ xs → lt x (foldr f a xs)).
+    { intros help xs []%help%HR. }
+    induction 1; simpl; auto.
   Qed.
-End fresh_generic.
+  Next Obligation. by apply (foldr_permutation_proper _ _ _). Qed.
+End max_infinite.
+
+(** Instances for number types *)
+Program Instance nat_infinite : Infinite nat :=
+  max_infinite (Nat.max ∘ S) 0 (<) _ _ _ _.
+Solve Obligations with (intros; simpl; lia).
+
+Program Instance N_infinite : Infinite N :=
+  max_infinite (N.max ∘ N.succ) 0%N N.lt _ _ _ _.
+Solve Obligations with (intros; simpl; lia).
+
+Program Instance positive_infinite : Infinite positive :=
+  max_infinite (Pos.max ∘ Pos.succ) 1%positive Pos.lt _ _ _ _.
+Solve Obligations with (intros; simpl; lia).
+
+Program Instance Z_infinite: Infinite Z :=
+  max_infinite (Z.max ∘ Z.succ) 0%Z Z.lt _ _ _ _.
+Solve Obligations with (intros; simpl; lia).
+
+(** Instances for option, sum, products *)
+Instance option_infinite `{Infinite A} : Infinite (option A) :=
+  inj_infinite Some id (λ _, eq_refl).
+
+Instance sum_infinite_l `{Infinite A} {B} : Infinite (A + B) :=
+  inj_infinite inl (maybe inl) (λ _, eq_refl).
+Instance sum_infinite_r {A} `{Infinite B} : Infinite (A + B) :=
+  inj_infinite inr (maybe inr)  (λ _, eq_refl).
+
+Instance prod_infinite_l `{Infinite A, Inhabited B} : Infinite (A * B) :=
+  inj_infinite (,inhabitant) (Some ∘ fst) (λ _, eq_refl).
+Instance prod_infinite_r `{Inhabited A, Infinite B} : Infinite (A * B) :=
+  inj_infinite (inhabitant,) (Some ∘ snd) (λ _, eq_refl).
+
+(** Instance for lists *)
+Program Instance list_infinite `{Inhabited A} : Infinite (list A) := {|
+  infinite_fresh xxs := replicate (fresh (length <$> xxs)) inhabitant
+|}.
+Next Obligation.
+  intros A ? xs ?. destruct (infinite_is_fresh (length <$> xs)).
+  apply elem_of_list_fmap. eexists; split; [|done].
+  unfold fresh. by rewrite replicate_length.
+Qed.
+Next Obligation. unfold fresh. by intros A ? xs1 xs2 ->. Qed.
+
+(** Instance for strings *)
+Program Instance string_infinite : Infinite string :=
+  search_infinite pretty.

theories/nmap.v

@@ -84,20 +84,3 @@ Qed.
 Notation Nset := (mapset Nmap).
 Instance Nmap_dom {A} : Dom (Nmap A) Nset := mapset_dom.
 Instance: FinMapDom N Nmap Nset := mapset_dom_spec.
-
-(** * Fresh numbers *)
-Definition Nfresh {A} (m : Nmap A) : N :=
-  match m with NMap None _ => 0 | NMap _ m => Npos (Pfresh m) end.
-Lemma Nfresh_fresh {A} (m : Nmap A) : m !! Nfresh m = None.
-Proof. destruct m as [[]]. apply Pfresh_fresh. done. Qed. 
-
-Instance Nset_fresh : Fresh N Nset := λ X,
-  let (m) := X in Nfresh m.
-Instance Nset_fresh_spec : FreshSpec N Nset.
-Proof.
-  split.
-  - apply _.
-  - intros X Y; rewrite <-elem_of_equiv_L. by intros ->.
-  - unfold elem_of, mapset_elem_of, fresh; intros [m]; simpl.
-    by rewrite Nfresh_fresh.
-Qed.

theories/pmap.v

@@ -314,66 +314,3 @@ Qed.
 Notation Pset := (mapset Pmap).
 Instance Pmap_dom {A} : Dom (Pmap A) Pset := mapset_dom.
 Instance Pmap_dom_spec : FinMapDom positive Pmap Pset := mapset_dom_spec.
-
-(** * Fresh numbers *)
-Fixpoint Pdepth {A} (m : Pmap_raw A) : nat :=
-  match m with
-  | PLeaf | PNode None _ _ => O | PNode _ l _ => S (Pdepth l)
-  end.
-Fixpoint Pfresh_at_depth {A} (m : Pmap_raw A) (d : nat) : option positive :=
-  match d, m with
-  | O, (PLeaf | PNode None _ _) => Some 1
-  | S d, PNode _ l r =>
-     match Pfresh_at_depth l d with
-     | Some i => Some (i~0) | None => (~1) <$> Pfresh_at_depth r d
-     end
-  | _, _ => None
-  end.
-Fixpoint Pfresh_go {A} (m : Pmap_raw A) (d : nat) : option positive :=
-  match d with
-  | O => None
-  | S d =>
-     match Pfresh_go m d with
-     | Some i => Some i | None => Pfresh_at_depth m d
-     end
-  end.
-Definition Pfresh {A} (m : Pmap A) : positive :=
-  let d := Pdepth (pmap_car m) in
-  match Pfresh_go (pmap_car m) d with
-  | Some i => i | None => Pos.shiftl_nat 1 d
-  end.
-
-Lemma Pfresh_at_depth_fresh {A} (m : Pmap_raw A) d i :
-  Pfresh_at_depth m d = Some i → m !! i = None.
-Proof.
-  revert i m; induction d as [|d IH].
-  { intros i [|[] l r] ?; naive_solver. }
-  intros i [|o l r] ?; simplify_eq/=.
-  destruct (Pfresh_at_depth l d) as [i'|] eqn:?,
-    (Pfresh_at_depth r d) as [i''|] eqn:?; simplify_eq/=; auto.
-Qed.
-Lemma Pfresh_go_fresh {A} (m : Pmap_raw A) d i :
-  Pfresh_go m d = Some i → m !! i = None.
-Proof.
-  induction d as [|d IH]; intros; simplify_eq/=.
-  destruct (Pfresh_go m d); eauto using Pfresh_at_depth_fresh.
-Qed.
-Lemma Pfresh_depth {A} (m : Pmap_raw A) :
-  m !! Pos.shiftl_nat 1 (Pdepth m) = None.
-Proof. induction m as [|[x|] l IHl r IHr]; auto. Qed.
-Lemma Pfresh_fresh {A} (m : Pmap A) : m !! Pfresh m = None.
-Proof.
-  destruct m as [m ?]; unfold lookup, Plookup, Pfresh; simpl.
-  destruct (Pfresh_go m _) eqn:?; eauto using Pfresh_go_fresh, Pfresh_depth.
-Qed.
-
-Instance Pset_fresh : Fresh positive Pset := λ X,
-  let (m) := X in Pfresh m.
-Instance Pset_fresh_spec : FreshSpec positive Pset.
-Proof.
-  split.
-  - apply _.
-  - intros X Y; rewrite <-elem_of_equiv_L. by intros ->.
-  - unfold elem_of, mapset_elem_of, fresh; intros [m]; simpl.
-    by rewrite Pfresh_fresh.
-Qed.

theories/sets.v

@@ -865,69 +865,6 @@ Section more_quantifiers.
   Proof. unfold set_Exists. naive_solver. Qed.
 End more_quantifiers.
 
-(** * Fresh elements *)
-(** We collect some properties on the [fresh] operation. In particular we
-generalize [fresh] to generate lists of fresh elements. *)
-Fixpoint fresh_list `{Fresh A C, Union C, Singleton A C}
-    (n : nat) (X : C) : list A :=
-  match n with
-  | 0 => []
-  | S n => let x := fresh X in x :: fresh_list n ({[ x ]} ∪ X)
-  end.
-Instance: Params (@fresh_list) 6 := {}.
-
-Inductive Forall_fresh `{ElemOf A C} (X : C) : list A → Prop :=
-  | Forall_fresh_nil : Forall_fresh X []
-  | Forall_fresh_cons x xs :
-     x ∉ xs → x ∉ X → Forall_fresh X xs → Forall_fresh X (x :: xs).
-
-Section fresh.
-  Context `{FreshSpec A C}.
-  Implicit Types X Y : C.
-
-  Global Instance fresh_proper: Proper ((≡@{C}) ==> (=)) fresh.
-  Proof. intros ???. by apply fresh_proper_alt, elem_of_equiv. Qed.
-  Global Instance fresh_list_proper n : Proper ((≡@{C}) ==> (=)) (fresh_list n).
-  Proof. induction n as [|n IH]; intros ?? E; by setoid_subst. Qed.
-
-  Lemma exist_fresh X : ∃ x, x ∉ X.
-  Proof. exists (fresh X). apply is_fresh. Qed.
-  Lemma Forall_fresh_NoDup X xs : Forall_fresh X xs → NoDup xs.
-  Proof. induction 1; by constructor. Qed.
-  Lemma Forall_fresh_elem_of X xs x : Forall_fresh X xs → x ∈ xs → x ∉ X.
-  Proof.
-    intros HX; revert x; rewrite <-Forall_forall. by induction HX; constructor.
-  Qed.
-  Lemma Forall_fresh_alt X xs :
-    Forall_fresh X xs ↔ NoDup xs ∧ ∀ x, x ∈ xs → x ∉ X.
-  Proof.
-    split; eauto using Forall_fresh_NoDup, Forall_fresh_elem_of.
-    rewrite <-Forall_forall.
-    intros [Hxs Hxs']. induction Hxs; decompose_Forall_hyps; constructor; auto.
-  Qed.
-  Lemma Forall_fresh_subseteq X Y xs :
-    Forall_fresh X xs → Y ⊆ X → Forall_fresh Y xs.
-  Proof. rewrite !Forall_fresh_alt; set_solver. Qed.
-
-  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 : x ∈ fresh_list n X → x ∉ X.
-  Proof.
-    revert X. induction n as [|n IH]; intros X; simpl;[by rewrite elem_of_nil|].
-    rewrite elem_of_cons; intros [->| Hin]; [apply is_fresh|].
-    apply IH in Hin; set_solver.
-  Qed.
-  Lemma NoDup_fresh_list n X : NoDup (fresh_list n X).
-  Proof.
-    revert X. induction n; simpl; constructor; auto.
-    intros Hin; apply fresh_list_is_fresh in Hin; set_solver.
-  Qed.
-  Lemma Forall_fresh_list X n : Forall_fresh X (fresh_list n X).
-  Proof.
-    rewrite Forall_fresh_alt; eauto using NoDup_fresh_list, fresh_list_is_fresh.
-  Qed.
-End fresh.
-
 (** * Properties of implementations of sets that form a monad *)
 Section set_monad.
   Context `{MonadSet M}.