port to Coq 8.18 and later

.github/workflows/docker-action.yml

@@ -18,17 +18,16 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:dev'
-          - 'coqorg/coq:8.16'
-          - 'coqorg/coq:8.15'
-          - 'coqorg/coq:8.14'
+          - 'coqorg/coq:8.18'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-qarith-stern-brocot.opam'
           custom_image: ${{ matrix.image }}
 
+
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme
 # https://github.com/erikmd/docker-coq-github-action-demo

README.md

@@ -5,7 +5,6 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 # Binary Rational Numbers
 
 [![Docker CI][docker-action-shield]][docker-action-link]
-[![Nix CI][nix-action-shield]][nix-action-link]
 [![Contributing][contributing-shield]][contributing-link]
 [![Code of Conduct][conduct-shield]][conduct-link]
 [![Zulip][zulip-shield]][zulip-link]
@@ -14,9 +13,6 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [docker-action-shield]: https://github.com/coq-community/qarith-stern-brocot/workflows/Docker%20CI/badge.svg?branch=master
 [docker-action-link]: https://github.com/coq-community/qarith-stern-brocot/actions?query=workflow:"Docker%20CI"
 
-[nix-action-shield]: https://github.com/coq-community/qarith-stern-brocot/workflows/Nix%20CI/badge.svg?branch=master
-[nix-action-link]: https://github.com/coq-community/qarith-stern-brocot/actions?query=workflow:"Nix%20CI"
-
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
 [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
 
@@ -42,7 +38,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.14 or later
+- Compatible Coq versions: 8.18 or later
 - Additional dependencies: none
 - Coq namespace: `QArithSternBrocot`
 - Related publication(s):

coq-qarith-stern-brocot.opam

@@ -15,8 +15,8 @@ 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.17~") | (= "dev")}
+  "dune" {>= "3.5"}
+  "coq" {>= "8.18"}
 ]
 
 tags: [

dune-project

@@ -1,3 +1,3 @@
-(lang dune 2.5)
-(using coq 0.2)
+(lang dune 3.5)
+(using coq 0.6)
 (name qarith-stern-brocot)

meta.yml

@@ -4,7 +4,7 @@ shortname: qarith-stern-brocot
 organization: coq-community
 community: true
 action: true
-nix: true
+nix: false
 
 synopsis: Binary rational numbers in Coq
 
@@ -34,14 +34,12 @@ license:
   identifier: LGPL-2.1-or-later
 
 supported_coq_versions:
-  text: 8.14 or later
-  opam: '{(>= "8.14" & < "8.17~") | (= "dev")}'
+  text: 8.18 or later
+  opam: '{>= "8.18"}'
 
 tested_coq_opam_versions:
 - version: dev
-- version: '8.16'
-- version: '8.15'
-- version: '8.14'
+- version: '8.18'
 
 tested_coq_nix_versions:
 - coq_version: 'master'

theories/Q_to_R.v

@@ -436,16 +436,16 @@ Proof.
   destruct (interp_non_zero p) as [p0 [q0 H]].
   rewrite (inv_correct p _ _ H); rewrite H.
   repeat rewrite <- INR_IZR_INZ.
-  rewrite Rpower.Rinv_Rdiv; auto.
+  rewrite Rinv_div; auto.
   (* Qneg *)
   unfold Q_to_R, numerator, denominator, decode_Q, Qinv, fst, snd.
   destruct (interp_non_zero p) as [p0 [q0 H]].
   rewrite (inv_correct p _ _ H); rewrite H.
   repeat rewrite Ropp_Ropp_IZR; repeat rewrite <- INR_IZR_INZ.
-  rewrite Rpower.Rinv_Rdiv; auto.
+  rewrite Rinv_div; auto.
   unfold Rdiv; rewrite <- Rmult_opp_opp;
   rewrite Ropp_involutive;
-  rewrite Ropp_inv_permute; auto.
+  rewrite Rinv_opp; auto.
 Qed.
 
 Lemma Q_to_Rminus: forall x y, Q_to_R (Qminus x y) = (Rminus (Q_to_R x) (Q_to_R y)).

theories/Qhomographic_Qpositive_to_Q_properties.v

@@ -25,12 +25,11 @@ Lemma fraction_encoding_equal :
 Proof.
  intros m n Hn1.
  unfold fraction_encoding at 2; fold fraction_encoding. 
- functional induction (fraction_encoding m n Hn1); intros Hn2;
- rewrite e;
-   trivial || (
- f_equal;
- apply positive_fraction_encoding_equal).
-Defined. 
+ functional induction (fraction_encoding m n Hn1); intros Hn2.
+ - rewrite e; f_equal; apply positive_fraction_encoding_equal.
+ - rewrite e; f_equal; apply positive_fraction_encoding_equal.
+ - rewrite e0; trivial.
+Defined.
 
 
 Ltac Rewrite_eq_ :=
@@ -399,7 +398,7 @@ generalize
 
  rewrite
   (Qhomographic_Qpositive_to_Q_0 a b c 0 p H_Qhomographic_sg_denom_nonzero2
-     Hc a0 (refl_equal 0%Z)).
+     Hc e (refl_equal 0%Z)).
  apply fraction_encoding_equal.
  Falsum.
 generalize
@@ -409,45 +408,45 @@ generalize
 
  rewrite
   (Qhomographic_Qpositive_to_Q_0 a b c 0 p H_Qhomographic_sg_denom_nonzero2
-     Hc a0 (refl_equal 0%Z)).
+     Hc e (refl_equal 0%Z)).
  apply fraction_encoding_equal.
  Falsum.
 
  (* 2 *)
  rewrite
   (Qhomographic_Qpositive_to_Q_1 a b c d p H_Qhomographic_sg_denom_nonzero2
-     b0 a0).
+     n e).
  apply fraction_encoding_equal.
  (* 3 *)
  clear e0.
  rewrite
   (h_sign_equal a b c d p H_Qhomographic_sg_denom_nonzero1
-     H_Qhomographic_sg_denom_nonzero2) in a1.
+     H_Qhomographic_sg_denom_nonzero2) in e1.
  rewrite
   (Qhomographic_Qpositive_to_Q_2 a b c d p H_Qhomographic_sg_denom_nonzero2
-     b0 a1).
+     n e1).
  reflexivity.
  (* 4 *)
 
  Clear_eq_.
  generalize
   (Qhomographic_Qpositive_to_Q_homographicAcc_pos_1 a b c d p
-     H_Qhomographic_sg_denom_nonzero1 b0 b1 a1).
- assert (l1_eq_one0 := b1).
+     H_Qhomographic_sg_denom_nonzero1 n e1 l).
+ assert (l1_eq_one0 := e1).
  rewrite
   (h_sign_equal a b c d p H_Qhomographic_sg_denom_nonzero1
      H_Qhomographic_sg_denom_nonzero2) in l1_eq_one0.
- assert (z0 := a1).
+ assert (z0 := l).
  rewrite (new_a_equal a b c d p H_Qhomographic_sg_denom_nonzero1
      H_Qhomographic_sg_denom_nonzero2) in z0.
  rewrite
   (new_b_equal a b c d p H_Qhomographic_sg_denom_nonzero1
      H_Qhomographic_sg_denom_nonzero2) in z0.
  rewrite
   (Qhomographic_Qpositive_to_Q_3 a b c d p H_Qhomographic_sg_denom_nonzero2
-     b0 l1_eq_one0
+     n l1_eq_one0
      (Qhomographic_Qpositive_to_Q_homographicAcc_pos_1 a b c d p
-        H_Qhomographic_sg_denom_nonzero2 b0 l1_eq_one0 z0) z0)
+        H_Qhomographic_sg_denom_nonzero2 n l1_eq_one0 z0) z0)
   .
  intro H_any_homographicAcc.
  apply f_equal with Qpositive.
@@ -472,12 +471,12 @@ generalize
  Clear_eq_.
  generalize
   (Qhomographic_Qpositive_to_Q_homographicAcc_pos_2 a b c d p
-     H_Qhomographic_sg_denom_nonzero1 b0 b1 b2).
- assert (l1_eq_one0 := b1).
+     H_Qhomographic_sg_denom_nonzero1 n e1 l).
+ assert (l1_eq_one0 := e1).
  rewrite
   (h_sign_equal a b c d p H_Qhomographic_sg_denom_nonzero1
      H_Qhomographic_sg_denom_nonzero2) in l1_eq_one0.
- assert (z0 := b2).
+ assert (z0 := l).
  rewrite
   (new_a_equal a b c d p H_Qhomographic_sg_denom_nonzero1
      H_Qhomographic_sg_denom_nonzero2) in z0.
@@ -486,9 +485,9 @@ generalize
      H_Qhomographic_sg_denom_nonzero2) in z0.
  rewrite
   (Qhomographic_Qpositive_to_Q_4 a b c d p H_Qhomographic_sg_denom_nonzero2
-     b0 l1_eq_one0
+     n l1_eq_one0
      (Qhomographic_Qpositive_to_Q_homographicAcc_pos_2 a b c d p
-        H_Qhomographic_sg_denom_nonzero2 b0 l1_eq_one0 z0) z0)
+        H_Qhomographic_sg_denom_nonzero2 n l1_eq_one0 z0) z0)
   .
  intro H_any_homographicAcc.
  apply f_equal with Qpositive.
@@ -512,12 +511,12 @@ generalize
  Clear_eq_.
  generalize
   (Qhomographic_Qpositive_to_Q_homographicAcc_neg_1 a b c d p
-     H_Qhomographic_sg_denom_nonzero1 b0 b1 a0).
- assert (l1_eq__minus_one0 := b1).
+     H_Qhomographic_sg_denom_nonzero1 n e0 l).
+ assert (l1_eq__minus_one0 := e0).
  rewrite
   (h_sign_equal a b c d p H_Qhomographic_sg_denom_nonzero1
      H_Qhomographic_sg_denom_nonzero2) in l1_eq__minus_one0.
- assert (z0 := a0).
+ assert (z0 := l).
  rewrite
   (new_a_equal a b c d p H_Qhomographic_sg_denom_nonzero1
      H_Qhomographic_sg_denom_nonzero2) in z0.
@@ -526,9 +525,9 @@ generalize
      H_Qhomographic_sg_denom_nonzero2) in z0.
  rewrite
   (Qhomographic_Qpositive_to_Q_5 a b c d p H_Qhomographic_sg_denom_nonzero2
-     b0 l1_eq__minus_one0
+     n l1_eq__minus_one0
      (Qhomographic_Qpositive_to_Q_homographicAcc_neg_1 a b c d p
-        H_Qhomographic_sg_denom_nonzero2 b0 l1_eq__minus_one0 z0) z0)
+        H_Qhomographic_sg_denom_nonzero2 n l1_eq__minus_one0 z0) z0)
   .
  intro H_any_homographicAcc.
  apply f_equal with Qpositive.
@@ -552,12 +551,12 @@ generalize
  Clear_eq_.
  generalize
   (Qhomographic_Qpositive_to_Q_homographicAcc_neg_2 a b c d p
-     H_Qhomographic_sg_denom_nonzero1 b0 b1 b2).
- assert (l1_eq__minus_one0 := b1).
+     H_Qhomographic_sg_denom_nonzero1 n e0 l).
+ assert (l1_eq__minus_one0 := e0).
  rewrite
   (h_sign_equal a b c d p H_Qhomographic_sg_denom_nonzero1
      H_Qhomographic_sg_denom_nonzero2) in l1_eq__minus_one0.
- assert (z0:=b2).
+ assert (z0:=l).
  rewrite
   (new_a_equal a b c d p H_Qhomographic_sg_denom_nonzero1
      H_Qhomographic_sg_denom_nonzero2) in z0.
@@ -566,9 +565,9 @@ generalize
      H_Qhomographic_sg_denom_nonzero2) in z0.
  rewrite
   (Qhomographic_Qpositive_to_Q_6 a b c d p H_Qhomographic_sg_denom_nonzero2
-     b0 l1_eq__minus_one0
+     n l1_eq__minus_one0
      (Qhomographic_Qpositive_to_Q_homographicAcc_neg_2 a b c d p
-        H_Qhomographic_sg_denom_nonzero2 b0 l1_eq__minus_one0 z0) z0)
+        H_Qhomographic_sg_denom_nonzero2 n l1_eq__minus_one0 z0) z0)
   .
  intro H_any_homographicAcc.
  apply f_equal with Qpositive.