From dfa4c3baf0f6bcf789adb5004c9c81c3e4d75575 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 12 Jan 2016 14:27:24 +0100
Subject: [PATCH] Generate multiple fresh strings.

---
 theories/stringmap.v | 21 +++++++++++++++------
 1 file changed, 15 insertions(+), 6 deletions(-)

diff --git a/theories/stringmap.v b/theories/stringmap.v
index 107cf23b..58c8862d 100644
--- a/theories/stringmap.v
+++ b/theories/stringmap.v
@@ -33,20 +33,29 @@ Definition fresh_string_go {A} (s : string) (m : stringmap A) (n : N)
   | inleft (_↾Hs') => go (1 + n)%N (fresh_string_step s m n _ Hs')
   | inright _ => s'
   end.
-Definition fresh_string {A} (m : stringmap A) (s : string) : string :=
+Definition fresh_string {A} (s : string) (m : stringmap A) : string :=
   match m !! s with
   | None => s
   | Some _ =>
      Fix_F _ (fresh_string_go s m) (wf_guard 32 (fresh_string_R_wf s m) 0)
   end.
-Lemma fresh_string_fresh {A} (m : stringmap A) s : m !! fresh_string m s = None.
+Lemma fresh_string_fresh {A} (m : stringmap A) s : m !! fresh_string s m = None.
 Proof.
   unfold fresh_string. destruct (m !! s) as [a|] eqn:Hs; [clear a Hs|done].
   generalize 0 (wf_guard 32 (fresh_string_R_wf s m) 0); revert m.
   fix 3; intros m n [?]; simpl; unfold fresh_string_go at 1; simpl.
   destruct (Some_dec (m !! _)) as [[??]|?]; auto.
 Qed.
-Definition fresh_string_of_set (X : stringset) (s : string) : string :=
-  fresh_string (mapset.mapset_car X) s.
-Lemma fresh_string_of_set_fresh (X : stringset) s : fresh_string_of_set X s ∉ X.
-Proof. apply eq_None_ne_Some, fresh_string_fresh. Qed.
\ No newline at end of file
+Definition fresh_string_of_set (s : string) (X : stringset) : string :=
+  fresh_string s (mapset.mapset_car X).
+Lemma fresh_string_of_set_fresh (X : stringset) s : fresh_string_of_set s X ∉ X.
+Proof. apply eq_None_ne_Some, fresh_string_fresh. Qed.
+
+Fixpoint fresh_strings_of_set
+    (s : string) (n : nat) (X : stringset) : list string :=
+  match n with
+  | 0 => []
+  | S n =>
+     let x := fresh_string_of_set s X in
+     x :: fresh_strings_of_set s n ({[ x ]} ∪ X)
+  end%nat.
\ No newline at end of file
-- 
GitLab