Pretty printer for N and Z, fresh string generator.

theories/pretty.v

+(* Copyright (c) 2012-2014, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
+Require Export numbers option.
+Require Import Ascii String ars.
+
+Infix "+:+" := String.append (at level 60, right associativity) : C_scope.
+Instance assci_eq_dec : ∀ a1 a2, Decision (a1 = a2) := ascii_dec.
+Instance string_eq_dec (s1 s2 : string) : Decision (s1 = s2).
+Proof. solve_decision. Defined.
+Instance: Injective (=) (=) (String.append s1).
+Proof. intros s1 ???. induction s1; simplify_equality'; f_equal'; auto. Qed.
+
+Class Pretty A := pretty : A → string.
+Definition pretty_N_char (x : N) : ascii :=
+  match x with
+  | 0 => "0" | 1 => "1" | 2 => "2" | 3 => "3" | 4 => "4"
+  | 5 => "5" | 6 => "6" | 7 => "7" | 8 => "8" | _ => "9"
+  end%char%N.
+Definition pretty_N_go (x : N)
+    (go : ∀ y, (y < x)%N → string → string) (s : string) : string :=
+  match decide (0 < x)%N with
+  | left H => go (x `div` 10)%N (N.div_lt x 10 H eq_refl)
+     (String (pretty_N_char (x `mod` 10)) s)
+  | right _ => s
+  end.
+Instance pretty_N : Pretty N := λ x,
+  Fix_F _ pretty_N_go (wf_guard 32 N.lt_wf_0 x) ""%string.
+Instance pretty_N_injective : Injective (@eq N) (=) pretty.
+Proof.
+  assert (∀ x y, x < 10 → y < 10 →
+    pretty_N_char x =  pretty_N_char y → x = y)%N.
+  { compute; intros. by repeat (discriminate || case_match). }
+  set (f x (acc : Acc _ x) := Fix_F _ pretty_N_go acc).
+  cut (∀ x acc y acc' s s', length s = length s' →
+    f x acc s = f y acc' s' → x = y ∧ s = s').
+  { intros help x y ?. eapply help; eauto. }
+  assert (∀ x acc s, ¬length (f x acc s) < length s) as help.
+  { setoid_rewrite <-Nat.le_ngt.
+    fix 2; intros x [?] s; simpl. unfold pretty_N_go; fold pretty_N_go.
+    destruct (decide (0 < x))%N; [|auto].
+    etransitivity; [|eauto]. simpl; lia. }
+  fix 2; intros x [?] y [?] s s' ?; simpl.
+  unfold pretty_N_go; fold pretty_N_go; intros Hs.
+  destruct (decide (0 < x))%N, (decide (0 < y))%N;
+    try match goal with
+    | H : f ?x ?acc ?s = _ |- _ =>
+       destruct (help x acc s); rewrite H; simpl; lia
+    | H : _ = f ?x ?acc ?s |- _ =>
+       destruct (help x acc s); rewrite <-H; simpl; lia
+    end; auto with lia.
+  apply pretty_N_injective in Hs; [|by f_equal']; destruct Hs.
+  simplify_equality; split; [|done].
+  rewrite (N.div_mod x 10), (N.div_mod y 10) by done.
+  auto using N.mod_lt with f_equal.
+Qed.
+Instance pretty_Z : Pretty Z := λ x,
+  match x with
+  | Z0 => "" | Zpos x => pretty (Npos x) | Zneg x => "-" +:+ pretty (Npos x)
+  end%string.

theories/stringmap.v

@@ -4,15 +4,9 @@
 range over Coq's data type of strings [string]. The implementation uses radix-2
 search trees (uncompressed Patricia trees) as implemented in the file [pmap]
 and guarantees logarithmic-time operations. *)
-Require Export fin_maps.
+Require Export fin_maps pretty.
 Require Import Ascii String list pmap mapset.
 
-Infix "+:+" := String.append (at level 60, right associativity) : C_scope.
-
-Instance assci_eq_dec : ∀ a1 a2, Decision (a1 = a2) := ascii_dec.
-Instance string_eq_dec (s1 s2 : string) : Decision (s1 = s2).
-Proof. solve_decision. Defined.
-
 (** * Encoding and decoding *)
 (** In order to reuse or existing implementation of radix-2 search trees over
 positive binary naturals [positive], we define an injection [string_to_pos]
@@ -167,3 +161,40 @@ Qed.
 Notation stringset := (mapset (stringmap unit)).
 Instance stringmap_dom {A} : Dom (stringmap A) stringset := mapset_dom.
 Instance: FinMapDom positive Pmap Pset := mapset_dom_spec.
+
+(** * Generating fresh strings *)
+Local Open Scope N_scope.
+Let R {A} (s : string) (m : stringmap A) (n1 n2 : N) :=
+  n2 < n1 ∧ is_Some (m !! (s +:+ pretty (n1 - 1))).
+Lemma fresh_string_step {A} s (m : stringmap A) n x :
+  m !! (s +:+ pretty n) = Some x → R s m (1 + n) n.
+Proof. split; [lia|]. replace (1 + n - 1) with n by lia; eauto. Qed.
+Lemma fresh_string_R_wf {A} s (m : stringmap A) : wf (R s m).
+Proof.
+  induction (map_wf m) as [m _ IH]. intros n1; constructor; intros n2 [Hn Hs].
+  specialize (IH _ (delete_subset m (s +:+ pretty (n2 - 1)) Hs) n2).
+  cut (n2 - 1 < n2); [|lia]. clear n1 Hn Hs; revert IH; generalize (n2 - 1).
+  intros n1. induction 1 as [n2 _ IH]; constructor; intros n3 [??].
+  apply IH; [|lia]; split; [lia|].
+  by rewrite lookup_delete_ne by (intros ?; simplify_equality'; lia).
+Qed.
+Definition fresh_string_go {A} (s : string) (m : stringmap A) (n : N)
+    (go : ∀ n', R s m n' n → string) : string :=
+  let s' := s +:+ pretty n in
+  match Some_dec (m !! s') with
+  | 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 :=
+  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.
+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.