pretty.v 2.88 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
3 4
From iris.prelude Require Export strings.
From iris.prelude Require Import relations.
5
From Coq Require Import Ascii.
Robbert Krebbers's avatar
Robbert Krebbers committed
6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38

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.
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
     (Acc_inv acc (N.div_lt x 10 H eq_refl))
     (String (pretty_N_char (x `mod` 10)) s)
  | right _ => s
  end.
Definition pretty_N_go (x : N) : string  string :=
  pretty_N_go_help x (wf_guard 32 N.lt_wf_0 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 :
  pretty_N_go_help x acc1 s = pretty_N_go_help x acc2 s.
Proof.
  revert x acc1 acc2 s; fix 2; intros x [acc1] [acc2] s; simpl.
  destruct (decide (0 < x)%N); auto.
Qed.
Lemma pretty_N_go_step x s :
  (0 < x)%N  pretty_N_go 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).
  unfold pretty_N_go_help; 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.
39
Instance pretty_N_inj : Inj (@eq N) (=) pretty.
Robbert Krebbers's avatar
Robbert Krebbers committed
40 41 42 43 44
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' 
45
    String.length s = String.length s'  x = y  s = s').
Robbert Krebbers's avatar
Robbert Krebbers committed
46
  { intros help x y ?. eapply help; eauto. }
47
  assert ( x s, ¬String.length (pretty_N_go x s) < String.length s) as help.
Robbert Krebbers's avatar
Robbert Krebbers committed
48 49 50 51
  { setoid_rewrite <-Nat.le_ngt.
    intros x; 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.
52
    etrans; [|by eapply IH, N.div_lt]; simpl; lia. }
Robbert Krebbers's avatar
Robbert Krebbers committed
53 54 55 56 57 58 59
  intros x; induction (N.lt_wf_0 x) as [x _ IH]; intros y s s'.
  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;
60
    simplify_eq/=; split_and?; auto using N.div_lt_upper_bound with lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
61 62 63 64 65 66 67
  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.