Merge branch 'robbert/pretty_0' into 'master'

Pretty-print 0 as "0" for N, Z, and nat

See merge request !200

CHANGELOG.md

@@ -36,6 +36,8 @@ Coq 8.8 and 8.9 are no longer supported.
     iterated addition.
   + Rename and restate many lemmas so as to be consistent with the conventions
     for Coq's number types `nat`, `N`, and `Z`.
+- Fix a bug where `pretty 0` was defined as `""`, the empty string. It now
+  returns `"0"` for `N`, `Z`, and `nat`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):

tests/pretty.v

+From stdpp Require Import pretty.
+
+Section N.
+  Local Open Scope N_scope.
+
+  Lemma pretty_N_0 : pretty 0 = "0".
+  Proof. reflexivity. Qed.
+  Lemma pretty_N_1 : pretty 1 = "1".
+  Proof. reflexivity. Qed.
+  Lemma pretty_N_9 : pretty 9 = "9".
+  Proof. reflexivity. Qed.
+  Lemma pretty_N_10 : pretty 10 = "10".
+  Proof. reflexivity. Qed.
+  Lemma pretty_N_100 : pretty 100 = "100".
+  Proof. reflexivity. Qed.
+  Lemma pretty_N_123456789 : pretty 123456789 = "123456789".
+  Proof. reflexivity. Qed.
+End N.
+
+Section nat.
+  Local Open Scope nat_scope.
+
+  Lemma pretty_nat_0 : pretty 0 = "0".
+  Proof. reflexivity. Qed.
+  Lemma pretty_nat_1 : pretty 1 = "1".
+  Proof. reflexivity. Qed.
+  Lemma pretty_nat_9 : pretty 9 = "9".
+  Proof. reflexivity. Qed.
+  Lemma pretty_nat_10 : pretty 10 = "10".
+  Proof. reflexivity. Qed.
+  Lemma pretty_nat_100 : pretty 100 = "100".
+  Proof. reflexivity. Qed.
+  Lemma pretty_nat_1234 : pretty 1234 = "1234".
+  Proof. reflexivity. Qed.
+End nat.
+
+Section Z.
+  Local Open Scope Z_scope.
+
+  Lemma pretty_Z_0 : pretty 0 = "0".
+  Proof. reflexivity. Qed.
+  Lemma pretty_Z_1 : pretty 1 = "1".
+  Proof. reflexivity. Qed.
+  Lemma pretty_Z_9 : pretty 9 = "9".
+  Proof. reflexivity. Qed.
+  Lemma pretty_Z_10 : pretty 10 = "10".
+  Proof. reflexivity. Qed.
+  Lemma pretty_Z_100 : pretty 100 = "100".
+  Proof. reflexivity. Qed.
+  Lemma pretty_Z_123456789 : pretty 123456789 = "123456789".
+  Proof. reflexivity. Qed.
+  Lemma pretty_Z_opp_1 : pretty (-1) = "-1".
+  Proof. reflexivity. Qed.
+  Lemma pretty_Z_opp_9 : pretty (-9) = "-9".
+  Proof. reflexivity. Qed.
+  Lemma pretty_Z_opp_10 : pretty (-10) = "-10".
+  Proof. reflexivity. Qed.
+  Lemma pretty_Z_opp_100 : pretty (-100) = "-100".
+  Proof. reflexivity. Qed.
+  Lemma pretty_Z_opp_123456789 : pretty (-123456789) = "-123456789".
+  Proof. reflexivity. Qed.
+End Z.
\ No newline at end of file

theories/pretty.v

@@ -4,11 +4,16 @@ From Coq Require Import Ascii.
 From stdpp Require Import options.
 
 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.
+Lemma pretty_N_char_inj x y :
+  (x < 10)%N → (y < 10)%N → pretty_N_char x = pretty_N_char y → x = y.
+Proof. compute; intros. by repeat (discriminate || case_match). Qed.
+
 Fixpoint pretty_N_go_help (x : N) (acc : Acc (<)%N x) (s : string) : string :=
   match decide (0 < x)%N with
   | left H => pretty_N_go_help (x `div` 10)%N
@@ -18,6 +23,9 @@ Fixpoint pretty_N_go_help (x : N) (acc : Acc (<)%N x) (s : string) : string :=
   end.
 Definition pretty_N_go (x : N) : string → string :=
   pretty_N_go_help x (wf_guard 32 N.lt_wf_0 x).
+Instance pretty_N : Pretty N := λ x,
+  if decide (x = 0)%N then "0" else pretty_N_go x "".
+
 Lemma pretty_N_go_0 s : pretty_N_go 0 s = s.
 Proof. done. Qed.
 Lemma pretty_N_go_help_irrel x acc1 acc2 s :
@@ -31,22 +39,45 @@ Lemma pretty_N_go_step x s :
   = pretty_N_go (x `div` 10) (String (pretty_N_char (x `mod` 10)) s).
 Proof.
   unfold pretty_N_go; intros; destruct (wf_guard 32 N.lt_wf_0 x).
-  destruct wf_guard. (* this makes coqchk happy. *)
+  destruct (wf_guard _ _). (* this makes coqchk happy. *)
   unfold pretty_N_go_help at 1; fold pretty_N_go_help.
   by destruct (decide (0 < x)%N); auto using pretty_N_go_help_irrel.
 Qed.
-Instance pretty_N : Pretty N := λ x, pretty_N_go x ""%string.
-Lemma pretty_N_unfold x : pretty x = pretty_N_go x "".
-Proof. done. Qed.
+
+(** Helper lemma to prove [pretty_N_inj] and [pretty_Z_inj]. *)
+Lemma pretty_N_go_ne_0 x s : s ≠ "0" → pretty_N_go x s ≠ "0".
+Proof.
+  revert s. induction (N.lt_wf_0 x) as [x _ IH]; intros s ?.
+  assert (x = 0 ∨ 0 < x < 10 ∨ 10 ≤ x)%N as [->|[[??]|?]] by lia.
+  - by rewrite pretty_N_go_0.
+  - rewrite pretty_N_go_step by done. apply IH.
+    { by apply N.div_lt. }
+    assert (x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4 ∨ x = 5 ∨ x = 6
+          ∨ x = 7 ∨ x = 8 ∨ x = 9)%N by lia; naive_solver.
+  - rewrite 2!pretty_N_go_step by (try apply N.div_str_pos_iff; lia).
+    apply IH; [|done].
+    trans (x `div` 10)%N; apply N.div_lt; auto using N.div_str_pos with lia.
+Qed.
+(** Helper lemma to prove [pretty_Z_inj]. *)
+Lemma pretty_N_go_ne_dash x s s' : s ≠ "-" +:+ s' → pretty_N_go x s ≠ "-" +:+ s'.
+Proof.
+  revert s. induction (N.lt_wf_0 x) as [x _ IH]; intros s ?.
+  assert (x = 0 ∨ 0 < x)%N as [->|?] by lia.
+  - by rewrite pretty_N_go_0.
+  - rewrite pretty_N_go_step by done. apply IH.
+    { by apply N.div_lt. }
+    unfold pretty_N_char. by repeat case_match.
+Qed.
+
 Instance pretty_N_inj : Inj (=@{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). }
   cut (∀ x y s s', pretty_N_go x s = pretty_N_go y s' →
     String.length s = String.length s' → x = y ∧ s = s').
-  { intros help x y Hp.
-    eapply (help x y "" ""); [by rewrite <-!pretty_N_unfold|done]. }
+  { intros help x y. unfold pretty, pretty_N. intros.
+    repeat case_decide; simplify_eq/=; [done|..].
+    - by destruct (pretty_N_go_ne_0 y "").
+    - by destruct (pretty_N_go_ne_0 x "").
+    - by apply (help x y "" ""). }
   assert (∀ x s, ¬String.length (pretty_N_go x s) < String.length s) as help.
   { setoid_rewrite <-Nat.le_ngt.
     intros x; induction (N.lt_wf_0 x) as [x _ IH]; intros s.
@@ -57,18 +88,30 @@ Proof.
   assert ((x = 0 ∨ 0 < x) ∧ (y = 0 ∨ 0 < y))%N as [[->|?] [->|?]] by lia;
     rewrite ?pretty_N_go_0, ?pretty_N_go_step, ?(pretty_N_go_step y) by done.
   { done. }
-  { intros -> Hlen; edestruct help; rewrite Hlen; simpl; lia. }
-  { intros <- Hlen; edestruct help; rewrite <-Hlen; simpl; lia. }
-  intros Hs Hlen; apply IH in Hs; destruct Hs;
-    simplify_eq/=; split_and?; auto using N.div_lt_upper_bound with lia.
-  rewrite (N.div_mod x 10), (N.div_mod y 10) by done.
-  auto using N.mod_lt with f_equal.
+  { intros -> Hlen. edestruct help; rewrite Hlen; simpl; lia. }
+  { intros <- Hlen. edestruct help; rewrite <-Hlen; simpl; lia. }
+  intros Hs Hlen.
+  apply IH in Hs as [? [= Hchar]];
+    [|auto using N.div_lt_upper_bound with lia|simpl; lia].
+  split; [|done].
+  apply pretty_N_char_inj in Hchar; [|by auto using N.mod_lt..].
+  rewrite (N.div_mod x 10), (N.div_mod y 10) by done. lia.
 Qed.
-Instance pretty_Z : Pretty Z := λ x,
-  match x with
-  | Z0 => "" | Zpos x => pretty (Npos x) | Zneg x => "-" +:+ pretty (Npos x)
-  end%string.
+
 Instance pretty_nat : Pretty nat := λ x, pretty (N.of_nat x).
 Instance pretty_nat_inj : Inj (=@{nat}) (=) pretty.
 Proof. apply _. Qed.
 
+Instance pretty_Z : Pretty Z := λ x,
+  match x with
+  | Z0 => "0" | Zpos x => pretty (Npos x) | Zneg x => "-" +:+ pretty (Npos x)
+  end%string.
+Instance pretty_Z_inj : Inj (=@{Z}) (=) pretty.
+Proof.
+  unfold pretty, pretty_Z.
+  intros [|x|x] [|y|y] Hpretty; simplify_eq/=; try done.
+  - by destruct (pretty_N_go_ne_0 (N.pos y) "").
+  - by destruct (pretty_N_go_ne_0 (N.pos x) "").
+  - by edestruct (pretty_N_go_ne_dash (N.pos x) "").
+  - by edestruct (pretty_N_go_ne_dash (N.pos y) "").
+Qed.