diff options
Diffstat (limited to 'theories/Numbers')
74 files changed, 1745 insertions, 334 deletions
diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v index d7e4185f74..f8b3d9e1d9 100644 --- a/theories/Numbers/BinNums.v +++ b/theories/Numbers/BinNums.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** * Binary Numerical Datatypes *) diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v index 1777743fab..951a4ef2b0 100644 --- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Cyclic/Abstract/DoubleType.v b/theories/Numbers/Cyclic/Abstract/DoubleType.v index 73a064acde..fe0476e4de 100644 --- a/theories/Numbers/Cyclic/Abstract/DoubleType.v +++ b/theories/Numbers/Cyclic/Abstract/DoubleType.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index 94f8608419..64935ffe1a 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index d2390e2ce5..bd4f0279d4 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** * Int31 numbers defines indeed a cyclic structure : Z/(2^31)Z *) diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index cc359bfdf6..9f8da831d8 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Cyclic/Int31/Ring31.v b/theories/Numbers/Cyclic/Int31/Ring31.v index c076dbd9a0..b693529451 100644 --- a/theories/Numbers/Cyclic/Int31/Ring31.v +++ b/theories/Numbers/Cyclic/Int31/Ring31.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** * Int31 numbers defines Z/(2^31)Z, and can hence be equipped diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index e7658841a3..784e81758c 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** * Type [Z] viewed modulo a particular constant corresponds to [Z/nZ] diff --git a/theories/Numbers/DecimalFacts.v b/theories/Numbers/DecimalFacts.v new file mode 100644 index 0000000000..0f49052777 --- /dev/null +++ b/theories/Numbers/DecimalFacts.v @@ -0,0 +1,143 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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) *) +(************************************************************************) + +(** * DecimalFacts : some facts about Decimal numbers *) + +Require Import Decimal. + +Lemma uint_dec (d d' : uint) : { d = d' } + { d <> d' }. +Proof. + decide equality. +Defined. + +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. + +(** 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. + +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_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 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 nzhead_invol d : nzhead (nzhead d) = nzhead d. +Proof. + now induction d. +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. diff --git a/theories/Numbers/DecimalN.v b/theories/Numbers/DecimalN.v new file mode 100644 index 0000000000..ef00e2805b --- /dev/null +++ b/theories/Numbers/DecimalN.v @@ -0,0 +1,107 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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) *) +(************************************************************************) + +(** * DecimalN + + Proofs that conversions between decimal numbers and [N] + are bijections *) + +Require Import Decimal DecimalFacts DecimalPos PArith NArith. + +Module Unsigned. + +Lemma of_to (n:N) : N.of_uint (N.to_uint n) = n. +Proof. + 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). +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. +Qed. + +Lemma to_uint_surj d : exists p, N.to_uint p = unorm d. +Proof. + 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. +Qed. + +Lemma of_inj d d' : + N.of_uint d = N.of_uint d' -> unorm d = unorm d'. +Proof. + 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. +Qed. + +End Unsigned. + +(** Conversion from/to signed decimal numbers *) + +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. +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 [= <-]. +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'. +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. +Qed. + +Lemma of_int_norm d : N.of_int (norm d) = N.of_int d. +Proof. + 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. +Qed. + +End Signed. diff --git a/theories/Numbers/DecimalNat.v b/theories/Numbers/DecimalNat.v new file mode 100644 index 0000000000..5ffe1688b5 --- /dev/null +++ b/theories/Numbers/DecimalNat.v @@ -0,0 +1,302 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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) *) +(************************************************************************) + +(** * DecimalNat + + Proofs that conversions between decimal numbers and [nat] + are bijections. *) + +Require Import Decimal DecimalFacts Arith. + +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. + +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. + +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) + end. + +(** 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. + +(** A direct version of [of_little_uint] *) +Fixpoint of_lu (d:uint) : nat := + match d with + | Nil => 0 + | D0 d => 10 * of_lu d + | D1 d => 1 + 10 * of_lu d + | D2 d => 2 + 10 * of_lu d + | D3 d => 3 + 10 * of_lu d + | D4 d => 4 + 10 * of_lu d + | D5 d => 5 + 10 * of_lu d + | D6 d => 6 + 10 * of_lu d + | D7 d => 7 + 10 * of_lu d + | D8 d => 8 + 10 * of_lu d + | D9 d => 9 + 10 * 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_uint n (Little.succ d) = + Little.succ (Nat.to_little_uint n d). +Proof. + 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. +Qed. + +Lemma to_uint_alt n : + Nat.to_uint n = rev (to_lu n). +Proof. + 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). +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 10). +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' * 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. +Qed. + +Lemma of_uint_acc_spec n 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. +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. +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. +Qed. + +(** The other direction *) + +Lemma to_lu_tenfold n : n<>0 -> + 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). +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_tenfold 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). +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. +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. +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. +Qed. + +Lemma to_uint_surj d : exists n, Nat.to_uint n = unorm d. +Proof. + 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. +Qed. + +Lemma of_inj d d' : + Nat.of_uint d = Nat.of_uint d' -> unorm d = unorm d'. +Proof. + 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. +Qed. + +End Unsigned. + +(** Conversion from/to signed decimal numbers *) + +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. +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 [= <-]. +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'. +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. +Qed. + +Lemma of_int_norm d : Nat.of_int (norm d) = Nat.of_int d. +Proof. + 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'. +Proof. + 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 new file mode 100644 index 0000000000..722e73d96b --- /dev/null +++ b/theories/Numbers/DecimalPos.v @@ -0,0 +1,383 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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) *) +(************************************************************************) + +(** * DecimalPos + + Proofs that conversions between decimal numbers and [positive] + are bijections. *) + +Require Import Decimal DecimalFacts 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 => 10 * of_lu d + | D1 d => 1 + 10 * of_lu d + | D2 d => 2 + 10 * of_lu d + | D3 d => 3 + 10 * of_lu d + | D4 d => 4 + 10 * of_lu d + | D5 d => 5 + 10 * of_lu d + | D6 d => 6 + 10 * of_lu d + | D7 d => 7 + 10 * of_lu d + | D8 d => 8 + 10 * of_lu d + | D9 d => 9 + 10 * of_lu d + 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. + +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. + +Lemma of_lu_eqn d : + of_lu d = hd d + 10 * (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) + end. + +Lemma of_lu_revapp d 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. +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_uint_acc d acc = Pos.of_uint_acc (tl d) (Nadd (hd d) (10*acc)). +Proof. + 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. +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_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_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_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. +Qed. + +(** The other direction *) + +Definition to_lu n := + match n with + | N0 => Decimal.zero + | Npos p => Pos.to_little_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_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. +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 (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). +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_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. +Qed. + +(** Some consequences *) + +Lemma to_uint_nonzero p : Pos.to_uint p <> zero. +Proof. + 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. +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'. +Qed. + +Lemma to_uint_pos_surj 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. +Qed. + +Lemma of_uint_norm d : Pos.of_uint (unorm d) = Pos.of_uint d. +Proof. + now induction d. +Qed. + +Lemma of_inj d d' : + Pos.of_uint d = Pos.of_uint d' -> unorm d = unorm d'. +Proof. + 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. +Qed. + +End Unsigned. + +(** Conversion from/to signed decimal numbers *) + +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. +Qed. + +Lemma to_of (d:int)(p:positive) : + 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 [= <-]. +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'. +Qed. + +Lemma to_int_pos_surj 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. +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. +Qed. + +Lemma of_inj_pos d 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. +Qed. + +End Signed. diff --git a/theories/Numbers/DecimalString.v b/theories/Numbers/DecimalString.v new file mode 100644 index 0000000000..1a3220f63a --- /dev/null +++ b/theories/Numbers/DecimalString.v @@ -0,0 +1,265 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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 Decimal Ascii String. + +(** * Conversion between decimal numbers and Coq strings *) + +(** Pretty straightforward, which is precisely the point of the + [Decimal.int] datatype. The only catch is [Decimal.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. *) + +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. + +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)%char. +Proof. + destruct c as [[|] [|] [|] [|] [|] [|] [|] [|]]; + intros [= <-]; intuition. +Qed. + +(** Decimal/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) + 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_dec 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. + + destruct ascii_dec; subst. + * 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. + destruct ascii_dec; subst; simpl. + - 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. + +(** Decimal/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_dec 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 Decimal.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 Decimal.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. + + destruct ascii_dec; subst. + * 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). +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. + destruct ascii_dec; subst; simpl. + - 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 new file mode 100644 index 0000000000..3a08379635 --- /dev/null +++ b/theories/Numbers/DecimalZ.v @@ -0,0 +1,75 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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) *) +(************************************************************************) + +(** * DecimalZ + + Proofs that conversions between decimal numbers and [Z] + are bijections. *) + +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. +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. +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. +Qed. + +Lemma to_int_surj d : exists n, Z.to_int n = norm d. +Proof. + 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. +Qed. + +Lemma of_inj d d' : + Z.of_int d = Z.of_int d' -> norm d = norm d'. +Proof. + 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. +Qed. diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v index 9d94ff65d5..c4c5174dac 100644 --- a/theories/Numbers/Integer/Abstract/ZAdd.v +++ b/theories/Numbers/Integer/Abstract/ZAdd.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v index 84bb1a24a5..7f5b0df68e 100644 --- a/theories/Numbers/Integer/Abstract/ZAddOrder.v +++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index 6efb7ea235..4f1ab7752d 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v index b2014135f1..7fdd018d33 100644 --- a/theories/Numbers/Integer/Abstract/ZBase.v +++ b/theories/Numbers/Integer/Abstract/ZBase.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v index 68d27fec93..2da4452819 100644 --- a/theories/Numbers/Integer/Abstract/ZBits.v +++ b/theories/Numbers/Integer/Abstract/ZBits.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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 diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index 967b68d365..d7f25a6613 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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 ZAxioms ZMulOrder ZSgnAbs NZDiv. diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v index a9077127ed..a0d1821b63 100644 --- a/theories/Numbers/Integer/Abstract/ZDivFloor.v +++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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 ZAxioms ZMulOrder ZSgnAbs NZDiv. diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v index bbb8ad5ae9..31e427383d 100644 --- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v +++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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 ZAxioms ZMulOrder ZSgnAbs NZDiv. diff --git a/theories/Numbers/Integer/Abstract/ZGcd.v b/theories/Numbers/Integer/Abstract/ZGcd.v index 1144bd2bfa..f0b7bf9d25 100644 --- a/theories/Numbers/Integer/Abstract/ZGcd.v +++ b/theories/Numbers/Integer/Abstract/ZGcd.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** Properties of the greatest common divisor *) diff --git a/theories/Numbers/Integer/Abstract/ZLcm.v b/theories/Numbers/Integer/Abstract/ZLcm.v index 4b0f9f9789..0ab528de80 100644 --- a/theories/Numbers/Integer/Abstract/ZLcm.v +++ b/theories/Numbers/Integer/Abstract/ZLcm.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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 ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor. diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v index f43d74d706..726b041c21 100644 --- a/theories/Numbers/Integer/Abstract/ZLt.v +++ b/theories/Numbers/Integer/Abstract/ZLt.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Integer/Abstract/ZMaxMin.v b/theories/Numbers/Integer/Abstract/ZMaxMin.v index 40c3980a5b..f3f3a861b7 100644 --- a/theories/Numbers/Integer/Abstract/ZMaxMin.v +++ b/theories/Numbers/Integer/Abstract/ZMaxMin.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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 ZAxioms ZMulOrder GenericMinMax. diff --git a/theories/Numbers/Integer/Abstract/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v index 2550ae1c5e..120647dcc4 100644 --- a/theories/Numbers/Integer/Abstract/ZMul.v +++ b/theories/Numbers/Integer/Abstract/ZMul.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v index adea36f0e8..cd9523d34e 100644 --- a/theories/Numbers/Integer/Abstract/ZMulOrder.v +++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Integer/Abstract/ZParity.v b/theories/Numbers/Integer/Abstract/ZParity.v index db379474bf..a5e53b3615 100644 --- a/theories/Numbers/Integer/Abstract/ZParity.v +++ b/theories/Numbers/Integer/Abstract/ZParity.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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 Bool ZMulOrder NZParity. diff --git a/theories/Numbers/Integer/Abstract/ZPow.v b/theories/Numbers/Integer/Abstract/ZPow.v index 478724e2ec..a4b964e52f 100644 --- a/theories/Numbers/Integer/Abstract/ZPow.v +++ b/theories/Numbers/Integer/Abstract/ZPow.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** Properties of the power function *) diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v index 4a0ce5e5bf..e4b997cfdc 100644 --- a/theories/Numbers/Integer/Abstract/ZProperties.v +++ b/theories/Numbers/Integer/Abstract/ZProperties.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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 Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow ZDivTrunc ZDivFloor diff --git a/theories/Numbers/Integer/Abstract/ZSgnAbs.v b/theories/Numbers/Integer/Abstract/ZSgnAbs.v index b2f77c3f59..dda1287269 100644 --- a/theories/Numbers/Integer/Abstract/ZSgnAbs.v +++ b/theories/Numbers/Integer/Abstract/ZSgnAbs.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** Properties of [abs] and [sgn] *) diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index 553bd68acf..bed827fd0e 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index c640145ba3..4b2d5c13b5 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/NaryFunctions.v b/theories/Numbers/NaryFunctions.v index cf0d2e8352..ee28628ed9 100644 --- a/theories/Numbers/NaryFunctions.v +++ b/theories/Numbers/NaryFunctions.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Pierre Letouzey, Jerome Vouillon, PPS, Paris 7, 2008 *) (************************************************************************) diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v index 4beab1e1ba..bc366c508d 100644 --- a/theories/Numbers/NatInt/NZAdd.v +++ b/theories/Numbers/NatInt/NZAdd.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v index 82e500ca21..99812ee3fe 100644 --- a/theories/Numbers/NatInt/NZAddOrder.v +++ b/theories/Numbers/NatInt/NZAddOrder.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index c0851791d7..8c364cde7d 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** Initial Author : Evgeny Makarov, INRIA, 2007 *) diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index e0d55b8937..595b2182ab 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/NatInt/NZBits.v b/theories/Numbers/NatInt/NZBits.v index d731de62d6..eefa51572f 100644 --- a/theories/Numbers/NatInt/NZBits.v +++ b/theories/Numbers/NatInt/NZBits.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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 Bool NZAxioms NZMulOrder NZParity NZPow NZDiv NZLog. diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index 5610eccb75..550aa226ac 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** Euclidean Division *) diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v index f5ee1351d4..3d0c005fd1 100644 --- a/theories/Numbers/NatInt/NZDomain.v +++ b/theories/Numbers/NatInt/NZDomain.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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 Export NumPrelude NZAxioms. diff --git a/theories/Numbers/NatInt/NZGcd.v b/theories/Numbers/NatInt/NZGcd.v index f8af97196a..c38d1aac31 100644 --- a/theories/Numbers/NatInt/NZGcd.v +++ b/theories/Numbers/NatInt/NZGcd.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** Greatest Common Divisor *) diff --git a/theories/Numbers/NatInt/NZLog.v b/theories/Numbers/NatInt/NZLog.v index 239f20a42d..794851a9dd 100644 --- a/theories/Numbers/NatInt/NZLog.v +++ b/theories/Numbers/NatInt/NZLog.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** Base-2 Logarithm *) diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v index 145f56352b..44cbc51712 100644 --- a/theories/Numbers/NatInt/NZMul.v +++ b/theories/Numbers/NatInt/NZMul.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v index 430f8fd2e1..292f0837c0 100644 --- a/theories/Numbers/NatInt/NZMulOrder.v +++ b/theories/Numbers/NatInt/NZMulOrder.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 37ec464108..60e1123b35 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v index 626d59d73e..93d99f08f5 100644 --- a/theories/Numbers/NatInt/NZParity.v +++ b/theories/Numbers/NatInt/NZParity.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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 Bool NZAxioms NZMulOrder. diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v index 350047fa1e..a1310667e1 100644 --- a/theories/Numbers/NatInt/NZPow.v +++ b/theories/Numbers/NatInt/NZPow.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** Power Function *) diff --git a/theories/Numbers/NatInt/NZProperties.v b/theories/Numbers/NatInt/NZProperties.v index aee3b6245a..fbcf43e880 100644 --- a/theories/Numbers/NatInt/NZProperties.v +++ b/theories/Numbers/NatInt/NZProperties.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v index c03107299f..c2d2c4ae19 100644 --- a/theories/Numbers/NatInt/NZSqrt.v +++ b/theories/Numbers/NatInt/NZSqrt.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** Square Root Function *) diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v index 899fa39333..dc5f8e5372 100644 --- a/theories/Numbers/Natural/Abstract/NAdd.v +++ b/theories/Numbers/Natural/Abstract/NAdd.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Natural/Abstract/NAddOrder.v b/theories/Numbers/Natural/Abstract/NAddOrder.v index d62903db61..2da3f0bfcb 100644 --- a/theories/Numbers/Natural/Abstract/NAddOrder.v +++ b/theories/Numbers/Natural/Abstract/NAddOrder.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v index d67689dbda..dd09ac5f3e 100644 --- a/theories/Numbers/Natural/Abstract/NAxioms.v +++ b/theories/Numbers/Natural/Abstract/NAxioms.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index 85a015cf26..ad0b3d3d2a 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v index 1e7644edaf..e1391f5990 100644 --- a/theories/Numbers/Natural/Abstract/NBits.v +++ b/theories/Numbers/Natural/Abstract/NBits.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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 Bool NAxioms NSub NPow NDiv NParity NLog. diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v index e934eda9b5..8e1be0d702 100644 --- a/theories/Numbers/Natural/Abstract/NDefOps.v +++ b/theories/Numbers/Natural/Abstract/NDefOps.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v index eff27abc52..4c26a071f0 100644 --- a/theories/Numbers/Natural/Abstract/NDiv.v +++ b/theories/Numbers/Natural/Abstract/NDiv.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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 NAxioms NSub NZDiv. diff --git a/theories/Numbers/Natural/Abstract/NGcd.v b/theories/Numbers/Natural/Abstract/NGcd.v index 943caef637..96fb4247cc 100644 --- a/theories/Numbers/Natural/Abstract/NGcd.v +++ b/theories/Numbers/Natural/Abstract/NGcd.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** Properties of the greatest common divisor *) diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v index 2b61f97840..d41d0aff56 100644 --- a/theories/Numbers/Natural/Abstract/NIso.v +++ b/theories/Numbers/Natural/Abstract/NIso.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Natural/Abstract/NLcm.v b/theories/Numbers/Natural/Abstract/NLcm.v index 2e7bcf40c2..47b74193ed 100644 --- a/theories/Numbers/Natural/Abstract/NLcm.v +++ b/theories/Numbers/Natural/Abstract/NLcm.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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 NAxioms NSub NDiv NGcd. diff --git a/theories/Numbers/Natural/Abstract/NLog.v b/theories/Numbers/Natural/Abstract/NLog.v index d22510ab9b..fe6fcee567 100644 --- a/theories/Numbers/Natural/Abstract/NLog.v +++ b/theories/Numbers/Natural/Abstract/NLog.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** Base-2 Logarithm Properties *) diff --git a/theories/Numbers/Natural/Abstract/NMaxMin.v b/theories/Numbers/Natural/Abstract/NMaxMin.v index 1020fe375d..3cf4d3f9f2 100644 --- a/theories/Numbers/Natural/Abstract/NMaxMin.v +++ b/theories/Numbers/Natural/Abstract/NMaxMin.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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 NAxioms NSub GenericMinMax. diff --git a/theories/Numbers/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v index ace1e736eb..b7f1c8e453 100644 --- a/theories/Numbers/Natural/Abstract/NMulOrder.v +++ b/theories/Numbers/Natural/Abstract/NMulOrder.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index f05d783ad0..acaecad93c 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Natural/Abstract/NParity.v b/theories/Numbers/Natural/Abstract/NParity.v index fd136ff93f..cb89e1d729 100644 --- a/theories/Numbers/Natural/Abstract/NParity.v +++ b/theories/Numbers/Natural/Abstract/NParity.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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 Bool NSub NZParity. diff --git a/theories/Numbers/Natural/Abstract/NPow.v b/theories/Numbers/Natural/Abstract/NPow.v index d31d67a1ce..fc1cc93b11 100644 --- a/theories/Numbers/Natural/Abstract/NPow.v +++ b/theories/Numbers/Natural/Abstract/NPow.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** Properties of the power function *) diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v index b753d659a9..bcf906cf92 100644 --- a/theories/Numbers/Natural/Abstract/NProperties.v +++ b/theories/Numbers/Natural/Abstract/NProperties.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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 Export NAxioms. diff --git a/theories/Numbers/Natural/Abstract/NSqrt.v b/theories/Numbers/Natural/Abstract/NSqrt.v index 68c06775e4..6bffe693e6 100644 --- a/theories/Numbers/Natural/Abstract/NSqrt.v +++ b/theories/Numbers/Natural/Abstract/NSqrt.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** Properties of Square Root Function *) diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v index 8e825ef7d8..f76d8ae8a2 100644 --- a/theories/Numbers/Natural/Abstract/NStrongRec.v +++ b/theories/Numbers/Natural/Abstract/NStrongRec.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v index dce78f610b..453b0c0d4c 100644 --- a/theories/Numbers/Natural/Abstract/NSub.v +++ b/theories/Numbers/Natural/Abstract/NSub.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index bdb715f330..c9e1c64013 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 787ef81dc9..6000bdcf79 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) @@ -18,74 +20,74 @@ Module Nat <: NAxiomsSig := Nat. (** Compat notations for stuff that used to be at the beginning of NPeano. *) -Notation leb := Nat.leb (compat "8.4"). -Notation ltb := Nat.ltb (compat "8.4"). -Notation leb_le := Nat.leb_le (compat "8.4"). -Notation ltb_lt := Nat.ltb_lt (compat "8.4"). -Notation pow := Nat.pow (compat "8.4"). -Notation pow_0_r := Nat.pow_0_r (compat "8.4"). -Notation pow_succ_r := Nat.pow_succ_r (compat "8.4"). -Notation square := Nat.square (compat "8.4"). -Notation square_spec := Nat.square_spec (compat "8.4"). -Notation Even := Nat.Even (compat "8.4"). -Notation Odd := Nat.Odd (compat "8.4"). -Notation even := Nat.even (compat "8.4"). -Notation odd := Nat.odd (compat "8.4"). -Notation even_spec := Nat.even_spec (compat "8.4"). -Notation odd_spec := Nat.odd_spec (compat "8.4"). +Notation leb := Nat.leb (only parsing). +Notation ltb := Nat.ltb (only parsing). +Notation leb_le := Nat.leb_le (only parsing). +Notation ltb_lt := Nat.ltb_lt (only parsing). +Notation pow := Nat.pow (only parsing). +Notation pow_0_r := Nat.pow_0_r (only parsing). +Notation pow_succ_r := Nat.pow_succ_r (only parsing). +Notation square := Nat.square (only parsing). +Notation square_spec := Nat.square_spec (only parsing). +Notation Even := Nat.Even (only parsing). +Notation Odd := Nat.Odd (only parsing). +Notation even := Nat.even (only parsing). +Notation odd := Nat.odd (only parsing). +Notation even_spec := Nat.even_spec (only parsing). +Notation odd_spec := Nat.odd_spec (only parsing). Lemma Even_equiv n : Even n <-> Even.even n. Proof. symmetry. apply Even.even_equiv. Qed. Lemma Odd_equiv n : Odd n <-> Even.odd n. Proof. symmetry. apply Even.odd_equiv. Qed. -Notation divmod := Nat.divmod (compat "8.4"). -Notation div := Nat.div (compat "8.4"). -Notation modulo := Nat.modulo (compat "8.4"). -Notation divmod_spec := Nat.divmod_spec (compat "8.4"). -Notation div_mod := Nat.div_mod (compat "8.4"). -Notation mod_bound_pos := Nat.mod_bound_pos (compat "8.4"). -Notation sqrt_iter := Nat.sqrt_iter (compat "8.4"). -Notation sqrt := Nat.sqrt (compat "8.4"). -Notation sqrt_iter_spec := Nat.sqrt_iter_spec (compat "8.4"). -Notation sqrt_spec := Nat.sqrt_spec (compat "8.4"). -Notation log2_iter := Nat.log2_iter (compat "8.4"). -Notation log2 := Nat.log2 (compat "8.4"). -Notation log2_iter_spec := Nat.log2_iter_spec (compat "8.4"). -Notation log2_spec := Nat.log2_spec (compat "8.4"). -Notation log2_nonpos := Nat.log2_nonpos (compat "8.4"). -Notation gcd := Nat.gcd (compat "8.4"). -Notation divide := Nat.divide (compat "8.4"). -Notation gcd_divide := Nat.gcd_divide (compat "8.4"). -Notation gcd_divide_l := Nat.gcd_divide_l (compat "8.4"). -Notation gcd_divide_r := Nat.gcd_divide_r (compat "8.4"). -Notation gcd_greatest := Nat.gcd_greatest (compat "8.4"). -Notation testbit := Nat.testbit (compat "8.4"). -Notation shiftl := Nat.shiftl (compat "8.4"). -Notation shiftr := Nat.shiftr (compat "8.4"). -Notation bitwise := Nat.bitwise (compat "8.4"). -Notation land := Nat.land (compat "8.4"). -Notation lor := Nat.lor (compat "8.4"). -Notation ldiff := Nat.ldiff (compat "8.4"). -Notation lxor := Nat.lxor (compat "8.4"). -Notation double_twice := Nat.double_twice (compat "8.4"). -Notation testbit_0_l := Nat.testbit_0_l (compat "8.4"). -Notation testbit_odd_0 := Nat.testbit_odd_0 (compat "8.4"). -Notation testbit_even_0 := Nat.testbit_even_0 (compat "8.4"). -Notation testbit_odd_succ := Nat.testbit_odd_succ (compat "8.4"). -Notation testbit_even_succ := Nat.testbit_even_succ (compat "8.4"). -Notation shiftr_spec := Nat.shiftr_spec (compat "8.4"). -Notation shiftl_spec_high := Nat.shiftl_spec_high (compat "8.4"). -Notation shiftl_spec_low := Nat.shiftl_spec_low (compat "8.4"). -Notation div2_bitwise := Nat.div2_bitwise (compat "8.4"). -Notation odd_bitwise := Nat.odd_bitwise (compat "8.4"). -Notation div2_decr := Nat.div2_decr (compat "8.4"). -Notation testbit_bitwise_1 := Nat.testbit_bitwise_1 (compat "8.4"). -Notation testbit_bitwise_2 := Nat.testbit_bitwise_2 (compat "8.4"). -Notation land_spec := Nat.land_spec (compat "8.4"). -Notation ldiff_spec := Nat.ldiff_spec (compat "8.4"). -Notation lor_spec := Nat.lor_spec (compat "8.4"). -Notation lxor_spec := Nat.lxor_spec (compat "8.4"). +Notation divmod := Nat.divmod (only parsing). +Notation div := Nat.div (only parsing). +Notation modulo := Nat.modulo (only parsing). +Notation divmod_spec := Nat.divmod_spec (only parsing). +Notation div_mod := Nat.div_mod (only parsing). +Notation mod_bound_pos := Nat.mod_bound_pos (only parsing). +Notation sqrt_iter := Nat.sqrt_iter (only parsing). +Notation sqrt := Nat.sqrt (only parsing). +Notation sqrt_iter_spec := Nat.sqrt_iter_spec (only parsing). +Notation sqrt_spec := Nat.sqrt_spec (only parsing). +Notation log2_iter := Nat.log2_iter (only parsing). +Notation log2 := Nat.log2 (only parsing). +Notation log2_iter_spec := Nat.log2_iter_spec (only parsing). +Notation log2_spec := Nat.log2_spec (only parsing). +Notation log2_nonpos := Nat.log2_nonpos (only parsing). +Notation gcd := Nat.gcd (only parsing). +Notation divide := Nat.divide (only parsing). +Notation gcd_divide := Nat.gcd_divide (only parsing). +Notation gcd_divide_l := Nat.gcd_divide_l (only parsing). +Notation gcd_divide_r := Nat.gcd_divide_r (only parsing). +Notation gcd_greatest := Nat.gcd_greatest (only parsing). +Notation testbit := Nat.testbit (only parsing). +Notation shiftl := Nat.shiftl (only parsing). +Notation shiftr := Nat.shiftr (only parsing). +Notation bitwise := Nat.bitwise (only parsing). +Notation land := Nat.land (only parsing). +Notation lor := Nat.lor (only parsing). +Notation ldiff := Nat.ldiff (only parsing). +Notation lxor := Nat.lxor (only parsing). +Notation double_twice := Nat.double_twice (only parsing). +Notation testbit_0_l := Nat.testbit_0_l (only parsing). +Notation testbit_odd_0 := Nat.testbit_odd_0 (only parsing). +Notation testbit_even_0 := Nat.testbit_even_0 (only parsing). +Notation testbit_odd_succ := Nat.testbit_odd_succ (only parsing). +Notation testbit_even_succ := Nat.testbit_even_succ (only parsing). +Notation shiftr_spec := Nat.shiftr_spec (only parsing). +Notation shiftl_spec_high := Nat.shiftl_spec_high (only parsing). +Notation shiftl_spec_low := Nat.shiftl_spec_low (only parsing). +Notation div2_bitwise := Nat.div2_bitwise (only parsing). +Notation odd_bitwise := Nat.odd_bitwise (only parsing). +Notation div2_decr := Nat.div2_decr (only parsing). +Notation testbit_bitwise_1 := Nat.testbit_bitwise_1 (only parsing). +Notation testbit_bitwise_2 := Nat.testbit_bitwise_2 (only parsing). +Notation land_spec := Nat.land_spec (only parsing). +Notation ldiff_spec := Nat.ldiff_spec (only parsing). +Notation lor_spec := Nat.lor_spec (only parsing). +Notation lxor_spec := Nat.lxor_spec (only parsing). Infix "<=?" := Nat.leb (at level 70) : nat_scope. Infix "<?" := Nat.ltb (at level 70) : nat_scope. diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v index f01d5880e4..7cf13feaea 100644 --- a/theories/Numbers/NumPrelude.v +++ b/theories/Numbers/NumPrelude.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) |