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

Preliminaries

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.

Numbers as lists of digits

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.

Conversions between nat and lists of digits

  
  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} :
      {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.

Conversions between nat and strings

  
  Section Ntostring.

    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 Ntostring.

Conversions between Z and strings

  
  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.

Integers in base 'n'

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.

Base 2

  
  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.

Base 8

  
  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.
  

Base 10

  
  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.
  

Base 16

  
  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.