diff options
Diffstat (limited to 'theories')
30 files changed, 4187 insertions, 554 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index b094f81dc6..cba90043d5 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -159,6 +159,9 @@ Inductive nat : Set := | O : nat | S : nat -> nat. +Declare Scope hex_nat_scope. +Delimit Scope hex_nat_scope with xnat. + Declare Scope nat_scope. Delimit Scope nat_scope with nat. Bind Scope nat_scope with nat. diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v index 2a84456500..5eae5567d7 100644 --- a/theories/Init/Decimal.v +++ b/theories/Init/Decimal.v @@ -16,7 +16,7 @@ We represent numbers in base 10 as lists of decimal digits, in big-endian order (most significant digit comes first). *) -Require Import Datatypes. +Require Import Datatypes Specif. (** Unsigned integers are just lists of digits. For instance, ten is (D1 (D0 Nil)) *) @@ -53,6 +53,10 @@ Variant decimal := | Decimal (i:int) (f:uint) | DecimalExp (i:int) (f:uint) (e:int). +Scheme Equality for uint. +Scheme Equality for int. +Scheme Equality for decimal. + Declare Scope dec_uint_scope. Delimit Scope dec_uint_scope with uint. Bind Scope dec_uint_scope with uint. @@ -172,8 +176,8 @@ Fixpoint del_head n d := Definition del_head_int n d := match d with - | Pos d => Pos (del_head n d) - | Neg d => Neg (del_head n d) + | Pos d => del_head n d + | Neg d => del_head n d end. (** [del_tail n d] removes [n] digits at end of [d] diff --git a/theories/Init/Hexadecimal.v b/theories/Init/Hexadecimal.v new file mode 100644 index 0000000000..a4ddad2875 --- /dev/null +++ b/theories/Init/Hexadecimal.v @@ -0,0 +1,245 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** * Hexadecimal numbers *) + +(** These numbers coded in base 16 will be used for parsing and printing + other Coq numeral datatypes in an human-readable way. + See the [Numeral Notation] command. + We represent numbers in base 16 as lists of hexadecimal digits, + in big-endian order (most significant digit comes first). *) + +Require Import Datatypes Specif Decimal. + +(** Unsigned integers are just lists of digits. + For instance, sixteen is (D1 (D0 Nil)) *) + +Inductive uint := + | Nil + | D0 (_:uint) + | D1 (_:uint) + | D2 (_:uint) + | D3 (_:uint) + | D4 (_:uint) + | D5 (_:uint) + | D6 (_:uint) + | D7 (_:uint) + | D8 (_:uint) + | D9 (_:uint) + | Da (_:uint) + | Db (_:uint) + | Dc (_:uint) + | Dd (_:uint) + | De (_:uint) + | Df (_:uint). + +(** [Nil] is the number terminator. Taken alone, it behaves as zero, + but rather use [D0 Nil] instead, since this form will be denoted + as [0], while [Nil] will be printed as [Nil]. *) + +Notation zero := (D0 Nil). + +(** For signed integers, we use two constructors [Pos] and [Neg]. *) + +Variant int := Pos (d:uint) | Neg (d:uint). + +(** For decimal numbers, we use two constructors [Hexadecimal] and + [HexadecimalExp], depending on whether or not they are given with an + exponent (e.g., 0x1.a2p+01). [i] is the integral part while [f] is + the fractional part (beware that leading zeroes do matter). *) + +Variant hexadecimal := + | Hexadecimal (i:int) (f:uint) + | HexadecimalExp (i:int) (f:uint) (e:Decimal.int). + +Scheme Equality for uint. +Scheme Equality for int. +Scheme Equality for hexadecimal. + +Declare Scope hex_uint_scope. +Delimit Scope hex_uint_scope with huint. +Bind Scope hex_uint_scope with uint. + +Declare Scope hex_int_scope. +Delimit Scope hex_int_scope with hint. +Bind Scope hex_int_scope with int. + +Register uint as num.hexadecimal_uint.type. +Register int as num.hexadecimal_int.type. +Register hexadecimal as num.hexadecimal.type. + +Fixpoint nb_digits d := + match d with + | Nil => O + | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d + | Da d | Db d | Dc d | Dd d | De d | Df d => + S (nb_digits d) + end. + +(** This representation favors simplicity over canonicity. + For normalizing numbers, we need to remove head zero digits, + and choose our canonical representation of 0 (here [D0 Nil] + for unsigned numbers and [Pos (D0 Nil)] for signed numbers). *) + +(** [nzhead] removes all head zero digits *) + +Fixpoint nzhead d := + match d with + | D0 d => nzhead d + | _ => d + end. + +(** [unorm] : normalization of unsigned integers *) + +Definition unorm d := + match nzhead d with + | Nil => zero + | d => d + end. + +(** [norm] : normalization of signed integers *) + +Definition norm d := + match d with + | Pos d => Pos (unorm d) + | Neg d => + match nzhead d with + | Nil => Pos zero + | d => Neg d + end + end. + +(** A few easy operations. For more advanced computations, use the conversions + with other Coq numeral datatypes (e.g. Z) and the operations on them. *) + +Definition opp (d:int) := + match d with + | Pos d => Neg d + | Neg d => Pos d + end. + +(** For conversions with binary numbers, it is easier to operate + on little-endian numbers. *) + +Fixpoint revapp (d d' : uint) := + match d with + | Nil => d' + | D0 d => revapp d (D0 d') + | D1 d => revapp d (D1 d') + | D2 d => revapp d (D2 d') + | D3 d => revapp d (D3 d') + | D4 d => revapp d (D4 d') + | D5 d => revapp d (D5 d') + | D6 d => revapp d (D6 d') + | D7 d => revapp d (D7 d') + | D8 d => revapp d (D8 d') + | D9 d => revapp d (D9 d') + | Da d => revapp d (Da d') + | Db d => revapp d (Db d') + | Dc d => revapp d (Dc d') + | Dd d => revapp d (Dd d') + | De d => revapp d (De d') + | Df d => revapp d (Df d') + end. + +Definition rev d := revapp d Nil. + +Definition app d d' := revapp (rev d) d'. + +Definition app_int d1 d2 := + match d1 with Pos d1 => Pos (app d1 d2) | Neg d1 => Neg (app d1 d2) end. + +(** [nztail] removes all trailing zero digits and return both the + result and the number of removed digits. *) + +Definition nztail d := + let fix aux d_rev := + match d_rev with + | D0 d_rev => let (r, n) := aux d_rev in pair r (S n) + | _ => pair d_rev O + end in + let (r, n) := aux (rev d) in pair (rev r) n. + +Definition nztail_int d := + match d with + | Pos d => let (r, n) := nztail d in pair (Pos r) n + | Neg d => let (r, n) := nztail d in pair (Neg r) n + end. + +Module Little. + +(** Successor of little-endian numbers *) + +Fixpoint succ d := + match d with + | Nil => D1 Nil + | D0 d => D1 d + | D1 d => D2 d + | D2 d => D3 d + | D3 d => D4 d + | D4 d => D5 d + | D5 d => D6 d + | D6 d => D7 d + | D7 d => D8 d + | D8 d => D9 d + | D9 d => Da d + | Da d => Db d + | Db d => Dc d + | Dc d => Dd d + | Dd d => De d + | De d => Df d + | Df d => D0 (succ d) + end. + +(** Doubling little-endian numbers *) + +Fixpoint double d := + match d with + | Nil => Nil + | D0 d => D0 (double d) + | D1 d => D2 (double d) + | D2 d => D4 (double d) + | D3 d => D6 (double d) + | D4 d => D8 (double d) + | D5 d => Da (double d) + | D6 d => Dc (double d) + | D7 d => De (double d) + | D8 d => D0 (succ_double d) + | D9 d => D2 (succ_double d) + | Da d => D4 (succ_double d) + | Db d => D6 (succ_double d) + | Dc d => D8 (succ_double d) + | Dd d => Da (succ_double d) + | De d => Dc (succ_double d) + | Df d => De (succ_double d) + end + +with succ_double d := + match d with + | Nil => D1 Nil + | D0 d => D1 (double d) + | D1 d => D3 (double d) + | D2 d => D5 (double d) + | D3 d => D7 (double d) + | D4 d => D9 (double d) + | D5 d => Db (double d) + | D6 d => Dd (double d) + | D7 d => Df (double d) + | D8 d => D1 (succ_double d) + | D9 d => D3 (succ_double d) + | Da d => D5 (succ_double d) + | Db d => D7 (succ_double d) + | Dc d => D9 (succ_double d) + | Dd d => Db (succ_double d) + | De d => Dd (succ_double d) + | Df d => Df (succ_double d) + end. + +End Little. diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v index bfd41c5017..7c8cf0b536 100644 --- a/theories/Init/Nat.v +++ b/theories/Init/Nat.v @@ -9,7 +9,7 @@ (************************************************************************) Require Import Notations Logic Datatypes. -Require Decimal. +Require Decimal Hexadecimal Numeral. Local Open Scope nat_scope. (**********************************************************************) @@ -187,6 +187,37 @@ Fixpoint of_uint_acc (d:Decimal.uint)(acc:nat) := Definition of_uint (d:Decimal.uint) := of_uint_acc d O. +Local Notation sixteen := (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))). + +Fixpoint of_hex_uint_acc (d:Hexadecimal.uint)(acc:nat) := + match d with + | Hexadecimal.Nil => acc + | Hexadecimal.D0 d => of_hex_uint_acc d (tail_mul sixteen acc) + | Hexadecimal.D1 d => of_hex_uint_acc d (S (tail_mul sixteen acc)) + | Hexadecimal.D2 d => of_hex_uint_acc d (S (S (tail_mul sixteen acc))) + | Hexadecimal.D3 d => of_hex_uint_acc d (S (S (S (tail_mul sixteen acc)))) + | Hexadecimal.D4 d => of_hex_uint_acc d (S (S (S (S (tail_mul sixteen acc))))) + | Hexadecimal.D5 d => of_hex_uint_acc d (S (S (S (S (S (tail_mul sixteen acc)))))) + | Hexadecimal.D6 d => of_hex_uint_acc d (S (S (S (S (S (S (tail_mul sixteen acc))))))) + | Hexadecimal.D7 d => of_hex_uint_acc d (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))) + | Hexadecimal.D8 d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))) + | Hexadecimal.D9 d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))) + | Hexadecimal.Da d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))) + | Hexadecimal.Db d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))))) + | Hexadecimal.Dc d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))))) + | Hexadecimal.Dd d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))))))) + | Hexadecimal.De d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))))))) + | Hexadecimal.Df d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))))))))) + end. + +Definition of_hex_uint (d:Hexadecimal.uint) := of_hex_uint_acc d O. + +Definition of_num_uint (d:Numeral.uint) := + match d with + | Numeral.UIntDec d => of_uint d + | Numeral.UIntHex d => of_hex_uint d + end. + Fixpoint to_little_uint n acc := match n with | O => acc @@ -196,14 +227,43 @@ Fixpoint to_little_uint n acc := Definition to_uint n := Decimal.rev (to_little_uint n Decimal.zero). +Fixpoint to_little_hex_uint n acc := + match n with + | O => acc + | S n => to_little_hex_uint n (Hexadecimal.Little.succ acc) + end. + +Definition to_hex_uint n := + Hexadecimal.rev (to_little_hex_uint n Hexadecimal.zero). + +Definition to_num_uint n := Numeral.UIntDec (to_uint n). + +Definition to_num_hex_uint n := Numeral.UIntHex (to_hex_uint n). + Definition of_int (d:Decimal.int) : option nat := match Decimal.norm d with | Decimal.Pos u => Some (of_uint u) | _ => None end. +Definition of_hex_int (d:Hexadecimal.int) : option nat := + match Hexadecimal.norm d with + | Hexadecimal.Pos u => Some (of_hex_uint u) + | _ => None + end. + +Definition of_num_int (d:Numeral.int) : option nat := + match d with + | Numeral.IntDec d => of_int d + | Numeral.IntHex d => of_hex_int d + end. + Definition to_int n := Decimal.Pos (to_uint n). +Definition to_hex_int n := Hexadecimal.Pos (to_hex_uint n). + +Definition to_num_int n := Numeral.IntDec (to_int n). + (** ** Euclidean division *) (** This division is linear and tail-recursive. diff --git a/theories/Init/Numeral.v b/theories/Init/Numeral.v new file mode 100644 index 0000000000..8a0531e004 --- /dev/null +++ b/theories/Init/Numeral.v @@ -0,0 +1,33 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** * Decimal or Hexadecimal numbers *) + +Require Import Decimal Hexadecimal. + +Variant uint := UIntDec (u:Decimal.uint) | UIntHex (u:Hexadecimal.uint). + +Variant int := IntDec (i:Decimal.int) | IntHex (i:Hexadecimal.int). + +Variant numeral := Dec (d:Decimal.decimal) | Hex (h:Hexadecimal.hexadecimal). + +Scheme Equality for uint. +Scheme Equality for int. +Scheme Equality for numeral. + +Register uint as num.num_uint.type. +Register int as num.num_int.type. +Register numeral as num.numeral.type. + +(** Pseudo-conversion functions used when declaring + Numeral Notations on [uint] and [int]. *) + +Definition uint_of_uint (i:uint) := i. +Definition int_of_int (i:int) := i. diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 6a81517d7e..8f862e8cec 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -15,6 +15,8 @@ Require Export Datatypes. Require Export Specif. Require Coq.Init.Byte. Require Coq.Init.Decimal. +Require Coq.Init.Hexadecimal. +Require Coq.Init.Numeral. Require Coq.Init.Nat. Require Export Peano. Require Export Coq.Init.Wf. @@ -30,16 +32,25 @@ Declare ML Module "ground_plugin". Declare ML Module "numeral_notation_plugin". Declare ML Module "string_notation_plugin". +(* Parsing / printing of hexadecimal numbers *) +Arguments Nat.of_hex_uint d%hex_uint_scope. +Arguments Nat.of_hex_int d%hex_int_scope. +Numeral Notation Numeral.uint Numeral.uint_of_uint Numeral.uint_of_uint + : hex_uint_scope. +Numeral Notation Numeral.int Numeral.int_of_int Numeral.int_of_int + : hex_int_scope. + (* Parsing / printing of decimal numbers *) Arguments Nat.of_uint d%dec_uint_scope. Arguments Nat.of_int d%dec_int_scope. -Numeral Notation Decimal.uint Decimal.uint_of_uint Decimal.uint_of_uint +Numeral Notation Numeral.uint Numeral.uint_of_uint Numeral.uint_of_uint : dec_uint_scope. -Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int +Numeral Notation Numeral.int Numeral.int_of_int Numeral.int_of_int : dec_int_scope. (* Parsing / printing of [nat] numbers *) -Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5001). +Numeral Notation nat Nat.of_num_uint Nat.to_num_hex_uint : hex_nat_scope (abstract after 5001). +Numeral Notation nat Nat.of_num_uint Nat.to_num_uint : nat_scope (abstract after 5001). (* Printing/Parsing of bytes *) Export Byte.ByteSyntaxNotations. diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index d68c32b371..1881e387a2 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -1007,7 +1007,7 @@ Bind Scope N_scope with N.t N. (** Exportation of notations *) -Numeral Notation N N.of_uint N.to_uint : N_scope. +Numeral Notation N N.of_num_uint N.to_num_uint : N_scope. Infix "+" := N.add : N_scope. Infix "-" := N.sub : N_scope. diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index 04685cc3eb..8a0aee9cf4 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -388,23 +388,55 @@ Definition iter (n:N) {A} (f:A->A) (x:A) : A := Definition of_uint (d:Decimal.uint) := Pos.of_uint d. +Definition of_hex_uint (d:Hexadecimal.uint) := Pos.of_hex_uint d. + +Definition of_num_uint (d:Numeral.uint) := + match d with + | Numeral.UIntDec d => of_uint d + | Numeral.UIntHex d => of_hex_uint d + end. + Definition of_int (d:Decimal.int) := match Decimal.norm d with | Decimal.Pos d => Some (Pos.of_uint d) | Decimal.Neg _ => None end. +Definition of_hex_int (d:Hexadecimal.int) := + match Hexadecimal.norm d with + | Hexadecimal.Pos d => Some (Pos.of_hex_uint d) + | Hexadecimal.Neg _ => None + end. + +Definition of_num_int (d:Numeral.int) := + match d with + | Numeral.IntDec d => of_int d + | Numeral.IntHex d => of_hex_int d + end. + Definition to_uint n := match n with | 0 => Decimal.zero | pos p => Pos.to_uint p end. +Definition to_hex_uint n := + match n with + | 0 => Hexadecimal.zero + | pos p => Pos.to_hex_uint p + end. + +Definition to_num_uint n := Numeral.UIntDec (to_uint n). + Definition to_int n := Decimal.Pos (to_uint n). -Numeral Notation N of_uint to_uint : N_scope. +Definition to_hex_int n := Hexadecimal.Pos (to_hex_uint n). + +Definition to_num_int n := Numeral.IntDec (to_int n). + +Numeral Notation N of_num_uint to_num_uint : N_scope. End N. (** Re-export the notation for those who just [Import NatIntDef] *) -Numeral Notation N N.of_uint N.to_uint : N_scope. +Numeral Notation N N.of_num_uint N.to_num_uint : N_scope. diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v index a074ec6d2a..5585f478b3 100644 --- a/theories/Numbers/AltBinNotations.v +++ b/theories/Numbers/AltBinNotations.v @@ -55,10 +55,10 @@ Definition n_of_z z := end. Definition n_to_z n := - match n with - | N0 => Z0 - | Npos p => Zpos p - end. + match n with + | N0 => Z0 + | Npos p => Zpos p + end. Numeral Notation N n_of_z n_to_z : N_scope. diff --git a/theories/Numbers/DecimalFacts.v b/theories/Numbers/DecimalFacts.v index a3bdcc579f..dd361562ba 100644 --- a/theories/Numbers/DecimalFacts.v +++ b/theories/Numbers/DecimalFacts.v @@ -10,134 +10,450 @@ (** * DecimalFacts : some facts about Decimal numbers *) -Require Import Decimal. +Require Import Decimal Arith. Lemma uint_dec (d d' : uint) : { d = d' } + { d <> d' }. Proof. - decide equality. + decide equality. Defined. Lemma rev_revapp d d' : - rev (revapp d d') = revapp d' d. + rev (revapp d d') = revapp d' d. Proof. - revert d'. induction d; simpl; intros; now rewrite ?IHd. + revert d'. induction d; simpl; intros; now rewrite ?IHd. Qed. Lemma rev_rev d : rev (rev d) = d. Proof. - apply rev_revapp. + apply rev_revapp. Qed. +Lemma revapp_rev_nil d : revapp (rev d) Nil = d. +Proof. now fold (rev (rev d)); rewrite rev_rev. Qed. + +Lemma app_nil_r d : app d Nil = d. +Proof. now unfold app; rewrite revapp_rev_nil. Qed. + +Lemma app_int_nil_r d : app_int d Nil = d. +Proof. now case d; intro d'; simpl; rewrite app_nil_r. Qed. + +Lemma revapp_revapp_1 d d' d'' : + nb_digits d <= 1 -> + revapp (revapp d d') d'' = revapp d' (revapp d d''). +Proof. + now case d; clear d; intro d; + [|case d; clear d; intro d; + [|simpl; case nb_digits; [|intros n]; intros Hn; exfalso; + [apply (Nat.nle_succ_diag_l _ Hn)| + apply (Nat.nle_succ_0 _ (le_S_n _ _ Hn))]..]..]. +Qed. + +Lemma nb_digits_pos d : d <> Nil -> 0 < nb_digits d. +Proof. now case d; [|intros d' _; apply Nat.lt_0_succ..]. Qed. + +Lemma nb_digits_revapp d d' : + nb_digits (revapp d d') = nb_digits d + nb_digits d'. +Proof. + now revert d'; induction d; [|intro d'; simpl; rewrite IHd; simpl..]. +Qed. + +Lemma nb_digits_rev u : nb_digits (rev u) = nb_digits u. +Proof. now unfold rev; rewrite nb_digits_revapp. Qed. + +Lemma nb_digits_nzhead u : nb_digits (nzhead u) <= nb_digits u. +Proof. now induction u; [|apply le_S|..]. Qed. + +Lemma del_head_nb_digits (u:uint) : del_head (nb_digits u) u = Nil. +Proof. now induction u. Qed. + +Lemma nb_digits_del_head n u : + n <= nb_digits u -> nb_digits (del_head n u) = nb_digits u - n. +Proof. + revert u; induction n; intros u; [now rewrite Nat.sub_0_r|]. + now case u; clear u; intro u; [|intro Hn; apply IHn, le_S_n..]. +Qed. + +Lemma nb_digits_iter_D0 n d : + nb_digits (Nat.iter n D0 d) = n + nb_digits d. +Proof. now induction n; simpl; [|rewrite IHn]. Qed. + +Fixpoint nth n u := + match n with + | O => + match u with + | Nil => Nil + | D0 d => D0 Nil + | D1 d => D1 Nil + | D2 d => D2 Nil + | D3 d => D3 Nil + | D4 d => D4 Nil + | D5 d => D5 Nil + | D6 d => D6 Nil + | D7 d => D7 Nil + | D8 d => D8 Nil + | D9 d => D9 Nil + end + | S n => + match u with + | Nil => Nil + | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d => + nth n d + end + end. + +Lemma nb_digits_nth n u : nb_digits (nth n u) <= 1. +Proof. + revert u; induction n. + - now intro u; case u; [apply Nat.le_0_1|..]. + - intro u; case u; [apply Nat.le_0_1|intro u'; apply IHn..]. +Qed. + +Lemma del_head_nth n u : + n < nb_digits u -> + del_head n u = revapp (nth n u) (del_head (S n) u). +Proof. + revert u; induction n; intro u; [now case u|]. + now case u; [|intro u'; intro H; apply IHn, le_S_n..]. +Qed. + +Lemma nth_revapp_r n d d' : + nb_digits d <= n -> + nth n (revapp d d') = nth (n - nb_digits d) d'. +Proof. + revert d d'; induction n; intro d. + - now case d; intro d'; + [case d'|intros d'' H; exfalso; revert H; apply Nat.nle_succ_0..]. + - now induction d; + [intro d'; case d'| + intros d' H; + simpl revapp; rewrite IHd; [|now apply le_Sn_le]; + rewrite Nat.sub_succ_l; [|now apply le_S_n]; + simpl; rewrite <-(IHn _ _ (le_S_n _ _ H))..]. +Qed. + +Lemma nth_revapp_l n d d' : + n < nb_digits d -> + nth n (revapp d d') = nth (nb_digits d - n - 1) d. +Proof. + revert d d'; induction n; intro d. + - rewrite Nat.sub_0_r. + now induction d; + [|intros d' _; simpl revapp; + revert IHd; case d; clear d; [|intro d..]; intro IHd; + [|rewrite IHd; [simpl nb_digits; rewrite (Nat.sub_succ_l _ (S _))|]; + [|apply le_n_S, Nat.le_0_l..]..]..]. + - now induction d; + [|intros d' H; + simpl revapp; simpl nb_digits; + simpl in H; generalize (lt_S_n _ _ H); clear H; intro H; + case (le_lt_eq_dec _ _ H); clear H; intro H; + [rewrite (IHd _ H), Nat.sub_succ_l; + [rewrite Nat.sub_succ_l; [|apply Nat.le_add_le_sub_r]| + apply le_Sn_le]| + rewrite nth_revapp_r; rewrite <-H; + [rewrite Nat.sub_succ, Nat.sub_succ_l; [rewrite !Nat.sub_diag|]|]]..]. +Qed. + +Lemma app_del_tail_head (u:uint) n : + n <= nb_digits u -> + app (del_tail n u) (del_head (nb_digits u - n) u) = u. +Proof. + unfold app, del_tail; rewrite rev_rev. + induction n. + - intros _; rewrite Nat.sub_0_r, del_head_nb_digits; simpl. + now rewrite revapp_rev_nil. + - intro Hn. + rewrite (del_head_nth (_ - _)); + [|now apply Nat.sub_lt; [|apply Nat.lt_0_succ]]. + rewrite Nat.sub_succ_r, <-Nat.sub_1_r. + rewrite <-(nth_revapp_l _ _ Nil Hn); fold (rev u). + rewrite <-revapp_revapp_1; [|now apply nb_digits_nth]. + rewrite <-(del_head_nth _ _); [|now rewrite nb_digits_rev]. + rewrite Nat.sub_1_r, Nat.succ_pred_pos; [|now apply Nat.lt_add_lt_sub_r]. + apply (IHn (le_Sn_le _ _ Hn)). +Qed. + +Lemma app_int_del_tail_head n (d:int) : + let ad := match d with Pos d | Neg d => d end in + n <= nb_digits ad -> + app_int (del_tail_int n d) (del_head (nb_digits ad - n) ad) = d. +Proof. now case d; clear d; simpl; intros u Hu; rewrite app_del_tail_head. Qed. + (** Normalization on little-endian numbers *) Fixpoint nztail d := - match d with - | Nil => Nil - | D0 d => match nztail d with Nil => Nil | d' => D0 d' end - | D1 d => D1 (nztail d) - | D2 d => D2 (nztail d) - | D3 d => D3 (nztail d) - | D4 d => D4 (nztail d) - | D5 d => D5 (nztail d) - | D6 d => D6 (nztail d) - | D7 d => D7 (nztail d) - | D8 d => D8 (nztail d) - | D9 d => D9 (nztail d) - end. + match d with + | Nil => Nil + | D0 d => match nztail d with Nil => Nil | d' => D0 d' end + | D1 d => D1 (nztail d) + | D2 d => D2 (nztail d) + | D3 d => D3 (nztail d) + | D4 d => D4 (nztail d) + | D5 d => D5 (nztail d) + | D6 d => D6 (nztail d) + | D7 d => D7 (nztail d) + | D8 d => D8 (nztail d) + | D9 d => D9 (nztail d) + end. Definition lnorm d := - match nztail d with - | Nil => zero - | d => d - end. + match nztail d with + | Nil => zero + | d => d + end. Lemma nzhead_revapp_0 d d' : nztail d = Nil -> - nzhead (revapp d d') = nzhead d'. + nzhead (revapp d d') = nzhead d'. Proof. - revert d'. induction d; intros d' [=]; simpl; trivial. - destruct (nztail d); now rewrite IHd. + revert d'. induction d; intros d' [=]; simpl; trivial. + destruct (nztail d); now rewrite IHd. Qed. Lemma nzhead_revapp d d' : nztail d <> Nil -> - nzhead (revapp d d') = revapp (nztail d) d'. + nzhead (revapp d d') = revapp (nztail d) d'. Proof. - revert d'. - induction d; intros d' H; simpl in *; - try destruct (nztail d) eqn:E; + revert d'. + induction d; intros d' H; simpl in *; + try destruct (nztail d) eqn:E; (now rewrite ?nzhead_revapp_0) || (now rewrite IHd). Qed. Lemma nzhead_rev d : nztail d <> Nil -> - nzhead (rev d) = rev (nztail d). + nzhead (rev d) = rev (nztail d). Proof. - apply nzhead_revapp. + apply nzhead_revapp. Qed. Lemma rev_nztail_rev d : rev (nztail (rev d)) = nzhead d. Proof. - destruct (uint_dec (nztail (rev d)) Nil) as [H|H]. - - rewrite H. unfold rev; simpl. - rewrite <- (rev_rev d). symmetry. - now apply nzhead_revapp_0. - - now rewrite <- nzhead_rev, rev_rev. + destruct (uint_dec (nztail (rev d)) Nil) as [H|H]. + - rewrite H. unfold rev; simpl. + rewrite <- (rev_rev d). symmetry. + now apply nzhead_revapp_0. + - now rewrite <- nzhead_rev, rev_rev. Qed. +Lemma nzhead_D0 u : nzhead (D0 u) = nzhead u. +Proof. reflexivity. Qed. + +Lemma nzhead_iter_D0 n u : nzhead (Nat.iter n D0 u) = nzhead u. +Proof. now induction n. Qed. + Lemma revapp_nil_inv d d' : revapp d d' = Nil -> d = Nil /\ d' = Nil. Proof. - revert d'. - induction d; simpl; intros d' H; auto; now apply IHd in H. + revert d'. + induction d; simpl; intros d' H; auto; now apply IHd in H. Qed. Lemma rev_nil_inv d : rev d = Nil -> d = Nil. Proof. - apply revapp_nil_inv. + apply revapp_nil_inv. Qed. Lemma rev_lnorm_rev d : rev (lnorm (rev d)) = unorm d. Proof. - unfold unorm, lnorm. - rewrite <- rev_nztail_rev. - destruct nztail; simpl; trivial; - destruct rev eqn:E; trivial; now apply rev_nil_inv in E. + unfold unorm, lnorm. + rewrite <- rev_nztail_rev. + destruct nztail; simpl; trivial; + destruct rev eqn:E; trivial; now apply rev_nil_inv in E. Qed. Lemma nzhead_nonzero d d' : nzhead d <> D0 d'. Proof. - induction d; easy. + induction d; easy. Qed. Lemma unorm_0 d : unorm d = zero <-> nzhead d = Nil. Proof. - unfold unorm. split. - - generalize (nzhead_nonzero d). - destruct nzhead; intros H [=]; trivial. now destruct (H u). - - now intros ->. + unfold unorm. split. + - generalize (nzhead_nonzero d). + destruct nzhead; intros H [=]; trivial. now destruct (H u). + - now intros ->. Qed. Lemma unorm_nonnil d : unorm d <> Nil. Proof. - unfold unorm. now destruct nzhead. + unfold unorm. now destruct nzhead. +Qed. + +Lemma unorm_D0 u : unorm (D0 u) = unorm u. +Proof. reflexivity. Qed. + +Lemma unorm_iter_D0 n u : unorm (Nat.iter n D0 u) = unorm u. +Proof. now induction n. Qed. + +Lemma nb_digits_unorm u : + u <> Nil -> nb_digits (unorm u) <= nb_digits u. +Proof. + case u; clear u; [now simpl|intro u..]; [|now simpl..]. + intros _; unfold unorm. + case_eq (nzhead (D0 u)); [|now intros u' <-; apply nb_digits_nzhead..]. + intros _; apply le_n_S, Nat.le_0_l. +Qed. + +Lemma del_head_nonnil n u : + n < nb_digits u -> del_head n u <> Nil. +Proof. + now revert n; induction u; intro n; + [|case n; [|intro n'; simpl; intro H; apply IHu, lt_S_n]..]. +Qed. + +Lemma del_tail_nonnil n u : + n < nb_digits u -> del_tail n u <> Nil. +Proof. + unfold del_tail. + rewrite <-nb_digits_rev. + generalize (rev u); clear u; intro u. + intros Hu H. + generalize (rev_nil_inv _ H); clear H. + now apply del_head_nonnil. Qed. Lemma nzhead_invol d : nzhead (nzhead d) = nzhead d. Proof. - now induction d. + now induction d. +Qed. + +Lemma nztail_invol d : nztail (nztail d) = nztail d. +Proof. + rewrite <-(rev_rev (nztail _)), <-(rev_rev (nztail d)), <-(rev_rev d). + now rewrite !rev_nztail_rev, nzhead_invol. Qed. Lemma unorm_invol d : unorm (unorm d) = unorm d. Proof. - unfold unorm. - destruct (nzhead d) eqn:E; trivial. - destruct (nzhead_nonzero _ _ E). + unfold unorm. + destruct (nzhead d) eqn:E; trivial. + destruct (nzhead_nonzero _ _ E). Qed. Lemma norm_invol d : norm (norm d) = norm d. Proof. - unfold norm. - destruct d. - - f_equal. apply unorm_invol. - - destruct (nzhead d) eqn:E; auto. - destruct (nzhead_nonzero _ _ E). + unfold norm. + destruct d. + - f_equal. apply unorm_invol. + - destruct (nzhead d) eqn:E; auto. + destruct (nzhead_nonzero _ _ E). +Qed. + +Lemma nzhead_del_tail_nzhead_eq n u : + nzhead u = u -> + n < nb_digits u -> + nzhead (del_tail n u) = del_tail n u. +Proof. + intros Hu Hn. + assert (Hhd : forall u, + nzhead u = u <-> match nth 0 u with D0 _ => False | _ => True end). + { clear n u Hu Hn; intro u. + case u; clear u; [|intro u..]; [now simpl| |now simpl..]; simpl. + split; [|now simpl]. + apply nzhead_nonzero. } + assert (Hhd' : nth 0 (del_tail n u) = nth 0 u). + { rewrite <-(app_del_tail_head _ _ (le_Sn_le _ _ Hn)) at 2. + unfold app. + rewrite nth_revapp_l. + - rewrite <-(nth_revapp_l _ _ Nil). + + now fold (rev (rev (del_tail n u))); rewrite rev_rev. + + unfold del_tail; rewrite rev_rev. + rewrite nb_digits_del_head; rewrite nb_digits_rev. + * now rewrite <-Nat.lt_add_lt_sub_r. + * now apply Nat.lt_le_incl. + - unfold del_tail; rewrite rev_rev. + rewrite nb_digits_del_head; rewrite nb_digits_rev. + + now rewrite <-Nat.lt_add_lt_sub_r. + + now apply Nat.lt_le_incl. } + revert Hu; rewrite Hhd; intro Hu. + now rewrite Hhd, Hhd'. +Qed. + +Lemma nzhead_del_tail_nzhead n u : + n < nb_digits (nzhead u) -> + nzhead (del_tail n (nzhead u)) = del_tail n (nzhead u). +Proof. apply nzhead_del_tail_nzhead_eq, nzhead_invol. Qed. + +Lemma unorm_del_tail_unorm n u : + n < nb_digits (unorm u) -> + unorm (del_tail n (unorm u)) = del_tail n (unorm u). +Proof. + case (uint_dec (nzhead u) Nil). + - unfold unorm; intros->; case n; [now simpl|]; intro n'. + now simpl; intro H; exfalso; generalize (lt_S_n _ _ H). + - unfold unorm. + set (m := match nzhead u with Nil => zero | _ => _ end). + intros H. + replace m with (nzhead u). + + intros H'. + rewrite (nzhead_del_tail_nzhead _ _ H'). + now generalize (del_tail_nonnil _ _ H'); case del_tail. + + now unfold m; revert H; case nzhead. +Qed. + +Lemma norm_del_tail_int_norm n d : + n < nb_digits (match norm d with Pos d | Neg d => d end) -> + norm (del_tail_int n (norm d)) = del_tail_int n (norm d). +Proof. + case d; clear d; intros u; simpl. + - now intro H; simpl; rewrite unorm_del_tail_unorm. + - case (uint_dec (nzhead u) Nil); intro Hu. + + now rewrite Hu; case n; [|intros n' Hn'; generalize (lt_S_n _ _ Hn')]. + + set (m := match nzhead u with Nil => Pos zero | _ => _ end). + replace m with (Neg (nzhead u)); [|now unfold m; revert Hu; case nzhead]. + unfold del_tail_int. + clear m Hu. + simpl. + intro H; generalize (del_tail_nonnil _ _ H). + rewrite (nzhead_del_tail_nzhead _ _ H). + now case del_tail. +Qed. + +Lemma nzhead_app_nzhead d d' : + nzhead (app (nzhead d) d') = nzhead (app d d'). +Proof. + unfold app. + rewrite <-(rev_nztail_rev d), rev_rev. + generalize (rev d); clear d; intro d. + generalize (nzhead_revapp_0 d d'). + generalize (nzhead_revapp d d'). + generalize (nzhead_revapp_0 (nztail d) d'). + generalize (nzhead_revapp (nztail d) d'). + rewrite nztail_invol. + now case nztail; + [intros _ H _ H'; rewrite (H eq_refl), (H' eq_refl) + |intros d'' H _ H' _; rewrite H; [rewrite H'|]..]. +Qed. + +Lemma unorm_app_unorm d d' : + unorm (app (unorm d) d') = unorm (app d d'). +Proof. + unfold unorm. + rewrite <-(nzhead_app_nzhead d d'). + now case (nzhead d). +Qed. + +Lemma norm_app_int_norm d d' : + unorm d' = zero -> + norm (app_int (norm d) d') = norm (app_int d d'). +Proof. + case d; clear d; intro d; simpl. + - now rewrite unorm_app_unorm. + - unfold app_int, app. + rewrite unorm_0; intro Hd'. + rewrite <-rev_nztail_rev. + generalize (nzhead_revapp (rev d) d'). + generalize (nzhead_revapp_0 (rev d) d'). + now case_eq (nztail (rev d)); + [intros Hd'' H _; rewrite (H eq_refl); simpl; + unfold unorm; simpl; rewrite Hd' + |intros d'' Hd'' _ H; rewrite H; clear H; [|now simpl]; + set (r := rev _); + set (m := match r with Nil => Pos zero | _ => _ end); + assert (H' : m = Neg r); + [now unfold m; case_eq r; unfold r; + [intro H''; generalize (rev_nil_inv _ H'')|..] + |rewrite H'; unfold r; clear m r H']; + unfold norm; + rewrite rev_rev, <-Hd''; + rewrite nzhead_revapp; rewrite nztail_invol; [|rewrite Hd'']..]. Qed. diff --git a/theories/Numbers/DecimalN.v b/theories/Numbers/DecimalN.v index ac6d9c663f..8bc5c38fb5 100644 --- a/theories/Numbers/DecimalN.v +++ b/theories/Numbers/DecimalN.v @@ -19,41 +19,41 @@ Module Unsigned. Lemma of_to (n:N) : N.of_uint (N.to_uint n) = n. Proof. - destruct n. - - reflexivity. - - apply DecimalPos.Unsigned.of_to. + destruct n. + - reflexivity. + - apply DecimalPos.Unsigned.of_to. Qed. Lemma to_of (d:uint) : N.to_uint (N.of_uint d) = unorm d. Proof. - exact (DecimalPos.Unsigned.to_of d). + exact (DecimalPos.Unsigned.to_of d). Qed. Lemma to_uint_inj n n' : N.to_uint n = N.to_uint n' -> n = n'. Proof. - intros E. now rewrite <- (of_to n), <- (of_to n'), E. + intros E. now rewrite <- (of_to n), <- (of_to n'), E. Qed. Lemma to_uint_surj d : exists p, N.to_uint p = unorm d. Proof. - exists (N.of_uint d). apply to_of. + exists (N.of_uint d). apply to_of. Qed. Lemma of_uint_norm d : N.of_uint (unorm d) = N.of_uint d. Proof. - now induction d. + now induction d. Qed. Lemma of_inj d d' : - N.of_uint d = N.of_uint d' -> unorm d = unorm d'. + N.of_uint d = N.of_uint d' -> unorm d = unorm d'. Proof. - intros. rewrite <- !to_of. now f_equal. + intros. rewrite <- !to_of. now f_equal. Qed. Lemma of_iff d d' : N.of_uint d = N.of_uint d' <-> unorm d = unorm d'. Proof. - split. apply of_inj. intros E. rewrite <- of_uint_norm, E. - apply of_uint_norm. + split. apply of_inj. intros E. rewrite <- of_uint_norm, E. + apply of_uint_norm. Qed. End Unsigned. @@ -64,44 +64,44 @@ Module Signed. Lemma of_to (n:N) : N.of_int (N.to_int n) = Some n. Proof. - unfold N.to_int, N.of_int, norm. f_equal. - rewrite Unsigned.of_uint_norm. apply Unsigned.of_to. + unfold N.to_int, N.of_int, norm. f_equal. + rewrite Unsigned.of_uint_norm. apply Unsigned.of_to. Qed. Lemma to_of (d:int)(n:N) : N.of_int d = Some n -> N.to_int n = norm d. Proof. - unfold N.of_int. - destruct (norm d) eqn:Hd; intros [= <-]. - unfold N.to_int. rewrite Unsigned.to_of. f_equal. - revert Hd; destruct d; simpl. - - intros [= <-]. apply unorm_invol. - - destruct (nzhead d); now intros [= <-]. + unfold N.of_int. + destruct (norm d) eqn:Hd; intros [= <-]. + unfold N.to_int. rewrite Unsigned.to_of. f_equal. + revert Hd; destruct d; simpl. + - intros [= <-]. apply unorm_invol. + - destruct (nzhead d); now intros [= <-]. Qed. Lemma to_int_inj n n' : N.to_int n = N.to_int n' -> n = n'. Proof. - intro E. - assert (E' : Some n = Some n'). - { now rewrite <- (of_to n), <- (of_to n'), E. } - now injection E'. + intro E. + assert (E' : Some n = Some n'). + { now rewrite <- (of_to n), <- (of_to n'), E. } + now injection E'. Qed. Lemma to_int_pos_surj d : exists n, N.to_int n = norm (Pos d). Proof. - exists (N.of_uint d). unfold N.to_int. now rewrite Unsigned.to_of. + exists (N.of_uint d). unfold N.to_int. now rewrite Unsigned.to_of. Qed. Lemma of_int_norm d : N.of_int (norm d) = N.of_int d. Proof. - unfold N.of_int. now rewrite norm_invol. + unfold N.of_int. now rewrite norm_invol. Qed. Lemma of_inj_pos d d' : N.of_int (Pos d) = N.of_int (Pos d') -> unorm d = unorm d'. Proof. - unfold N.of_int. simpl. intros [= H]. apply Unsigned.of_inj. - change Pos.of_uint with N.of_uint in H. - now rewrite <- Unsigned.of_uint_norm, H, Unsigned.of_uint_norm. + unfold N.of_int. simpl. intros [= H]. apply Unsigned.of_inj. + change Pos.of_uint with N.of_uint in H. + now rewrite <- Unsigned.of_uint_norm, H, Unsigned.of_uint_norm. Qed. End Signed. diff --git a/theories/Numbers/DecimalNat.v b/theories/Numbers/DecimalNat.v index e0ba8dc631..1962ac5d9d 100644 --- a/theories/Numbers/DecimalNat.v +++ b/theories/Numbers/DecimalNat.v @@ -20,25 +20,25 @@ Module Unsigned. (** A few helper functions used during proofs *) Definition hd d := - match d with - | Nil => 0 - | D0 _ => 0 - | D1 _ => 1 - | D2 _ => 2 - | D3 _ => 3 - | D4 _ => 4 - | D5 _ => 5 - | D6 _ => 6 - | D7 _ => 7 - | D8 _ => 8 - | D9 _ => 9 -end. + match d with + | Nil => 0 + | D0 _ => 0 + | D1 _ => 1 + | D2 _ => 2 + | D3 _ => 3 + | D4 _ => 4 + | D5 _ => 5 + | D6 _ => 6 + | D7 _ => 7 + | D8 _ => 8 + | D9 _ => 9 + end. Definition tl d := - match d with - | Nil => d - | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d => d -end. + match d with + | Nil => d + | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d => d + end. Fixpoint usize (d:uint) : nat := match d with @@ -57,10 +57,10 @@ Fixpoint usize (d:uint) : nat := (** A direct version of [to_little_uint], not tail-recursive *) Fixpoint to_lu n := - match n with - | 0 => Decimal.zero - | S n => Little.succ (to_lu n) - end. + match n with + | 0 => Decimal.zero + | S n => Little.succ (to_lu n) + end. (** A direct version of [of_little_uint] *) Fixpoint of_lu (d:uint) : nat := @@ -82,174 +82,174 @@ Fixpoint of_lu (d:uint) : nat := Lemma to_lu_succ n : to_lu (S n) = Little.succ (to_lu n). Proof. - reflexivity. + reflexivity. Qed. Lemma to_little_uint_succ n d : - Nat.to_little_uint n (Little.succ d) = - Little.succ (Nat.to_little_uint n d). + Nat.to_little_uint n (Little.succ d) = + Little.succ (Nat.to_little_uint n d). Proof. - revert d; induction n; simpl; trivial. + revert d; induction n; simpl; trivial. Qed. Lemma to_lu_equiv n : to_lu n = Nat.to_little_uint n zero. Proof. - induction n; simpl; trivial. - now rewrite IHn, <- to_little_uint_succ. + induction n; simpl; trivial. + now rewrite IHn, <- to_little_uint_succ. Qed. Lemma to_uint_alt n : - Nat.to_uint n = rev (to_lu n). + Nat.to_uint n = rev (to_lu n). Proof. - unfold Nat.to_uint. f_equal. symmetry. apply to_lu_equiv. + unfold Nat.to_uint. f_equal. symmetry. apply to_lu_equiv. Qed. (** Properties of [of_lu] *) Lemma of_lu_eqn d : - of_lu d = hd d + 10 * of_lu (tl d). + of_lu d = hd d + 10 * of_lu (tl d). Proof. - induction d; simpl; trivial. + induction d; simpl; trivial. Qed. Ltac simpl_of_lu := - match goal with - | |- context [ of_lu (?f ?x) ] => - rewrite (of_lu_eqn (f x)); simpl hd; simpl tl - end. + match goal with + | |- context [ of_lu (?f ?x) ] => + rewrite (of_lu_eqn (f x)); simpl hd; simpl tl + end. Lemma of_lu_succ d : - of_lu (Little.succ d) = S (of_lu d). + of_lu (Little.succ d) = S (of_lu d). Proof. - induction d; trivial. - simpl_of_lu. rewrite IHd. simpl_of_lu. - now rewrite Nat.mul_succ_r, <- (Nat.add_comm 10). + induction d; trivial. + simpl_of_lu. rewrite IHd. simpl_of_lu. + now rewrite Nat.mul_succ_r, <- (Nat.add_comm 10). Qed. Lemma of_to_lu n : - of_lu (to_lu n) = n. + of_lu (to_lu n) = n. Proof. - induction n; simpl; trivial. rewrite of_lu_succ. now f_equal. + induction n; simpl; trivial. rewrite of_lu_succ. now f_equal. Qed. Lemma of_lu_revapp d d' : -of_lu (revapp d d') = - of_lu (rev d) + of_lu d' * 10^usize d. + of_lu (revapp d d') = + of_lu (rev d) + of_lu d' * 10^usize d. Proof. - revert d'. - induction d; intro d'; simpl usize; - [ simpl; now rewrite Nat.mul_1_r | .. ]; - unfold rev; simpl revapp; rewrite 2 IHd; - rewrite <- Nat.add_assoc; f_equal; simpl_of_lu; simpl of_lu; - rewrite Nat.pow_succ_r'; ring. + revert d'. + induction d; intro d'; simpl usize; + [ simpl; now rewrite Nat.mul_1_r | .. ]; + unfold rev; simpl revapp; rewrite 2 IHd; + rewrite <- Nat.add_assoc; f_equal; simpl_of_lu; simpl of_lu; + rewrite Nat.pow_succ_r'; ring. Qed. Lemma of_uint_acc_spec n d : - Nat.of_uint_acc d n = of_lu (rev d) + n * 10^usize d. + Nat.of_uint_acc d n = of_lu (rev d) + n * 10^usize d. Proof. - revert n. induction d; intros; - simpl Nat.of_uint_acc; rewrite ?Nat.tail_mul_spec, ?IHd; - simpl rev; simpl usize; rewrite ?Nat.pow_succ_r'; - [ simpl; now rewrite Nat.mul_1_r | .. ]; - unfold rev at 2; simpl revapp; rewrite of_lu_revapp; - simpl of_lu; ring. + revert n. induction d; intros; + simpl Nat.of_uint_acc; rewrite ?Nat.tail_mul_spec, ?IHd; + simpl rev; simpl usize; rewrite ?Nat.pow_succ_r'; + [ simpl; now rewrite Nat.mul_1_r | .. ]; + unfold rev at 2; simpl revapp; rewrite of_lu_revapp; + simpl of_lu; ring. Qed. Lemma of_uint_alt d : Nat.of_uint d = of_lu (rev d). Proof. - unfold Nat.of_uint. now rewrite of_uint_acc_spec. + unfold Nat.of_uint. now rewrite of_uint_acc_spec. Qed. (** First main bijection result *) Lemma of_to (n:nat) : Nat.of_uint (Nat.to_uint n) = n. Proof. - rewrite to_uint_alt, of_uint_alt, rev_rev. apply of_to_lu. + rewrite to_uint_alt, of_uint_alt, rev_rev. apply of_to_lu. Qed. (** The other direction *) Lemma to_lu_tenfold n : n<>0 -> - to_lu (10 * n) = D0 (to_lu n). + to_lu (10 * n) = D0 (to_lu n). Proof. - induction n. - - simpl. now destruct 1. - - intros _. - destruct (Nat.eq_dec n 0) as [->|H]; simpl; trivial. - rewrite !Nat.add_succ_r. - simpl in *. rewrite (IHn H). now destruct (to_lu n). + induction n. + - simpl. now destruct 1. + - intros _. + destruct (Nat.eq_dec n 0) as [->|H]; simpl; trivial. + rewrite !Nat.add_succ_r. + simpl in *. rewrite (IHn H). now destruct (to_lu n). Qed. Lemma of_lu_0 d : of_lu d = 0 <-> nztail d = Nil. Proof. - induction d; try simpl_of_lu; try easy. - rewrite Nat.add_0_l. - split; intros H. - - apply Nat.eq_mul_0_r in H; auto. - rewrite IHd in H. simpl. now rewrite H. - - simpl in H. destruct (nztail d); try discriminate. - now destruct IHd as [_ ->]. + induction d; try simpl_of_lu; try easy. + rewrite Nat.add_0_l. + split; intros H. + - apply Nat.eq_mul_0_r in H; auto. + rewrite IHd in H. simpl. now rewrite H. + - simpl in H. destruct (nztail d); try discriminate. + now destruct IHd as [_ ->]. Qed. Lemma to_of_lu_tenfold d : - to_lu (of_lu d) = lnorm d -> - to_lu (10 * of_lu d) = lnorm (D0 d). + to_lu (of_lu d) = lnorm d -> + to_lu (10 * of_lu d) = lnorm (D0 d). Proof. - intro IH. - destruct (Nat.eq_dec (of_lu d) 0) as [H|H]. - - rewrite H. simpl. rewrite of_lu_0 in H. - unfold lnorm. simpl. now rewrite H. - - rewrite (to_lu_tenfold _ H), IH. - rewrite of_lu_0 in H. - unfold lnorm. simpl. now destruct (nztail d). + intro IH. + destruct (Nat.eq_dec (of_lu d) 0) as [H|H]. + - rewrite H. simpl. rewrite of_lu_0 in H. + unfold lnorm. simpl. now rewrite H. + - rewrite (to_lu_tenfold _ H), IH. + rewrite of_lu_0 in H. + unfold lnorm. simpl. now destruct (nztail d). Qed. Lemma to_of_lu d : to_lu (of_lu d) = lnorm d. Proof. - induction d; [ reflexivity | .. ]; - simpl_of_lu; - rewrite ?Nat.add_succ_l, Nat.add_0_l, ?to_lu_succ, to_of_lu_tenfold - by assumption; - unfold lnorm; simpl; now destruct nztail. + induction d; [ reflexivity | .. ]; + simpl_of_lu; + rewrite ?Nat.add_succ_l, Nat.add_0_l, ?to_lu_succ, to_of_lu_tenfold + by assumption; + unfold lnorm; simpl; now destruct nztail. Qed. (** Second bijection result *) Lemma to_of (d:uint) : Nat.to_uint (Nat.of_uint d) = unorm d. Proof. - rewrite to_uint_alt, of_uint_alt, to_of_lu. - apply rev_lnorm_rev. + rewrite to_uint_alt, of_uint_alt, to_of_lu. + apply rev_lnorm_rev. Qed. (** Some consequences *) Lemma to_uint_inj n n' : Nat.to_uint n = Nat.to_uint n' -> n = n'. Proof. - intro EQ. - now rewrite <- (of_to n), <- (of_to n'), EQ. + intro EQ. + now rewrite <- (of_to n), <- (of_to n'), EQ. Qed. Lemma to_uint_surj d : exists n, Nat.to_uint n = unorm d. Proof. - exists (Nat.of_uint d). apply to_of. + exists (Nat.of_uint d). apply to_of. Qed. Lemma of_uint_norm d : Nat.of_uint (unorm d) = Nat.of_uint d. Proof. - unfold Nat.of_uint. now induction d. + unfold Nat.of_uint. now induction d. Qed. Lemma of_inj d d' : - Nat.of_uint d = Nat.of_uint d' -> unorm d = unorm d'. + Nat.of_uint d = Nat.of_uint d' -> unorm d = unorm d'. Proof. - intros. rewrite <- !to_of. now f_equal. + intros. rewrite <- !to_of. now f_equal. Qed. Lemma of_iff d d' : Nat.of_uint d = Nat.of_uint d' <-> unorm d = unorm d'. Proof. - split. apply of_inj. intros E. rewrite <- of_uint_norm, E. - apply of_uint_norm. + split. apply of_inj. intros E. rewrite <- of_uint_norm, E. + apply of_uint_norm. Qed. End Unsigned. @@ -260,43 +260,43 @@ Module Signed. Lemma of_to (n:nat) : Nat.of_int (Nat.to_int n) = Some n. Proof. - unfold Nat.to_int, Nat.of_int, norm. f_equal. - rewrite Unsigned.of_uint_norm. apply Unsigned.of_to. + unfold Nat.to_int, Nat.of_int, norm. f_equal. + rewrite Unsigned.of_uint_norm. apply Unsigned.of_to. Qed. Lemma to_of (d:int)(n:nat) : Nat.of_int d = Some n -> Nat.to_int n = norm d. Proof. - unfold Nat.of_int. - destruct (norm d) eqn:Hd; intros [= <-]. - unfold Nat.to_int. rewrite Unsigned.to_of. f_equal. - revert Hd; destruct d; simpl. - - intros [= <-]. apply unorm_invol. - - destruct (nzhead d); now intros [= <-]. + unfold Nat.of_int. + destruct (norm d) eqn:Hd; intros [= <-]. + unfold Nat.to_int. rewrite Unsigned.to_of. f_equal. + revert Hd; destruct d; simpl. + - intros [= <-]. apply unorm_invol. + - destruct (nzhead d); now intros [= <-]. Qed. Lemma to_int_inj n n' : Nat.to_int n = Nat.to_int n' -> n = n'. Proof. - intro E. - assert (E' : Some n = Some n'). - { now rewrite <- (of_to n), <- (of_to n'), E. } - now injection E'. + intro E. + assert (E' : Some n = Some n'). + { now rewrite <- (of_to n), <- (of_to n'), E. } + now injection E'. Qed. Lemma to_int_pos_surj d : exists n, Nat.to_int n = norm (Pos d). Proof. - exists (Nat.of_uint d). unfold Nat.to_int. now rewrite Unsigned.to_of. + exists (Nat.of_uint d). unfold Nat.to_int. now rewrite Unsigned.to_of. Qed. Lemma of_int_norm d : Nat.of_int (norm d) = Nat.of_int d. Proof. - unfold Nat.of_int. now rewrite norm_invol. + unfold Nat.of_int. now rewrite norm_invol. Qed. Lemma of_inj_pos d d' : - Nat.of_int (Pos d) = Nat.of_int (Pos d') -> unorm d = unorm d'. + Nat.of_int (Pos d) = Nat.of_int (Pos d') -> unorm d = unorm d'. Proof. - unfold Nat.of_int. simpl. intros [= H]. apply Unsigned.of_inj. - now rewrite <- Unsigned.of_uint_norm, H, Unsigned.of_uint_norm. + unfold Nat.of_int. simpl. intros [= H]. apply Unsigned.of_inj. + now rewrite <- Unsigned.of_uint_norm, H, Unsigned.of_uint_norm. Qed. End Signed. diff --git a/theories/Numbers/DecimalPos.v b/theories/Numbers/DecimalPos.v index 803688f476..5611329b12 100644 --- a/theories/Numbers/DecimalPos.v +++ b/theories/Numbers/DecimalPos.v @@ -36,37 +36,37 @@ Fixpoint of_lu (d:uint) : N := end. Definition hd d := -match d with - | Nil => 0 - | D0 _ => 0 - | D1 _ => 1 - | D2 _ => 2 - | D3 _ => 3 - | D4 _ => 4 - | D5 _ => 5 - | D6 _ => 6 - | D7 _ => 7 - | D8 _ => 8 - | D9 _ => 9 -end. + match d with + | Nil => 0 + | D0 _ => 0 + | D1 _ => 1 + | D2 _ => 2 + | D3 _ => 3 + | D4 _ => 4 + | D5 _ => 5 + | D6 _ => 6 + | D7 _ => 7 + | D8 _ => 8 + | D9 _ => 9 + end. Definition tl d := - match d with - | Nil => d - | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d => d -end. + match d with + | Nil => d + | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d => d + end. Lemma of_lu_eqn d : - of_lu d = hd d + 10 * (of_lu (tl d)). + of_lu d = hd d + 10 * (of_lu (tl d)). Proof. - induction d; simpl; trivial. + induction d; simpl; trivial. Qed. Ltac simpl_of_lu := - match goal with - | |- context [ of_lu (?f ?x) ] => - rewrite (of_lu_eqn (f x)); simpl hd; simpl tl - end. + match goal with + | |- context [ of_lu (?f ?x) ] => + rewrite (of_lu_eqn (f x)); simpl hd; simpl tl + end. Fixpoint usize (d:uint) : N := match d with @@ -84,89 +84,89 @@ Fixpoint usize (d:uint) : N := end. Lemma of_lu_revapp d d' : - of_lu (revapp d d') = - of_lu (rev d) + of_lu d' * 10^usize d. + of_lu (revapp d d') = + of_lu (rev d) + of_lu d' * 10^usize d. Proof. - revert d'. - induction d; simpl; intro d'; [ now rewrite N.mul_1_r | .. ]; - unfold rev; simpl revapp; rewrite 2 IHd; - rewrite <- N.add_assoc; f_equal; simpl_of_lu; simpl of_lu; - rewrite N.pow_succ_r'; ring. + revert d'. + induction d; simpl; intro d'; [ now rewrite N.mul_1_r | .. ]; + unfold rev; simpl revapp; rewrite 2 IHd; + rewrite <- N.add_assoc; f_equal; simpl_of_lu; simpl of_lu; + rewrite N.pow_succ_r'; ring. Qed. Definition Nadd n p := - match n with - | N0 => p - | Npos p0 => (p0+p)%positive - end. + match n with + | N0 => p + | Npos p0 => (p0+p)%positive + end. Lemma Nadd_simpl n p q : Npos (Nadd n (p * q)) = n + Npos p * Npos q. Proof. - now destruct n. + now destruct n. Qed. Lemma of_uint_acc_eqn d acc : d<>Nil -> - Pos.of_uint_acc d acc = Pos.of_uint_acc (tl d) (Nadd (hd d) (10*acc)). + Pos.of_uint_acc d acc = Pos.of_uint_acc (tl d) (Nadd (hd d) (10*acc)). Proof. - destruct d; simpl; trivial. now destruct 1. + destruct d; simpl; trivial. now destruct 1. Qed. Lemma of_uint_acc_rev d acc : - Npos (Pos.of_uint_acc d acc) = - of_lu (rev d) + (Npos acc) * 10^usize d. + Npos (Pos.of_uint_acc d acc) = + of_lu (rev d) + (Npos acc) * 10^usize d. Proof. - revert acc. - induction d; intros; simpl usize; - [ simpl; now rewrite Pos.mul_1_r | .. ]; - rewrite N.pow_succ_r'; - unfold rev; simpl revapp; try rewrite of_lu_revapp; simpl of_lu; - rewrite of_uint_acc_eqn by easy; simpl tl; simpl hd; - rewrite IHd, Nadd_simpl; ring. + revert acc. + induction d; intros; simpl usize; + [ simpl; now rewrite Pos.mul_1_r | .. ]; + rewrite N.pow_succ_r'; + unfold rev; simpl revapp; try rewrite of_lu_revapp; simpl of_lu; + rewrite of_uint_acc_eqn by easy; simpl tl; simpl hd; + rewrite IHd, Nadd_simpl; ring. Qed. Lemma of_uint_alt d : Pos.of_uint d = of_lu (rev d). Proof. - induction d; simpl; trivial; unfold rev; simpl revapp; - rewrite of_lu_revapp; simpl of_lu; try apply of_uint_acc_rev. - rewrite IHd. ring. + induction d; simpl; trivial; unfold rev; simpl revapp; + rewrite of_lu_revapp; simpl of_lu; try apply of_uint_acc_rev. + rewrite IHd. ring. Qed. Lemma of_lu_rev d : Pos.of_uint (rev d) = of_lu d. Proof. - rewrite of_uint_alt. now rewrite rev_rev. + rewrite of_uint_alt. now rewrite rev_rev. Qed. Lemma of_lu_double_gen d : of_lu (Little.double d) = N.double (of_lu d) /\ of_lu (Little.succ_double d) = N.succ_double (of_lu d). Proof. - rewrite N.double_spec, N.succ_double_spec. - induction d; try destruct IHd as (IH1,IH2); - simpl Little.double; simpl Little.succ_double; - repeat (simpl_of_lu; rewrite ?IH1, ?IH2); split; reflexivity || ring. + rewrite N.double_spec, N.succ_double_spec. + induction d; try destruct IHd as (IH1,IH2); + simpl Little.double; simpl Little.succ_double; + repeat (simpl_of_lu; rewrite ?IH1, ?IH2); split; reflexivity || ring. Qed. Lemma of_lu_double d : of_lu (Little.double d) = N.double (of_lu d). Proof. - apply of_lu_double_gen. + apply of_lu_double_gen. Qed. Lemma of_lu_succ_double d : of_lu (Little.succ_double d) = N.succ_double (of_lu d). Proof. - apply of_lu_double_gen. + apply of_lu_double_gen. Qed. (** First bijection result *) Lemma of_to (p:positive) : Pos.of_uint (Pos.to_uint p) = Npos p. Proof. - unfold Pos.to_uint. - rewrite of_lu_rev. - induction p; simpl; trivial. - - now rewrite of_lu_succ_double, IHp. - - now rewrite of_lu_double, IHp. + unfold Pos.to_uint. + rewrite of_lu_rev. + induction p; simpl; trivial. + - now rewrite of_lu_succ_double, IHp. + - now rewrite of_lu_double, IHp. Qed. (** The other direction *) @@ -180,149 +180,164 @@ Definition to_lu n := Lemma succ_double_alt d : Little.succ_double d = Little.succ (Little.double d). Proof. - now induction d. + now induction d. Qed. Lemma double_succ d : Little.double (Little.succ d) = Little.succ (Little.succ_double d). Proof. - induction d; simpl; f_equal; auto using succ_double_alt. + induction d; simpl; f_equal; auto using succ_double_alt. Qed. Lemma to_lu_succ n : - to_lu (N.succ n) = Little.succ (to_lu n). + to_lu (N.succ n) = Little.succ (to_lu n). Proof. - destruct n; simpl; trivial. - induction p; simpl; rewrite ?IHp; - auto using succ_double_alt, double_succ. + destruct n; simpl; trivial. + induction p; simpl; rewrite ?IHp; + auto using succ_double_alt, double_succ. Qed. Lemma nat_iter_S n {A} (f:A->A) i : - Nat.iter (S n) f i = f (Nat.iter n f i). + Nat.iter (S n) f i = f (Nat.iter n f i). Proof. - reflexivity. + reflexivity. Qed. Lemma nat_iter_0 {A} (f:A->A) i : Nat.iter 0 f i = i. Proof. - reflexivity. + reflexivity. Qed. Lemma to_ldec_tenfold p : to_lu (10 * Npos p) = D0 (to_lu (Npos p)). Proof. - induction p using Pos.peano_rect. - - trivial. - - change (N.pos (Pos.succ p)) with (N.succ (N.pos p)). - rewrite N.mul_succ_r. - change 10 at 2 with (Nat.iter 10%nat N.succ 0). - rewrite ?nat_iter_S, nat_iter_0. - rewrite !N.add_succ_r, N.add_0_r, !to_lu_succ, IHp. - destruct (to_lu (N.pos p)); simpl; auto. + induction p using Pos.peano_rect. + - trivial. + - change (N.pos (Pos.succ p)) with (N.succ (N.pos p)). + rewrite N.mul_succ_r. + change 10 at 2 with (Nat.iter 10%nat N.succ 0). + rewrite ?nat_iter_S, nat_iter_0. + rewrite !N.add_succ_r, N.add_0_r, !to_lu_succ, IHp. + destruct (to_lu (N.pos p)); simpl; auto. Qed. Lemma of_lu_0 d : of_lu d = 0 <-> nztail d = Nil. Proof. - induction d; try simpl_of_lu; split; trivial; try discriminate; - try (intros H; now apply N.eq_add_0 in H). - - rewrite N.add_0_l. intros H. - apply N.eq_mul_0_r in H; [|easy]. rewrite IHd in H. - simpl. now rewrite H. - - simpl. destruct (nztail d); try discriminate. - now destruct IHd as [_ ->]. -Qed. + induction d; try simpl_of_lu; split; trivial; try discriminate; + try (intros H; now apply N.eq_add_0 in H). + - rewrite N.add_0_l. intros H. + apply N.eq_mul_0_r in H; [|easy]. rewrite IHd in H. + simpl. now rewrite H. + - simpl. destruct (nztail d); try discriminate. + now destruct IHd as [_ ->]. + Qed. Lemma to_of_lu_tenfold d : - to_lu (of_lu d) = lnorm d -> - to_lu (10 * of_lu d) = lnorm (D0 d). + to_lu (of_lu d) = lnorm d -> + to_lu (10 * of_lu d) = lnorm (D0 d). Proof. - intro IH. - destruct (N.eq_dec (of_lu d) 0) as [H|H]. - - rewrite H. simpl. rewrite of_lu_0 in H. - unfold lnorm. simpl. now rewrite H. - - destruct (of_lu d) eqn:Eq; [easy| ]. - rewrite to_ldec_tenfold; auto. rewrite IH. - rewrite <- Eq in H. rewrite of_lu_0 in H. - unfold lnorm. simpl. now destruct (nztail d). + intro IH. + destruct (N.eq_dec (of_lu d) 0) as [H|H]. + - rewrite H. simpl. rewrite of_lu_0 in H. + unfold lnorm. simpl. now rewrite H. + - destruct (of_lu d) eqn:Eq; [easy| ]. + rewrite to_ldec_tenfold; auto. rewrite IH. + rewrite <- Eq in H. rewrite of_lu_0 in H. + unfold lnorm. simpl. now destruct (nztail d). Qed. Lemma Nadd_alt n m : n + m = Nat.iter (N.to_nat n) N.succ m. Proof. - destruct n. trivial. - induction p using Pos.peano_rect. - - now rewrite N.add_1_l. - - change (N.pos (Pos.succ p)) with (N.succ (N.pos p)). - now rewrite N.add_succ_l, IHp, N2Nat.inj_succ. + destruct n. trivial. + induction p using Pos.peano_rect. + - now rewrite N.add_1_l. + - change (N.pos (Pos.succ p)) with (N.succ (N.pos p)). + now rewrite N.add_succ_l, IHp, N2Nat.inj_succ. Qed. Ltac simpl_to_nat := simpl N.to_nat; unfold Pos.to_nat; simpl Pos.iter_op. Lemma to_of_lu d : to_lu (of_lu d) = lnorm d. Proof. - induction d; [reflexivity|..]; - simpl_of_lu; rewrite Nadd_alt; simpl_to_nat; - rewrite ?nat_iter_S, nat_iter_0, ?to_lu_succ, to_of_lu_tenfold by assumption; - unfold lnorm; simpl; destruct nztail; auto. + induction d; [reflexivity|..]; + simpl_of_lu; rewrite Nadd_alt; simpl_to_nat; + rewrite ?nat_iter_S, nat_iter_0, ?to_lu_succ, to_of_lu_tenfold by assumption; + unfold lnorm; simpl; destruct nztail; auto. Qed. (** Second bijection result *) Lemma to_of (d:uint) : N.to_uint (Pos.of_uint d) = unorm d. Proof. - rewrite of_uint_alt. - unfold N.to_uint, Pos.to_uint. - destruct (of_lu (rev d)) eqn:H. - - rewrite of_lu_0 in H. rewrite <- rev_lnorm_rev. - unfold lnorm. now rewrite H. - - change (Pos.to_little_uint p) with (to_lu (N.pos p)). - rewrite <- H. rewrite to_of_lu. apply rev_lnorm_rev. + rewrite of_uint_alt. + unfold N.to_uint, Pos.to_uint. + destruct (of_lu (rev d)) eqn:H. + - rewrite of_lu_0 in H. rewrite <- rev_lnorm_rev. + unfold lnorm. now rewrite H. + - change (Pos.to_little_uint p) with (to_lu (N.pos p)). + rewrite <- H. rewrite to_of_lu. apply rev_lnorm_rev. Qed. (** Some consequences *) Lemma to_uint_nonzero p : Pos.to_uint p <> zero. Proof. - intro E. generalize (of_to p). now rewrite E. + intro E. generalize (of_to p). now rewrite E. Qed. Lemma to_uint_nonnil p : Pos.to_uint p <> Nil. Proof. - intros E. generalize (of_to p). now rewrite E. + intros E. generalize (of_to p). now rewrite E. Qed. Lemma to_uint_inj p p' : Pos.to_uint p = Pos.to_uint p' -> p = p'. Proof. - intro E. - assert (E' : N.pos p = N.pos p'). - { now rewrite <- (of_to p), <- (of_to p'), E. } - now injection E'. + intro E. + assert (E' : N.pos p = N.pos p'). + { now rewrite <- (of_to p), <- (of_to p'), E. } + now injection E'. Qed. Lemma to_uint_pos_surj d : - unorm d<>zero -> exists p, Pos.to_uint p = unorm d. + unorm d<>zero -> exists p, Pos.to_uint p = unorm d. Proof. - intros. - destruct (Pos.of_uint d) eqn:E. - - destruct H. generalize (to_of d). now rewrite E. - - exists p. generalize (to_of d). now rewrite E. + intros. + destruct (Pos.of_uint d) eqn:E. + - destruct H. generalize (to_of d). now rewrite E. + - exists p. generalize (to_of d). now rewrite E. Qed. Lemma of_uint_norm d : Pos.of_uint (unorm d) = Pos.of_uint d. Proof. - now induction d. + now induction d. Qed. Lemma of_inj d d' : - Pos.of_uint d = Pos.of_uint d' -> unorm d = unorm d'. + Pos.of_uint d = Pos.of_uint d' -> unorm d = unorm d'. Proof. - intros. rewrite <- !to_of. now f_equal. + intros. rewrite <- !to_of. now f_equal. Qed. Lemma of_iff d d' : Pos.of_uint d = Pos.of_uint d' <-> unorm d = unorm d'. Proof. - split. apply of_inj. intros E. rewrite <- of_uint_norm, E. - apply of_uint_norm. + split. apply of_inj. intros E. rewrite <- of_uint_norm, E. + apply of_uint_norm. +Qed. + +Lemma nztail_to_uint p : + let (h, n) := Decimal.nztail (Pos.to_uint p) in + Npos p = Pos.of_uint h * 10^(N.of_nat n). +Proof. + rewrite <-(of_to p), <-(rev_rev (Pos.to_uint p)), of_lu_rev. + unfold Decimal.nztail. + rewrite rev_rev. + induction (rev (Pos.to_uint p)); [reflexivity| | + now simpl N.of_nat; simpl N.pow; rewrite N.mul_1_r, of_lu_rev..]. + revert IHu. + set (t := _ u); case t; clear t; intros u0 n H. + rewrite of_lu_eqn; unfold hd, tl. + rewrite N.add_0_l, H, Nat2N.inj_succ, N.pow_succ_r'; ring. Qed. End Unsigned. @@ -333,51 +348,51 @@ Module Signed. Lemma of_to (p:positive) : Pos.of_int (Pos.to_int p) = Some p. Proof. - unfold Pos.to_int, Pos.of_int, norm. - now rewrite Unsigned.of_to. + unfold Pos.to_int, Pos.of_int, norm. + now rewrite Unsigned.of_to. Qed. Lemma to_of (d:int)(p:positive) : - Pos.of_int d = Some p -> Pos.to_int p = norm d. + Pos.of_int d = Some p -> Pos.to_int p = norm d. Proof. - unfold Pos.of_int. - destruct d; [ | intros [=]]. - simpl norm. rewrite <- Unsigned.to_of. - destruct (Pos.of_uint d); now intros [= <-]. + unfold Pos.of_int. + destruct d; [ | intros [=]]. + simpl norm. rewrite <- Unsigned.to_of. + destruct (Pos.of_uint d); now intros [= <-]. Qed. Lemma to_int_inj p p' : Pos.to_int p = Pos.to_int p' -> p = p'. Proof. - intro E. - assert (E' : Some p = Some p'). - { now rewrite <- (of_to p), <- (of_to p'), E. } - now injection E'. + intro E. + assert (E' : Some p = Some p'). + { now rewrite <- (of_to p), <- (of_to p'), E. } + now injection E'. Qed. Lemma to_int_pos_surj d : - unorm d <> zero -> exists p, Pos.to_int p = norm (Pos d). + unorm d <> zero -> exists p, Pos.to_int p = norm (Pos d). Proof. - simpl. unfold Pos.to_int. intros H. - destruct (Unsigned.to_uint_pos_surj d H) as (p,Hp). - exists p. now f_equal. + simpl. unfold Pos.to_int. intros H. + destruct (Unsigned.to_uint_pos_surj d H) as (p,Hp). + exists p. now f_equal. Qed. Lemma of_int_norm d : Pos.of_int (norm d) = Pos.of_int d. Proof. - unfold Pos.of_int. - destruct d. - - simpl. now rewrite Unsigned.of_uint_norm. - - simpl. now destruct (nzhead d) eqn:H. + unfold Pos.of_int. + destruct d. + - simpl. now rewrite Unsigned.of_uint_norm. + - simpl. now destruct (nzhead d) eqn:H. Qed. Lemma of_inj_pos d d' : - Pos.of_int (Pos d) = Pos.of_int (Pos d') -> unorm d = unorm d'. + Pos.of_int (Pos d) = Pos.of_int (Pos d') -> unorm d = unorm d'. Proof. - unfold Pos.of_int. - destruct (Pos.of_uint d) eqn:Hd, (Pos.of_uint d') eqn:Hd'; - intros [=]. - - apply Unsigned.of_inj; now rewrite Hd, Hd'. - - apply Unsigned.of_inj; rewrite Hd, Hd'; now f_equal. + unfold Pos.of_int. + destruct (Pos.of_uint d) eqn:Hd, (Pos.of_uint d') eqn:Hd'; + intros [=]. + - apply Unsigned.of_inj; now rewrite Hd, Hd'. + - apply Unsigned.of_inj; rewrite Hd, Hd'; now f_equal. Qed. End Signed. diff --git a/theories/Numbers/DecimalQ.v b/theories/Numbers/DecimalQ.v new file mode 100644 index 0000000000..c51cced024 --- /dev/null +++ b/theories/Numbers/DecimalQ.v @@ -0,0 +1,561 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** * DecimalQ + + Proofs that conversions between decimal numbers and [Q] + are bijections. *) + +Require Import Decimal DecimalFacts DecimalPos DecimalN DecimalZ QArith. + +Lemma of_to (q:Q) : forall d, to_decimal q = Some d -> of_decimal d = q. +Proof. + cut (match to_decimal q with None => True | Some d => of_decimal d = q end). + { now case to_decimal; [intros d <- d' Hd'; injection Hd'; intros ->|]. } + destruct q as (num, den). + unfold to_decimal; simpl. + generalize (DecimalPos.Unsigned.nztail_to_uint den). + case Decimal.nztail; intros u n. + case u; clear u; [intros; exact I|intros; exact I|intro u|intros; exact I..]. + case u; clear u; [|intros; exact I..]. + unfold Pos.of_uint, Pos.of_uint_acc; rewrite N.mul_1_l. + case n. + - unfold of_decimal, app_int, app, Z.to_int; simpl. + intro H; inversion H as (H1); clear H H1. + case num; [reflexivity|intro pnum; fold (rev (rev (Pos.to_uint pnum)))..]. + + rewrite rev_rev; simpl. + now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to. + + rewrite rev_rev; simpl. + now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to. + - clear n; intros n H. + injection H; clear H; intros ->. + case Nat.ltb. + + unfold of_decimal. + rewrite of_to. + apply f_equal2; [|now simpl]. + unfold app_int, app, Z.to_int; simpl. + now case num; + [|intro pnum; fold (rev (rev (Pos.to_uint pnum))); + rewrite rev_rev; unfold Z.of_int, Z.of_uint; + rewrite DecimalPos.Unsigned.of_to..]. + + unfold of_decimal; case Nat.ltb_spec; intro Hn; simpl. + * rewrite nb_digits_del_head; [|now apply Nat.le_sub_l]. + rewrite Nat2Z.inj_sub; [|now apply Nat.le_sub_l]. + rewrite Nat2Z.inj_sub; [|now apply le_Sn_le]. + rewrite Z.sub_sub_distr, Z.sub_diag; simpl. + rewrite <-(of_to num) at 4. + now revert Hn; case Z.to_int; clear num; intros pnum Hn; simpl; + (rewrite app_del_tail_head; [|now apply le_Sn_le]). + * revert Hn. + set (anum := match Z.to_int num with Pos i => i | _ => _ end). + intro Hn. + assert (H : exists l, nb_digits anum = S l). + { exists (Nat.pred (nb_digits anum)); apply S_pred_pos. + now unfold anum; case num; + [apply Nat.lt_0_1| + intro pnum; apply nb_digits_pos, Unsigned.to_uint_nonnil..]. } + destruct H as (l, Hl); rewrite Hl. + assert (H : forall n d, (nb_digits (Nat.iter n D0 d) = n + nb_digits d)%nat). + { now intros n'; induction n'; intro d; [|simpl; rewrite IHn']. } + rewrite H, Hl. + rewrite Nat.add_succ_r, Nat.sub_add; [|now apply le_S_n; rewrite <-Hl]. + assert (H' : forall n d, Pos.of_uint (Nat.iter n D0 d) = Pos.of_uint d). + { now intro n'; induction n'; intro d; [|simpl; rewrite IHn']. } + now unfold anum; case num; simpl; [|intro pnum..]; + unfold app, Z.of_uint; simpl; + rewrite H', ?DecimalPos.Unsigned.of_to. +Qed. + +(* normalize without fractional part, for instance norme 12.3e-1 is 123e-2 *) +Definition dnorme (d:decimal) : decimal := + let '(i, f, e) := + match d with + | Decimal i f => (i, f, Pos Nil) + | DecimalExp i f e => (i, f, e) + end in + let i := norm (app_int i f) in + let e := norm (Z.to_int (Z.of_int e - Z.of_nat (nb_digits f))) in + match e with + | Pos zero => Decimal i Nil + | _ => DecimalExp i Nil e + end. + +(* normalize without exponent part, for instance norme 12.3e-1 is 1.23 *) +Definition dnormf (d:decimal) : decimal := + match dnorme d with + | Decimal i _ => Decimal i Nil + | DecimalExp i _ e => + match Z.of_int e with + | Z0 => Decimal i Nil + | Zpos e => Decimal (norm (app_int i (Pos.iter D0 Nil e))) Nil + | Zneg e => + let ne := Pos.to_nat e in + let ai := match i with Pos d | Neg d => d end in + let ni := nb_digits ai in + if ne <? ni then + Decimal (del_tail_int ne i) (del_head (ni - ne) ai) + else + let z := match i with Pos _ => Pos zero | Neg _ => Neg zero end in + Decimal z (Nat.iter (ne - ni) D0 ai) + end + end. + +Lemma dnorme_spec d : + match dnorme d with + | Decimal i Nil => i = norm i + | DecimalExp i Nil e => i = norm i /\ e = norm e /\ e <> Pos zero + | _ => False + end. +Proof. + case d; clear d; intros i f; [|intro e]; unfold dnorme; simpl. + - set (e' := Z.to_int _). + case (int_eq_dec (norm e') (Pos zero)); [intros->|intro Hne']. + + now rewrite norm_invol. + + set (r := DecimalExp _ _ _). + set (m := match norm e' with Pos zero => _ | _ => _ end). + replace m with r; [now unfold r; rewrite !norm_invol|]. + unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl]. + now case e''; [|intro e'''; case e'''..]. + - set (e' := Z.to_int _). + case (int_eq_dec (norm e') (Pos zero)); [intros->|intro Hne']. + + now rewrite norm_invol. + + set (r := DecimalExp _ _ _). + set (m := match norm e' with Pos zero => _ | _ => _ end). + replace m with r; [now unfold r; rewrite !norm_invol|]. + unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl]. + now case e''; [|intro e'''; case e'''..]. +Qed. + +Lemma dnormf_spec d : + match dnormf d with + | Decimal i f => i = Neg zero \/ i = norm i + | _ => False + end. +Proof. + case d; clear d; intros i f; [|intro e]; unfold dnormf, dnorme; simpl. + - set (e' := Z.to_int _). + case (int_eq_dec (norm e') (Pos zero)); [intros->|intro Hne']. + + now right; rewrite norm_invol. + + set (r := DecimalExp _ _ _). + set (m := match norm e' with Pos zero => _ | _ => _ end). + assert (H : m = r); [|rewrite H; unfold m, r; clear m r H]. + { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl]. + now case e''; [|intro e'''; case e'''..]. } + rewrite <-DecimalZ.to_of, DecimalZ.of_to. + case_eq (Z.of_int e'); [|intros pe'..]; intro Hpe'; + [now right; rewrite norm_invol..|]. + case Nat.ltb_spec. + * now intro H; rewrite (norm_del_tail_int_norm _ _ H); right. + * now intros _; case norm; intros _; [right|left]. + - set (e' := Z.to_int _). + case (int_eq_dec (norm e') (Pos zero)); [intros->|intro Hne']. + + now right; rewrite norm_invol. + + set (r := DecimalExp _ _ _). + set (m := match norm e' with Pos zero => _ | _ => _ end). + assert (H : m = r); [|rewrite H; unfold m, r; clear m r H]. + { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl]. + now case e''; [|intro e'''; case e'''..]. } + rewrite <-DecimalZ.to_of, DecimalZ.of_to. + case_eq (Z.of_int e'); [|intros pe'..]; intro Hpe'; + [now right; rewrite norm_invol..|]. + case Nat.ltb_spec. + * now intro H; rewrite (norm_del_tail_int_norm _ _ H); right. + * now intros _; case norm; intros _; [right|left]. +Qed. + +Lemma dnorme_invol d : dnorme (dnorme d) = dnorme d. +Proof. + case d; clear d; intros i f; [|intro e]; unfold dnorme; simpl. + - set (e' := Z.to_int _). + case (int_eq_dec (norm e') (Pos zero)); intro Hne'. + + rewrite Hne'; simpl; rewrite app_int_nil_r, norm_invol. + revert Hne'. + rewrite <-to_of. + change (Pos zero) with (Z.to_int 0). + intro H; generalize (to_int_inj _ _ H); clear H. + unfold e'; rewrite DecimalZ.of_to. + now case f; [rewrite app_int_nil_r|..]. + + set (r := DecimalExp _ _ _). + set (m := match norm e' with Pos zero => _ | _ => _ end). + assert (H : m = r); [|rewrite H; unfold m, r; clear m r H]. + { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl]. + now case e''; [|intro e'''; case e'''..]. } + rewrite <-DecimalZ.to_of, DecimalZ.of_to. + unfold nb_digits, Z.of_nat; rewrite Z.sub_0_r, to_of, norm_invol. + rewrite app_int_nil_r, norm_invol. + set (r := DecimalExp _ _ _). + set (m := match norm e' with Pos zero => _ | _ => _ end). + unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl]. + now case e''; [|intro e'''; case e'''..]. + - set (e' := Z.to_int _). + case (int_eq_dec (norm e') (Pos zero)); intro Hne'. + + rewrite Hne'; simpl; rewrite app_int_nil_r, norm_invol. + revert Hne'. + rewrite <-to_of. + change (Pos zero) with (Z.to_int 0). + intro H; generalize (to_int_inj _ _ H); clear H. + unfold e'; rewrite DecimalZ.of_to. + now case f; [rewrite app_int_nil_r|..]. + + set (r := DecimalExp _ _ _). + set (m := match norm e' with Pos zero => _ | _ => _ end). + assert (H : m = r); [|rewrite H; unfold m, r; clear m r H]. + { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl]. + now case e''; [|intro e'''; case e'''..]. } + rewrite <-DecimalZ.to_of, DecimalZ.of_to. + unfold nb_digits, Z.of_nat; rewrite Z.sub_0_r, to_of, norm_invol. + rewrite app_int_nil_r, norm_invol. + set (r := DecimalExp _ _ _). + set (m := match norm e' with Pos zero => _ | _ => _ end). + unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl]. + now case e''; [|intro e'''; case e'''..]. +Qed. + +Lemma dnormf_invol d : dnormf (dnormf d) = dnormf d. +Proof. + case d; clear d; intros i f; [|intro e]; unfold dnormf, dnorme; simpl. + - set (e' := Z.to_int _). + case (int_eq_dec (norm e') (Pos zero)); intro Hne'. + + rewrite Hne'; simpl; rewrite app_int_nil_r, norm_invol. + revert Hne'. + rewrite <-to_of. + change (Pos zero) with (Z.to_int 0). + intro H; generalize (to_int_inj _ _ H); clear H. + unfold e'; rewrite DecimalZ.of_to. + now case f; [rewrite app_int_nil_r|..]. + + set (r := DecimalExp _ _ _). + set (m := match norm e' with Pos zero => _ | _ => _ end). + assert (H : m = r); [|rewrite H; unfold m, r; clear m r H]. + { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl]. + now case e''; [|intro e'''; case e'''..]. } + rewrite of_int_norm. + case_eq (Z.of_int e'); [|intro pe'..]; intro Hnpe'; + [now simpl; rewrite app_int_nil_r, norm_invol..|]. + case Nat.ltb_spec; intro Hpe'. + * rewrite nb_digits_del_head; [|now apply Nat.le_sub_l]. + rewrite Nat2Z.inj_sub; [|now apply Nat.le_sub_l]. + rewrite Nat2Z.inj_sub; [|now apply Nat.lt_le_incl]. + simpl. + rewrite Z.sub_sub_distr, Z.sub_diag, Z.add_0_l. + rewrite <-DecimalZ.to_of, DecimalZ.of_to. + rewrite positive_nat_Z; simpl. + unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. + rewrite app_int_del_tail_head; [|now apply Nat.lt_le_incl]. + now rewrite norm_invol, (proj2 (Nat.ltb_lt _ _) Hpe'). + * simpl. + rewrite nb_digits_iter_D0. + rewrite (Nat.sub_add _ _ Hpe'). + rewrite <-DecimalZ.to_of, DecimalZ.of_to. + rewrite positive_nat_Z; simpl. + unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. + revert Hpe'. + set (i' := norm (app_int i f)). + case_eq i'; intros u Hu Hpe'. + ++ simpl; unfold app; simpl. + rewrite unorm_D0, unorm_iter_D0. + assert (Hu' : unorm u = u). + { generalize (f_equal norm Hu). + unfold i'; rewrite norm_invol; fold i'. + now simpl; rewrite Hu; intro H; injection H. } + now rewrite Hu', (proj2 (Nat.ltb_ge _ _) Hpe'). + ++ simpl; rewrite nzhead_iter_D0. + assert (Hu' : nzhead u = u). + { generalize (f_equal norm Hu). + unfold i'; rewrite norm_invol; fold i'. + now rewrite Hu; simpl; case (nzhead u); [|intros u' H; injection H..]. } + rewrite Hu'. + assert (Hu'' : u <> Nil). + { intro H; revert Hu; rewrite H; unfold i'. + now case app_int; intro u'; [|simpl; case nzhead]. } + set (m := match u with Nil => Pos zero | _ => _ end). + assert (H : m = Neg u); [|rewrite H; clear m H]. + { now revert Hu''; unfold m; case u. } + now rewrite (proj2 (Nat.ltb_ge _ _) Hpe'). + - set (e' := Z.to_int _). + case (int_eq_dec (norm e') (Pos zero)); intro Hne'. + + rewrite Hne'; simpl; rewrite app_int_nil_r, norm_invol. + revert Hne'. + rewrite <-to_of. + change (Pos zero) with (Z.to_int 0). + intro H; generalize (to_int_inj _ _ H); clear H. + unfold e'; rewrite DecimalZ.of_to. + now case f; [rewrite app_int_nil_r|..]. + + set (r := DecimalExp _ _ _). + set (m := match norm e' with Pos zero => _ | _ => _ end). + assert (H : m = r); [|rewrite H; unfold m, r; clear m r H]. + { unfold m; revert Hne'; case (norm e'); intro e''; [|now simpl]. + now case e''; [|intro e'''; case e'''..]. } + rewrite of_int_norm. + case_eq (Z.of_int e'); [|intro pe'..]; intro Hnpe'; + [now simpl; rewrite app_int_nil_r, norm_invol..|]. + case Nat.ltb_spec; intro Hpe'. + * rewrite nb_digits_del_head; [|now apply Nat.le_sub_l]. + rewrite Nat2Z.inj_sub; [|now apply Nat.le_sub_l]. + rewrite Nat2Z.inj_sub; [|now apply Nat.lt_le_incl]. + simpl. + rewrite Z.sub_sub_distr, Z.sub_diag, Z.add_0_l. + rewrite <-DecimalZ.to_of, DecimalZ.of_to. + rewrite positive_nat_Z; simpl. + unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. + rewrite app_int_del_tail_head; [|now apply Nat.lt_le_incl]. + now rewrite norm_invol, (proj2 (Nat.ltb_lt _ _) Hpe'). + * simpl. + rewrite nb_digits_iter_D0. + rewrite (Nat.sub_add _ _ Hpe'). + rewrite <-DecimalZ.to_of, DecimalZ.of_to. + rewrite positive_nat_Z; simpl. + unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. + revert Hpe'. + set (i' := norm (app_int i f)). + case_eq i'; intros u Hu Hpe'. + ++ simpl; unfold app; simpl. + rewrite unorm_D0, unorm_iter_D0. + assert (Hu' : unorm u = u). + { generalize (f_equal norm Hu). + unfold i'; rewrite norm_invol; fold i'. + now simpl; rewrite Hu; intro H; injection H. } + now rewrite Hu', (proj2 (Nat.ltb_ge _ _) Hpe'). + ++ simpl; rewrite nzhead_iter_D0. + assert (Hu' : nzhead u = u). + { generalize (f_equal norm Hu). + unfold i'; rewrite norm_invol; fold i'. + now rewrite Hu; simpl; case (nzhead u); [|intros u' H; injection H..]. } + rewrite Hu'. + assert (Hu'' : u <> Nil). + { intro H; revert Hu; rewrite H; unfold i'. + now case app_int; intro u'; [|simpl; case nzhead]. } + set (m := match u with Nil => Pos zero | _ => _ end). + assert (H : m = Neg u); [|rewrite H; clear m H]. + { now revert Hu''; unfold m; case u. } + now rewrite (proj2 (Nat.ltb_ge _ _) Hpe'). +Qed. + +Lemma to_of (d:decimal) : + to_decimal (of_decimal d) = Some (dnorme d) + \/ to_decimal (of_decimal d) = Some (dnormf d). +Proof. + unfold to_decimal. + pose (t10 := fun y => ((y + y~0~0)~0)%positive). + assert (H : exists e_den, + Decimal.nztail (Pos.to_uint (Qden (of_decimal d))) = (D1 Nil, e_den)). + { assert (H : forall p, + Decimal.nztail (Pos.to_uint (Pos.iter t10 1%positive p)) + = (D1 Nil, Pos.to_nat p)). + { intro p; rewrite Pos2Nat.inj_iter. + fold (Nat.iter (Pos.to_nat p) t10 1%positive). + induction (Pos.to_nat p); [now simpl|]. + rewrite DecimalPos.Unsigned.nat_iter_S. + unfold Pos.to_uint. + change (Pos.to_little_uint _) + with (Unsigned.to_lu (10 * N.pos (Nat.iter n t10 1%positive))). + rewrite Unsigned.to_ldec_tenfold. + revert IHn; unfold Pos.to_uint. + unfold Decimal.nztail; rewrite !rev_rev; simpl. + set (f'' := _ (Pos.to_little_uint _)). + now case f''; intros r n' H; inversion H. } + case d; intros i f; [|intro e]; unfold of_decimal; simpl. + - case (- Z.of_nat _)%Z; [|intro p..]; simpl; [now exists O..|]. + exists (Pos.to_nat p); apply H. + - case (_ - _)%Z; [|intros p..]; simpl; [now exists O..|]. + exists (Pos.to_nat p); apply H. } + generalize (DecimalPos.Unsigned.nztail_to_uint (Qden (of_decimal d))). + destruct H as (e, He); rewrite He; clear He; simpl. + assert (Hn1 : forall p, N.pos (Pos.iter t10 1%positive p) = 1%N -> False). + { intro p. + rewrite Pos2Nat.inj_iter. + case_eq (Pos.to_nat p); [|now simpl]. + intro H; exfalso; apply (lt_irrefl O). + rewrite <-H at 2; apply Pos2Nat.is_pos. } + assert (Ht10inj : forall n m, t10 n = t10 m -> n = m). + { intros n m H; generalize (f_equal Z.pos H); clear H. + change (Z.pos (t10 n)) with (Z.mul 10 (Z.pos n)). + change (Z.pos (t10 m)) with (Z.mul 10 (Z.pos m)). + rewrite Z.mul_comm, (Z.mul_comm 10). + intro H; generalize (f_equal (fun z => Z.div z 10) H); clear H. + now rewrite !Z.div_mul; [|now simpl..]; intro H; inversion H. } + assert (Hinj : forall n m, + Nat.iter n t10 1%positive = Nat.iter m t10 1%positive -> n = m). + { induction n; [now intro m; case m|]. + intro m; case m; [now simpl|]; clear m; intro m. + rewrite !Unsigned.nat_iter_S. + intro H; generalize (Ht10inj _ _ H); clear H; intro H. + now rewrite (IHn _ H). } + case e; clear e; [|intro e]; simpl; unfold of_decimal, dnormf, dnorme. + - case d; clear d; intros i f; [|intro e]; simpl. + + intro H; left; revert H. + generalize (nb_digits_pos f). + case f; + [|now clear f; intro f; intros H1 H2; exfalso; revert H1 H2; + case nb_digits; simpl; + [intros H _; apply (lt_irrefl O), H|intros n _; apply Hn1]..]. + now intros _ _; simpl; rewrite to_of. + + intro H; right; revert H. + rewrite <-to_of, DecimalZ.of_to. + set (emf := (_ - _)%Z). + case_eq emf; [|intro pemf..]. + * now simpl; rewrite to_of. + * set (r := DecimalExp _ _ _). + set (m := match _ with Pos _ => _ | _ => r end). + assert (H : m = r). + { unfold m, Z.to_int. + generalize (Unsigned.to_uint_nonzero pemf). + now case Pos.to_uint; [|intro u; case u..]. } + rewrite H; unfold r; clear H m r. + rewrite DecimalZ.of_to. + simpl Qnum. + intros Hpemf _. + apply f_equal; apply f_equal2; [|reflexivity]. + rewrite !Pos2Nat.inj_iter. + set (n := _ pemf). + fold (Nat.iter n (Z.mul 10) (Z.of_int (app_int i f))). + fold (Nat.iter n D0 Nil). + rewrite <-of_int_iter_D0, to_of. + now rewrite norm_app_int_norm; [|induction n]. + * simpl Qden; intros _ H; exfalso; revert H; apply Hn1. + - case d; clear d; intros i f; [|intro e']; simpl. + + case_eq (nb_digits f); [|intros nf' Hnf']; + [now simpl; intros _ H; exfalso; symmetry in H; revert H; apply Hn1|]. + unfold Z.of_nat, Z.opp. + simpl Qden. + intro H; injection H; clear H; unfold Pos.pow. + rewrite !Pos2Nat.inj_iter. + intro H; generalize (Hinj _ _ H); clear H; intro H. + generalize (SuccNat2Pos.inj _ _ ((Pos2Nat.inj _ _ H))); clear H. + intro He; rewrite <-He; clear e He. + simpl Qnum. + case Nat.ltb; [left|right]. + * now rewrite <-to_of, DecimalZ.of_to, to_of. + * rewrite to_of. + set (nif := norm _). + set (anif := match nif with Pos i0 => i0 | _ => _ end). + set (r := DecimalExp nif Nil _). + set (m := match _ with Pos _ => _ | _ => r end). + assert (H : m = r); [|rewrite H; unfold m, r; clear m r H]. + { now unfold m; rewrite <-to_of, DecimalZ.of_to. } + rewrite <-to_of, !DecimalZ.of_to. + fold anif. + now rewrite SuccNat2Pos.id_succ. + + set (nemf := (_ - _)%Z); intro H. + assert (H' : exists pnemf, nemf = Z.neg pnemf); [|revert H]. + { revert H; case nemf; [|intro pnemf..]; [..|now intros _; exists pnemf]; + simpl Qden; intro H; exfalso; symmetry in H; revert H; apply Hn1. } + destruct H' as (pnemf,Hpnemf); rewrite Hpnemf. + simpl Qden. + intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter. + intro H; generalize (Hinj _ _ H); clear H; intro H. + generalize (Pos2Nat.inj _ _ H); clear H. + intro H; revert Hpnemf; rewrite H; clear pnemf H; intro Hnemf. + simpl Qnum. + case Nat.ltb; [left|right]. + * now rewrite <-to_of, DecimalZ.of_to, to_of. + * rewrite to_of. + set (nif := norm _). + set (anif := match nif with Pos i0 => i0 | _ => _ end). + set (r := DecimalExp nif Nil _). + set (m := match _ with Pos _ => _ | _ => r end). + assert (H : m = r); [|rewrite H; unfold m, r; clear m r H]. + { now unfold m; rewrite <-to_of, DecimalZ.of_to. } + rewrite <-to_of, !DecimalZ.of_to. + fold anif. + now rewrite SuccNat2Pos.id_succ. +Qed. + +(** Some consequences *) + +Lemma to_decimal_inj q q' : + to_decimal q <> None -> to_decimal q = to_decimal q' -> q = q'. +Proof. + intros Hnone EQ. + generalize (of_to q) (of_to q'). + rewrite <-EQ. + revert Hnone; case to_decimal; [|now simpl]. + now intros d _ H1 H2; rewrite <-(H1 d eq_refl), <-(H2 d eq_refl). +Qed. + +Lemma to_decimal_surj d : + exists q, to_decimal q = Some (dnorme d) \/ to_decimal q = Some (dnormf d). +Proof. + exists (of_decimal d). apply to_of. +Qed. + +Lemma of_decimal_dnorme d : of_decimal (dnorme d) = of_decimal d. +Proof. + unfold of_decimal, dnorme. + destruct d. + - rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl. + case_eq (nb_digits f); [|intro nf]; intro Hnf. + + now simpl; rewrite app_int_nil_r, <-DecimalZ.to_of, DecimalZ.of_to. + + simpl; rewrite Z.sub_0_r. + unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. + rewrite app_int_nil_r. + now rewrite <-DecimalZ.to_of, DecimalZ.of_to. + - rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl. + set (emf := (_ - _)%Z). + case_eq emf; [|intro pemf..]; intro Hemf. + + now simpl; rewrite app_int_nil_r, <-DecimalZ.to_of, DecimalZ.of_to. + + simpl. + set (r := DecimalExp _ Nil _). + set (m := match Pos.to_uint pemf with zero => _ | _ => r end). + assert (H : m = r); [|rewrite H; unfold r; clear m r H]. + { generalize (Unsigned.to_uint_nonzero pemf). + now unfold m; case Pos.to_uint; [|intro u; case u|..]. } + simpl; rewrite Z.sub_0_r. + unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. + rewrite app_int_nil_r. + now rewrite <-DecimalZ.to_of, DecimalZ.of_to. + + simpl. + unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl. + rewrite app_int_nil_r. + now rewrite <-DecimalZ.to_of, DecimalZ.of_to. +Qed. + +Lemma of_decimal_dnormf d : of_decimal (dnormf d) = of_decimal d. +Proof. + rewrite <-(of_decimal_dnorme d). + unfold of_decimal, dnormf. + assert (H : match dnorme d with Decimal _ f | DecimalExp _ f _ => f end = Nil). + { now unfold dnorme; destruct d; + (case norm; intro d; [case d; [|intro u; case u|..]|]). } + revert H; generalize (dnorme d); clear d; intro d. + destruct d; intro H; rewrite H; clear H; [now simpl|]. + case (Z.of_int e); clear e; [|intro e..]. + - now simpl. + - simpl. + rewrite app_int_nil_r. + apply f_equal2; [|reflexivity]. + rewrite app_int_nil_r. + rewrite <-DecimalZ.to_of, DecimalZ.of_to. + rewrite !Pos2Nat.inj_iter. + fold (Nat.iter (Pos.to_nat e) D0 Nil). + now rewrite of_int_iter_D0. + - simpl. + set (ai := match i with Pos _ => _ | _ => _ end). + rewrite app_int_nil_r. + case Nat.ltb_spec; intro Hei; simpl. + + rewrite nb_digits_del_head; [|now apply Nat.le_sub_l]. + rewrite Nat2Z.inj_sub; [|now apply Nat.le_sub_l]. + rewrite Nat2Z.inj_sub; [|now apply le_Sn_le]. + rewrite Z.sub_sub_distr, Z.sub_diag; simpl. + rewrite positive_nat_Z; simpl. + now revert Hei; unfold ai; case i; clear i ai; intros i Hei; simpl; + (rewrite app_del_tail_head; [|now apply le_Sn_le]). + + set (n := nb_digits _). + assert (H : (n = Pos.to_nat e - nb_digits ai + nb_digits ai)%nat). + { unfold n; induction (_ - _)%nat; [now simpl|]. + now rewrite Unsigned.nat_iter_S; simpl; rewrite IHn0. } + rewrite H; clear n H. + rewrite Nat2Z.inj_add, (Nat2Z.inj_sub _ _ Hei). + rewrite <-Z.sub_sub_distr, Z.sub_diag, Z.sub_0_r. + rewrite positive_nat_Z; simpl. + rewrite <-(DecimalZ.of_to (Z.of_int (app_int _ _))), DecimalZ.to_of. + rewrite <-(DecimalZ.of_to (Z.of_int i)), DecimalZ.to_of. + apply f_equal2; [|reflexivity]; apply f_equal. + now unfold ai; case i; clear i ai Hei; intro i; + (induction (_ - _)%nat; [|rewrite <-IHn]). +Qed. diff --git a/theories/Numbers/DecimalString.v b/theories/Numbers/DecimalString.v index 7a4906a183..de577592e4 100644 --- a/theories/Numbers/DecimalString.v +++ b/theories/Numbers/DecimalString.v @@ -24,23 +24,23 @@ Local Open Scope string_scope. (** Parsing one char *) Definition uint_of_char (a:ascii)(d:option uint) := - match d with - | None => None - | Some d => - match a with - | "0" => Some (D0 d) - | "1" => Some (D1 d) - | "2" => Some (D2 d) - | "3" => Some (D3 d) - | "4" => Some (D4 d) - | "5" => Some (D5 d) - | "6" => Some (D6 d) - | "7" => Some (D7 d) - | "8" => Some (D8 d) - | "9" => Some (D9 d) - | _ => None - end - end%char. + match d with + | None => None + | Some d => + match a with + | "0" => Some (D0 d) + | "1" => Some (D1 d) + | "2" => Some (D2 d) + | "3" => Some (D3 d) + | "4" => Some (D4 d) + | "5" => Some (D5 d) + | "6" => Some (D6 d) + | "7" => Some (D7 d) + | "8" => Some (D8 d) + | "9" => Some (D9 d) + | _ => None + end + end%char. Lemma uint_of_char_spec c d d' : uint_of_char c (Some d) = Some d' -> @@ -55,8 +55,8 @@ Lemma uint_of_char_spec c d d' : c = "8" /\ d' = D8 d \/ c = "9" /\ d' = D9 d)%char. Proof. - destruct c as [[|] [|] [|] [|] [|] [|] [|] [|]]; - intros [= <-]; intuition. + destruct c as [[|] [|] [|] [|] [|] [|] [|] [|]]; + intros [= <-]; intuition. Qed. (** Decimal/String conversion where [Nil] is [""] *) @@ -64,39 +64,39 @@ Qed. Module NilEmpty. Fixpoint string_of_uint (d:uint) := - match d with - | Nil => EmptyString - | D0 d => String "0" (string_of_uint d) - | D1 d => String "1" (string_of_uint d) - | D2 d => String "2" (string_of_uint d) - | D3 d => String "3" (string_of_uint d) - | D4 d => String "4" (string_of_uint d) - | D5 d => String "5" (string_of_uint d) - | D6 d => String "6" (string_of_uint d) - | D7 d => String "7" (string_of_uint d) - | D8 d => String "8" (string_of_uint d) - | D9 d => String "9" (string_of_uint d) - end. + match d with + | Nil => EmptyString + | D0 d => String "0" (string_of_uint d) + | D1 d => String "1" (string_of_uint d) + | D2 d => String "2" (string_of_uint d) + | D3 d => String "3" (string_of_uint d) + | D4 d => String "4" (string_of_uint d) + | D5 d => String "5" (string_of_uint d) + | D6 d => String "6" (string_of_uint d) + | D7 d => String "7" (string_of_uint d) + | D8 d => String "8" (string_of_uint d) + | D9 d => String "9" (string_of_uint d) + end. Fixpoint uint_of_string s := - match s with - | EmptyString => Some Nil - | String a s => uint_of_char a (uint_of_string s) - end. + match s with + | EmptyString => Some Nil + | String a s => uint_of_char a (uint_of_string s) + end. Definition string_of_int (d:int) := - match d with - | Pos d => string_of_uint d - | Neg d => String "-" (string_of_uint d) - end. + match d with + | Pos d => string_of_uint d + | Neg d => String "-" (string_of_uint d) + end. Definition int_of_string s := - match s with - | EmptyString => Some (Pos Nil) - | String a s' => - if Ascii.eqb a "-" then option_map Neg (uint_of_string s') - else option_map Pos (uint_of_string s) - end. + match s with + | EmptyString => Some (Pos Nil) + | String a s' => + if Ascii.eqb a "-" then option_map Neg (uint_of_string s') + else option_map Pos (uint_of_string s) + end. (* NB: For the moment whitespace between - and digits are not accepted. And in this variant [int_of_string "-" = Some (Neg Nil)]. @@ -110,44 +110,44 @@ Compute string_of_int (-123456890123456890123456890123456890). Lemma usu d : uint_of_string (string_of_uint d) = Some d. Proof. - induction d; simpl; rewrite ?IHd; simpl; auto. + induction d; simpl; rewrite ?IHd; simpl; auto. Qed. Lemma sus s d : uint_of_string s = Some d -> string_of_uint d = s. Proof. - revert d. - induction s; simpl. - - now intros d [= <-]. - - intros d. - destruct (uint_of_string s); [intros H | intros [=]]. - apply uint_of_char_spec in H. - intuition subst; simpl; f_equal; auto. + revert d. + induction s; simpl. + - now intros d [= <-]. + - intros d. + destruct (uint_of_string s); [intros H | intros [=]]. + apply uint_of_char_spec in H. + intuition subst; simpl; f_equal; auto. Qed. Lemma isi d : int_of_string (string_of_int d) = Some d. Proof. - destruct d; simpl. - - unfold int_of_string. - destruct (string_of_uint d) eqn:Hd. - + now destruct d. - + case Ascii.eqb_spec. - * intros ->. now destruct d. - * rewrite <- Hd, usu; auto. - - rewrite usu; auto. + destruct d; simpl. + - unfold int_of_string. + destruct (string_of_uint d) eqn:Hd. + + now destruct d. + + case Ascii.eqb_spec. + * intros ->. now destruct d. + * rewrite <- Hd, usu; auto. + - rewrite usu; auto. Qed. Lemma sis s d : - int_of_string s = Some d -> string_of_int d = s. + int_of_string s = Some d -> string_of_int d = s. Proof. - destruct s; [intros [= <-]| ]; simpl; trivial. - case Ascii.eqb_spec. - - intros ->. destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-]. - simpl; f_equal. now apply sus. - - destruct d; [ | now destruct uint_of_char]. - simpl string_of_int. - intros. apply sus; simpl. - destruct uint_of_char; simpl in *; congruence. + destruct s; [intros [= <-]| ]; simpl; trivial. + case Ascii.eqb_spec. + - intros ->. destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-]. + simpl; f_equal. now apply sus. + - destruct d; [ | now destruct uint_of_char]. + simpl string_of_int. + intros. apply sus; simpl. + destruct uint_of_char; simpl in *; congruence. Qed. End NilEmpty. @@ -157,109 +157,109 @@ End NilEmpty. Module NilZero. Definition string_of_uint (d:uint) := - match d with - | Nil => "0" - | _ => NilEmpty.string_of_uint d - end. + match d with + | Nil => "0" + | _ => NilEmpty.string_of_uint d + end. Definition uint_of_string s := - match s with - | EmptyString => None - | _ => NilEmpty.uint_of_string s - end. + match s with + | EmptyString => None + | _ => NilEmpty.uint_of_string s + end. Definition string_of_int (d:int) := - match d with - | Pos d => string_of_uint d - | Neg d => String "-" (string_of_uint d) - end. + match d with + | Pos d => string_of_uint d + | Neg d => String "-" (string_of_uint d) + end. Definition int_of_string s := - match s with - | EmptyString => None - | String a s' => - if Ascii.eqb a "-" then option_map Neg (uint_of_string s') - else option_map Pos (uint_of_string s) - end. + match s with + | EmptyString => None + | String a s' => + if Ascii.eqb a "-" then option_map Neg (uint_of_string s') + else option_map Pos (uint_of_string s) + end. (** Corresponding proofs *) Lemma uint_of_string_nonnil s : uint_of_string s <> Some Nil. Proof. - destruct s; simpl. - - easy. - - destruct (NilEmpty.uint_of_string s); [intros H | intros [=]]. - apply uint_of_char_spec in H. - now intuition subst. + destruct s; simpl. + - easy. + - destruct (NilEmpty.uint_of_string s); [intros H | intros [=]]. + apply uint_of_char_spec in H. + now intuition subst. Qed. Lemma sus s d : uint_of_string s = Some d -> string_of_uint d = s. Proof. - destruct s; [intros [=] | intros H]. - apply NilEmpty.sus in H. now destruct d. + destruct s; [intros [=] | intros H]. + apply NilEmpty.sus in H. now destruct d. Qed. Lemma usu d : d<>Nil -> uint_of_string (string_of_uint d) = Some d. Proof. - destruct d; (now destruct 1) || (intros _; apply NilEmpty.usu). + destruct d; (now destruct 1) || (intros _; apply NilEmpty.usu). Qed. Lemma usu_nil : uint_of_string (string_of_uint Nil) = Some Decimal.zero. Proof. - reflexivity. + reflexivity. Qed. Lemma usu_gen d : uint_of_string (string_of_uint d) = Some d \/ uint_of_string (string_of_uint d) = Some Decimal.zero. Proof. - destruct d; (now right) || (left; now apply usu). + destruct d; (now right) || (left; now apply usu). Qed. Lemma isi d : d<>Pos Nil -> d<>Neg Nil -> int_of_string (string_of_int d) = Some d. Proof. - destruct d; simpl. - - intros H _. - unfold int_of_string. - destruct (string_of_uint d) eqn:Hd. - + now destruct d. - + case Ascii.eqb_spec. - * intros ->. now destruct d. - * rewrite <- Hd, usu; auto. now intros ->. - - intros _ H. - rewrite usu; auto. now intros ->. + destruct d; simpl. + - intros H _. + unfold int_of_string. + destruct (string_of_uint d) eqn:Hd. + + now destruct d. + + case Ascii.eqb_spec. + * intros ->. now destruct d. + * rewrite <- Hd, usu; auto. now intros ->. + - intros _ H. + rewrite usu; auto. now intros ->. Qed. Lemma isi_posnil : - int_of_string (string_of_int (Pos Nil)) = Some (Pos Decimal.zero). + int_of_string (string_of_int (Pos Nil)) = Some (Pos Decimal.zero). Proof. - reflexivity. + reflexivity. Qed. (** Warning! (-0) won't parse (compatibility with the behavior of Z). *) Lemma isi_negnil : - int_of_string (string_of_int (Neg Nil)) = Some (Neg (D0 Nil)). + int_of_string (string_of_int (Neg Nil)) = Some (Neg (D0 Nil)). Proof. - reflexivity. + reflexivity. Qed. Lemma sis s d : - int_of_string s = Some d -> string_of_int d = s. + int_of_string s = Some d -> string_of_int d = s. Proof. - destruct s; [intros [=]| ]; simpl. - case Ascii.eqb_spec. - - intros ->. destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-]. - simpl; f_equal. now apply sus. - - destruct d; [ | now destruct uint_of_char]. - simpl string_of_int. - intros. apply sus; simpl. - destruct uint_of_char; simpl in *; congruence. + destruct s; [intros [=]| ]; simpl. + case Ascii.eqb_spec. + - intros ->. destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-]. + simpl; f_equal. now apply sus. + - destruct d; [ | now destruct uint_of_char]. + simpl string_of_int. + intros. apply sus; simpl. + destruct uint_of_char; simpl in *; congruence. Qed. End NilZero. diff --git a/theories/Numbers/DecimalZ.v b/theories/Numbers/DecimalZ.v index 6055ebb5d3..69d8073fc7 100644 --- a/theories/Numbers/DecimalZ.v +++ b/theories/Numbers/DecimalZ.v @@ -17,59 +17,86 @@ Require Import Decimal DecimalFacts DecimalPos DecimalN ZArith. Lemma of_to (z:Z) : Z.of_int (Z.to_int z) = z. Proof. - destruct z; simpl. - - trivial. - - unfold Z.of_uint. rewrite DecimalPos.Unsigned.of_to. now destruct p. - - unfold Z.of_uint. rewrite DecimalPos.Unsigned.of_to. destruct p; auto. + destruct z; simpl. + - trivial. + - unfold Z.of_uint. rewrite DecimalPos.Unsigned.of_to. now destruct p. + - unfold Z.of_uint. rewrite DecimalPos.Unsigned.of_to. destruct p; auto. Qed. Lemma to_of (d:int) : Z.to_int (Z.of_int d) = norm d. Proof. - destruct d; simpl; unfold Z.to_int, Z.of_uint. - - rewrite <- (DecimalN.Unsigned.to_of d). unfold N.of_uint. - now destruct (Pos.of_uint d). - - destruct (Pos.of_uint d) eqn:Hd; simpl; f_equal. - + generalize (DecimalPos.Unsigned.to_of d). rewrite Hd. simpl. - intros H. symmetry in H. apply unorm_0 in H. now rewrite H. - + assert (Hp := DecimalPos.Unsigned.to_of d). rewrite Hd in Hp. simpl in *. - rewrite Hp. unfold unorm in *. - destruct (nzhead d); trivial. - generalize (DecimalPos.Unsigned.of_to p). now rewrite Hp. + destruct d; simpl; unfold Z.to_int, Z.of_uint. + - rewrite <- (DecimalN.Unsigned.to_of d). unfold N.of_uint. + now destruct (Pos.of_uint d). + - destruct (Pos.of_uint d) eqn:Hd; simpl; f_equal. + + generalize (DecimalPos.Unsigned.to_of d). rewrite Hd. simpl. + intros H. symmetry in H. apply unorm_0 in H. now rewrite H. + + assert (Hp := DecimalPos.Unsigned.to_of d). rewrite Hd in Hp. simpl in *. + rewrite Hp. unfold unorm in *. + destruct (nzhead d); trivial. + generalize (DecimalPos.Unsigned.of_to p). now rewrite Hp. Qed. (** Some consequences *) Lemma to_int_inj n n' : Z.to_int n = Z.to_int n' -> n = n'. Proof. - intro EQ. - now rewrite <- (of_to n), <- (of_to n'), EQ. + intro EQ. + now rewrite <- (of_to n), <- (of_to n'), EQ. Qed. Lemma to_int_surj d : exists n, Z.to_int n = norm d. Proof. - exists (Z.of_int d). apply to_of. + exists (Z.of_int d). apply to_of. Qed. Lemma of_int_norm d : Z.of_int (norm d) = Z.of_int d. Proof. - unfold Z.of_int, Z.of_uint. - destruct d. - - simpl. now rewrite DecimalPos.Unsigned.of_uint_norm. - - simpl. destruct (nzhead d) eqn:H; - [ induction d; simpl; auto; discriminate | - destruct (nzhead_nonzero _ _ H) | .. ]; - f_equal; f_equal; apply DecimalPos.Unsigned.of_iff; - unfold unorm; now rewrite H. + unfold Z.of_int, Z.of_uint. + destruct d. + - simpl. now rewrite DecimalPos.Unsigned.of_uint_norm. + - simpl. destruct (nzhead d) eqn:H; + [ induction d; simpl; auto; discriminate | + destruct (nzhead_nonzero _ _ H) | .. ]; + f_equal; f_equal; apply DecimalPos.Unsigned.of_iff; + unfold unorm; now rewrite H. Qed. Lemma of_inj d d' : - Z.of_int d = Z.of_int d' -> norm d = norm d'. + Z.of_int d = Z.of_int d' -> norm d = norm d'. Proof. - intros. rewrite <- !to_of. now f_equal. + intros. rewrite <- !to_of. now f_equal. Qed. Lemma of_iff d d' : Z.of_int d = Z.of_int d' <-> norm d = norm d'. Proof. - split. apply of_inj. intros E. rewrite <- of_int_norm, E. - apply of_int_norm. + split. apply of_inj. intros E. rewrite <- of_int_norm, E. + apply of_int_norm. +Qed. + +(** Various lemmas *) + +Lemma of_uint_iter_D0 d n : + Z.of_uint (app d (Nat.iter n D0 Nil)) = Nat.iter n (Z.mul 10) (Z.of_uint d). +Proof. + unfold Z.of_uint. + unfold app; rewrite <-rev_revapp. + rewrite Unsigned.of_lu_rev, Unsigned.of_lu_revapp. + rewrite <-!Unsigned.of_lu_rev, !rev_rev. + assert (H' : Pos.of_uint (Nat.iter n D0 Nil) = 0%N). + { now induction n; [|rewrite Unsigned.nat_iter_S]. } + rewrite H', N.add_0_l; clear H'. + induction n; [now simpl; rewrite N.mul_1_r|]. + rewrite !Unsigned.nat_iter_S, <-IHn. + simpl Unsigned.usize; rewrite N.pow_succ_r'. + rewrite !N2Z.inj_mul; simpl Z.of_N; ring. +Qed. + +Lemma of_int_iter_D0 d n : + Z.of_int (app_int d (Nat.iter n D0 Nil)) = Nat.iter n (Z.mul 10) (Z.of_int d). +Proof. + case d; clear d; intro d; simpl. + - now rewrite of_uint_iter_D0. + - rewrite of_uint_iter_D0; induction n; [now simpl|]. + rewrite !Unsigned.nat_iter_S, <-IHn; ring. Qed. diff --git a/theories/Numbers/HexadecimalFacts.v b/theories/Numbers/HexadecimalFacts.v new file mode 100644 index 0000000000..7328b2303d --- /dev/null +++ b/theories/Numbers/HexadecimalFacts.v @@ -0,0 +1,340 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** * HexadecimalFacts : some facts about Hexadecimal numbers *) + +Require Import Hexadecimal Arith. + +Scheme Equality for uint. + +Scheme Equality for int. + +Lemma rev_revapp d d' : + rev (revapp d d') = revapp d' d. +Proof. + revert d'. induction d; simpl; intros; now rewrite ?IHd. +Qed. + +Lemma rev_rev d : rev (rev d) = d. +Proof. + apply rev_revapp. +Qed. + +Lemma revapp_rev_nil d : revapp (rev d) Nil = d. +Proof. now fold (rev (rev d)); rewrite rev_rev. Qed. + +Lemma app_nil_r d : app d Nil = d. +Proof. now unfold app; rewrite revapp_rev_nil. Qed. + +Lemma app_int_nil_r d : app_int d Nil = d. +Proof. now case d; intro d'; simpl; rewrite app_nil_r. Qed. + +Lemma revapp_revapp_1 d d' d'' : + nb_digits d <= 1 -> + revapp (revapp d d') d'' = revapp d' (revapp d d''). +Proof. + now case d; clear d; intro d; + [|case d; clear d; intro d; + [|simpl; case nb_digits; [|intros n]; intros Hn; exfalso; + [apply (Nat.nle_succ_diag_l _ Hn)| + apply (Nat.nle_succ_0 _ (le_S_n _ _ Hn))]..]..]. +Qed. + +Lemma nb_digits_pos d : d <> Nil -> 0 < nb_digits d. +Proof. now case d; [|intros d' _; apply Nat.lt_0_succ..]. Qed. + +Lemma nb_digits_revapp d d' : + nb_digits (revapp d d') = nb_digits d + nb_digits d'. +Proof. + now revert d'; induction d; [|intro d'; simpl; rewrite IHd; simpl..]. +Qed. + +Lemma nb_digits_rev u : nb_digits (rev u) = nb_digits u. +Proof. now unfold rev; rewrite nb_digits_revapp. Qed. + +Lemma nb_digits_nzhead u : nb_digits (nzhead u) <= nb_digits u. +Proof. now induction u; [|apply le_S|..]. Qed. + +Lemma nb_digits_iter_D0 n d : + nb_digits (Nat.iter n D0 d) = n + nb_digits d. +Proof. now induction n; simpl; [|rewrite IHn]. Qed. + +Fixpoint nth n u := + match n with + | O => + match u with + | Nil => Nil + | D0 d => D0 Nil + | D1 d => D1 Nil + | D2 d => D2 Nil + | D3 d => D3 Nil + | D4 d => D4 Nil + | D5 d => D5 Nil + | D6 d => D6 Nil + | D7 d => D7 Nil + | D8 d => D8 Nil + | D9 d => D9 Nil + | Da d => Da Nil + | Db d => Db Nil + | Dc d => Dc Nil + | Dd d => Dd Nil + | De d => De Nil + | Df d => Df Nil + end + | S n => + match u with + | Nil => Nil + | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d + | Da d | Db d | Dc d | Dd d | De d | Df d => + nth n d + end + end. + +Lemma nb_digits_nth n u : nb_digits (nth n u) <= 1. +Proof. + revert u; induction n. + - now intro u; case u; [apply Nat.le_0_1|..]. + - intro u; case u; [apply Nat.le_0_1|intro u'; apply IHn..]. +Qed. + +Lemma nth_revapp_r n d d' : + nb_digits d <= n -> + nth n (revapp d d') = nth (n - nb_digits d) d'. +Proof. + revert d d'; induction n; intro d. + - now case d; intro d'; + [case d'|intros d'' H; exfalso; revert H; apply Nat.nle_succ_0..]. + - now induction d; + [intro d'; case d'| + intros d' H; + simpl revapp; rewrite IHd; [|now apply le_Sn_le]; + rewrite Nat.sub_succ_l; [|now apply le_S_n]; + simpl; rewrite <-(IHn _ _ (le_S_n _ _ H))..]. +Qed. + +Lemma nth_revapp_l n d d' : + n < nb_digits d -> + nth n (revapp d d') = nth (nb_digits d - n - 1) d. +Proof. + revert d d'; induction n; intro d. + - rewrite Nat.sub_0_r. + now induction d; + [|intros d' _; simpl revapp; + revert IHd; case d; clear d; [|intro d..]; intro IHd; + [|rewrite IHd; [simpl nb_digits; rewrite (Nat.sub_succ_l _ (S _))|]; + [|apply le_n_S, Nat.le_0_l..]..]..]. + - now induction d; + [|intros d' H; + simpl revapp; simpl nb_digits; + simpl in H; generalize (lt_S_n _ _ H); clear H; intro H; + case (le_lt_eq_dec _ _ H); clear H; intro H; + [rewrite (IHd _ H), Nat.sub_succ_l; + [rewrite Nat.sub_succ_l; [|apply Nat.le_add_le_sub_r]| + apply le_Sn_le]| + rewrite nth_revapp_r; rewrite <-H; + [rewrite Nat.sub_succ, Nat.sub_succ_l; [rewrite !Nat.sub_diag|]|]]..]. +Qed. + +(** Normalization on little-endian numbers *) + +Fixpoint nztail d := + match d with + | Nil => Nil + | D0 d => match nztail d with Nil => Nil | d' => D0 d' end + | D1 d => D1 (nztail d) + | D2 d => D2 (nztail d) + | D3 d => D3 (nztail d) + | D4 d => D4 (nztail d) + | D5 d => D5 (nztail d) + | D6 d => D6 (nztail d) + | D7 d => D7 (nztail d) + | D8 d => D8 (nztail d) + | D9 d => D9 (nztail d) + | Da d => Da (nztail d) + | Db d => Db (nztail d) + | Dc d => Dc (nztail d) + | Dd d => Dd (nztail d) + | De d => De (nztail d) + | Df d => Df (nztail d) + end. + +Definition lnorm d := + match nztail d with + | Nil => zero + | d => d + end. + +Lemma nzhead_revapp_0 d d' : nztail d = Nil -> + nzhead (revapp d d') = nzhead d'. +Proof. + revert d'. induction d; intros d' [=]; simpl; trivial. + destruct (nztail d); now rewrite IHd. +Qed. + +Lemma nzhead_revapp d d' : nztail d <> Nil -> + nzhead (revapp d d') = revapp (nztail d) d'. +Proof. + revert d'. + induction d; intros d' H; simpl in *; + try destruct (nztail d) eqn:E; + (now rewrite ?nzhead_revapp_0) || (now rewrite IHd). +Qed. + +Lemma nzhead_rev d : nztail d <> Nil -> + nzhead (rev d) = rev (nztail d). +Proof. + apply nzhead_revapp. +Qed. + +Lemma rev_nztail_rev d : + rev (nztail (rev d)) = nzhead d. +Proof. + destruct (uint_eq_dec (nztail (rev d)) Nil) as [H|H]. + - rewrite H. unfold rev; simpl. + rewrite <- (rev_rev d). symmetry. + now apply nzhead_revapp_0. + - now rewrite <- nzhead_rev, rev_rev. +Qed. + +Lemma nzhead_D0 u : nzhead (D0 u) = nzhead u. +Proof. reflexivity. Qed. + +Lemma nzhead_iter_D0 n u : nzhead (Nat.iter n D0 u) = nzhead u. +Proof. now induction n. Qed. + +Lemma revapp_nil_inv d d' : revapp d d' = Nil -> d = Nil /\ d' = Nil. +Proof. + revert d'. + induction d; simpl; intros d' H; auto; now apply IHd in H. +Qed. + +Lemma rev_nil_inv d : rev d = Nil -> d = Nil. +Proof. + apply revapp_nil_inv. +Qed. + +Lemma rev_lnorm_rev d : + rev (lnorm (rev d)) = unorm d. +Proof. + unfold unorm, lnorm. + rewrite <- rev_nztail_rev. + destruct nztail; simpl; trivial; + destruct rev eqn:E; trivial; now apply rev_nil_inv in E. +Qed. + +Lemma nzhead_nonzero d d' : nzhead d <> D0 d'. +Proof. + induction d; easy. +Qed. + +Lemma unorm_0 d : unorm d = zero <-> nzhead d = Nil. +Proof. + unfold unorm. split. + - generalize (nzhead_nonzero d). + destruct nzhead; intros H [=]; trivial. now destruct (H u). + - now intros ->. +Qed. + +Lemma unorm_nonnil d : unorm d <> Nil. +Proof. + unfold unorm. now destruct nzhead. +Qed. + +Lemma unorm_D0 u : unorm (D0 u) = unorm u. +Proof. reflexivity. Qed. + +Lemma unorm_iter_D0 n u : unorm (Nat.iter n D0 u) = unorm u. +Proof. now induction n. Qed. + +Lemma nb_digits_unorm u : + u <> Nil -> nb_digits (unorm u) <= nb_digits u. +Proof. + case u; clear u; [now simpl|intro u..]; [|now simpl..]. + intros _; unfold unorm. + case_eq (nzhead (D0 u)); [|now intros u' <-; apply nb_digits_nzhead..]. + intros _; apply le_n_S, Nat.le_0_l. +Qed. + +Lemma nzhead_invol d : nzhead (nzhead d) = nzhead d. +Proof. + now induction d. +Qed. + +Lemma nztail_invol d : nztail (nztail d) = nztail d. +Proof. + rewrite <-(rev_rev (nztail _)), <-(rev_rev (nztail d)), <-(rev_rev d). + now rewrite !rev_nztail_rev, nzhead_invol. +Qed. + +Lemma unorm_invol d : unorm (unorm d) = unorm d. +Proof. + unfold unorm. + destruct (nzhead d) eqn:E; trivial. + destruct (nzhead_nonzero _ _ E). +Qed. + +Lemma norm_invol d : norm (norm d) = norm d. +Proof. + unfold norm. + destruct d. + - f_equal. apply unorm_invol. + - destruct (nzhead d) eqn:E; auto. + destruct (nzhead_nonzero _ _ E). +Qed. + +Lemma nzhead_app_nzhead d d' : + nzhead (app (nzhead d) d') = nzhead (app d d'). +Proof. + unfold app. + rewrite <-(rev_nztail_rev d), rev_rev. + generalize (rev d); clear d; intro d. + generalize (nzhead_revapp_0 d d'). + generalize (nzhead_revapp d d'). + generalize (nzhead_revapp_0 (nztail d) d'). + generalize (nzhead_revapp (nztail d) d'). + rewrite nztail_invol. + now case nztail; + [intros _ H _ H'; rewrite (H eq_refl), (H' eq_refl) + |intros d'' H _ H' _; rewrite H; [rewrite H'|]..]. +Qed. + +Lemma unorm_app_unorm d d' : + unorm (app (unorm d) d') = unorm (app d d'). +Proof. + unfold unorm. + rewrite <-(nzhead_app_nzhead d d'). + now case (nzhead d). +Qed. + +Lemma norm_app_int_norm d d' : + unorm d' = zero -> + norm (app_int (norm d) d') = norm (app_int d d'). +Proof. + case d; clear d; intro d; simpl. + - now rewrite unorm_app_unorm. + - unfold app_int, app. + rewrite unorm_0; intro Hd'. + rewrite <-rev_nztail_rev. + generalize (nzhead_revapp (rev d) d'). + generalize (nzhead_revapp_0 (rev d) d'). + now case_eq (nztail (rev d)); + [intros Hd'' H _; rewrite (H eq_refl); simpl; + unfold unorm; simpl; rewrite Hd' + |intros d'' Hd'' _ H; rewrite H; clear H; [|now simpl]; + set (r := rev _); + set (m := match r with Nil => Pos zero | _ => _ end); + assert (H' : m = Neg r); + [now unfold m; case_eq r; unfold r; + [intro H''; generalize (rev_nil_inv _ H'')|..] + |rewrite H'; unfold r; clear m r H']; + unfold norm; + rewrite rev_rev, <-Hd''; + rewrite nzhead_revapp; rewrite nztail_invol; [|rewrite Hd'']..]. +Qed. diff --git a/theories/Numbers/HexadecimalN.v b/theories/Numbers/HexadecimalN.v new file mode 100644 index 0000000000..f333e2b7f6 --- /dev/null +++ b/theories/Numbers/HexadecimalN.v @@ -0,0 +1,107 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** * HexadecimalN + + Proofs that conversions between hexadecimal numbers and [N] + are bijections *) + +Require Import Hexadecimal HexadecimalFacts HexadecimalPos PArith NArith. + +Module Unsigned. + +Lemma of_to (n:N) : N.of_hex_uint (N.to_hex_uint n) = n. +Proof. + destruct n. + - reflexivity. + - apply HexadecimalPos.Unsigned.of_to. +Qed. + +Lemma to_of (d:uint) : N.to_hex_uint (N.of_hex_uint d) = unorm d. +Proof. + exact (HexadecimalPos.Unsigned.to_of d). +Qed. + +Lemma to_uint_inj n n' : N.to_hex_uint n = N.to_hex_uint n' -> n = n'. +Proof. + intros E. now rewrite <- (of_to n), <- (of_to n'), E. +Qed. + +Lemma to_uint_surj d : exists p, N.to_hex_uint p = unorm d. +Proof. + exists (N.of_hex_uint d). apply to_of. +Qed. + +Lemma of_uint_norm d : N.of_hex_uint (unorm d) = N.of_hex_uint d. +Proof. + now induction d. +Qed. + +Lemma of_inj d d' : + N.of_hex_uint d = N.of_hex_uint d' -> unorm d = unorm d'. +Proof. + intros. rewrite <- !to_of. now f_equal. +Qed. + +Lemma of_iff d d' : N.of_hex_uint d = N.of_hex_uint d' <-> unorm d = unorm d'. +Proof. + split. apply of_inj. intros E. rewrite <- of_uint_norm, E. + apply of_uint_norm. +Qed. + +End Unsigned. + +(** Conversion from/to signed hexadecimal numbers *) + +Module Signed. + +Lemma of_to (n:N) : N.of_hex_int (N.to_hex_int n) = Some n. +Proof. + unfold N.to_hex_int, N.of_hex_int, norm. f_equal. + rewrite Unsigned.of_uint_norm. apply Unsigned.of_to. +Qed. + +Lemma to_of (d:int)(n:N) : N.of_hex_int d = Some n -> N.to_hex_int n = norm d. +Proof. + unfold N.of_hex_int. + destruct (norm d) eqn:Hd; intros [= <-]. + unfold N.to_hex_int. rewrite Unsigned.to_of. f_equal. + revert Hd; destruct d; simpl. + - intros [= <-]. apply unorm_invol. + - destruct (nzhead d); now intros [= <-]. +Qed. + +Lemma to_int_inj n n' : N.to_hex_int n = N.to_hex_int n' -> n = n'. +Proof. + intro E. + assert (E' : Some n = Some n'). + { now rewrite <- (of_to n), <- (of_to n'), E. } + now injection E'. +Qed. + +Lemma to_int_pos_surj d : exists n, N.to_hex_int n = norm (Pos d). +Proof. + exists (N.of_hex_uint d). unfold N.to_hex_int. now rewrite Unsigned.to_of. +Qed. + +Lemma of_int_norm d : N.of_hex_int (norm d) = N.of_hex_int d. +Proof. + unfold N.of_hex_int. now rewrite norm_invol. +Qed. + +Lemma of_inj_pos d d' : + N.of_hex_int (Pos d) = N.of_hex_int (Pos d') -> unorm d = unorm d'. +Proof. + unfold N.of_hex_int. simpl. intros [= H]. apply Unsigned.of_inj. + change Pos.of_hex_uint with N.of_hex_uint in H. + now rewrite <- Unsigned.of_uint_norm, H, Unsigned.of_uint_norm. +Qed. + +End Signed. diff --git a/theories/Numbers/HexadecimalNat.v b/theories/Numbers/HexadecimalNat.v new file mode 100644 index 0000000000..b05184e821 --- /dev/null +++ b/theories/Numbers/HexadecimalNat.v @@ -0,0 +1,321 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** * HexadecimalNat + + Proofs that conversions between hexadecimal numbers and [nat] + are bijections. *) + +Require Import Hexadecimal HexadecimalFacts Arith. + +Module Unsigned. + +(** A few helper functions used during proofs *) + +Definition hd d := + match d with + | Nil => 0x0 + | D0 _ => 0x0 + | D1 _ => 0x1 + | D2 _ => 0x2 + | D3 _ => 0x3 + | D4 _ => 0x4 + | D5 _ => 0x5 + | D6 _ => 0x6 + | D7 _ => 0x7 + | D8 _ => 0x8 + | D9 _ => 0x9 + | Da _ => 0xa + | Db _ => 0xb + | Dc _ => 0xc + | Dd _ => 0xd + | De _ => 0xe + | Df _ => 0xf + end. + +Definition tl d := + match d with + | Nil => d + | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d + | Da d | Db d | Dc d | Dd d | De d | Df d => d + end. + +Fixpoint usize (d:uint) : nat := + match d with + | Nil => 0 + | D0 d => S (usize d) + | D1 d => S (usize d) + | D2 d => S (usize d) + | D3 d => S (usize d) + | D4 d => S (usize d) + | D5 d => S (usize d) + | D6 d => S (usize d) + | D7 d => S (usize d) + | D8 d => S (usize d) + | D9 d => S (usize d) + | Da d => S (usize d) + | Db d => S (usize d) + | Dc d => S (usize d) + | Dd d => S (usize d) + | De d => S (usize d) + | Df d => S (usize d) + end. + +(** A direct version of [to_little_uint], not tail-recursive *) +Fixpoint to_lu n := + match n with + | 0 => Hexadecimal.zero + | S n => Little.succ (to_lu n) + end. + +(** A direct version of [of_little_uint] *) +Fixpoint of_lu (d:uint) : nat := + match d with + | Nil => 0x0 + | D0 d => 0x10 * of_lu d + | D1 d => 0x1 + 0x10 * of_lu d + | D2 d => 0x2 + 0x10 * of_lu d + | D3 d => 0x3 + 0x10 * of_lu d + | D4 d => 0x4 + 0x10 * of_lu d + | D5 d => 0x5 + 0x10 * of_lu d + | D6 d => 0x6 + 0x10 * of_lu d + | D7 d => 0x7 + 0x10 * of_lu d + | D8 d => 0x8 + 0x10 * of_lu d + | D9 d => 0x9 + 0x10 * of_lu d + | Da d => 0xa + 0x10 * of_lu d + | Db d => 0xb + 0x10 * of_lu d + | Dc d => 0xc + 0x10 * of_lu d + | Dd d => 0xd + 0x10 * of_lu d + | De d => 0xe + 0x10 * of_lu d + | Df d => 0xf + 0x10 * of_lu d + end. + +(** Properties of [to_lu] *) + +Lemma to_lu_succ n : to_lu (S n) = Little.succ (to_lu n). +Proof. + reflexivity. +Qed. + +Lemma to_little_uint_succ n d : + Nat.to_little_hex_uint n (Little.succ d) = + Little.succ (Nat.to_little_hex_uint n d). +Proof. + revert d; induction n; simpl; trivial. +Qed. + +Lemma to_lu_equiv n : + to_lu n = Nat.to_little_hex_uint n zero. +Proof. + induction n; simpl; trivial. + now rewrite IHn, <- to_little_uint_succ. +Qed. + +Lemma to_uint_alt n : + Nat.to_hex_uint n = rev (to_lu n). +Proof. + unfold Nat.to_hex_uint. f_equal. symmetry. apply to_lu_equiv. +Qed. + +(** Properties of [of_lu] *) + +Lemma of_lu_eqn d : + of_lu d = hd d + 0x10 * of_lu (tl d). +Proof. + induction d; simpl; trivial. +Qed. + +Ltac simpl_of_lu := + match goal with + | |- context [ of_lu (?f ?x) ] => + rewrite (of_lu_eqn (f x)); simpl hd; simpl tl + end. + +Lemma of_lu_succ d : + of_lu (Little.succ d) = S (of_lu d). +Proof. + induction d; trivial. + simpl_of_lu. rewrite IHd. simpl_of_lu. + now rewrite Nat.mul_succ_r, <- (Nat.add_comm 0x10). +Qed. + +Lemma of_to_lu n : + of_lu (to_lu n) = n. +Proof. + induction n; simpl; trivial. rewrite of_lu_succ. now f_equal. +Qed. + +Lemma of_lu_revapp d d' : + of_lu (revapp d d') = + of_lu (rev d) + of_lu d' * 0x10^usize d. +Proof. + revert d'. + induction d; intro d'; simpl usize; + [ simpl; now rewrite Nat.mul_1_r | .. ]; + unfold rev; simpl revapp; rewrite 2 IHd; + rewrite <- Nat.add_assoc; f_equal; simpl_of_lu; simpl of_lu; + rewrite Nat.pow_succ_r'; ring. +Qed. + +Lemma of_uint_acc_spec n d : + Nat.of_hex_uint_acc d n = of_lu (rev d) + n * 0x10^usize d. +Proof. + revert n. induction d; intros; + simpl Nat.of_hex_uint_acc; rewrite ?Nat.tail_mul_spec, ?IHd; + simpl rev; simpl usize; rewrite ?Nat.pow_succ_r'; + [ simpl; now rewrite Nat.mul_1_r | .. ]; + unfold rev at 2; simpl revapp; rewrite of_lu_revapp; + simpl of_lu; ring. +Qed. + +Lemma of_uint_alt d : Nat.of_hex_uint d = of_lu (rev d). +Proof. + unfold Nat.of_hex_uint. now rewrite of_uint_acc_spec. +Qed. + +(** First main bijection result *) + +Lemma of_to (n:nat) : Nat.of_hex_uint (Nat.to_hex_uint n) = n. +Proof. + rewrite to_uint_alt, of_uint_alt, rev_rev. apply of_to_lu. +Qed. + +(** The other direction *) + +Lemma to_lu_sixteenfold n : n<>0 -> + to_lu (0x10 * n) = D0 (to_lu n). +Proof. + induction n. + - simpl. now destruct 1. + - intros _. + destruct (Nat.eq_dec n 0) as [->|H]; simpl; trivial. + rewrite !Nat.add_succ_r. + simpl in *. rewrite (IHn H). now destruct (to_lu n). +Qed. + +Lemma of_lu_0 d : of_lu d = 0 <-> nztail d = Nil. +Proof. + induction d; try simpl_of_lu; try easy. + rewrite Nat.add_0_l. + split; intros H. + - apply Nat.eq_mul_0_r in H; auto. + rewrite IHd in H. simpl. now rewrite H. + - simpl in H. destruct (nztail d); try discriminate. + now destruct IHd as [_ ->]. +Qed. + +Lemma to_of_lu_sixteenfold d : + to_lu (of_lu d) = lnorm d -> + to_lu (0x10 * of_lu d) = lnorm (D0 d). +Proof. + intro IH. + destruct (Nat.eq_dec (of_lu d) 0) as [H|H]. + - rewrite H. simpl. rewrite of_lu_0 in H. + unfold lnorm. simpl. now rewrite H. + - rewrite (to_lu_sixteenfold _ H), IH. + rewrite of_lu_0 in H. + unfold lnorm. simpl. now destruct (nztail d). +Qed. + +Lemma to_of_lu d : to_lu (of_lu d) = lnorm d. +Proof. + induction d; [ reflexivity | .. ]; + simpl_of_lu; + rewrite ?Nat.add_succ_l, Nat.add_0_l, ?to_lu_succ, to_of_lu_sixteenfold + by assumption; + unfold lnorm; simpl; now destruct nztail. +Qed. + +(** Second bijection result *) + +Lemma to_of (d:uint) : Nat.to_hex_uint (Nat.of_hex_uint d) = unorm d. +Proof. + rewrite to_uint_alt, of_uint_alt, to_of_lu. + apply rev_lnorm_rev. +Qed. + +(** Some consequences *) + +Lemma to_uint_inj n n' : Nat.to_hex_uint n = Nat.to_hex_uint n' -> n = n'. +Proof. + intro EQ. + now rewrite <- (of_to n), <- (of_to n'), EQ. +Qed. + +Lemma to_uint_surj d : exists n, Nat.to_hex_uint n = unorm d. +Proof. + exists (Nat.of_hex_uint d). apply to_of. +Qed. + +Lemma of_uint_norm d : Nat.of_hex_uint (unorm d) = Nat.of_hex_uint d. +Proof. + unfold Nat.of_hex_uint. now induction d. +Qed. + +Lemma of_inj d d' : + Nat.of_hex_uint d = Nat.of_hex_uint d' -> unorm d = unorm d'. +Proof. + intros. rewrite <- !to_of. now f_equal. +Qed. + +Lemma of_iff d d' : Nat.of_hex_uint d = Nat.of_hex_uint d' <-> unorm d = unorm d'. +Proof. + split. apply of_inj. intros E. rewrite <- of_uint_norm, E. + apply of_uint_norm. +Qed. + +End Unsigned. + +(** Conversion from/to signed hexadecimal numbers *) + +Module Signed. + +Lemma of_to (n:nat) : Nat.of_hex_int (Nat.to_hex_int n) = Some n. +Proof. + unfold Nat.to_hex_int, Nat.of_hex_int, norm. f_equal. + rewrite Unsigned.of_uint_norm. apply Unsigned.of_to. +Qed. + +Lemma to_of (d:int)(n:nat) : Nat.of_hex_int d = Some n -> Nat.to_hex_int n = norm d. +Proof. + unfold Nat.of_hex_int. + destruct (norm d) eqn:Hd; intros [= <-]. + unfold Nat.to_hex_int. rewrite Unsigned.to_of. f_equal. + revert Hd; destruct d; simpl. + - intros [= <-]. apply unorm_invol. + - destruct (nzhead d); now intros [= <-]. +Qed. + +Lemma to_int_inj n n' : Nat.to_hex_int n = Nat.to_hex_int n' -> n = n'. +Proof. + intro E. + assert (E' : Some n = Some n'). + { now rewrite <- (of_to n), <- (of_to n'), E. } + now injection E'. +Qed. + +Lemma to_int_pos_surj d : exists n, Nat.to_hex_int n = norm (Pos d). +Proof. + exists (Nat.of_hex_uint d). unfold Nat.to_hex_int. now rewrite Unsigned.to_of. +Qed. + +Lemma of_int_norm d : Nat.of_hex_int (norm d) = Nat.of_hex_int d. +Proof. + unfold Nat.of_hex_int. now rewrite norm_invol. +Qed. + +Lemma of_inj_pos d d' : + Nat.of_hex_int (Pos d) = Nat.of_hex_int (Pos d') -> unorm d = unorm d'. +Proof. + unfold Nat.of_hex_int. simpl. intros [= H]. apply Unsigned.of_inj. + now rewrite <- Unsigned.of_uint_norm, H, Unsigned.of_uint_norm. +Qed. + +End Signed. diff --git a/theories/Numbers/HexadecimalPos.v b/theories/Numbers/HexadecimalPos.v new file mode 100644 index 0000000000..47f6d983b7 --- /dev/null +++ b/theories/Numbers/HexadecimalPos.v @@ -0,0 +1,446 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** * HexadecimalPos + + Proofs that conversions between hexadecimal numbers and [positive] + are bijections. *) + +Require Import Hexadecimal HexadecimalFacts PArith NArith. + +Module Unsigned. + +Local Open Scope N. + +(** A direct version of [of_little_uint] *) +Fixpoint of_lu (d:uint) : N := + match d with + | Nil => 0 + | D0 d => 0x10 * of_lu d + | D1 d => 0x1 + 0x10 * of_lu d + | D2 d => 0x2 + 0x10 * of_lu d + | D3 d => 0x3 + 0x10 * of_lu d + | D4 d => 0x4 + 0x10 * of_lu d + | D5 d => 0x5 + 0x10 * of_lu d + | D6 d => 0x6 + 0x10 * of_lu d + | D7 d => 0x7 + 0x10 * of_lu d + | D8 d => 0x8 + 0x10 * of_lu d + | D9 d => 0x9 + 0x10 * of_lu d + | Da d => 0xa + 0x10 * of_lu d + | Db d => 0xb + 0x10 * of_lu d + | Dc d => 0xc + 0x10 * of_lu d + | Dd d => 0xd + 0x10 * of_lu d + | De d => 0xe + 0x10 * of_lu d + | Df d => 0xf + 0x10 * of_lu d + end. + +Definition hd d := + match d with + | Nil => 0x0 + | D0 _ => 0x0 + | D1 _ => 0x1 + | D2 _ => 0x2 + | D3 _ => 0x3 + | D4 _ => 0x4 + | D5 _ => 0x5 + | D6 _ => 0x6 + | D7 _ => 0x7 + | D8 _ => 0x8 + | D9 _ => 0x9 + | Da _ => 0xa + | Db _ => 0xb + | Dc _ => 0xc + | Dd _ => 0xd + | De _ => 0xe + | Df _ => 0xf + end. + +Definition tl d := + match d with + | Nil => d + | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d + | Da d | Db d | Dc d | Dd d | De d | Df d => d + end. + +Lemma of_lu_eqn d : + of_lu d = hd d + 0x10 * (of_lu (tl d)). +Proof. + induction d; simpl; trivial. +Qed. + +Ltac simpl_of_lu := + match goal with + | |- context [ of_lu (?f ?x) ] => + rewrite (of_lu_eqn (f x)); simpl hd; simpl tl + end. + +Fixpoint usize (d:uint) : N := + match d with + | Nil => 0 + | D0 d => N.succ (usize d) + | D1 d => N.succ (usize d) + | D2 d => N.succ (usize d) + | D3 d => N.succ (usize d) + | D4 d => N.succ (usize d) + | D5 d => N.succ (usize d) + | D6 d => N.succ (usize d) + | D7 d => N.succ (usize d) + | D8 d => N.succ (usize d) + | D9 d => N.succ (usize d) + | Da d => N.succ (usize d) + | Db d => N.succ (usize d) + | Dc d => N.succ (usize d) + | Dd d => N.succ (usize d) + | De d => N.succ (usize d) + | Df d => N.succ (usize d) + end. + +Lemma of_lu_revapp d d' : + of_lu (revapp d d') = + of_lu (rev d) + of_lu d' * 0x10^usize d. +Proof. + revert d'. + induction d; simpl; intro d'; [ now rewrite N.mul_1_r | .. ]; + unfold rev; simpl revapp; rewrite 2 IHd; + rewrite <- N.add_assoc; f_equal; simpl_of_lu; simpl of_lu; + rewrite N.pow_succ_r'; ring. +Qed. + +Definition Nadd n p := + match n with + | N0 => p + | Npos p0 => (p0+p)%positive + end. + +Lemma Nadd_simpl n p q : Npos (Nadd n (p * q)) = n + Npos p * Npos q. +Proof. + now destruct n. +Qed. + +Lemma of_uint_acc_eqn d acc : d<>Nil -> + Pos.of_hex_uint_acc d acc = Pos.of_hex_uint_acc (tl d) (Nadd (hd d) (0x10*acc)). +Proof. + destruct d; simpl; trivial. now destruct 1. +Qed. + +Lemma of_uint_acc_rev d acc : + Npos (Pos.of_hex_uint_acc d acc) = + of_lu (rev d) + (Npos acc) * 0x10^usize d. +Proof. + revert acc. + induction d; intros; simpl usize; + [ simpl; now rewrite Pos.mul_1_r | .. ]; + rewrite N.pow_succ_r'; + unfold rev; simpl revapp; try rewrite of_lu_revapp; simpl of_lu; + rewrite of_uint_acc_eqn by easy; simpl tl; simpl hd; + rewrite IHd, Nadd_simpl; ring. +Qed. + +Lemma of_uint_alt d : Pos.of_hex_uint d = of_lu (rev d). +Proof. + induction d; simpl; trivial; unfold rev; simpl revapp; + rewrite of_lu_revapp; simpl of_lu; try apply of_uint_acc_rev. + rewrite IHd. ring. +Qed. + +Lemma of_lu_rev d : Pos.of_hex_uint (rev d) = of_lu d. +Proof. + rewrite of_uint_alt. now rewrite rev_rev. +Qed. + +Lemma of_lu_double_gen d : + of_lu (Little.double d) = N.double (of_lu d) /\ + of_lu (Little.succ_double d) = N.succ_double (of_lu d). +Proof. + rewrite N.double_spec, N.succ_double_spec. + induction d; try destruct IHd as (IH1,IH2); + simpl Little.double; simpl Little.succ_double; + repeat (simpl_of_lu; rewrite ?IH1, ?IH2); split; reflexivity || ring. +Qed. + +Lemma of_lu_double d : + of_lu (Little.double d) = N.double (of_lu d). +Proof. + apply of_lu_double_gen. +Qed. + +Lemma of_lu_succ_double d : + of_lu (Little.succ_double d) = N.succ_double (of_lu d). +Proof. + apply of_lu_double_gen. +Qed. + +(** First bijection result *) + +Lemma of_to (p:positive) : Pos.of_hex_uint (Pos.to_hex_uint p) = Npos p. +Proof. + unfold Pos.to_hex_uint. + rewrite of_lu_rev. + induction p; simpl; trivial. + - now rewrite of_lu_succ_double, IHp. + - now rewrite of_lu_double, IHp. +Qed. + +(** The other direction *) + +Definition to_lu n := + match n with + | N0 => Hexadecimal.zero + | Npos p => Pos.to_little_hex_uint p + end. + +Lemma succ_double_alt d : + Little.succ_double d = Little.succ (Little.double d). +Proof. + now induction d. +Qed. + +Lemma double_succ d : + Little.double (Little.succ d) = + Little.succ (Little.succ_double d). +Proof. + induction d; simpl; f_equal; auto using succ_double_alt. +Qed. + +Lemma to_lu_succ n : + to_lu (N.succ n) = Little.succ (to_lu n). +Proof. + destruct n; simpl; trivial. + induction p; simpl; rewrite ?IHp; + auto using succ_double_alt, double_succ. +Qed. + +Lemma nat_iter_S n {A} (f:A->A) i : + Nat.iter (S n) f i = f (Nat.iter n f i). +Proof. + reflexivity. +Qed. + +Lemma nat_iter_0 {A} (f:A->A) i : Nat.iter 0 f i = i. +Proof. + reflexivity. +Qed. + +Lemma to_lhex_tenfold p : + to_lu (0x10 * Npos p) = D0 (to_lu (Npos p)). +Proof. + induction p using Pos.peano_rect. + - trivial. + - change (N.pos (Pos.succ p)) with (N.succ (N.pos p)). + rewrite N.mul_succ_r. + change 0x10 at 2 with (Nat.iter 0x10%nat N.succ 0). + rewrite ?nat_iter_S, nat_iter_0. + rewrite !N.add_succ_r, N.add_0_r, !to_lu_succ, IHp. + destruct (to_lu (N.pos p)); simpl; auto. +Qed. + +Lemma of_lu_0 d : of_lu d = 0 <-> nztail d = Nil. +Proof. + induction d; try simpl_of_lu; split; trivial; try discriminate; + try (intros H; now apply N.eq_add_0 in H). + - rewrite N.add_0_l. intros H. + apply N.eq_mul_0_r in H; [|easy]. rewrite IHd in H. + simpl. now rewrite H. + - simpl. destruct (nztail d); try discriminate. + now destruct IHd as [_ ->]. +Qed. + +Lemma to_of_lu_tenfold d : + to_lu (of_lu d) = lnorm d -> + to_lu (0x10 * of_lu d) = lnorm (D0 d). +Proof. + intro IH. + destruct (N.eq_dec (of_lu d) 0) as [H|H]. + - rewrite H. simpl. rewrite of_lu_0 in H. + unfold lnorm. simpl. now rewrite H. + - destruct (of_lu d) eqn:Eq; [easy| ]. + rewrite to_lhex_tenfold; auto. rewrite IH. + rewrite <- Eq in H. rewrite of_lu_0 in H. + unfold lnorm. simpl. now destruct (nztail d). +Qed. + +Lemma Nadd_alt n m : n + m = Nat.iter (N.to_nat n) N.succ m. +Proof. + destruct n. trivial. + induction p using Pos.peano_rect. + - now rewrite N.add_1_l. + - change (N.pos (Pos.succ p)) with (N.succ (N.pos p)). + now rewrite N.add_succ_l, IHp, N2Nat.inj_succ. +Qed. + +Ltac simpl_to_nat := simpl N.to_nat; unfold Pos.to_nat; simpl Pos.iter_op. + +Lemma to_of_lu d : to_lu (of_lu d) = lnorm d. +Proof. + induction d; [reflexivity|..]; + simpl_of_lu; rewrite Nadd_alt; simpl_to_nat; + rewrite ?nat_iter_S, nat_iter_0, ?to_lu_succ, to_of_lu_tenfold by assumption; + unfold lnorm; simpl; destruct nztail; auto. +Qed. + +(** Second bijection result *) + +Lemma to_of (d:uint) : N.to_hex_uint (Pos.of_hex_uint d) = unorm d. +Proof. + rewrite of_uint_alt. + unfold N.to_hex_uint, Pos.to_hex_uint. + destruct (of_lu (rev d)) eqn:H. + - rewrite of_lu_0 in H. rewrite <- rev_lnorm_rev. + unfold lnorm. now rewrite H. + - change (Pos.to_little_hex_uint p) with (to_lu (N.pos p)). + rewrite <- H. rewrite to_of_lu. apply rev_lnorm_rev. +Qed. + +(** Some consequences *) + +Lemma to_uint_nonzero p : Pos.to_hex_uint p <> zero. +Proof. + intro E. generalize (of_to p). now rewrite E. +Qed. + +Lemma to_uint_nonnil p : Pos.to_hex_uint p <> Nil. +Proof. + intros E. generalize (of_to p). now rewrite E. +Qed. + +Lemma to_uint_inj p p' : Pos.to_hex_uint p = Pos.to_hex_uint p' -> p = p'. +Proof. + intro E. + assert (E' : N.pos p = N.pos p'). + { now rewrite <- (of_to p), <- (of_to p'), E. } + now injection E'. +Qed. + +Lemma to_uint_pos_surj d : + unorm d<>zero -> exists p, Pos.to_hex_uint p = unorm d. +Proof. + intros. + destruct (Pos.of_hex_uint d) eqn:E. + - destruct H. generalize (to_of d). now rewrite E. + - exists p. generalize (to_of d). now rewrite E. +Qed. + +Lemma of_uint_norm d : Pos.of_hex_uint (unorm d) = Pos.of_hex_uint d. +Proof. + now induction d. +Qed. + +Lemma of_inj d d' : + Pos.of_hex_uint d = Pos.of_hex_uint d' -> unorm d = unorm d'. +Proof. + intros. rewrite <- !to_of. now f_equal. +Qed. + +Lemma of_iff d d' : Pos.of_hex_uint d = Pos.of_hex_uint d' <-> unorm d = unorm d'. +Proof. + split. apply of_inj. intros E. rewrite <- of_uint_norm, E. + apply of_uint_norm. +Qed. + +(* various lemmas *) + +Lemma nztail_to_hex_uint p : + let (h, n) := Hexadecimal.nztail (Pos.to_hex_uint p) in + Npos p = Pos.of_hex_uint h * 0x10^(N.of_nat n). +Proof. + rewrite <-(of_to p), <-(rev_rev (Pos.to_hex_uint p)), of_lu_rev. + unfold Hexadecimal.nztail. + rewrite rev_rev. + induction (rev (Pos.to_hex_uint p)); [reflexivity| | + now simpl N.of_nat; simpl N.pow; rewrite N.mul_1_r, of_lu_rev..]. + revert IHu. + set (t := _ u); case t; clear t; intros u0 n H. + rewrite of_lu_eqn; unfold hd, tl. + rewrite N.add_0_l, H, Nat2N.inj_succ, N.pow_succ_r'; ring. +Qed. + +Definition double d := rev (Little.double (rev d)). + +Lemma double_unorm d : double (unorm d) = unorm (double d). +Proof. + unfold double. + rewrite <-!rev_lnorm_rev, !rev_rev, <-!to_of_lu, of_lu_double. + now case of_lu; [now simpl|]; intro p; induction p. +Qed. + +Lemma double_nzhead d : double (nzhead d) = nzhead (double d). +Proof. + unfold double. + rewrite <-!rev_nztail_rev, !rev_rev. + apply f_equal; generalize (rev d); clear d; intro d. + cut (Little.double (nztail d) = nztail (Little.double d) + /\ Little.succ_double (nztail d) = nztail (Little.succ_double d)). + { now simpl. } + now induction d; + [|split; simpl; rewrite <-?(proj1 IHd), <-?(proj2 IHd); case nztail..]. +Qed. + +Lemma of_hex_uint_double d : + Pos.of_hex_uint (double d) = N.double (Pos.of_hex_uint d). +Proof. + now unfold double; rewrite of_lu_rev, of_lu_double, <-of_lu_rev, rev_rev. +Qed. + +End Unsigned. + +(** Conversion from/to signed decimal numbers *) + +Module Signed. + +Lemma of_to (p:positive) : Pos.of_hex_int (Pos.to_hex_int p) = Some p. +Proof. + unfold Pos.to_hex_int, Pos.of_hex_int, norm. + now rewrite Unsigned.of_to. +Qed. + +Lemma to_of (d:int)(p:positive) : + Pos.of_hex_int d = Some p -> Pos.to_hex_int p = norm d. +Proof. + unfold Pos.of_hex_int. + destruct d; [ | intros [=]]. + simpl norm. rewrite <- Unsigned.to_of. + destruct (Pos.of_hex_uint d); now intros [= <-]. +Qed. + +Lemma to_int_inj p p' : Pos.to_hex_int p = Pos.to_hex_int p' -> p = p'. +Proof. + intro E. + assert (E' : Some p = Some p'). + { now rewrite <- (of_to p), <- (of_to p'), E. } + now injection E'. +Qed. + +Lemma to_int_pos_surj d : + unorm d <> zero -> exists p, Pos.to_hex_int p = norm (Pos d). +Proof. + simpl. unfold Pos.to_hex_int. intros H. + destruct (Unsigned.to_uint_pos_surj d H) as (p,Hp). + exists p. now f_equal. +Qed. + +Lemma of_int_norm d : Pos.of_hex_int (norm d) = Pos.of_hex_int d. +Proof. + unfold Pos.of_int. + destruct d. + - simpl. now rewrite Unsigned.of_uint_norm. + - simpl. now destruct (nzhead d) eqn:H. +Qed. + +Lemma of_inj_pos d d' : + Pos.of_hex_int (Pos d) = Pos.of_hex_int (Pos d') -> unorm d = unorm d'. +Proof. + unfold Pos.of_hex_int. + destruct (Pos.of_hex_uint d) eqn:Hd, (Pos.of_hex_uint d') eqn:Hd'; + intros [=]. + - apply Unsigned.of_inj; now rewrite Hd, Hd'. + - apply Unsigned.of_inj; rewrite Hd, Hd'; now f_equal. +Qed. + +End Signed. diff --git a/theories/Numbers/HexadecimalQ.v b/theories/Numbers/HexadecimalQ.v new file mode 100644 index 0000000000..9bf43ceb88 --- /dev/null +++ b/theories/Numbers/HexadecimalQ.v @@ -0,0 +1,533 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** * HexadecimalQ + + Proofs that conversions between hexadecimal numbers and [Q] + are bijections. *) + +Require Import Decimal DecimalFacts DecimalPos DecimalN DecimalZ. +Require Import Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN HexadecimalZ QArith. + +Lemma of_to (q:Q) : forall d, to_hexadecimal q = Some d -> of_hexadecimal d = q. +Proof. + cut (match to_hexadecimal q with None => True | Some d => of_hexadecimal d = q end). + { now case to_hexadecimal; [intros d <- d' Hd'; injection Hd'; intros ->|]. } + destruct q as (num, den). + unfold to_hexadecimal; simpl Qnum; simpl Qden. + generalize (HexadecimalPos.Unsigned.nztail_to_hex_uint den). + case Hexadecimal.nztail; intros u n. + change 16%N with (2^4)%N; rewrite <-N.pow_mul_r. + change 4%N with (N.of_nat 4); rewrite <-Nnat.Nat2N.inj_mul. + change 4%Z with (Z.of_nat 4); rewrite <-Nat2Z.inj_mul. + case u; clear u; try (intros; exact I); [| | |]; intro u; + (case u; clear u; [|intros; exact I..]). + - unfold Pos.of_hex_uint, Pos.of_hex_uint_acc; rewrite N.mul_1_l. + case n. + + unfold of_hexadecimal, app_int, app, Z.to_hex_int; simpl. + intro H; inversion H as (H1); clear H H1. + case num; [reflexivity|intro pnum; fold (rev (rev (Pos.to_hex_uint pnum)))..]. + * rewrite rev_rev; simpl. + now unfold Z.of_hex_uint; rewrite HexadecimalPos.Unsigned.of_to. + * rewrite rev_rev; simpl. + now unfold Z.of_hex_uint; rewrite HexadecimalPos.Unsigned.of_to. + + clear n; intros n. + intro H; injection H; intros ->; clear H. + unfold of_hexadecimal. + rewrite DecimalZ.of_to. + simpl nb_digits; rewrite Nat2Z.inj_0, Z.mul_0_r, Z.sub_0_r. + now apply f_equal2; [rewrite app_int_nil_r, of_to|]. + - unfold Pos.of_hex_uint, Pos.of_hex_uint_acc. + rewrite <-N.pow_succ_r', <-Nnat.Nat2N.inj_succ. + intro H; injection H; intros ->; clear H. + fold (4 * n)%nat. + change 1%Z with (Z.of_nat 1); rewrite <-Znat.Nat2Z.inj_add. + unfold of_hexadecimal. + rewrite DecimalZ.of_to. + simpl nb_digits; rewrite Nat2Z.inj_0, Z.mul_0_r, Z.sub_0_r. + now apply f_equal2; [rewrite app_int_nil_r, of_to|]. + - change 2%Z with (Z.of_nat 2); rewrite <-Znat.Nat2Z.inj_add. + unfold Pos.of_hex_uint, Pos.of_hex_uint_acc. + change 4%N with (2^2)%N; rewrite <-N.pow_add_r. + change 2%N with (N.of_nat 2); rewrite <-Nnat.Nat2N.inj_add. + intro H; injection H; intros ->; clear H. + fold (4 * n)%nat. + unfold of_hexadecimal. + rewrite DecimalZ.of_to. + simpl nb_digits; rewrite Nat2Z.inj_0, Z.mul_0_r, Z.sub_0_r. + now apply f_equal2; [rewrite app_int_nil_r, of_to|]. + - change 3%Z with (Z.of_nat 3); rewrite <-Znat.Nat2Z.inj_add. + unfold Pos.of_hex_uint, Pos.of_hex_uint_acc. + change 8%N with (2^3)%N; rewrite <-N.pow_add_r. + change 3%N with (N.of_nat 3); rewrite <-Nnat.Nat2N.inj_add. + intro H; injection H; intros ->; clear H. + fold (4 * n)%nat. + unfold of_hexadecimal. + rewrite DecimalZ.of_to. + simpl nb_digits; rewrite Nat2Z.inj_0, Z.mul_0_r, Z.sub_0_r. + now apply f_equal2; [rewrite app_int_nil_r, of_to|]. +Qed. + +(* normalize without fractional part, for instance norme 0x1.2p-1 is 0x12e-5 *) +Definition hnorme (d:hexadecimal) : hexadecimal := + let '(i, f, e) := + match d with + | Hexadecimal i f => (i, f, Decimal.Pos Decimal.Nil) + | HexadecimalExp i f e => (i, f, e) + end in + let i := norm (app_int i f) in + let e := (Z.of_int e - 4 * Z.of_nat (nb_digits f))%Z in + match e with + | Z0 => Hexadecimal i Nil + | Zpos e => Hexadecimal (Pos.iter double i e) Nil + | Zneg _ => HexadecimalExp i Nil (Decimal.norm (Z.to_int e)) + end. + +Lemma hnorme_spec d : + match hnorme d with + | Hexadecimal i Nil => i = norm i + | HexadecimalExp i Nil e => + i = norm i /\ e = Decimal.norm e /\ e <> Decimal.Pos Decimal.zero + | _ => False + end. +Proof. + case d; clear d; intros i f; [|intro e]; unfold hnorme; simpl. + - case_eq (nb_digits f); [now simpl; rewrite norm_invol|]; intros nf Hnf. + split; [now simpl; rewrite norm_invol|]. + unfold Z.of_nat. + now rewrite <-!DecimalZ.to_of, !DecimalZ.of_to. + - set (e' := (_ - _)%Z). + case_eq e'; [|intro pe'..]; intro He'. + + now rewrite norm_invol. + + rewrite Pos2Nat.inj_iter. + set (ne' := Pos.to_nat pe'). + fold (Nat.iter ne' double (norm (app_int i f))). + induction ne'; [now simpl; rewrite norm_invol|]. + now rewrite Unsigned.nat_iter_S, <-double_norm, IHne', norm_invol. + + split; [now rewrite norm_invol|]. + split; [now rewrite DecimalFacts.norm_invol|]. + rewrite <-DecimalZ.to_of, DecimalZ.of_to. + change (Decimal.Pos _) with (Z.to_int 0). + now intro H; generalize (DecimalZ.to_int_inj _ _ H). +Qed. + +Lemma hnorme_invol d : hnorme (hnorme d) = hnorme d. +Proof. + case d; clear d; intros i f; [|intro e]; unfold hnorme; simpl. + - case_eq (nb_digits f); [now simpl; rewrite app_int_nil_r, norm_invol|]. + intros nf Hnf. + unfold Z.of_nat. + simpl. + set (pnf := Pos.to_uint _). + set (nz := Decimal.nzhead pnf). + assert (Hnz : nz <> Decimal.Nil). + { unfold nz, pnf. + rewrite <-DecimalFacts.unorm_0. + rewrite <-DecimalPos.Unsigned.to_of. + rewrite DecimalPos.Unsigned.of_to. + change Decimal.zero with (N.to_uint 0). + now intro H; generalize (DecimalN.Unsigned.to_uint_inj _ _ H). } + set (m := match nz with Decimal.Nil => _ | _ => _ end). + assert (Hm : m = (Decimal.Neg (Decimal.unorm pnf))). + { now revert Hnz; unfold m, nz, Decimal.unorm; fold nz; case nz. } + rewrite Hm; unfold pnf. + rewrite <-DecimalPos.Unsigned.to_of, DecimalPos.Unsigned.of_to. + simpl; unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to. + rewrite Z.sub_0_r; simpl. + fold pnf; fold nz; fold m; rewrite Hm; unfold pnf. + rewrite <-DecimalPos.Unsigned.to_of, DecimalPos.Unsigned.of_to. + now rewrite app_int_nil_r, norm_invol. + - set (e' := (_ - _)%Z). + case_eq e'; [|intro pe'..]; intro Hpe'. + + now simpl; rewrite app_int_nil_r, norm_invol. + + simpl; rewrite app_int_nil_r. + apply f_equal2; [|reflexivity]. + rewrite Pos2Nat.inj_iter. + set (ne' := Pos.to_nat pe'). + fold (Nat.iter ne' double (norm (app_int i f))). + induction ne'; [now simpl; rewrite norm_invol|]. + now rewrite Unsigned.nat_iter_S, <-double_norm, IHne'. + + rewrite <-DecimalZ.to_of, !DecimalZ.of_to; simpl. + rewrite app_int_nil_r, norm_invol. + set (pnf := Pos.to_uint _). + set (nz := Decimal.nzhead pnf). + assert (Hnz : nz <> Decimal.Nil). + { unfold nz, pnf. + rewrite <-DecimalFacts.unorm_0. + rewrite <-DecimalPos.Unsigned.to_of. + rewrite DecimalPos.Unsigned.of_to. + change Decimal.zero with (N.to_uint 0). + now intro H; generalize (DecimalN.Unsigned.to_uint_inj _ _ H). } + set (m := match nz with Decimal.Nil => _ | _ => _ end). + assert (Hm : m = (Decimal.Neg (Decimal.unorm pnf))). + { now revert Hnz; unfold m, nz, Decimal.unorm; fold nz; case nz. } + rewrite Hm; unfold pnf. + now rewrite <-DecimalPos.Unsigned.to_of, DecimalPos.Unsigned.of_to. +Qed. + +Lemma to_of (d:hexadecimal) : + to_hexadecimal (of_hexadecimal d) = Some (hnorme d). +Proof. + unfold to_hexadecimal. + pose (t10 := fun y => (y~0~0~0~0)%positive). + assert (H : exists h e_den, + Hexadecimal.nztail (Pos.to_hex_uint (Qden (of_hexadecimal d))) + = (h, e_den) + /\ (h = D1 Nil \/ h = D2 Nil \/ h = D4 Nil \/ h = D8 Nil)). + { assert (H : forall p, + Hexadecimal.nztail (Pos.to_hex_uint (Pos.iter (Pos.mul 2) 1%positive p)) + = ((match (Pos.to_nat p) mod 4 with 0%nat => D1 | 1 => D2 | 2 => D4 | _ => D8 end)%nat Nil, + (Pos.to_nat p / 4)%nat)). + { intro p; clear d; rewrite Pos2Nat.inj_iter. + fold (Nat.iter (Pos.to_nat p) (Pos.mul 2) 1%positive). + set (n := Pos.to_nat p). + fold (Nat.iter n t10 1%positive). + set (nm4 := (n mod 4)%nat); set (nd4 := (n / 4)%nat). + rewrite (Nat.div_mod n 4); [|now simpl]. + unfold nm4, nd4; clear nm4 nd4. + generalize (Nat.mod_upper_bound n 4 ltac:(now simpl)). + generalize (n mod 4); generalize (n / 4)%nat. + intros d r Hr; clear p n. + induction d. + { simpl; revert Hr. + do 4 (case r; [now simpl|clear r; intro r]). + intro H; exfalso. + now do 4 (generalize (lt_S_n _ _ H); clear H; intro H). } + rewrite Nat.mul_succ_r, <-Nat.add_assoc, (Nat.add_comm 4), Nat.add_assoc. + rewrite (Nat.add_comm _ 4). + change (4 + _)%nat with (S (S (S (S (4 * d + r))))). + rewrite !Unsigned.nat_iter_S. + rewrite !Pos.mul_assoc. + unfold Pos.to_hex_uint. + change (2 * 2 * 2 * 2)%positive with 0x10%positive. + set (n := Nat.iter _ _ _). + change (Pos.to_little_hex_uint _) with (Unsigned.to_lu (16 * N.pos n)). + rewrite Unsigned.to_lhex_tenfold. + unfold Hexadecimal.nztail; rewrite rev_rev. + rewrite <-(rev_rev (Unsigned.to_lu _)). + set (m := _ (rev _)). + replace m with (let (r, n) := let (r, n) := m in (rev r, n) in (rev r, n)). + 2:{ now case m; intros r' n'; rewrite rev_rev. } + change (let (r, n) := m in (rev r, n)) + with (Hexadecimal.nztail (Pos.to_hex_uint n)). + now unfold n; rewrite IHd, rev_rev; clear n m. } + unfold of_hexadecimal. + case d; intros i f; [|intro e]; unfold of_hexadecimal; simpl. + - case (Z.of_nat _)%Z; [|intro p..]; + [now exists (D1 Nil), O; split; [|left] + | |now exists (D1 Nil), O; split; [|left]]. + exists (D1 Nil), (Pos.to_nat p). + split; [|now left]; simpl. + change (Pos.iter _ _ _) with (Pos.iter (Pos.mul 2) 1%positive (4 * p)). + rewrite H. + rewrite Pos2Nat.inj_mul, Nat.mul_comm, Nat.div_mul; [|now simpl]. + now rewrite Nat.mod_mul; [|now simpl]. + - case (_ - _)%Z; [|intros p..]; [now exists (D1 Nil), O; split; [|left]..|]. + simpl Qden; rewrite H. + eexists; eexists; split; [reflexivity|]. + case (_ mod _); [now left|intro n]. + case n; [now right; left|clear n; intro n]. + case n; [now right; right; left|clear n; intro n]. + now right; right; right. } + generalize (HexadecimalPos.Unsigned.nztail_to_hex_uint (Qden (of_hexadecimal d))). + destruct H as (h, (e, (He, Hh))); rewrite He; clear He. + assert (Hn1 : forall p, N.pos (Pos.iter (Pos.mul 2) 1%positive p) = 1%N -> False). + { intro p. + rewrite Pos2Nat.inj_iter. + case_eq (Pos.to_nat p); [|now simpl]. + intro H; exfalso; apply (lt_irrefl O). + rewrite <-H at 2; apply Pos2Nat.is_pos. } + assert (H16_2 : forall p, (16^p = 2^(4 * p))%positive). + { intro p. + apply (@f_equal _ _ (fun z => match z with Z.pos p => p | _ => 1%positive end) + (Z.pos _) (Z.pos _)). + rewrite !Pos2Z.inj_pow_pos, !Z.pow_pos_fold, Pos2Z.inj_mul. + now change 16%Z with (2^4)%Z; rewrite <-Z.pow_mul_r. } + assert (HN16_2 : forall n, (16^n = 2^(4 * n))%N). + { intro n. + apply N2Z.inj; rewrite !N2Z.inj_pow, N2Z.inj_mul. + change (Z.of_N 16) with (2^4)%Z. + now rewrite <-Z.pow_mul_r; [| |apply N2Z.is_nonneg]. } + assert (Hn1' : forall p, N.pos (Pos.iter (Pos.mul 16) 1%positive p) = 1%N -> False). + { intro p; fold (16^p)%positive; rewrite H16_2; apply Hn1. } + assert (Ht10inj : forall n m, t10 n = t10 m -> n = m). + { intros n m H; generalize (f_equal Z.pos H); clear H. + change (Z.pos (t10 n)) with (Z.mul 0x10 (Z.pos n)). + change (Z.pos (t10 m)) with (Z.mul 0x10 (Z.pos m)). + rewrite Z.mul_comm, (Z.mul_comm 0x10). + intro H; generalize (f_equal (fun z => Z.div z 0x10) H); clear H. + now rewrite !Z.div_mul; [|now simpl..]; intro H; inversion H. } + assert (Ht2inj : forall n m, Pos.mul 2 n = Pos.mul 2 m -> n = m). + { intros n m H; generalize (f_equal Z.pos H); clear H. + change (Z.pos (Pos.mul 2 n)) with (Z.mul 2 (Z.pos n)). + change (Z.pos (Pos.mul 2 m)) with (Z.mul 2 (Z.pos m)). + rewrite Z.mul_comm, (Z.mul_comm 2). + intro H; generalize (f_equal (fun z => Z.div z 2) H); clear H. + now rewrite !Z.div_mul; [|now simpl..]; intro H; inversion H. } + assert (Hinj : forall n m, + Nat.iter n (Pos.mul 2) 1%positive = Nat.iter m (Pos.mul 2) 1%positive + -> n = m). + { induction n; [now intro m; case m|]. + intro m; case m; [now simpl|]; clear m; intro m. + rewrite !Unsigned.nat_iter_S. + intro H; generalize (Ht2inj _ _ H); clear H; intro H. + now rewrite (IHn _ H). } + change 4%Z with (Z.of_nat 4); rewrite <-Nat2Z.inj_mul. + change 1%Z with (Z.of_nat 1); rewrite <-Nat2Z.inj_add. + change 2%Z with (Z.of_nat 2); rewrite <-Nat2Z.inj_add. + change 3%Z with (Z.of_nat 3); rewrite <-Nat2Z.inj_add. + destruct Hh as [Hh|[Hh|[Hh|Hh]]]; rewrite Hh; clear h Hh. + - case e; clear e; [|intro e]; simpl; unfold of_hexadecimal, hnorme. + + case d; clear d; intros i f; [|intro e]. + * generalize (nb_digits_pos f). + case f; + [|now clear f; intro f; intros H1 H2; exfalso; revert H1 H2; + case nb_digits; + [intros H _; apply (lt_irrefl O), H|intros n _; apply Hn1]..]. + now intros _ _; simpl; rewrite to_of. + * rewrite <-DecimalZ.to_of, DecimalZ.of_to. + set (emf := (_ - _)%Z). + case_eq emf; [|intro pemf..]. + ++ now simpl; rewrite to_of. + ++ intros Hemf _; simpl. + apply f_equal, f_equal2; [|reflexivity]. + rewrite !Pos2Nat.inj_iter. + fold (Nat.iter (Pos.to_nat pemf) (Z.mul 2) (Z.of_hex_int (app_int i f))). + fold (Nat.iter (Pos.to_nat pemf) double (norm (app_int i f))). + induction Pos.to_nat; [now simpl; rewrite HexadecimalZ.to_of|]. + now rewrite !Unsigned.nat_iter_S, <-IHn, double_to_hex_int. + ++ simpl Qden; intros _ H; exfalso; revert H; apply Hn1. + + case d; clear d; intros i f; [|intro e']. + * simpl; case_eq (nb_digits f); [|intros nf' Hnf']; + [now simpl; intros _ H; exfalso; symmetry in H; revert H; apply Hn1'|]. + unfold Z.of_nat, Z.opp, Qnum, Qden. + rewrite H16_2. + fold (Pos.mul 2); fold (2^(Pos.of_succ_nat nf')~0~0)%positive. + intro H; injection H; clear H. + unfold Pos.pow; rewrite !Pos2Nat.inj_iter. + intro H; generalize (Hinj _ _ H); clear H; intro H. + generalize (Pos2Nat.inj _ _ H); clear H; intro H; injection H. + clear H; intro H; generalize (SuccNat2Pos.inj _ _ H); clear H. + intros <-. + rewrite to_of. + rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl. + do 4 apply f_equal. + apply Pos2Nat.inj. + rewrite SuccNat2Pos.id_succ. + change (_~0)%positive with (4 * Pos.of_succ_nat nf')%positive. + now rewrite Pos2Nat.inj_mul, SuccNat2Pos.id_succ. + * set (nemf := (_ - _)%Z); intro H. + assert (H' : exists pnemf, nemf = Z.neg pnemf); [|revert H]. + { revert H; case nemf; [|intro pnemf..]; [..|now intros _; exists pnemf]; + simpl Qden; intro H; exfalso; symmetry in H; revert H; apply Hn1'. } + destruct H' as (pnemf,Hpnemf); rewrite Hpnemf. + unfold Qnum, Qden. + rewrite H16_2. + intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter. + intro H; generalize (Hinj _ _ H); clear H; intro H. + generalize (Pos2Nat.inj _ _ H); clear H. + intro H; revert Hpnemf; rewrite H; clear pnemf H; intro Hnemf. + rewrite to_of. + rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl. + do 4 apply f_equal. + apply Pos2Nat.inj. + rewrite SuccNat2Pos.id_succ. + change (_~0)%positive with (4 * Pos.of_succ_nat e)%positive. + now rewrite Pos2Nat.inj_mul, SuccNat2Pos.id_succ. + - simpl Pos.of_hex_uint. + rewrite HN16_2. + rewrite <-N.pow_succ_r; [|now apply N.le_0_l]. + rewrite <-N.succ_pos_spec. + case d; clear d; intros i f; [|intro e']; unfold of_hexadecimal, hnorme. + + set (em4f := (_ - _)%Z). + case_eq em4f; [|intros pem4f..]; intro Hpem4f; + [now simpl; intros H; exfalso; symmetry in H; revert H; apply Hn1..|]. + unfold Qnum, Qden. + intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter. + intro H; generalize (Hinj _ _ H); clear H; intro H. + generalize (Pos2Nat.inj _ _ H); clear H; intros ->. + rewrite to_of. + rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl. + do 4 apply f_equal. + apply Pos2Nat.inj. + rewrite SuccNat2Pos.id_succ. + case e; [now simpl|intro e'']; simpl. + unfold Pos.to_nat; simpl. + now rewrite Pmult_nat_mult, SuccNat2Pos.id_succ, Nat.mul_comm. + + set (em4f := (_ - _)%Z). + case_eq em4f; [|intros pem4f..]; intro Hpem4f; + [now simpl; intros H; exfalso; symmetry in H; revert H; apply Hn1..|]. + unfold Qnum, Qden. + intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter. + intro H; generalize (Hinj _ _ H); clear H; intro H. + generalize (Pos2Nat.inj _ _ H); clear H; intros ->. + rewrite to_of. + rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl. + do 4 apply f_equal. + apply Pos2Nat.inj. + rewrite SuccNat2Pos.id_succ. + case e; [now simpl|intro e'']; simpl. + unfold Pos.to_nat; simpl. + now rewrite Pmult_nat_mult, SuccNat2Pos.id_succ, Nat.mul_comm. + - simpl Pos.of_hex_uint. + rewrite HN16_2. + change 4%N with (2 * 2)%N at 1; rewrite <-!N.mul_assoc. + do 2 (rewrite <-N.pow_succ_r; [|now apply N.le_0_l]). + rewrite <-N.succ_pos_spec. + case d; clear d; intros i f; [|intro e']; unfold of_hexadecimal, hnorme. + + set (em4f := (_ - _)%Z). + case_eq em4f; [|intros pem4f..]; intro Hpem4f; + [now simpl; intros H; exfalso; symmetry in H; revert H; apply Hn1..|]. + unfold Qnum, Qden. + intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter. + intro H; generalize (Hinj _ _ H); clear H; intro H. + generalize (Pos2Nat.inj _ _ H); clear H; intros ->. + rewrite to_of. + rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl. + do 4 apply f_equal. + apply Pos2Nat.inj. + rewrite <-SuccNat2Pos.inj_succ. + rewrite SuccNat2Pos.id_succ. + case e; [now simpl|intro e'']; simpl. + unfold Pos.to_nat; simpl. + now rewrite Pmult_nat_mult, SuccNat2Pos.id_succ, Nat.mul_comm. + + set (em4f := (_ - _)%Z). + case_eq em4f; [|intros pem4f..]; intro Hpem4f; + [now simpl; intros H; exfalso; symmetry in H; revert H; apply Hn1..|]. + unfold Qnum, Qden. + intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter. + intro H; generalize (Hinj _ _ H); clear H; intro H. + generalize (Pos2Nat.inj _ _ H); clear H; intros ->. + rewrite to_of. + rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl. + do 4 apply f_equal. + apply Pos2Nat.inj. + rewrite <-SuccNat2Pos.inj_succ. + rewrite SuccNat2Pos.id_succ. + case e; [now simpl|intro e'']; simpl. + unfold Pos.to_nat; simpl. + now rewrite Pmult_nat_mult, SuccNat2Pos.id_succ, Nat.mul_comm. + - simpl Pos.of_hex_uint. + rewrite HN16_2. + change 8%N with (2 * 2 * 2)%N; rewrite <-!N.mul_assoc. + do 3 (rewrite <-N.pow_succ_r; [|now apply N.le_0_l]). + rewrite <-N.succ_pos_spec. + case d; clear d; intros i f; [|intro e']; unfold of_hexadecimal, hnorme. + + set (em4f := (_ - _)%Z). + case_eq em4f; [|intros pem4f..]; intro Hpem4f; + [now simpl; intros H; exfalso; symmetry in H; revert H; apply Hn1..|]. + unfold Qnum, Qden. + intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter. + intro H; generalize (Hinj _ _ H); clear H; intro H. + generalize (Pos2Nat.inj _ _ H); clear H; intros ->. + rewrite to_of. + rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl. + do 4 apply f_equal. + apply Pos2Nat.inj. + rewrite <-!SuccNat2Pos.inj_succ. + rewrite SuccNat2Pos.id_succ. + case e; [now simpl|intro e'']; simpl. + unfold Pos.to_nat; simpl. + now rewrite Pmult_nat_mult, SuccNat2Pos.id_succ, Nat.mul_comm. + + set (em4f := (_ - _)%Z). + case_eq em4f; [|intros pem4f..]; intro Hpem4f; + [now simpl; intros H; exfalso; symmetry in H; revert H; apply Hn1..|]. + unfold Qnum, Qden. + intro H; injection H; clear H; unfold Pos.pow; rewrite !Pos2Nat.inj_iter. + intro H; generalize (Hinj _ _ H); clear H; intro H. + generalize (Pos2Nat.inj _ _ H); clear H; intros ->. + rewrite to_of. + rewrite <-DecimalZ.to_of, DecimalZ.of_to; simpl. + do 4 apply f_equal. + apply Pos2Nat.inj. + rewrite <-!SuccNat2Pos.inj_succ. + rewrite SuccNat2Pos.id_succ. + case e; [now simpl|intro e'']; simpl. + unfold Pos.to_nat; simpl. + now rewrite Pmult_nat_mult, SuccNat2Pos.id_succ, Nat.mul_comm. +Qed. + +(** Some consequences *) + +Lemma to_hexadecimal_inj q q' : + to_hexadecimal q <> None -> to_hexadecimal q = to_hexadecimal q' -> q = q'. +Proof. + intros Hnone EQ. + generalize (of_to q) (of_to q'). + rewrite <-EQ. + revert Hnone; case to_hexadecimal; [|now simpl]. + now intros d _ H1 H2; rewrite <-(H1 d eq_refl), <-(H2 d eq_refl). +Qed. + +Lemma to_hexadecimal_surj d : exists q, to_hexadecimal q = Some (hnorme d). +Proof. + exists (of_hexadecimal d). apply to_of. +Qed. + +Lemma of_hexadecimal_hnorme d : of_hexadecimal (hnorme d) = of_hexadecimal d. +Proof. + unfold of_hexadecimal, hnorme. + destruct d. + - simpl Z.of_int; unfold Z.of_uint, Z.of_N, Pos.of_uint. + rewrite Z.sub_0_l. + set (n4f := (- _)%Z). + case_eq n4f; [|intro pn4f..]; intro Hn4f. + + apply f_equal2; [|reflexivity]. + rewrite app_int_nil_r. + now rewrite <-HexadecimalZ.to_of, HexadecimalZ.of_to. + + apply f_equal2; [|reflexivity]. + rewrite app_int_nil_r. + generalize (app_int i f); intro i'. + rewrite !Pos2Nat.inj_iter. + generalize (Pos.to_nat pn4f); intro n. + fold (Nat.iter n double (norm i')). + fold (Nat.iter n (Z.mul 2) (Z.of_hex_int i')). + induction n; [now simpl; rewrite <-HexadecimalZ.to_of, HexadecimalZ.of_to|]. + now rewrite !Unsigned.nat_iter_S, <-IHn, of_hex_int_double. + + unfold nb_digits, Z.of_nat. + rewrite Z.mul_0_r, Z.sub_0_r. + rewrite <-DecimalZ.to_of, !DecimalZ.of_to. + rewrite app_int_nil_r. + now rewrite <-HexadecimalZ.to_of, HexadecimalZ.of_to. + - set (nem4f := (_ - _)%Z). + case_eq nem4f; [|intro pnem4f..]; intro Hnem4f. + + apply f_equal2; [|reflexivity]. + rewrite app_int_nil_r. + now rewrite <-HexadecimalZ.to_of, HexadecimalZ.of_to. + + apply f_equal2; [|reflexivity]. + rewrite app_int_nil_r. + generalize (app_int i f); intro i'. + rewrite !Pos2Nat.inj_iter. + generalize (Pos.to_nat pnem4f); intro n. + fold (Nat.iter n double (norm i')). + fold (Nat.iter n (Z.mul 2) (Z.of_hex_int i')). + induction n; [now simpl; rewrite <-HexadecimalZ.to_of, HexadecimalZ.of_to|]. + now rewrite !Unsigned.nat_iter_S, <-IHn, of_hex_int_double. + + unfold nb_digits, Z.of_nat. + rewrite Z.mul_0_r, Z.sub_0_r. + rewrite <-DecimalZ.to_of, !DecimalZ.of_to. + rewrite app_int_nil_r. + now rewrite <-HexadecimalZ.to_of, HexadecimalZ.of_to. +Qed. + +Lemma of_inj d d' : + of_hexadecimal d = of_hexadecimal d' -> hnorme d = hnorme d'. +Proof. + intros. + cut (Some (hnorme d) = Some (hnorme d')); [now intro H'; injection H'|]. + rewrite <- !to_of. now f_equal. +Qed. + +Lemma of_iff d d' : + of_hexadecimal d = of_hexadecimal d' <-> hnorme d = hnorme d'. +Proof. + split. apply of_inj. intros E. rewrite <- of_hexadecimal_hnorme, E. + apply of_hexadecimal_hnorme. +Qed. diff --git a/theories/Numbers/HexadecimalString.v b/theories/Numbers/HexadecimalString.v new file mode 100644 index 0000000000..7017bdf60f --- /dev/null +++ b/theories/Numbers/HexadecimalString.v @@ -0,0 +1,286 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Require Import Hexadecimal Ascii String. + +(** * Conversion between hexadecimal numbers and Coq strings *) + +(** Pretty straightforward, which is precisely the point of the + [Hexadecimal.int] datatype. The only catch is [Hexadecimal.Nil] : we could + choose to convert it as [""] or as ["0"]. In the first case, it is + awkward to consider "" (or "-") as a number, while in the second case + we don't have a perfect bijection. Since the second variant is implemented + thanks to the first one, we provide both. + + Hexadecimal digits are lower case ('a'..'f'). We ignore upper case + digits ('A'..'F') for the sake of simplicity. *) + +Local Open Scope string_scope. + +(** Parsing one char *) + +Definition uint_of_char (a:ascii)(d:option uint) := + match d with + | None => None + | Some d => + match a with + | "0" => Some (D0 d) + | "1" => Some (D1 d) + | "2" => Some (D2 d) + | "3" => Some (D3 d) + | "4" => Some (D4 d) + | "5" => Some (D5 d) + | "6" => Some (D6 d) + | "7" => Some (D7 d) + | "8" => Some (D8 d) + | "9" => Some (D9 d) + | "a" => Some (Da d) + | "b" => Some (Db d) + | "c" => Some (Dc d) + | "d" => Some (Dd d) + | "e" => Some (De d) + | "f" => Some (Df d) + | _ => None + end + end%char. + +Lemma uint_of_char_spec c d d' : + uint_of_char c (Some d) = Some d' -> + (c = "0" /\ d' = D0 d \/ + c = "1" /\ d' = D1 d \/ + c = "2" /\ d' = D2 d \/ + c = "3" /\ d' = D3 d \/ + c = "4" /\ d' = D4 d \/ + c = "5" /\ d' = D5 d \/ + c = "6" /\ d' = D6 d \/ + c = "7" /\ d' = D7 d \/ + c = "8" /\ d' = D8 d \/ + c = "9" /\ d' = D9 d \/ + c = "a" /\ d' = Da d \/ + c = "b" /\ d' = Db d \/ + c = "c" /\ d' = Dc d \/ + c = "d" /\ d' = Dd d \/ + c = "e" /\ d' = De d \/ + c = "f" /\ d' = Df d)%char. +Proof. + destruct c as [[|] [|] [|] [|] [|] [|] [|] [|]]; + intros [= <-]; intuition. +Qed. + +(** Hexadecimal/String conversion where [Nil] is [""] *) + +Module NilEmpty. + +Fixpoint string_of_uint (d:uint) := + match d with + | Nil => EmptyString + | D0 d => String "0" (string_of_uint d) + | D1 d => String "1" (string_of_uint d) + | D2 d => String "2" (string_of_uint d) + | D3 d => String "3" (string_of_uint d) + | D4 d => String "4" (string_of_uint d) + | D5 d => String "5" (string_of_uint d) + | D6 d => String "6" (string_of_uint d) + | D7 d => String "7" (string_of_uint d) + | D8 d => String "8" (string_of_uint d) + | D9 d => String "9" (string_of_uint d) + | Da d => String "a" (string_of_uint d) + | Db d => String "b" (string_of_uint d) + | Dc d => String "c" (string_of_uint d) + | Dd d => String "d" (string_of_uint d) + | De d => String "e" (string_of_uint d) + | Df d => String "f" (string_of_uint d) + end. + +Fixpoint uint_of_string s := + match s with + | EmptyString => Some Nil + | String a s => uint_of_char a (uint_of_string s) + end. + +Definition string_of_int (d:int) := + match d with + | Pos d => string_of_uint d + | Neg d => String "-" (string_of_uint d) + end. + +Definition int_of_string s := + match s with + | EmptyString => Some (Pos Nil) + | String a s' => + if Ascii.eqb a "-" then option_map Neg (uint_of_string s') + else option_map Pos (uint_of_string s) + end. + +(* NB: For the moment whitespace between - and digits are not accepted. + And in this variant [int_of_string "-" = Some (Neg Nil)]. + +Compute int_of_string "-123456890123456890123456890123456890". +Compute string_of_int (-123456890123456890123456890123456890). +*) + +(** Corresponding proofs *) + +Lemma usu d : + uint_of_string (string_of_uint d) = Some d. +Proof. + induction d; simpl; rewrite ?IHd; simpl; auto. +Qed. + +Lemma sus s d : + uint_of_string s = Some d -> string_of_uint d = s. +Proof. + revert d. + induction s; simpl. + - now intros d [= <-]. + - intros d. + destruct (uint_of_string s); [intros H | intros [=]]. + apply uint_of_char_spec in H. + intuition subst; simpl; f_equal; auto. +Qed. + +Lemma isi d : int_of_string (string_of_int d) = Some d. +Proof. + destruct d; simpl. + - unfold int_of_string. + destruct (string_of_uint d) eqn:Hd. + + now destruct d. + + case Ascii.eqb_spec. + * intros ->. now destruct d. + * rewrite <- Hd, usu; auto. + - rewrite usu; auto. +Qed. + +Lemma sis s d : + int_of_string s = Some d -> string_of_int d = s. +Proof. + destruct s; [intros [= <-]| ]; simpl; trivial. + case Ascii.eqb_spec. + - intros ->. destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-]. + simpl; f_equal. now apply sus. + - destruct d; [ | now destruct uint_of_char]. + simpl string_of_int. + intros. apply sus; simpl. + destruct uint_of_char; simpl in *; congruence. +Qed. + +End NilEmpty. + +(** Hexadecimal/String conversions where [Nil] is ["0"] *) + +Module NilZero. + +Definition string_of_uint (d:uint) := + match d with + | Nil => "0" + | _ => NilEmpty.string_of_uint d + end. + +Definition uint_of_string s := + match s with + | EmptyString => None + | _ => NilEmpty.uint_of_string s + end. + +Definition string_of_int (d:int) := + match d with + | Pos d => string_of_uint d + | Neg d => String "-" (string_of_uint d) + end. + +Definition int_of_string s := + match s with + | EmptyString => None + | String a s' => + if Ascii.eqb a "-" then option_map Neg (uint_of_string s') + else option_map Pos (uint_of_string s) + end. + +(** Corresponding proofs *) + +Lemma uint_of_string_nonnil s : uint_of_string s <> Some Nil. +Proof. + destruct s; simpl. + - easy. + - destruct (NilEmpty.uint_of_string s); [intros H | intros [=]]. + apply uint_of_char_spec in H. + now intuition subst. +Qed. + +Lemma sus s d : + uint_of_string s = Some d -> string_of_uint d = s. +Proof. + destruct s; [intros [=] | intros H]. + apply NilEmpty.sus in H. now destruct d. +Qed. + +Lemma usu d : + d<>Nil -> uint_of_string (string_of_uint d) = Some d. +Proof. + destruct d; (now destruct 1) || (intros _; apply NilEmpty.usu). +Qed. + +Lemma usu_nil : + uint_of_string (string_of_uint Nil) = Some Hexadecimal.zero. +Proof. + reflexivity. +Qed. + +Lemma usu_gen d : + uint_of_string (string_of_uint d) = Some d \/ + uint_of_string (string_of_uint d) = Some Hexadecimal.zero. +Proof. + destruct d; (now right) || (left; now apply usu). +Qed. + +Lemma isi d : + d<>Pos Nil -> d<>Neg Nil -> + int_of_string (string_of_int d) = Some d. +Proof. + destruct d; simpl. + - intros H _. + unfold int_of_string. + destruct (string_of_uint d) eqn:Hd. + + now destruct d. + + case Ascii.eqb_spec. + * intros ->. now destruct d. + * rewrite <- Hd, usu; auto. now intros ->. + - intros _ H. + rewrite usu; auto. now intros ->. +Qed. + +Lemma isi_posnil : + int_of_string (string_of_int (Pos Nil)) = Some (Pos Hexadecimal.zero). +Proof. + reflexivity. +Qed. + +(** Warning! (-0) won't parse (compatibility with the behavior of Z). *) + +Lemma isi_negnil : + int_of_string (string_of_int (Neg Nil)) = Some (Neg (D0 Nil)). +Proof. + reflexivity. +Qed. + +Lemma sis s d : + int_of_string s = Some d -> string_of_int d = s. +Proof. + destruct s; [intros [=]| ]; simpl. + case Ascii.eqb_spec. + - intros ->. destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-]. + simpl; f_equal. now apply sus. + - destruct d; [ | now destruct uint_of_char]. + simpl string_of_int. + intros. apply sus; simpl. + destruct uint_of_char; simpl in *; congruence. +Qed. + +End NilZero. diff --git a/theories/Numbers/HexadecimalZ.v b/theories/Numbers/HexadecimalZ.v new file mode 100644 index 0000000000..c5ed0b5b28 --- /dev/null +++ b/theories/Numbers/HexadecimalZ.v @@ -0,0 +1,142 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** * HexadecimalZ + + Proofs that conversions between hexadecimal numbers and [Z] + are bijections. *) + +Require Import Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN ZArith. + +Lemma of_to (z:Z) : Z.of_hex_int (Z.to_hex_int z) = z. +Proof. + destruct z; simpl. + - trivial. + - unfold Z.of_hex_uint. rewrite HexadecimalPos.Unsigned.of_to. now destruct p. + - unfold Z.of_hex_uint. rewrite HexadecimalPos.Unsigned.of_to. destruct p; auto. +Qed. + +Lemma to_of (d:int) : Z.to_hex_int (Z.of_hex_int d) = norm d. +Proof. + destruct d; simpl; unfold Z.to_hex_int, Z.of_hex_uint. + - rewrite <- (HexadecimalN.Unsigned.to_of d). unfold N.of_hex_uint. + now destruct (Pos.of_hex_uint d). + - destruct (Pos.of_hex_uint d) eqn:Hd; simpl; f_equal. + + generalize (HexadecimalPos.Unsigned.to_of d). rewrite Hd. simpl. + intros H. symmetry in H. apply unorm_0 in H. now rewrite H. + + assert (Hp := HexadecimalPos.Unsigned.to_of d). rewrite Hd in Hp. simpl in *. + rewrite Hp. unfold unorm in *. + destruct (nzhead d); trivial. + generalize (HexadecimalPos.Unsigned.of_to p). now rewrite Hp. +Qed. + +(** Some consequences *) + +Lemma to_int_inj n n' : Z.to_hex_int n = Z.to_hex_int n' -> n = n'. +Proof. + intro EQ. + now rewrite <- (of_to n), <- (of_to n'), EQ. +Qed. + +Lemma to_int_surj d : exists n, Z.to_hex_int n = norm d. +Proof. + exists (Z.of_hex_int d). apply to_of. +Qed. + +Lemma of_int_norm d : Z.of_hex_int (norm d) = Z.of_hex_int d. +Proof. + unfold Z.of_hex_int, Z.of_hex_uint. + destruct d. + - simpl. now rewrite HexadecimalPos.Unsigned.of_uint_norm. + - simpl. destruct (nzhead d) eqn:H; + [ induction d; simpl; auto; discriminate | + destruct (nzhead_nonzero _ _ H) | .. ]; + f_equal; f_equal; apply HexadecimalPos.Unsigned.of_iff; + unfold unorm; now rewrite H. +Qed. + +Lemma of_inj d d' : + Z.of_hex_int d = Z.of_hex_int d' -> norm d = norm d'. +Proof. + intros. rewrite <- !to_of. now f_equal. +Qed. + +Lemma of_iff d d' : Z.of_hex_int d = Z.of_hex_int d' <-> norm d = norm d'. +Proof. + split. apply of_inj. intros E. rewrite <- of_int_norm, E. + apply of_int_norm. +Qed. + +(** Various lemmas *) + +Lemma of_hex_uint_iter_D0 d n : + Z.of_hex_uint (app d (Nat.iter n D0 Nil)) + = Nat.iter n (Z.mul 0x10) (Z.of_hex_uint d). +Proof. + unfold Z.of_hex_uint. + unfold app; rewrite <-rev_revapp. + rewrite Unsigned.of_lu_rev, Unsigned.of_lu_revapp. + rewrite <-!Unsigned.of_lu_rev, !rev_rev. + assert (H' : Pos.of_hex_uint (Nat.iter n D0 Nil) = 0%N). + { now induction n; [|rewrite Unsigned.nat_iter_S]. } + rewrite H', N.add_0_l; clear H'. + induction n; [now simpl; rewrite N.mul_1_r|]. + rewrite !Unsigned.nat_iter_S, <-IHn. + simpl Unsigned.usize; rewrite N.pow_succ_r'. + rewrite !N2Z.inj_mul; simpl Z.of_N; ring. +Qed. + +Lemma of_hex_int_iter_D0 d n : + Z.of_hex_int (app_int d (Nat.iter n D0 Nil)) + = Nat.iter n (Z.mul 0x10) (Z.of_hex_int d). +Proof. + case d; clear d; intro d; simpl. + - now rewrite of_hex_uint_iter_D0. + - rewrite of_hex_uint_iter_D0; induction n; [now simpl|]. + rewrite !Unsigned.nat_iter_S, <-IHn; ring. +Qed. + +Definition double d := + match d with + | Pos u => Pos (Unsigned.double u) + | Neg u => Neg (Unsigned.double u) + end. + +Lemma double_norm d : double (norm d) = norm (double d). +Proof. + destruct d. + - now simpl; rewrite Unsigned.double_unorm. + - simpl; rewrite <-Unsigned.double_nzhead. + case (uint_eq_dec (nzhead d) Nil); intro Hnzd. + + now rewrite Hnzd. + + assert (H : Unsigned.double (nzhead d) <> Nil). + { unfold Unsigned.double. + intro H; apply Hnzd, rev_nil_inv. + now generalize (rev_nil_inv _ H); case rev. } + revert H. + set (r := Unsigned.double _). + set (m := match r with Nil => Pos zero | _ => _ end). + intro H. + assert (H' : m = Neg r). + { now unfold m; clear m; revert H; case r. } + rewrite H'; unfold r; clear m r H H'. + now revert Hnzd; case nzhead. +Qed. + +Lemma of_hex_int_double d : + Z.of_hex_int (double d) = Z.double (Z.of_hex_int d). +Proof. + now destruct d; simpl; unfold Z.of_hex_uint; + rewrite Unsigned.of_hex_uint_double; case Pos.of_hex_uint. +Qed. + +Lemma double_to_hex_int n : + double (Z.to_hex_int n) = Z.to_hex_int (Z.double n). +Proof. now rewrite <-(of_to n), <-of_hex_int_double, !to_of, double_norm. Qed. diff --git a/theories/Numbers/NaryFunctions.v b/theories/Numbers/NaryFunctions.v index 80ad41f7c0..270cd4d111 100644 --- a/theories/Numbers/NaryFunctions.v +++ b/theories/Numbers/NaryFunctions.v @@ -20,70 +20,70 @@ Require Import List. [A -> ... -> A -> B] with [n] occurrences of [A] in this type. *) Fixpoint nfun A n B := - match n with + match n with | O => B | S n => A -> (nfun A n B) - end. + end. Notation " A ^^ n --> B " := (nfun A n B) - (at level 50, n at next level) : type_scope. + (at level 50, n at next level) : type_scope. (** [napply_cst _ _ a n f] iterates [n] times the application of a particular constant [a] to the [n]-ary function [f]. *) Fixpoint napply_cst (A B:Type)(a:A) n : (A^^n-->B) -> B := - match n return (A^^n-->B) -> B with + match n return (A^^n-->B) -> B with | O => fun x => x | S n => fun x => napply_cst _ _ a n (x a) - end. + end. (** A generic transformation from an n-ary function to another one.*) Fixpoint nfun_to_nfun (A B C:Type)(f:B -> C) n : - (A^^n-->B) -> (A^^n-->C) := - match n return (A^^n-->B) -> (A^^n-->C) with + (A^^n-->B) -> (A^^n-->C) := + match n return (A^^n-->B) -> (A^^n-->C) with | O => f | S n => fun g a => nfun_to_nfun _ _ _ f n (g a) - end. + end. (** [napply_except_last _ _ n f] expects [n] arguments of type [A], applies [n-1] of them to [f] and discard the last one. *) Definition napply_except_last (A B:Type) := - nfun_to_nfun A B (A->B) (fun b a => b). + nfun_to_nfun A B (A->B) (fun b a => b). (** [napply_then_last _ _ a n f] expects [n] arguments of type [A], applies them to [f] and then apply [a] to the result. *) Definition napply_then_last (A B:Type)(a:A) := - nfun_to_nfun A (A->B) B (fun fab => fab a). + nfun_to_nfun A (A->B) B (fun fab => fab a). (** [napply_discard _ b n] expects [n] arguments, discards then, and returns [b]. *) Fixpoint napply_discard (A B:Type)(b:B) n : A^^n-->B := - match n return A^^n-->B with + match n return A^^n-->B with | O => b | S n => fun _ => napply_discard _ _ b n - end. + end. (** A fold function *) Fixpoint nfold A B (f:A->B->B)(b:B) n : (A^^n-->B) := - match n return (A^^n-->B) with + match n return (A^^n-->B) with | O => b | S n => fun a => (nfold _ _ f (f a b) n) - end. + end. (** [n]-ary products : [nprod A n] is [A*...*A*unit], with [n] occurrences of [A] in this type. *) Fixpoint nprod A n : Type := match n with - | O => unit - | S n => (A * nprod A n)%type -end. + | O => unit + | S n => (A * nprod A n)%type + end. Notation "A ^ n" := (nprod A n) : type_scope. @@ -96,44 +96,44 @@ Fixpoint ncurry (A B:Type) n : (A^n -> B) -> (A^^n-->B) := end. Fixpoint nuncurry (A B:Type) n : (A^^n-->B) -> (A^n -> B) := - match n return (A^^n-->B) -> (A^n -> B) with + match n return (A^^n-->B) -> (A^n -> B) with | O => fun x _ => x | S n => fun f p => let (x,p) := p in nuncurry _ _ n (f x) p - end. + end. (** Earlier functions can also be defined via [ncurry/nuncurry]. For instance : *) Definition nfun_to_nfun_bis A B C (f:B->C) n : - (A^^n-->B) -> (A^^n-->C) := - fun anb => ncurry _ _ n (fun an => f ((nuncurry _ _ n anb) an)). + (A^^n-->B) -> (A^^n-->C) := + fun anb => ncurry _ _ n (fun an => f ((nuncurry _ _ n anb) an)). (** We can also us it to obtain another [fold] function, equivalent to the previous one, but with a nicer expansion (see for instance Int31.iszero). *) Fixpoint nfold_bis A B (f:A->B->B)(b:B) n : (A^^n-->B) := - match n return (A^^n-->B) with + match n return (A^^n-->B) with | O => b | S n => fun a => nfun_to_nfun_bis _ _ _ (f a) n (nfold_bis _ _ f b n) - end. + end. (** From [nprod] to [list] *) Fixpoint nprod_to_list (A:Type) n : A^n -> list A := - match n with + match n with | O => fun _ => nil | S n => fun p => let (x,p) := p in x::(nprod_to_list _ n p) - end. + end. (** From [list] to [nprod] *) Fixpoint nprod_of_list (A:Type)(l:list A) : A^(length l) := - match l return A^(length l) with + match l return A^(length l) with | nil => tt | x::l => (x, nprod_of_list _ l) - end. + end. (** This gives an additional way to write the fold *) diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 4179765dca..c8414c241d 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -1886,7 +1886,7 @@ Bind Scope positive_scope with Pos.t positive. (** Exportation of notations *) -Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope. +Numeral Notation positive Pos.of_num_int Pos.to_num_uint : positive_scope. Infix "+" := Pos.add : positive_scope. Infix "-" := Pos.sub : positive_scope. diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index 953068b010..cdb9af542c 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -595,6 +595,56 @@ Fixpoint of_uint (d:Decimal.uint) : N := | Decimal.D9 l => Npos (of_uint_acc l 1~0~0~1) end. +Local Notation sixteen := 1~0~0~0~0. + +Fixpoint of_hex_uint_acc (d:Hexadecimal.uint)(acc:positive) := + match d with + | Hexadecimal.Nil => acc + | Hexadecimal.D0 l => of_hex_uint_acc l (mul sixteen acc) + | Hexadecimal.D1 l => of_hex_uint_acc l (add 1 (mul sixteen acc)) + | Hexadecimal.D2 l => of_hex_uint_acc l (add 1~0 (mul sixteen acc)) + | Hexadecimal.D3 l => of_hex_uint_acc l (add 1~1 (mul sixteen acc)) + | Hexadecimal.D4 l => of_hex_uint_acc l (add 1~0~0 (mul sixteen acc)) + | Hexadecimal.D5 l => of_hex_uint_acc l (add 1~0~1 (mul sixteen acc)) + | Hexadecimal.D6 l => of_hex_uint_acc l (add 1~1~0 (mul sixteen acc)) + | Hexadecimal.D7 l => of_hex_uint_acc l (add 1~1~1 (mul sixteen acc)) + | Hexadecimal.D8 l => of_hex_uint_acc l (add 1~0~0~0 (mul sixteen acc)) + | Hexadecimal.D9 l => of_hex_uint_acc l (add 1~0~0~1 (mul sixteen acc)) + | Hexadecimal.Da l => of_hex_uint_acc l (add 1~0~1~0 (mul sixteen acc)) + | Hexadecimal.Db l => of_hex_uint_acc l (add 1~0~1~1 (mul sixteen acc)) + | Hexadecimal.Dc l => of_hex_uint_acc l (add 1~1~0~0 (mul sixteen acc)) + | Hexadecimal.Dd l => of_hex_uint_acc l (add 1~1~0~1 (mul sixteen acc)) + | Hexadecimal.De l => of_hex_uint_acc l (add 1~1~1~0 (mul sixteen acc)) + | Hexadecimal.Df l => of_hex_uint_acc l (add 1~1~1~1 (mul sixteen acc)) + end. + +Fixpoint of_hex_uint (d:Hexadecimal.uint) : N := + match d with + | Hexadecimal.Nil => N0 + | Hexadecimal.D0 l => of_hex_uint l + | Hexadecimal.D1 l => Npos (of_hex_uint_acc l 1) + | Hexadecimal.D2 l => Npos (of_hex_uint_acc l 1~0) + | Hexadecimal.D3 l => Npos (of_hex_uint_acc l 1~1) + | Hexadecimal.D4 l => Npos (of_hex_uint_acc l 1~0~0) + | Hexadecimal.D5 l => Npos (of_hex_uint_acc l 1~0~1) + | Hexadecimal.D6 l => Npos (of_hex_uint_acc l 1~1~0) + | Hexadecimal.D7 l => Npos (of_hex_uint_acc l 1~1~1) + | Hexadecimal.D8 l => Npos (of_hex_uint_acc l 1~0~0~0) + | Hexadecimal.D9 l => Npos (of_hex_uint_acc l 1~0~0~1) + | Hexadecimal.Da l => Npos (of_hex_uint_acc l 1~0~1~0) + | Hexadecimal.Db l => Npos (of_hex_uint_acc l 1~0~1~1) + | Hexadecimal.Dc l => Npos (of_hex_uint_acc l 1~1~0~0) + | Hexadecimal.Dd l => Npos (of_hex_uint_acc l 1~1~0~1) + | Hexadecimal.De l => Npos (of_hex_uint_acc l 1~1~1~0) + | Hexadecimal.Df l => Npos (of_hex_uint_acc l 1~1~1~1) + end. + +Definition of_num_uint (d:Numeral.uint) : N := + match d with + | Numeral.UIntDec d => of_uint d + | Numeral.UIntHex d => of_hex_uint d + end. + Definition of_int (d:Decimal.int) : option positive := match d with | Decimal.Pos d => @@ -605,6 +655,22 @@ Definition of_int (d:Decimal.int) : option positive := | Decimal.Neg _ => None end. +Definition of_hex_int (d:Hexadecimal.int) : option positive := + match d with + | Hexadecimal.Pos d => + match of_hex_uint d with + | N0 => None + | Npos p => Some p + end + | Hexadecimal.Neg _ => None + end. + +Definition of_num_int (d:Numeral.int) : option positive := + match d with + | Numeral.IntDec d => of_int d + | Numeral.IntHex d => of_hex_int d + end. + Fixpoint to_little_uint p := match p with | 1 => Decimal.D1 Decimal.Nil @@ -614,11 +680,26 @@ Fixpoint to_little_uint p := Definition to_uint p := Decimal.rev (to_little_uint p). +Fixpoint to_little_hex_uint p := + match p with + | 1 => Hexadecimal.D1 Hexadecimal.Nil + | p~1 => Hexadecimal.Little.succ_double (to_little_hex_uint p) + | p~0 => Hexadecimal.Little.double (to_little_hex_uint p) + end. + +Definition to_hex_uint p := Hexadecimal.rev (to_little_hex_uint p). + +Definition to_num_uint p := Numeral.UIntDec (to_uint p). + Definition to_int n := Decimal.Pos (to_uint n). -Numeral Notation positive of_int to_uint : positive_scope. +Definition to_hex_int p := Hexadecimal.Pos (to_hex_uint p). + +Definition to_num_int n := Numeral.IntDec (to_int n). + +Numeral Notation positive of_num_int to_num_uint : positive_scope. End Pos. (** Re-export the notation for those who just [Import BinPosDef] *) -Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope. +Numeral Notation positive Pos.of_num_int Pos.to_num_uint : positive_scope. diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index 03401aea2b..7a8ddbe71e 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -30,7 +30,4 @@ Arguments snd {A B} _. Arguments nil {A}. Arguments cons {A} _ _. -Require List. -Export List.ListNotations. - Require Import Bvector. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 74cdd1797c..84d70e56de 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -85,7 +85,51 @@ Definition to_decimal (q:Q) : option Decimal.decimal := | _ => None end. -Numeral Notation Q of_decimal to_decimal : Q_scope. +Definition of_hexadecimal (d:Hexadecimal.hexadecimal) : Q := + let '(i, f, e) := + match d with + | Hexadecimal.Hexadecimal i f => (i, f, Decimal.Pos Decimal.Nil) + | Hexadecimal.HexadecimalExp i f e => (i, f, e) + end in + let num := Z.of_hex_int (Hexadecimal.app_int i f) in + let e := Z.sub (Z.of_int e) (Z.mul 4 (Z.of_nat (Hexadecimal.nb_digits f))) in + match e with + | Z0 => Qmake num 1 + | Zpos e => Qmake (Pos.iter (Z.mul 2) num e) 1 + | Zneg e => Qmake num (Pos.iter (Pos.mul 2) 1%positive e) + end. + +Definition to_hexadecimal (q:Q) : option Hexadecimal.hexadecimal := + let mk_exp i e := + Hexadecimal.HexadecimalExp i Hexadecimal.Nil (Z.to_int (Z.opp e)) in + let num := Z.to_hex_int (Qnum q) in + let (den, e_den) := Hexadecimal.nztail (Pos.to_hex_uint (Qden q)) in + let e := Z.of_nat e_den in + match den with + | Hexadecimal.D1 Hexadecimal.Nil => + match e_den with + | O => Some (Hexadecimal.Hexadecimal num Hexadecimal.Nil) + | _ => Some (mk_exp num (4 * e)%Z) + end + | Hexadecimal.D2 Hexadecimal.Nil => Some (mk_exp num (1 + 4 * e)%Z) + | Hexadecimal.D4 Hexadecimal.Nil => Some (mk_exp num (2 + 4 * e)%Z) + | Hexadecimal.D8 Hexadecimal.Nil => Some (mk_exp num (3 + 4 * e)%Z) + | _ => None + end. + +Definition of_numeral (d:Numeral.numeral) : option Q := + match d with + | Numeral.Dec d => Some (of_decimal d) + | Numeral.Hex d => Some (of_hexadecimal d) + end. + +Definition to_numeral (q:Q) : option Numeral.numeral := + match to_decimal q with + | None => None + | Some q => Some (Numeral.Dec q) + end. + +Numeral Notation Q of_numeral to_numeral : Q_scope. Definition inject_Z (x : Z) := Qmake x 1. Arguments inject_Z x%Z. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 78b26c83ea..1729b9f85e 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1290,7 +1290,7 @@ Bind Scope Z_scope with Z.t Z. (** Re-export Notations *) -Numeral Notation Z Z.of_int Z.to_int : Z_scope. +Numeral Notation Z Z.of_num_int Z.to_num_int : Z_scope. Infix "+" := Z.add : Z_scope. Notation "- x" := (Z.opp x) : Z_scope. diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index c05ed9ebf4..8464ad1012 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -309,12 +309,32 @@ Definition to_pos (z:Z) : positive := Definition of_uint (d:Decimal.uint) := of_N (Pos.of_uint d). +Definition of_hex_uint (d:Hexadecimal.uint) := of_N (Pos.of_hex_uint d). + +Definition of_num_uint (d:Numeral.uint) := + match d with + | Numeral.UIntDec d => of_uint d + | Numeral.UIntHex d => of_hex_uint d + end. + Definition of_int (d:Decimal.int) := match d with | Decimal.Pos d => of_uint d | Decimal.Neg d => opp (of_uint d) end. +Definition of_hex_int (d:Hexadecimal.int) := + match d with + | Hexadecimal.Pos d => of_hex_uint d + | Hexadecimal.Neg d => opp (of_hex_uint d) + end. + +Definition of_num_int (d:Numeral.int) := + match d with + | Numeral.IntDec d => of_int d + | Numeral.IntHex d => of_hex_int d + end. + Definition to_int n := match n with | 0 => Decimal.Pos Decimal.zero @@ -322,6 +342,15 @@ Definition to_int n := | neg p => Decimal.Neg (Pos.to_uint p) end. +Definition to_hex_int n := + match n with + | 0 => Hexadecimal.Pos Hexadecimal.zero + | pos p => Hexadecimal.Pos (Pos.to_hex_uint p) + | neg p => Hexadecimal.Neg (Pos.to_hex_uint p) + end. + +Definition to_num_int n := Numeral.IntDec (to_int n). + (** ** Iteration of a function By convention, iterating a negative number of times is identity. @@ -639,9 +668,9 @@ Definition lxor a b := | neg a, neg b => of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b)) end. -Numeral Notation Z of_int to_int : Z_scope. +Numeral Notation Z of_num_int to_num_int : Z_scope. End Z. (** Re-export the notation for those who just [Import BinIntDef] *) -Numeral Notation Z Z.of_int Z.to_int : Z_scope. +Numeral Notation Z Z.of_num_int Z.to_num_int : Z_scope. |