pretty.v 3.07 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
2
(* This file is distributed under the terms of the BSD license. *)
3 4 5
From stdpp Require Export strings.
From stdpp Require Import relations.
From Coq Require Import Ascii.
6
Set Default Proof Using "Type*".
7 8 9 10 11 12 13

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.
Robbert Krebbers's avatar
Robbert Krebbers committed
14
Fixpoint pretty_N_go_help (x : N) (acc : Acc (<)%N x) (s : string) : string :=
15
  match decide (0 < x)%N with
Robbert Krebbers's avatar
Robbert Krebbers committed
16 17
  | left H => pretty_N_go_help (x `div` 10)%N
     (Acc_inv acc (N.div_lt x 10 H eq_refl))
18 19 20
     (String (pretty_N_char (x `mod` 10)) s)
  | right _ => s
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
21 22 23 24 25 26 27 28 29 30 31 32 33 34 35
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).
36 37
  destruct wf_guard. (* this makes coqchk happy. *)
  unfold pretty_N_go_help at 1; fold pretty_N_go_help.
Robbert Krebbers's avatar
Robbert Krebbers committed
38 39 40
  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.
41
Lemma pretty_N_unfold x : pretty x = pretty_N_go x "".
42
Proof. done. Qed.
43
Instance pretty_N_inj : Inj (@eq N) (=) pretty.
44 45 46 47
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). }
Robbert Krebbers's avatar
Robbert Krebbers committed
48
  cut ( x y s s', pretty_N_go x s = pretty_N_go y s' 
Robbert Krebbers's avatar
Robbert Krebbers committed
49
    String.length s = String.length s'  x = y  s = s').
50
  { intros help x y Hp.
51
    eapply (help x y "" ""); [by rewrite <-!pretty_N_unfold|done]. }
Robbert Krebbers's avatar
Robbert Krebbers committed
52
  assert ( x s, ¬String.length (pretty_N_go x s) < String.length s) as help.
53
  { setoid_rewrite <-Nat.le_ngt.
Robbert Krebbers's avatar
Robbert Krebbers committed
54 55 56
    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.
57
    etrans; [|by eapply IH, N.div_lt]; simpl; lia. }
Robbert Krebbers's avatar
Robbert Krebbers committed
58 59 60 61 62 63 64
  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;
65
    simplify_eq/=; split_and?; auto using N.div_lt_upper_bound with lia.
66 67 68 69 70 71 72
  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.