update boilerplate for 8.16

coq-community · Oct 29, 2022 · a36a015 · a36a015
1 parent 24c5670
commit a36a015
Show file tree

Hide file tree

Showing 39 changed files with 123 additions and 153 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -6,11 +6,9 @@
 (*                  <http://www.gnu.org/licenses/lgpl-2.1.html>         *)
 (************************************************************************)
 
-
-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
@@ -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
@@ -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
@@ -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
@@ -6,9 +6,8 @@
 (*                  <http://www.gnu.org/licenses/lgpl-2.1.html>         *)
 (************************************************************************)
 
-
-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
@@ -6,13 +6,12 @@
 (*                  <http://www.gnu.org/licenses/lgpl-2.1.html>         *)
 (************************************************************************)
 
-(* 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
@@ -6,10 +6,9 @@
 (*                  <http://www.gnu.org/licenses/lgpl-2.1.html>         *)
 (************************************************************************)
 
-
-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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -6,10 +6,9 @@
 (*                  <http://www.gnu.org/licenses/lgpl-2.1.html>         *)
 (************************************************************************)
 
-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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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 /\