diff --git a/theories/fresh_numbers.v b/theories/fresh_numbers.v deleted file mode 100644 index 27f34b25cf76df2373c043ec452e42da42d94508..0000000000000000000000000000000000000000 --- a/theories/fresh_numbers.v +++ /dev/null @@ -1,34 +0,0 @@ -(* 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. diff --git a/theories/nmap.v b/theories/nmap.v index b6fcf98c321cdd49fb87d8ffe62bd20d8cf59d38..d534989e4f5768ce7924dfc9bbbcb9724fc4035e 100644 --- a/theories/nmap.v +++ b/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. diff --git a/theories/pmap.v b/theories/pmap.v index 7bccbf96928cb079e7f89ffa35bbaec957ee922c..c8c35fd6e6fd94104fb206845e8940283c58dadc 100644 --- a/theories/pmap.v +++ b/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. diff --git a/theories/prelude.v b/theories/prelude.v index 219e3c9a759d3965244643c5c515c38ff4a8e624..75e7d67262788fd6f6b82c9c84e082812f25b8b1 100644 --- a/theories/prelude.v +++ b/theories/prelude.v @@ -12,6 +12,5 @@ Require Export collections fin_collections listset - fresh_numbers list lexico.