Qcert.Basic.Util.Digits
Section prelude.
Theorem K_nat :
∀ (x:nat) (P:x = x → Prop), P (refl_equal x) → ∀ p:x = x, P p.
Theorem eq_rect_eq_nat :
∀ (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 : ∀ (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 ∧ (∀ 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.
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
: ∀ 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
: ∀ 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
: ∀ 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
: ∀ 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
: ∀ 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
: ∀ 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
: ∀ 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
: ∀ 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.