Module Digits

Require Import Orders.
Require Import Ascii.
Require Import String.
Require Import List.
Require Import Equivalence.
Require Import EquivDec.
Require Import Compare_dec.
Require Import Omega.
Require Import Nat.
Require Import ZArith.
Require Import Eqdep_dec.
Require Import Peano_dec.

Section prelude.
  

  Theorem K_nat :
    forall (x:nat) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.

  Theorem eq_rect_eq_nat :
    forall (p:nat) (Q:nat->Type) (x:Q p) (h:p=p), x = eq_rect p Q x p h.
  
  Scheme le_ind' := Induction for le Sort Prop.

  Theorem le_uniqueness_proof : forall (n m : nat) (p q : n <= m), p = q.

  End prelude.

Section Digits.
  Definition maxbase := 36.

  Context (base:nat) (basenzero:1<base).
  Definition digit := {n:nat | n < base}.

  Definition digit_proj (d:digit) : nat := proj1_sig d.

Section natexplosion.

  Lemma digit_pf_irrel a (pf1 pf2:a<base) : pf1 = pf2.

  Lemma digit_ext (a b:digit) : proj1_sig a = proj1_sig b -> a = b.
  
  Fixpoint digits_to_nat_aux (l:list digit) (acc:nat) : nat
  := match l with
     | nil => acc
     | d::lx => digits_to_nat_aux lx (acc*base+(proj1_sig d))
     end.

  Lemma digits_to_nat_aux_app l1 l2 n :
    digits_to_nat_aux (l1 ++ l2) n = digits_to_nat_aux l2 (digits_to_nat_aux l1 n).

  Definition digits_to_nat (l:list digit) : nat
    := digits_to_nat_aux l 0.
  
  Fixpoint trim_digits (l:list digit) : list digit
    := match l with
       | (exist _ 0 _)::lx => trim_digits lx
       | _ => l
       end.

  Program Fixpoint nat_to_digits_backwards (n:nat) {measure n lt_wf} :
    {l:list digit | digits_to_nat (rev l) = n /\ (forall a, hd_error (rev l) = Some a -> proj1_sig a <> 0)}
    := if n == 0
       then nil
       else exist _ (cons (n mod base)
                     (nat_to_digits_backwards (n / base)%nat)
                    ) _.

Program Definition nat_to_digits (n:nat) : list digit
  := rev (nat_to_digits_backwards n).

Lemma trim_digits_to_nat l : digits_to_nat (trim_digits l) = digits_to_nat l.


Lemma digits_to_nat_aux_acc_le_preserve l acc acc':
  acc <= acc' ->
  digits_to_nat_aux l acc <= digits_to_nat_aux l acc'.

Lemma digits_to_nat_aux_le l acc : acc <= digits_to_nat_aux l acc.

Lemma digits_to_nat_aux_bound l c:
  c*(base^length l) <= digits_to_nat_aux l c < (c+1)*(base^(length l)).

Lemma digits_to_nat_aux_acc_inj_helper1 a b c n1 n2 :
  0 <> c ->
  a < base ->
  b < base ->
  (c * base + a) * base ^ n2 < (c * base + b + 1) * base ^ n1 ->
  ~ n1 < n2.

  Lemma digits_to_nat_aux_acc_inj_helper12 a b c n1 n2 :
    a <> 0 ->
  a < base ->
  b < base ->
  (c * base + a) * base ^ n2 < (c * base + b + 1) * base ^ n1 ->
  ~ n1 < n2.

  Lemma digits_to_nat_aux_acc_inj_helper2 a b c n :
  (c * base + a) * base ^ n < (c * base + b + 1) * base ^ n ->
  ~ b < a.

  Lemma digits_to_nat_aux_acc_inj_helper01 a b n1 n2 :
    a <> 0 ->
    a < base ->
    b < base ->
    a * base ^ n1 < (b + 1) * base ^ n2 ->
    ~ n2 < n1.
    
Lemma digits_to_nat_aux_acc_inj l1 l2 c (a b:digit):
      0 <> c ->
      digits_to_nat_aux l1 (c*base+proj1_sig a) = digits_to_nat_aux l2 (c*base+proj1_sig b) ->
      (length l1 = length l2) /\ a = b.

Lemma digits_to_nat_aux_acc_inj2 l1 l2 c (a b:digit):
  proj1_sig a <> 0 ->
  proj1_sig b <> 0 ->
      digits_to_nat_aux l1 (c*base+proj1_sig a) = digits_to_nat_aux l2 (c*base+proj1_sig b) ->
      (length l1 = length l2) /\ a = b.
  
Lemma digits_to_nat_aux_digits_inj l1 l2 n :
  n <> 0 ->
  digits_to_nat_aux l1 n = digits_to_nat_aux l2 n ->
  l1 = l2.

Lemma trim_digits_nz {y d l}: trim_digits y = d :: l -> proj1_sig d <> 0.

Lemma digits_to_nat_nzero l x :
  x <> 0 ->
  digits_to_nat_aux l x <> 0.


Lemma trim_nat_to_digits x :
  trim_digits (nat_to_digits x) = nat_to_digits x.

Theorem digits_to_nat_inv x y :
  digits_to_nat x = digits_to_nat y ->
  trim_digits x = trim_digits y.

Theorem nat_to_digits_inv x y :
  nat_to_digits x = nat_to_digits y ->
  x = y.

Theorem nat_to_digits_to_nat (n:nat) :
  digits_to_nat (nat_to_digits n) = n.


Theorem digits_to_nat_to_digits (ld:list digit) :
  nat_to_digits (digits_to_nat ld) = trim_digits ld.

End natexplosion.

Section tostring.

Definition digit_to_char (n:digit) : ascii
  := match proj1_sig n with
         | 0 => "0"%char
         | 1 => "1"%char
         | 2 => "2"%char
         | 3 => "3"%char
         | 4 => "4"%char
         | 5 => "5"%char
         | 6 => "6"%char
         | 7 => "7"%char
         | 8 => "8"%char
         | 9 => "9"%char
         | 10 => "A"%char
         | 11 => "B"%char
         | 12 => "C"%char
         | 13 => "D"%char
         | 14 => "E"%char
         | 15 => "F"%char
         | 16 => "G"%char
         | 17 => "H"%char
         | 18 => "I"%char
         | 19 => "J"%char
         | 20 => "K"%char
         | 21 => "L"%char
         | 22 => "M"%char
         | 23 => "N"%char
         | 24 => "O"%char
         | 25 => "P"%char
         | 26 => "Q"%char
         | 27 => "R"%char
         | 28 => "S"%char
         | 29 => "T"%char
         | 30 => "U"%char
         | 31 => "V"%char
         | 32 => "W"%char
         | 33 => "X"%char
         | 34 => "Y"%char
         | 35 => "Z"%char
         | _ => "?"%char
     end.

Definition char_to_digit_aux (a:ascii) : option nat
  := match a with
         | "0"%char => Some 0
         | "1"%char => Some 1
         | "2"%char => Some 2
         | "3"%char => Some 3
         | "4"%char => Some 4
         | "5"%char => Some 5
         | "6"%char => Some 6
         | "7"%char => Some 7
         | "8"%char => Some 8
         | "9"%char => Some 9
         | "A"%char => Some 10
         | "B"%char => Some 11
         | "C"%char => Some 12
         | "D"%char => Some 13
         | "E"%char => Some 14
         | "F"%char => Some 15
         | "G"%char => Some 16
         | "H"%char => Some 17
         | "I"%char => Some 18
         | "J"%char => Some 19
         | "K"%char => Some 20
         | "L"%char => Some 21
         | "M"%char => Some 22
         | "N"%char => Some 23
         | "O"%char => Some 24
         | "P"%char => Some 25
         | "Q"%char => Some 26
         | "R"%char => Some 27
         | "S"%char => Some 28
         | "T"%char => Some 29
         | "U"%char => Some 30
         | "V"%char => Some 31
         | "W"%char => Some 32
         | "X"%char => Some 33
         | "Y"%char => Some 34
         | "Z"%char => Some 35
         | _ => None
     end.

Program Definition char_to_digit (a:ascii) : option digit
  := match char_to_digit_aux a with
     | Some n =>
       match lt_dec n base with
           | left pf => Some (exist _ n pf)
           | right _ => None
       end
     | None => None
     end.

Lemma char_to_digit_to_char (a:ascii) (d:digit) :
  char_to_digit a = Some d -> digit_to_char d = a.

Lemma digit_to_char_to_digit (basesmall:base<=maxbase) (d:digit) :
  char_to_digit (digit_to_char d) = Some d.

Fixpoint string_to_digits (s:string) : option (list digit*string)
  := match s with
     | ""%string => None
     | String a s' =>
       match char_to_digit a with
       | Some dd =>
         match string_to_digits s' with
         | Some (ld,rest) => Some (dd::ld,rest)
         | None => Some (dd::nil,s')
         end
       | None => None
       end
     end.

Fixpoint list_to_string (l:list ascii) : string
  := match l with
         | nil => EmptyString
         | cons x xs => String x (list_to_string xs)
     end.

Definition digits_to_string_aux (ld:list digit) : string
  := list_to_string (map digit_to_char ld).


Definition digits_to_string (ld:list digit) : string
  := match digits_to_string_aux ld with
     | ""%string => "0"
     | s => s
     end.

Lemma string_to_digits_to_string_aux (s:string) (ld:list digit) (rest:string) :
  string_to_digits s = Some (ld,rest) ->
  (digits_to_string_aux ld ++ rest)%string = s.

Lemma string_to_digits_to_string (s:string) (ld:list digit) (rest:string) :
  string_to_digits s = Some (ld,rest) ->
  (digits_to_string ld ++ rest)%string = s.

Lemma string_to_digits_empty : string_to_digits ""%string = None.

Fixpoint iszeros (s:string)
  := match s with
     | ""%string => True
     | String a s' => "a"%char = "0"%char /\ iszeros s'
     end.

Fixpoint trim_extra_stringdigits (s:string)
  := match s with
      | String "0" s => trim_extra_stringdigits s
      | _ => s
      end.

Definition default_to_string0 (s:string)
  := match string_to_digits s with
      | Some _ => s
      | None => String "0" s
      end.


Definition trim_stringdigits (s:string)
  := default_to_string0 (trim_extra_stringdigits s).

Lemma digit0pf : 0 < base.

Definition digit0 : digit := exist _ 0 digit0pf.

Definition default_to_digits0 l
  := match l with
      | nil => digit0::nil
      | _ => l
      end.

Lemma char_to_digit0 : (char_to_digit "0") = Some digit0.

Lemma char_to_digit0_inv a pf :
  char_to_digit a = Some (exist _ 0 pf) -> a = "0"%char.

Lemma trim_stringdigits_some s l1 rest :
  string_to_digits s = Some (l1, rest) ->
  string_to_digits (trim_stringdigits (String "0" s)) =
  string_to_digits (trim_stringdigits s).

Lemma trim_extra_stringdigits_None rest :
  string_to_digits rest = None ->
  trim_extra_stringdigits rest = rest.

Lemma trim_extra_stringdigits_nzero a s :
    a<> "0"%char ->
    trim_extra_stringdigits (String a s) = String a s.

Lemma string_to_digits_trim s l rest:
  string_to_digits s = Some (l, rest) ->
  string_to_digits (trim_stringdigits s) = Some (default_to_digits0 (trim_digits l),rest).


Lemma digits_to_string_aux_to_digits_None
      (basesmall:base<=maxbase) (ld:list digit) (rest:string) :
  string_to_digits rest = None ->
  ld <> nil ->
  string_to_digits (digits_to_string_aux ld ++ rest) = Some (ld,rest).

Definition nat_to_string (n:nat) : string
  := digits_to_string (nat_to_digits n).

Definition string_to_nat (s:string) : option (nat*string)
  := match string_to_digits s with
     | Some (dl,rest) => Some (digits_to_nat dl, rest)
     | None => None
     end.

Lemma digits_to_string_default l :
  digits_to_string (default_to_digits0 l) = digits_to_string l.
  
Theorem string_to_nat_to_string (s:string) (n:nat) (rest:string) :
  string_to_nat s = Some (n,rest) ->
  (nat_to_string n ++ rest)%string = trim_stringdigits s.

Lemma digits_to_string_aux_empty n:
  digits_to_string_aux (nat_to_digits n) = ""%string -> n = 0.

Lemma append_nil_r s : (s ++ "")%string = s.
      
Theorem nat_to_string_to_nat (basesmall:base<=maxbase) n (rest:string) :
  string_to_digits rest = None ->
  string_to_nat (nat_to_string n ++ rest) = Some (n, rest).

Theorem nat_to_string_inj_full (basesmall:base<=maxbase) n1 n2 rest1 rest2 :
  string_to_digits rest1 = None ->
  string_to_digits rest2 = None ->
  (nat_to_string n1 ++ rest1 = nat_to_string n2 ++ rest2)%string ->
  n1 = n2 /\ rest1 = rest2.

Theorem nat_to_string_inj (basesmall:base<=maxbase) n1 n2 :
  nat_to_string n1 = nat_to_string n2 -> n1 = n2.

End tostring.

Section Ztostring.

  Local Open Scope Z.

  Definition Z_to_string (z:Z) :=
    match z with
    | Z0 => "0"%string
    | Zpos n => nat_to_string (Pos.to_nat n)
    | Zneg n => String ("-"%char) (nat_to_string (Pos.to_nat n))
    end.

  Definition string_to_Z (s:string) : option (Z* string)
    := match s with
       | ""%string => None
       | String ("+"%char) l' =>
         match string_to_nat l' with
         | Some (n,rest) => Some (Z.of_nat n, rest)
         | None => None
         end
       | String ("-"%char) l' =>
         match string_to_nat l' with
         | Some (n,rest) =>
           match n with
           | 0%nat => None
           | _ => Some (Zneg (Pos.of_nat n), rest)
           end
         | None => None
         end
       | l' =>
         match string_to_nat l' with
         | Some (n,rest) => Some (Z.of_nat n, rest)
         | None => None
         end
       end.

  Definition trim_stringZdigits (s:string)
    := match s with
       | String "+" l => trim_stringdigits l
       | String "-" l => String "-" (trim_stringdigits l)
       | l => trim_stringdigits l
       end.

  Lemma nat_to_string_nempty n : nat_to_string n <> ""%string.

  Lemma append_empty_both l1 l2
    : (l1 ++ l2)%string = ""%string ->
      l1 = ""%string /\ l2 = ""%string.

  Theorem string_to_Z_to_string (s:string) (n:Z) (rest:string) :
    string_to_Z s = Some (n,rest) ->
    (Z_to_string n ++ rest)%string = trim_stringZdigits s.
    
  Theorem Z_to_string_to_Z (basesmall:(base<=maxbase)%nat) n (rest:string) :
    string_to_digits rest = None ->
    string_to_Z (Z_to_string n ++ rest) = Some (n, rest).

  Theorem Z_to_string_inj_full
          (basesmall:(base<=maxbase)%nat) n1 n2 rest1 rest2 :
  string_to_digits rest1 = None ->
  string_to_digits rest2 = None ->
  (Z_to_string n1 ++ rest1 = Z_to_string n2 ++ rest2)%string ->
  n1 = n2 /\ rest1 = rest2.

  Theorem Z_to_string_inj (basesmall:(base<=maxbase)%nat) n1 n2 :
    Z_to_string n1 = Z_to_string n2 -> n1 = n2.

End Ztostring.

End Digits.

Section Bases.
  
  Definition lt_decider (a b:nat) :
    match lt_dec a b with
    | left pf => lt a b
    | right _ => True
    end.

  Definition le_decider (a b:nat) :
    match le_dec a b with
    | left pf => le a b
    | right _ => True
    end.

  Section base2.
    Definition base2valid : 1 < 2 := lt_decider 1 2.
    Definition base2small : 2 <= maxbase := le_decider 2 maxbase.

    Section nat.
      Definition nat_to_string2 := nat_to_string 2 base2valid.
      Definition string2_to_nat := string_to_nat 2.

      Definition nat_to_string2_to_nat
        := nat_to_string_to_nat 2 base2valid base2small.
      
      Definition string2_to_nat_to_string2
        := string_to_nat_to_string 2 base2valid.
      
      Definition nat_to_string2_inj
        : forall x y : nat, nat_to_string2 x = nat_to_string2 y -> x = y
        := nat_to_string_inj 2 base2valid base2small.
      
    End nat.
    
    Section Z.
      Definition Z_to_string2 := Z_to_string 2 base2valid.
      Definition string2_to_Z := string_to_Z 2.

      Definition Z_to_string2_to_Z
        := Z_to_string_to_Z 2 base2valid base2small.
      
      Definition string2_to_Z_to_string2
        := string_to_Z_to_string 2 base2valid.
      
      Definition Z_to_string2_inj
        : forall x y : Z, Z_to_string2 x = Z_to_string2 y -> x = y
        := Z_to_string_inj 2 base2valid base2small.
      
    End Z.
  End base2.

  Section base8.
    Definition base8valid : 1 < 8 := lt_decider 1 8.
    Definition base8small : 8 <= maxbase := le_decider 8 maxbase.

    Section nat.
      Definition nat_to_string8 := nat_to_string 8 base8valid.
      Definition string8_to_nat := string_to_nat 8.

      Definition nat_to_string8_to_nat
        := nat_to_string_to_nat 8 base8valid base8small.
      
      Definition string8_to_nat_to_string8
        := string_to_nat_to_string 8 base8valid.
      
      Definition nat_to_string8_inj
        : forall x y : nat, nat_to_string8 x = nat_to_string8 y -> x = y
        := nat_to_string_inj 8 base8valid base8small.

    End nat.
    
    Section Z.
      Definition Z_to_string8 := Z_to_string 8 base8valid.
      Definition string8_to_Z := string_to_Z 8.

      Definition Z_to_string8_to_Z
        := Z_to_string_to_Z 8 base8valid base8small.
      
      Definition string8_to_Z_to_string8
        := string_to_Z_to_string 8 base8valid.
      
      Definition Z_to_string8_inj
        : forall x y : Z, Z_to_string8 x = Z_to_string8 y -> x = y
        := Z_to_string_inj 8 base8valid base8small.
      
    End Z.
    
  End base8.
  
  Section base10.
    Definition base10valid : 1 < 10 := lt_decider 1 10.
    Definition base10small : 10 <= maxbase := le_decider 10 maxbase.

    Section nat.
      Definition nat_to_string10 := nat_to_string 10 base10valid.
      Definition string10_to_nat := string_to_nat 10.
      
      Definition nat_to_string10_to_nat
        := nat_to_string_to_nat 10 base10valid base10small.
      
      Definition string10_to_nat_to_string10
        := string_to_nat_to_string 10 base10valid.
      
      Definition nat_to_string10_inj
        : forall x y : nat, nat_to_string10 x = nat_to_string10 y -> x = y
        := nat_to_string_inj 10 base10valid base10small.

    End nat.
    
    Section Z.
      Definition Z_to_string10 := Z_to_string 10 base10valid.
      Definition string10_to_Z := string_to_Z 10.
            
      Definition Z_to_string10_to_Z
        := Z_to_string_to_Z 10 base10valid base10small.
      
      Definition string10_to_Z_to_string10
        := string_to_Z_to_string 10 base10valid.
      
      Definition Z_to_string10_inj
        : forall x y : Z, Z_to_string10 x = Z_to_string10 y -> x = y
        := Z_to_string_inj 10 base10valid base10small.
      
    End Z.
  End base10.
  
  Section base16.
    Definition base16valid : 1 < 16 := lt_decider 1 16.
    Definition base16small : 16 <= maxbase := le_decider 16 maxbase.

    Section nat.
      Definition nat_to_string16 := nat_to_string 16 base16valid.
      Definition string16_to_nat := string_to_nat 16.


      Definition nat_to_string16_to_nat
        := nat_to_string_to_nat 16 base16valid base16small.
      
      Definition string16_to_nat_to_string16
        := string_to_nat_to_string 16 base16valid.
      
      Definition nat_to_string16_inj
        : forall x y : nat, nat_to_string16 x = nat_to_string16 y -> x = y
        := nat_to_string_inj 16 base16valid base16small.

    End nat.
    
    Section Z.
      Definition Z_to_string16 := Z_to_string 16 base16valid.
      Definition string16_to_Z := string_to_Z 16.

      Definition Z_to_string16_to_Z
        := Z_to_string_to_Z 16 base16valid base16small.
      
      Definition string16_to_Z_to_string16
        := string_to_Z_to_string 16 base16valid.
      
      Definition Z_to_string16_inj
        : forall x y : Z, Z_to_string16 x = Z_to_string16 y -> x = y
        := Z_to_string_inj 16 base16valid base16small.
      
    End Z.
  End base16.

End Bases.