From a36a01526e76f4ef92bc87445da33dfb025e2db4 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sat, 29 Oct 2022 17:26:26 +0200 Subject: [PATCH] update boilerplate for 8.16 --- .github/workflows/docker-action.yml | 1 + coq-qarith-stern-brocot.opam | 2 +- meta.yml | 3 ++- theories/Field_Theory_Q.v | 8 +++----- theories/QArith_Stern_Brocot.v | 17 ++++++++--------- theories/Q_Archimedean.v | 8 +++----- theories/Q_denumerable.v | 8 ++++---- theories/Q_field.v | 4 +--- theories/Q_order.v | 2 +- theories/Q_ordered_field_properties.v | 5 ++--- theories/Q_to_R.v | 12 +++++------- theories/Qabs.v | 7 +++---- theories/Qhomographic.v | 8 ++------ .../Qhomographic_Qpositive_to_Q_properties.v | 4 ++-- theories/Qhomographic_Qpositive_to_Qpositive.v | 8 ++++---- theories/Qhomographic_sign.v | 6 ++---- theories/Qhomographic_sign_properties.v | 6 +++--- theories/Qmax_min.v | 7 +++---- theories/Qpositive.v | 12 ++++++------ theories/Qpositive_le.v | 2 +- theories/Qpositive_order.v | 4 ++-- theories/Qpositive_plus_mult.v | 2 +- theories/Qpositive_sub.v | 2 +- theories/Qquadratic.v | 9 +++------ .../Qquadratic_Qpositive_to_Q_properties.v | 6 +++--- theories/Qquadratic_Qpositive_to_Qpositive.v | 6 ++---- theories/Qquadratic_sign.v | 8 +++----- theories/Qquadratic_sign_properties.v | 9 ++++----- theories/Qsyntax.v | 3 +-- theories/R_addenda.v | 10 +++++----- theories/Zaux.v | 12 +++++------- theories/general_Q.v | 12 ++++++------ theories/homographicAcc_Qhomographic_sign.v | 8 +++----- theories/homographic_correctness.v | 6 +++--- theories/positive_fraction_encoding.v | 11 +++++------ theories/quadraticAcc_Qquadratic_sign.v | 6 +++--- theories/quadratic_correctness.v | 18 +++++++++--------- theories/second_Field_Theory_Q.v | 4 ++-- theories/sqrt2.v | 10 +++++----- 39 files changed, 123 insertions(+), 153 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 3a10361..62aea63 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -18,6 +18,7 @@ jobs: matrix: image: - 'coqorg/coq:dev' + - 'coqorg/coq:8.16' - 'coqorg/coq:8.15' - 'coqorg/coq:8.14' fail-fast: false diff --git a/coq-qarith-stern-brocot.opam b/coq-qarith-stern-brocot.opam index 114869f..ab6fbcd 100644 --- a/coq-qarith-stern-brocot.opam +++ b/coq-qarith-stern-brocot.opam @@ -16,7 +16,7 @@ field operations on them in two different ways: strict and lazy. build: ["dune" "build" "-p" name "-j" jobs] depends: [ "dune" {>= "2.5"} - "coq" {(>= "8.14" & < "8.16~") | (= "dev")} + "coq" {(>= "8.14" & < "8.17~") | (= "dev")} ] tags: [ diff --git a/meta.yml b/meta.yml index fd7e9e0..9b12632 100644 --- a/meta.yml +++ b/meta.yml @@ -35,10 +35,11 @@ license: supported_coq_versions: text: 8.14 or later - opam: '{(>= "8.14" & < "8.16~") | (= "dev")}' + opam: '{(>= "8.14" & < "8.17~") | (= "dev")}' tested_coq_opam_versions: - version: dev +- version: '8.16' - version: '8.15' - version: '8.14' diff --git a/theories/Field_Theory_Q.v b/theories/Field_Theory_Q.v index 59c80c1..f888027 100644 --- a/theories/Field_Theory_Q.v +++ b/theories/Field_Theory_Q.v @@ -13,11 +13,9 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) - -Require Import Eqdep_dec. -Require Export Field. -Require Export Q_order. - +From Coq Require Import Eqdep_dec. +From Coq Require Export Field. +From QArithSternBrocot Require Export Q_order. (*###########################################################################*) (** The Filed Structure for Field Tactic *) diff --git a/theories/QArith_Stern_Brocot.v b/theories/QArith_Stern_Brocot.v index 65ae6f4..9281356 100644 --- a/theories/QArith_Stern_Brocot.v +++ b/theories/QArith_Stern_Brocot.v @@ -15,12 +15,11 @@ library. If you do not want to use these (classical) real numbers you should not import this file. Instead you can use all the other modules that are imported here, except Q_to_R. *) -Require Export Qsyntax. -Require Export Field_Theory_Q. -Require Export Q_ordered_field_properties. -Require Export QArithSternBrocot.Qabs. -Require Export Qmax_min. -Require Export Q_Archimedean. -Require Export Q_denumerable. -Require Export Q_to_R. - +From QArithSternBrocot Require Export Qsyntax. +From QArithSternBrocot Require Export Field_Theory_Q. +From QArithSternBrocot Require Export Q_ordered_field_properties. +From QArithSternBrocot Require Export Qabs. +From QArithSternBrocot Require Export Qmax_min. +From QArithSternBrocot Require Export Q_Archimedean. +From QArithSternBrocot Require Export Q_denumerable. +From QArithSternBrocot Require Export Q_to_R. diff --git a/theories/Q_Archimedean.v b/theories/Q_Archimedean.v index 9c6a6f7..d2f1d22 100644 --- a/theories/Q_Archimedean.v +++ b/theories/Q_Archimedean.v @@ -6,11 +6,9 @@ (* *) (************************************************************************) - -Require Export Qsyntax. -Require Export Field_Theory_Q. -Require Export Q_ordered_field_properties. - +From QArithSternBrocot Require Export Qsyntax. +From QArithSternBrocot Require Export Field_Theory_Q. +From QArithSternBrocot Require Export Q_ordered_field_properties. Lemma Qpositive_in_Q_Archimedean_inf:forall qp:Qpositive, {z:Z | (Qpos qp)<=z /\ (z-(Qpos qp))<= Qone}. Proof. diff --git a/theories/Q_denumerable.v b/theories/Q_denumerable.v index 222ba55..fff4ce2 100644 --- a/theories/Q_denumerable.v +++ b/theories/Q_denumerable.v @@ -61,9 +61,9 @@ End Denumerability. (** We first prove that [Z] is denumerable *) -Require Div2. -Require Import ZArith. -Require Import Lia. +From Coq Require Div2. +From Coq Require Import ZArith. +From Coq Require Import Lia. (** An injection from [Z] to [nat] *) Definition Z_to_nat_i (z:Z) :nat := @@ -229,7 +229,7 @@ Defined. (** Next we prove that [Q] and [Z] have the same cardinality *) -Require Import Q_field. +From QArithSternBrocot Require Import Q_field. (** Here there is not much to prove, as [Z] and [Q] are isomorphic data-types.*) diff --git a/theories/Q_field.v b/theories/Q_field.v index 6593a0c..a5e0579 100644 --- a/theories/Q_field.v +++ b/theories/Q_field.v @@ -13,9 +13,7 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) - -Require Export Qpositive_sub. - +From QArithSternBrocot Require Export Qpositive_sub. Inductive Q : Set := | Zero : Q diff --git a/theories/Q_order.v b/theories/Q_order.v index 68addb4..7ea76a7 100644 --- a/theories/Q_order.v +++ b/theories/Q_order.v @@ -13,7 +13,7 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) -Require Export Q_field. +From QArithSternBrocot Require Export Q_field. Theorem Qmult_sym : forall n m : Q, Qmult n m = Qmult m n. intros n m; case m; case n; auto; intros n' m'; simpl in |- *; diff --git a/theories/Q_ordered_field_properties.v b/theories/Q_ordered_field_properties.v index 341a2c6..9fc98a3 100644 --- a/theories/Q_ordered_field_properties.v +++ b/theories/Q_ordered_field_properties.v @@ -6,9 +6,8 @@ (* *) (************************************************************************) - -Require Export Qsyntax. -Require Export Field_Theory_Q. +From QArithSternBrocot Require Export Qsyntax. +From QArithSternBrocot Require Export Field_Theory_Q. Lemma Qmult_absorb_nonzero_r: forall x y : Q, x * y <> Zero -> y <> Zero. Proof. diff --git a/theories/Q_to_R.v b/theories/Q_to_R.v index fbabf22..168caeb 100644 --- a/theories/Q_to_R.v +++ b/theories/Q_to_R.v @@ -6,13 +6,12 @@ (* *) (************************************************************************) -(* This file contains properties of the injection from Q into R. *) - -Require Import Q_ordered_field_properties. -Require Import R_addenda. -Require Import Raxioms. -Require Import RIneq. +(** This file contains properties of the injection from Q into R. *) +From QArithSternBrocot Require Import Q_ordered_field_properties. +From QArithSternBrocot Require Import R_addenda. +From Coq Require Import Raxioms. +From Coq Require Import RIneq. (** We define the injection from Q into R *) @@ -449,7 +448,6 @@ Proof. rewrite Ropp_inv_permute; auto. Qed. - Lemma Q_to_Rminus: forall x y, Q_to_R (Qminus x y) = (Rminus (Q_to_R x) (Q_to_R y)). Proof. intros x y; unfold Qminus; rewrite Q_to_Rplus; rewrite Q_to_Ropp; trivial. diff --git a/theories/Qabs.v b/theories/Qabs.v index 93f47f3..ea8ef78 100644 --- a/theories/Qabs.v +++ b/theories/Qabs.v @@ -6,10 +6,9 @@ (* *) (************************************************************************) - -Require Export Qsyntax. -Require Export Field_Theory_Q. -Require Export Q_ordered_field_properties. +From QArithSternBrocot Require Export Qsyntax. +From QArithSternBrocot Require Export Field_Theory_Q. +From QArithSternBrocot Require Export Q_ordered_field_properties. Definition Qabs (q:Q):Q:= match q with diff --git a/theories/Qhomographic.v b/theories/Qhomographic.v index 7ca7d04..d345ef4 100644 --- a/theories/Qhomographic.v +++ b/theories/Qhomographic.v @@ -13,12 +13,8 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) - - -Require Export homographicAcc_Qhomographic_sign. -Require Import ZArithRing. - - +From QArithSternBrocot Require Export homographicAcc_Qhomographic_sign. +From Coq Require Import ZArithRing. (** note that ~(`c=0`/\`d=0`)<->`c<>0`\/`c<>d` *) diff --git a/theories/Qhomographic_Qpositive_to_Q_properties.v b/theories/Qhomographic_Qpositive_to_Q_properties.v index 62c9d64..52ef182 100644 --- a/theories/Qhomographic_Qpositive_to_Q_properties.v +++ b/theories/Qhomographic_Qpositive_to_Q_properties.v @@ -13,8 +13,8 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) -Require Import FunInd. -Require Export Qhomographic. +From Coq Require Import FunInd. +From QArithSternBrocot Require Export Qhomographic. Functional Scheme fraction_encoding_ind := Induction for fraction_encoding Sort Prop. diff --git a/theories/Qhomographic_Qpositive_to_Qpositive.v b/theories/Qhomographic_Qpositive_to_Qpositive.v index ebf6b3c..f42961d 100644 --- a/theories/Qhomographic_Qpositive_to_Qpositive.v +++ b/theories/Qhomographic_Qpositive_to_Qpositive.v @@ -13,10 +13,10 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) -Require Export general_Q. -Require Export positive_fraction_encoding. -Require Import Merge_Order. -Require Import Wf_nat. +From QArithSternBrocot Require Export general_Q. +From QArithSternBrocot Require Export positive_fraction_encoding. +From QArithSternBrocot Require Import Merge_Order. +From Coq Require Import Wf_nat. Definition top_more (a b c d : Z) := (c <= a)%Z /\ (d < b)%Z \/ (c < a)%Z /\ (d <= b)%Z. diff --git a/theories/Qhomographic_sign.v b/theories/Qhomographic_sign.v index 629e502..9a756fc 100644 --- a/theories/Qhomographic_sign.v +++ b/theories/Qhomographic_sign.v @@ -13,10 +13,8 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) - - -Require Export positive_fraction_encoding. -Require Import ZArithRing. +From QArithSternBrocot Require Export positive_fraction_encoding. +From Coq Require Import ZArithRing. Definition outside_interval (a b : Z) := (Z.sgn a + Z.sgn b)%Z. diff --git a/theories/Qhomographic_sign_properties.v b/theories/Qhomographic_sign_properties.v index 7fd3500..3ba84fd 100644 --- a/theories/Qhomographic_sign_properties.v +++ b/theories/Qhomographic_sign_properties.v @@ -13,9 +13,9 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) - -Require Export Qhomographic_sign. -Require Import ZArithRing Zaux. +From QArithSternBrocot Require Export Qhomographic_sign. +From Coq Require Import ZArithRing. +From QArithSternBrocot Require Import Zaux. Lemma sg_tuple_equal : forall (l1 a1 b1 c1 d1 : Z) (p1 : Qpositive) (l2 a2 b2 c2 d2 : Z) diff --git a/theories/Qmax_min.v b/theories/Qmax_min.v index 5ed60ac..49d1502 100644 --- a/theories/Qmax_min.v +++ b/theories/Qmax_min.v @@ -6,10 +6,9 @@ (* *) (************************************************************************) -Require Export Qsyntax. -Require Export Field_Theory_Q. -Require Export Q_ordered_field_properties. - +From QArithSternBrocot Require Export Qsyntax. +From QArithSternBrocot Require Export Field_Theory_Q. +From QArithSternBrocot Require Export Q_ordered_field_properties. Definition Qmax p q := if Q_le_lt_dec p q then q else p. diff --git a/theories/Qpositive.v b/theories/Qpositive.v index 85f02f4..2d6a504 100644 --- a/theories/Qpositive.v +++ b/theories/Qpositive.v @@ -13,12 +13,12 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) -Require Export Arith. -Require Export Compare_dec. -Require Export ArithRing. -Require Export Lia. -Require Export ZArith. -Require Export ZArithRing. +From Coq Require Export Arith. +From Coq Require Export Compare_dec. +From Coq Require Export ArithRing. +From Coq Require Export Lia. +From Coq Require Export ZArith. +From Coq Require Export ZArithRing. Ltac CaseEq f := generalize (refl_equal f); pattern f at -1 in |- *; case f. diff --git a/theories/Qpositive_le.v b/theories/Qpositive_le.v index f5f526d..dc00112 100644 --- a/theories/Qpositive_le.v +++ b/theories/Qpositive_le.v @@ -13,7 +13,7 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) -Require Export Qpositive. +From QArithSternBrocot Require Export Qpositive. Fixpoint Qpositive_le_bool (w w' : Qpositive) {struct w'} : bool := match w with diff --git a/theories/Qpositive_order.v b/theories/Qpositive_order.v index e9d3ee6..ec06719 100644 --- a/theories/Qpositive_order.v +++ b/theories/Qpositive_order.v @@ -13,8 +13,8 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) -Require Export Qpositive_le. -Require Export Qpositive_plus_mult. +From QArithSternBrocot Require Export Qpositive_le. +From QArithSternBrocot Require Export Qpositive_plus_mult. (* These tactics were originally in a different file, but moved here *) diff --git a/theories/Qpositive_plus_mult.v b/theories/Qpositive_plus_mult.v index e0295e5..a5177c2 100644 --- a/theories/Qpositive_plus_mult.v +++ b/theories/Qpositive_plus_mult.v @@ -13,7 +13,7 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) -Require Export Qpositive. +From QArithSternBrocot Require Export Qpositive. Definition Qpositive_plus (w w' : Qpositive) : Qpositive := let (p, q) := Qpositive_i w in diff --git a/theories/Qpositive_sub.v b/theories/Qpositive_sub.v index 8324d71..9458991 100644 --- a/theories/Qpositive_sub.v +++ b/theories/Qpositive_sub.v @@ -13,7 +13,7 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) -Require Export Qpositive_order. +From QArithSternBrocot Require Export Qpositive_order. Definition Qpositive_sub (w w' : Qpositive) := let (p, q) := Qpositive_i w in diff --git a/theories/Qquadratic.v b/theories/Qquadratic.v index bb1a5af..d8c1415 100644 --- a/theories/Qquadratic.v +++ b/theories/Qquadratic.v @@ -13,8 +13,6 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) - - (** -- These are arithmetic operations on signed Stern-Brocot numbers Qplus_lazy :: [Char] -> [Char] -> [Char] @@ -27,10 +25,9 @@ Qminus_lazy :: [Char] -> [Char] -> [Char] Qminus_lazy = Qquadratic 0 1 (-1) 0 0 0 0 1 *) -Require Export Qhomographic. -Require Export quadraticAcc_Qquadratic_sign. -Require Import general_Q Zaux. - +From QArithSternBrocot Require Export Qhomographic. +From QArithSternBrocot Require Export quadraticAcc_Qquadratic_sign. +From QArithSternBrocot Require Import general_Q Zaux. Lemma Qquadratic_sg_denom_nonzero_always : forall (k e f g h : Z) (p1 p2 : Qpositive), diff --git a/theories/Qquadratic_Qpositive_to_Q_properties.v b/theories/Qquadratic_Qpositive_to_Q_properties.v index 47f2e78..50f69b1 100644 --- a/theories/Qquadratic_Qpositive_to_Q_properties.v +++ b/theories/Qquadratic_Qpositive_to_Q_properties.v @@ -13,9 +13,9 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) -Require Import FunInd. -Require Export Qquadratic. -Require Import homographic_correctness. +From Coq Require Import FunInd. +From QArithSternBrocot Require Export Qquadratic. +From QArithSternBrocot Require Import homographic_correctness. Lemma fraction_encoding_reduces : forall (a b m n : Z) (Hb : b <> 0%Z) (Hn : n <> 0%Z), diff --git a/theories/Qquadratic_Qpositive_to_Qpositive.v b/theories/Qquadratic_Qpositive_to_Qpositive.v index 1ff5552..09c47ae 100644 --- a/theories/Qquadratic_Qpositive_to_Qpositive.v +++ b/theories/Qquadratic_Qpositive_to_Qpositive.v @@ -13,10 +13,8 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) - - -Require Import Merge_Order. -Require Export Qhomographic_Qpositive_to_Qpositive. +From QArithSternBrocot Require Import Merge_Order. +From QArithSternBrocot Require Export Qhomographic_Qpositive_to_Qpositive. Definition quadratic_top_more (a b c d e f g h : Z) := (e <= a)%Z /\ (f <= b)%Z /\ (g <= c)%Z /\ (h < d)%Z \/ diff --git a/theories/Qquadratic_sign.v b/theories/Qquadratic_sign.v index 829c6cd..a50d08b 100644 --- a/theories/Qquadratic_sign.v +++ b/theories/Qquadratic_sign.v @@ -13,11 +13,9 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) - - -Require Import ZArithRing. -Require Import Qhomographic_sign. -Require Import Zaux. +From Coq Require Import ZArithRing. +From QArithSternBrocot Require Import Qhomographic_sign. +From QArithSternBrocot Require Import Zaux. Definition outside_square (a b c d : Z) := (Z.sgn a + Z.sgn b + Z.sgn c + Z.sgn d)%Z. diff --git a/theories/Qquadratic_sign_properties.v b/theories/Qquadratic_sign_properties.v index a33f1da..f993172 100644 --- a/theories/Qquadratic_sign_properties.v +++ b/theories/Qquadratic_sign_properties.v @@ -13,11 +13,10 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) - -Require Import ZArithRing. -Require Export Qhomographic_sign. -Require Export Qquadratic_sign. -Require Export Qhomographic_sign_properties. +From Coq Require Import ZArithRing. +From QArithSternBrocot Require Export Qhomographic_sign. +From QArithSternBrocot Require Export Qquadratic_sign. +From QArithSternBrocot Require Export Qhomographic_sign_properties. Definition same_ratio (a b c d e f g h : Z) := (a * f)%Z = (b * e)%Z /\ diff --git a/theories/Qsyntax.v b/theories/Qsyntax.v index 2d5b408..bf1a0ae 100644 --- a/theories/Qsyntax.v +++ b/theories/Qsyntax.v @@ -13,8 +13,7 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) - -Require Export general_Q. +From QArithSternBrocot Require Export general_Q. Infix "/" := make_Q : Q_scope. diff --git a/theories/R_addenda.v b/theories/R_addenda.v index 337444f..ad3bea7 100644 --- a/theories/R_addenda.v +++ b/theories/R_addenda.v @@ -8,11 +8,11 @@ (* This file contains various properties of R that are not in the standard library. *) -Require Import Reals. -Require Import Lra. -Require Import Fourier. -Require Import Euclid. -Require Import Lia. +From Coq Require Import Reals. +From Coq Require Import Lra. +From Coq Require Import Fourier. +From Coq Require Import Euclid. +From Coq Require Import Lia. Open Scope R_scope. diff --git a/theories/Zaux.v b/theories/Zaux.v index faf6d9b..834a7ea 100644 --- a/theories/Zaux.v +++ b/theories/Zaux.v @@ -18,9 +18,9 @@ development but are rather useful. *) -Require Export ZArith. -Require Export ZArithRing. -Require Import Lia. +From Coq Require Export ZArith. +From Coq Require Export ZArithRing. +From Coq Require Import Lia. Tactic Notation "ElimCompare" constr(c) constr(d) := elim_compare c d. @@ -2983,8 +2983,7 @@ Proof. intros. apply Zplus_minus_eq. rewrite Zplus_comm. - apply Z_div_mod_eq. - Flip. + apply Z_div_mod_eq_full. Qed. Lemma Z_div_le : @@ -3006,7 +3005,7 @@ Qed. Lemma Z_div_neg : forall a b : Z, (0 < b)%Z -> (a < 0)%Z -> (a / b < 0)%Z. Proof. intros. - rewrite (Z_div_mod_eq a b) in H0. + rewrite (Z_div_mod_eq_full a b) in H0. elim (Z_mod_lt a b). intros H1 _. apply Znot_ge_lt. @@ -3018,7 +3017,6 @@ Proof. Flip. assumption. Flip. - Flip. Qed. #[export] Hint Resolve Z_div_mod_eq_2 Z_div_le Z_div_nonneg Z_div_neg: zarith. diff --git a/theories/general_Q.v b/theories/general_Q.v index bd5f215..936c6aa 100644 --- a/theories/general_Q.v +++ b/theories/general_Q.v @@ -15,12 +15,12 @@ (** General Facts About Q and Qpositive, the functions Qpositive_c and Qpositive_i and the operations Qmult, Qpositive, Qlt *) -Require Import FunInd. -Require Export Qpositive. -Require Export Q_field. -Require Export Q_order. -Require Import Field_Theory_Q. -Require Export Zaux. +From Coq Require Import FunInd. +From QArithSternBrocot Require Export Qpositive. +From QArithSternBrocot Require Export Q_field. +From QArithSternBrocot Require Export Q_order. +From QArithSternBrocot Require Import Field_Theory_Q. +From QArithSternBrocot Require Export Zaux. (* An auxiliary lemma about [Z] *) diff --git a/theories/homographicAcc_Qhomographic_sign.v b/theories/homographicAcc_Qhomographic_sign.v index 82adfa9..0b4c671 100644 --- a/theories/homographicAcc_Qhomographic_sign.v +++ b/theories/homographicAcc_Qhomographic_sign.v @@ -13,11 +13,9 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) - - -Require Export Qhomographic_sign. -Require Export Qhomographic_Qpositive_to_Qpositive. -Require Export Qhomographic_sign_properties. +From QArithSternBrocot Require Export Qhomographic_sign. +From QArithSternBrocot Require Export Qhomographic_Qpositive_to_Qpositive. +From QArithSternBrocot Require Export Qhomographic_sign_properties. Definition new_a (a b c d : Z) (p : Qpositive) (H_Qhomographic_sg_denom_nonzero : Qhomographic_sg_denom_nonzero c d p) := diff --git a/theories/homographic_correctness.v b/theories/homographic_correctness.v index fda442f..ef99dbf 100644 --- a/theories/homographic_correctness.v +++ b/theories/homographic_correctness.v @@ -13,9 +13,9 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) -Require Import FunInd. -Require Import Field_Theory_Q. -Require Export Qhomographic_Qpositive_to_Q_properties. +From Coq Require Import FunInd. +From QArithSternBrocot Require Import Field_Theory_Q. +From QArithSternBrocot Require Export Qhomographic_Qpositive_to_Q_properties. Definition spec_fraction_encoding (a b : Z) : Q := Qmult a (Qinv b). diff --git a/theories/positive_fraction_encoding.v b/theories/positive_fraction_encoding.v index 29c9418..a00e87b 100644 --- a/theories/positive_fraction_encoding.v +++ b/theories/positive_fraction_encoding.v @@ -13,12 +13,11 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) - -Require Export Zaux. -Require Import ZArithRing. -Require Export Qpositive. -Require Export Q_field. -Require Import FunInd. +From QArithSternBrocot Require Export Zaux. +From Coq Require Import ZArithRing. +From QArithSternBrocot Require Export Qpositive. +From QArithSternBrocot Require Export Q_field. +From Coq Require Import FunInd. Inductive fractionalAcc : Z -> Z -> Prop := | fractionalacc0 : forall m n : Z, m = n -> fractionalAcc m n diff --git a/theories/quadraticAcc_Qquadratic_sign.v b/theories/quadraticAcc_Qquadratic_sign.v index e6a341e..26a8c6c 100644 --- a/theories/quadraticAcc_Qquadratic_sign.v +++ b/theories/quadraticAcc_Qquadratic_sign.v @@ -13,9 +13,9 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) -Require Export Qquadratic_sign_properties. -Require Export Qquadratic_Qpositive_to_Qpositive. -Require Export homographicAcc_Qhomographic_sign. +From QArithSternBrocot Require Export Qquadratic_sign_properties. +From QArithSternBrocot Require Export Qquadratic_Qpositive_to_Qpositive. +From QArithSternBrocot Require Export homographicAcc_Qhomographic_sign. Definition qnew_a (a b c d e f g h : Z) (p1 p2 : Qpositive) (H_Qquadratic_sg_denom_nonzero : Qquadratic_sg_denom_nonzero e f g h p1 p2) := diff --git a/theories/quadratic_correctness.v b/theories/quadratic_correctness.v index 7123a45..be7838d 100644 --- a/theories/quadratic_correctness.v +++ b/theories/quadratic_correctness.v @@ -13,15 +13,15 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) -Require Import FunInd. -Require Export homographic_correctness. -Require Import Field_Theory_Q. -Require Export Qquadratic_sign. -Require Export Qquadratic_Qpositive_to_Qpositive. -Require Export Qquadratic_sign_properties. -Require Export Qquadratic. -Require Export quadraticAcc_Qquadratic_sign. -Require Export Qquadratic_Qpositive_to_Q_properties. +From Coq Require Import FunInd. +From QArithSternBrocot Require Export homographic_correctness. +From QArithSternBrocot Require Import Field_Theory_Q. +From QArithSternBrocot Require Export Qquadratic_sign. +From QArithSternBrocot Require Export Qquadratic_Qpositive_to_Qpositive. +From QArithSternBrocot Require Export Qquadratic_sign_properties. +From QArithSternBrocot Require Export Qquadratic. +From QArithSternBrocot Require Export quadraticAcc_Qquadratic_sign. +From QArithSternBrocot Require Export Qquadratic_Qpositive_to_Q_properties. Definition spec_q (a b c d e f g h : Z) (q1 q2 : Q) : Q := Qmult diff --git a/theories/second_Field_Theory_Q.v b/theories/second_Field_Theory_Q.v index 05c519d..4385fa3 100644 --- a/theories/second_Field_Theory_Q.v +++ b/theories/second_Field_Theory_Q.v @@ -14,8 +14,8 @@ (* 02110-1301 USA *) -Require Export quadratic_correctness. -Require Import Eqdep_dec. +From QArithSternBrocot Require Export quadratic_correctness. +From Coq Require Import Eqdep_dec. Import Field_Theory_Q. diff --git a/theories/sqrt2.v b/theories/sqrt2.v index adf955c..85a2bb9 100644 --- a/theories/sqrt2.v +++ b/theories/sqrt2.v @@ -13,11 +13,11 @@ (* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *) (* 02110-1301 USA *) -Require Import ArithRing. -Require Import Compare_dec. -Require Import Wf_nat. -Require Import Arith. -Require Import Lia. +From Coq Require Import ArithRing. +From Coq Require Import Compare_dec. +From Coq Require Import Wf_nat. +From Coq Require Import Arith. +From Coq Require Import Lia. Theorem minus_minus : forall a b c : nat, a - b - c = a - (b + c). intros a; elim a; auto.