Merge pull request #11 from coq-community/fix-8.11

port to 8.11

.gitignore

@@ -3,6 +3,9 @@
 *.aux
 *.d
 *.vo
+*.vos
+*.vok
+_build
 Makefile.coq
 Makefile.coq.conf
 result

.travis.yml

@@ -46,6 +46,15 @@ jobs:
   include:
 
   # Test supported versions of Coq via Nix
+  - env:
+    - COQ=https://github.com/coq/coq-on-cachix/tarball/master
+    <<: *NIX
+  - env:
+    - COQ=8.12
+    <<: *NIX
+  - env:
+    - COQ=8.11
+    <<: *NIX
   - env:
     - COQ=8.10
     <<: *NIX
@@ -61,7 +70,7 @@ jobs:
 
   # Test supported versions of Coq via OPAM
   - env:
-    - COQ_IMAGE=coqorg/coq:8.10
+    - COQ_IMAGE=coqorg/coq:dev
     - PACKAGE=coq-qarith-stern-brocot.dev
     - NJOBS=2
     <<: *OPAM

Q_order.v

@@ -117,7 +117,7 @@ Inductive Qgt : Q -> Q -> Prop :=
   | Qgt_pos_zero : forall x' : Qpositive, Qgt (Qpos x') Zero
   | Qgt_pos_neg : forall x' y' : Qpositive, Qgt (Qpos x') (Qneg y')
   | Qgt_zero_neg : forall x' : Qpositive, Qgt Zero (Qneg x').
-Hint Resolve Qgt_pos_pos Qgt_neg_neg Qgt_pos_zero Qgt_pos_neg Qgt_zero_neg.
+Hint Resolve Qgt_pos_pos Qgt_neg_neg Qgt_pos_zero Qgt_pos_neg Qgt_zero_neg : core.
 
 Theorem Qgt_total : forall x y : Q, Qgt x y \/ x = y \/ Qgt y x.
 intros x y; case y; case x; auto.

Q_ordered_field_properties.v

@@ -338,7 +338,7 @@ Qed.
 
 Hint Resolve Qinv_pos Qinv_resp_nonzero Qminus_Qeq Qeq_Qminus
              Qlt_not_eq' Qinv_neg Qle_Qopp_pos Qlt_Qopp_pos 
-             Qlt_Qopp_neg Qopp_Qone_Qlt_Qone.
+             Qlt_Qopp_neg Qopp_Qone_Qlt_Qone : core.
 
 Lemma Qle_mult_nonneg_pos: forall x y : Q, Zero <= x -> Zero < y -> Zero <= x * y.
 Proof.

Qhomographic_sign_properties.v

@@ -1580,15 +1580,15 @@ Proof.
               end ].
    case (not_Zeq_inf (Z.sgn (a + b)) 0 Hab); intro Hab';
     [ right; split; [ apply Zsgn_11; assumption | apply Zsgn_12 ];
-       generalize (Zsgn_1 (c + d)); intros [[Hcd| Hcd]| Hcd];
+       generalize (Zsgn_1' (c + d)); intros [[Hcd| Hcd]| Hcd];
        [ apply False_ind;
           apply (Qhomographic_signok_1 c d H_Qhomographic_sg_denom_nonzero);
           apply Zsgn_2
        | rewrite Hcd; constructor
        | apply False_ind; apply Habcd; rewrite Hcd; apply Zsgn_8;
           apply Zsgn_11 ]; assumption
     | left; split; [ apply Zsgn_12; assumption | apply Zsgn_11 ];
-       generalize (Zsgn_1 (c + d)); intros [[Hcd| Hcd]| Hcd];
+       generalize (Zsgn_1' (c + d)); intros [[Hcd| Hcd]| Hcd];
        [ apply False_ind;
           apply (Qhomographic_signok_1 c d H_Qhomographic_sg_denom_nonzero);
           apply Zsgn_2

Qpositive.v

@@ -357,53 +357,57 @@ change
   (dL (Qpositive_c (S p) (S q2) (S n0)) =
    dL (Qpositive_c (S p'2) (S q'2) (S n''))) in |- *.
 apply f_equal with (f := dL).
-apply Hrec with d; auto with *.
-rewrite <- Heqp'2; assumption.
-rewrite <- Heq4; rewrite <- Heq2; rewrite (mult_comm (S d)).
-rewrite mult_minus_distr_r.
-repeat rewrite <- (mult_comm (S d)).
-rewrite <- Heqd2; rewrite <- Heqd1.
-simpl in |- *; auto.
-apply mult_S_le_reg_l with d.
-rewrite <- Heqd2; rewrite <- Heqd1.
-apply le_n_S.
-apply minus_O_le; assumption.
-intros p2 Heqp2.
-CaseEq (p' - q').
-intros Heqm'; cut (S p - S q = 0).
-simpl in |- *; rewrite Heqp2; intros Dummy; discriminate Dummy.
-rewrite Heqd2; rewrite Heqd1.
-repeat rewrite (mult_comm (S d)).
-rewrite <- mult_minus_distr_r.
-rewrite Heqm'; simpl in |- *; auto.
-intros p'2.
-generalize Hle2; case n'.
-generalize Heqd1 Heqd2; case p'; case q'.
-simpl in |- *; intros H'1 H'2 H'3 H'4; discriminate H'4.
-intros x; rewrite <- (mult_comm 0); simpl in |- *; intros Dummy;
- discriminate Dummy.
-intros x; rewrite <- (mult_comm 0); simpl in |- *; intros Dummy1 Dummy2;
- discriminate Dummy2.
-simpl in |- *; intros n n1 H'1 H'2; rewrite <- plus_n_Sm; intros H'3;
- inversion H'3.
-inversion H0.
-intros n''.
-intros Hle3 Heq4.
-CaseEq q'.
-intros Heq5; generalize Heqd2; rewrite Heq5; simpl in |- *.
-rewrite <- (mult_comm 0); simpl in |- *; intros Dummy; discriminate Dummy.
-intros q'2 Heqq'2.
-change
-  (nR (Qpositive_c (S p2) (S q) (S n0)) =
-   nR (Qpositive_c (S p'2) (S q'2) (S n''))) in |- *.
-apply f_equal with (f := nR).
-apply Hrec with d; auto with *.
-rewrite <- Heq4; rewrite <- Heqp2; rewrite (mult_comm (S d)).
-rewrite mult_minus_distr_r.
-repeat rewrite <- (mult_comm (S d)).
-rewrite <- Heqd2; rewrite <- Heqd1.
-simpl in |- *; auto.
-rewrite <- Heqq'2; assumption.
+apply Hrec with d.
+- rewrite <- Heqp'2; assumption.
+- rewrite <- Heq4; rewrite <- Heq2; rewrite (mult_comm (S d)).
+  rewrite mult_minus_distr_r.
+  repeat rewrite <- (mult_comm (S d)).
+  rewrite <- Heqd2; rewrite <- Heqd1.
+  simpl in |- *; auto.
+- auto with zarith.
+- auto with zarith.
+- apply mult_S_le_reg_l with d.
+  rewrite <- Heqd2; rewrite <- Heqd1.
+  apply le_n_S.
+  apply minus_O_le; assumption.
+- intros p2 Heqp2.
+  CaseEq (p' - q').
+  intros Heqm'; cut (S p - S q = 0).
+  simpl in |- *; rewrite Heqp2; intros Dummy; discriminate Dummy.
+  rewrite Heqd2; rewrite Heqd1.
+  repeat rewrite (mult_comm (S d)).
+  rewrite <- mult_minus_distr_r.
+  rewrite Heqm'; simpl in |- *; auto.
+  intros p'2.
+  generalize Hle2; case n'.
+  generalize Heqd1 Heqd2; case p'; case q'.
+  simpl in |- *; intros H'1 H'2 H'3 H'4; discriminate H'4.
+  intros x; rewrite <- (mult_comm 0); simpl in |- *; intros Dummy;
+   discriminate Dummy.
+  intros x; rewrite <- (mult_comm 0); simpl in |- *; intros Dummy1 Dummy2;
+   discriminate Dummy2.
+  simpl in |- *; intros n n1 H'1 H'2; rewrite <- plus_n_Sm; intros H'3;
+   inversion H'3.
+  inversion H0.
+  intros n''.
+  intros Hle3 Heq4.
+  CaseEq q'.
+  intros Heq5; generalize Heqd2; rewrite Heq5; simpl in |- *.
+  rewrite <- (mult_comm 0); simpl in |- *; intros Dummy; discriminate Dummy.
+  intros q'2 Heqq'2.
+  change
+    (nR (Qpositive_c (S p2) (S q) (S n0)) =
+     nR (Qpositive_c (S p'2) (S q'2) (S n''))) in |- *.
+  apply f_equal with (f := nR).
+  apply Hrec with d.
+  * rewrite <- Heq4; rewrite <- Heqp2; rewrite (mult_comm (S d)).
+    rewrite mult_minus_distr_r.
+    repeat rewrite <- (mult_comm (S d)).
+    rewrite <- Heqd2; rewrite <- Heqd1.
+    simpl in |- *; auto.
+  * rewrite <- Heqq'2; assumption.
+  * auto with zarith.
+  * auto with zarith.
 Qed.
 
 Theorem construct_correct4 :

Qquadratic.v

@@ -507,7 +507,7 @@ case (Qquadratic_sign_sign_dec a b c d e f g h p1 p2 H_qsign).
 
  (* still l1=1 -> Q *)
  case
-  (Zsgn_1
+  (Zsgn_1'
      (qnew_a a b c d e f g h p1 p2 H_qsign +
       qnew_b a b c d e f g h p1 p2 H_qsign +
       qnew_c a b c d e f g h p1 p2 H_qsign +
@@ -598,7 +598,7 @@ case (Qquadratic_sign_sign_dec a b c d e f g h p1 p2 H_qsign).
 
  (* still l1= -1 -> Q *)
  case
-  (Zsgn_1
+  (Zsgn_1'
      (qnew_a a b c d e f g h p1 p2 H_qsign +
       qnew_b a b c d e f g h p1 p2 H_qsign +
       qnew_c a b c d e f g h p1 p2 H_qsign +

Qquadratic_sign.v

@@ -1553,15 +1553,15 @@ Proof.
      case (three_integers_dec_inf f g h); intro Hfgh;
      [ rewrite Qquadratic_sign_nRdL_nRdL_1;
         try solve [ discriminate | assumption ]; rewrite <- Zsgn_15;
-        apply Zsgn_1
+        apply Zsgn_1'
      | case (Z_lt_dec 2 (outside_square e f g h)); intro Ho2;
         [ rewrite Qquadratic_sign_nRdL_nRdL_2;
            try solve [ discriminate | assumption ]; 
-           apply Zsgn_1
+           apply Zsgn_1'
         | case (Z_lt_dec (outside_square e f g h) (-2)); intro Ho2';
            [ rewrite Qquadratic_sign_nRdL_nRdL_3;
               try solve [ discriminate | assumption ]; 
-              rewrite <- Zsgn_25; apply Zsgn_1
+              rewrite <- Zsgn_25; apply Zsgn_1'
            | match goal with
              | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 =>
                  rewrite
@@ -1599,11 +1599,11 @@ Proof.
      | case (Z_lt_dec 2 (outside_square a b c d)); intro Ho1;
         [ rewrite Qquadratic_sign_nRdL_nRdL_5;
            try solve [ discriminate | assumption ]; 
-           apply Zsgn_1
+           apply Zsgn_1'
         | case (Z_lt_dec (outside_square a b c d) (-2)); intro Ho1';
            [ rewrite Qquadratic_sign_nRdL_nRdL_6;
               try solve [ discriminate | assumption ]; 
-              rewrite <- Zsgn_25; apply Zsgn_1
+              rewrite <- Zsgn_25; apply Zsgn_1'
            | match goal with
              | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 =>
                  rewrite
@@ -1690,15 +1690,15 @@ Proof.
      case (three_integers_dec_inf f g h); intro Hfgh;
      [ rewrite Qquadratic_sign_nRdL_nRdL_1;
         try solve [ discriminate | assumption ]; rewrite <- Zsgn_15;
-        apply Zsgn_1
+        apply Zsgn_1'
      | case (Z_lt_dec 2 (outside_square e f g h)); intro Ho2;
         [ rewrite Qquadratic_sign_nRdL_nRdL_2;
            try solve [ discriminate | assumption ]; 
-           apply Zsgn_1
+           apply Zsgn_1'
         | case (Z_lt_dec (outside_square e f g h) (-2)); intro Ho2';
            [ rewrite Qquadratic_sign_nRdL_nRdL_3;
               try solve [ discriminate | assumption ]; 
-              rewrite <- Zsgn_25; apply Zsgn_1
+              rewrite <- Zsgn_25; apply Zsgn_1'
            | match goal with
              | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 =>
                  rewrite
@@ -1736,11 +1736,11 @@ Proof.
      | case (Z_lt_dec 2 (outside_square a b c d)); intro Ho1;
         [ rewrite Qquadratic_sign_nRdL_nRdL_5;
            try solve [ discriminate | assumption ]; 
-           apply Zsgn_1
+           apply Zsgn_1'
         | case (Z_lt_dec (outside_square a b c d) (-2)); intro Ho1';
            [ rewrite Qquadratic_sign_nRdL_nRdL_6;
               try solve [ discriminate | assumption ]; 
-              rewrite <- Zsgn_25; apply Zsgn_1
+              rewrite <- Zsgn_25; apply Zsgn_1'
            | match goal with
              | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 =>
                  rewrite
@@ -1851,15 +1851,15 @@ Proof.
      case (three_integers_dec_inf f g h); intro Hfgh;
      [ rewrite Qquadratic_sign_nRdL_nRdL_1;
         try solve [ discriminate | assumption ]; rewrite <- Zsgn_15;
-        apply Zsgn_1
+        apply Zsgn_1'
      | case (Z_lt_dec 2 (outside_square e f g h)); intro Ho2;
         [ rewrite Qquadratic_sign_nRdL_nRdL_2;
            try solve [ discriminate | assumption ]; 
-           apply Zsgn_1
+           apply Zsgn_1'
         | case (Z_lt_dec (outside_square e f g h) (-2)); intro Ho2';
            [ rewrite Qquadratic_sign_nRdL_nRdL_3;
               try solve [ discriminate | assumption ]; 
-              rewrite <- Zsgn_25; apply Zsgn_1
+              rewrite <- Zsgn_25; apply Zsgn_1'
            | match goal with
              | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 =>
                  rewrite
@@ -1897,11 +1897,11 @@ Proof.
      | case (Z_lt_dec 2 (outside_square a b c d)); intro Ho1;
         [ rewrite Qquadratic_sign_nRdL_nRdL_5;
            try solve [ discriminate | assumption ]; 
-           apply Zsgn_1
+           apply Zsgn_1'
         | case (Z_lt_dec (outside_square a b c d) (-2)); intro Ho1';
            [ rewrite Qquadratic_sign_nRdL_nRdL_6;
               try solve [ discriminate | assumption ]; 
-              rewrite <- Zsgn_25; apply Zsgn_1
+              rewrite <- Zsgn_25; apply Zsgn_1'
            | match goal with
              | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 =>
                  rewrite
@@ -1988,15 +1988,15 @@ Proof.
      case (three_integers_dec_inf f g h); intro Hfgh;
      [ rewrite Qquadratic_sign_nRdL_nRdL_1;
         try solve [ discriminate | assumption ]; rewrite <- Zsgn_15;
-        apply Zsgn_1
+        apply Zsgn_1'
      | case (Z_lt_dec 2 (outside_square e f g h)); intro Ho2;
         [ rewrite Qquadratic_sign_nRdL_nRdL_2;
            try solve [ discriminate | assumption ]; 
-           apply Zsgn_1
+           apply Zsgn_1'
         | case (Z_lt_dec (outside_square e f g h) (-2)); intro Ho2';
            [ rewrite Qquadratic_sign_nRdL_nRdL_3;
               try solve [ discriminate | assumption ]; 
-              rewrite <- Zsgn_25; apply Zsgn_1
+              rewrite <- Zsgn_25; apply Zsgn_1'
            | match goal with
              | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 =>
                  rewrite
@@ -2034,11 +2034,11 @@ Proof.
      | case (Z_lt_dec 2 (outside_square a b c d)); intro Ho1;
         [ rewrite Qquadratic_sign_nRdL_nRdL_5;
            try solve [ discriminate | assumption ]; 
-           apply Zsgn_1
+           apply Zsgn_1'
         | case (Z_lt_dec (outside_square a b c d) (-2)); intro Ho1';
            [ rewrite Qquadratic_sign_nRdL_nRdL_6;
               try solve [ discriminate | assumption ]; 
-              rewrite <- Zsgn_25; apply Zsgn_1
+              rewrite <- Zsgn_25; apply Zsgn_1'
            | match goal with
              | id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 =>
                  rewrite

README.md

@@ -34,7 +34,7 @@ field operations on them in two different ways: strict and lazy.
 - Coq-community maintainer(s):
   - Hugo Herbelin ([**@herbelin**](https://github.com/herbelin))
 - License: [GNU Lesser General Public License v2.1 or later](LICENSE)
-- Compatible Coq versions: 8.7 to 8.10
+- Compatible Coq versions: 8.7 and later
 - Additional dependencies: none
 - Coq namespace: `QArithSternBrocot`
 - Related publication(s):

R_addenda.v

@@ -14,6 +14,8 @@ Require Import Fourier.
 Require Import Euclid. 
 Require Import Omega.
 
+Open Scope R_scope.
+
 Lemma Rlt_stepl:forall x y z, Rlt x y -> x=z -> Rlt z y.
 Proof.
  intros x y z H_lt H_eq; subst; assumption.
@@ -111,7 +113,7 @@ Definition Ropp_resp_nonzero:=RIneq.Ropp_neq_0_compat.
 
 Hint Resolve Rlt_Ropp_pos Rinv_pos R1_neq_R0 Rle_mult_nonneg_nonneg
              Rlt_mult_pos_pos Rlt_mult_neg_neg Rlt_not_eq' Rlt_not_eq
-             Rmult_resp_nonzero Rinv_resp_nonzero Ropp_resp_nonzero.
+             Rmult_resp_nonzero Rinv_resp_nonzero Ropp_resp_nonzero : core.
 
 Lemma Rmult_mult_nonneg: forall r, 0<=r*r.
 Proof.
@@ -386,7 +388,7 @@ Proof.
  intros n; apply lt_INR_0; auto with arith.  
 Qed.
 
-Hint Resolve not_O_S_INR pos_S_INR pos_INR.
+Hint Resolve not_O_S_INR pos_S_INR pos_INR : core.
 
 
 Lemma Req_Rdiv_Rone:forall x y, y<>0 -> x=y -> x/y =1.