Less inefficient fresh function for pset/nset.

It would still be far more efficient to have a counter for the next memory
index in the executable semantics/frontend.

theories/fresh_numbers.v

-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
-(* This file is distributed under the terms of the BSD license. *)
-(** Given a finite set of binary naturals [N], we generate a fresh element by
-taking the maximum, and adding one to it. We declare this operation as an
-instance of the type class [Fresh]. *)
-Require Export numbers fin_collections.
-
-Definition Nmax `{Elements N C} : C → N := collection_fold Nmax 0%N.
-
-Instance Nmax_proper `{FinCollection N C} : Proper ((≡) ==> (=)) Nmax.
-Proof.
-  apply (collection_fold_proper (=)).
-  * solve_proper.
-  * intros. rewrite !N.max_assoc. f_equal. apply N.max_comm.
-Qed.
-
-Lemma Nmax_max `{FinCollection N C} X x : x ∈ X → (x ≤ Nmax X)%N.
-Proof.
-  apply (collection_fold_ind (λ b X, x ∈ X → (x ≤ b)%N)).
-  * solve_proper.
-  * solve_elem_of.
-  * solve_elem_of (eauto using N.le_max_l, N.le_max_r, N.le_trans).
-Qed.
-
-Instance Nfresh `{FinCollection N C} : Fresh N C := λ l, (1 + Nmax l)%N.
-Instance Nfresh_spec `{FinCollection N C} : FreshSpec N C.
-Proof.
-  split.
-  * apply _.
-  * intros. unfold fresh, Nfresh.
-    setoid_replace X with Y; [done |]. by apply elem_of_equiv.
-  * intros X E. assert (1 ≤ 0)%N as []; [| done].
-    apply N.add_le_mono_r with (Nmax X). by apply Nmax_max.
-Qed.

theories/nmap.v

@@ -84,3 +84,20 @@ Qed.
 Notation Nset := (mapset (Nmap unit)).
 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

@@ -390,3 +390,66 @@ Qed.
 Notation Pset := (mapset (Pmap unit)).
 Instance Pmap_dom {A} : Dom (Pmap A) Pset := mapset_dom.
 Instance: 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 [|l o r] ?; simplify_equality'.
+  destruct (Pfresh_at_depth l d) as [i'|] eqn:?,
+    (Pfresh_at_depth r d) as [i''|] eqn:?; simplify_equality'; 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_equality'.
+  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 [|l IHl [x|] 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/prelude.v

@@ -12,6 +12,5 @@ Require Export
   collections
   fin_collections
   listset
-  fresh_numbers
   list
   lexico.