Merge pull request #23 from coq-community/archimedean

.github/workflows/docker-action.yml

@@ -17,9 +17,6 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.0.0-coq-8.16'
-          - 'mathcomp/mathcomp:2.0.0-coq-8.17'
-          - 'mathcomp/mathcomp:2.0.0-coq-8.18'
           - 'mathcomp/mathcomp:2.1.0-coq-8.16'
           - 'mathcomp/mathcomp:2.1.0-coq-8.17'
           - 'mathcomp/mathcomp:2.1.0-coq-8.18'
@@ -28,7 +25,6 @@ jobs:
           - 'mathcomp/mathcomp:2.2.0-coq-8.18'
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
           - 'mathcomp/mathcomp:2.2.0-coq-dev'
-          - 'mathcomp/mathcomp-dev:coq-8.17'
           - 'mathcomp/mathcomp-dev:coq-8.18'
           - 'mathcomp/mathcomp-dev:coq-8.19'
           - 'mathcomp/mathcomp-dev:coq-dev'

README.md

@@ -43,14 +43,14 @@ remains the sole trusted code base.
 - License: [CeCILL-C](LICENSE)
 - Compatible Coq versions: 8.16 or later
 - Additional dependencies:
-  - [MathComp ssreflect 2.0 or later](https://math-comp.github.io)
+  - [MathComp ssreflect 2.1 or later](https://math-comp.github.io)
   - [MathComp algebra](https://math-comp.github.io)
   - [MathComp field](https://math-comp.github.io)
   - [CoqEAL 2.0.0 or later](https://github.com/coq-community/coqeal)
   - [MathComp real closed fields 2.0.0 or later](https://github.com/math-comp/real-closed)
   - [MathComp bigenough 1.0.1 or later](https://github.com/math-comp/bigenough)
   - [Mczify](https://github.com/math-comp/mczify) 1.5.0 or later
-  - [Algebra Tactics](https://github.com/math-comp/algebra-tactics) 1.2.0 or later
+  - [Algebra Tactics](https://github.com/math-comp/algebra-tactics) 1.2.2 or later
 - Coq namespace: `mathcomp.apery`
 - Related publication(s):
   - [A Formal Proof of the Irrationality of ζ(3)](https://arxiv.org/abs/1912.06611) 

coq-mathcomp-apery.opam

@@ -24,14 +24,14 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
   "coq" {(>= "8.16" & < "8.20~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "2.0" & < "2.3~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {(>= "2.1" & < "2.3~") | (= "dev")}
   "coq-mathcomp-algebra" 
   "coq-mathcomp-field" 
   "coq-coqeal" {>= "2.0.0"}
   "coq-mathcomp-real-closed" {>= "2.0.0"}
   "coq-mathcomp-bigenough" {>= "1.0.1"}
   "coq-mathcomp-zify" {>= "1.5.0"}
-  "coq-mathcomp-algebra-tactics" {>= "1.2.0"}
+  "coq-mathcomp-algebra-tactics" {>= "1.2.2"}
 ]
 
 tags: [

meta.yml

@@ -55,12 +55,6 @@ supported_coq_versions:
   opam: '{(>= "8.16" & < "8.20~") | (= "dev")}'
 
 tested_coq_opam_versions:
-- version: '2.0.0-coq-8.16'
-  repo: 'mathcomp/mathcomp'
-- version: '2.0.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
-- version: '2.0.0-coq-8.18'
-  repo: 'mathcomp/mathcomp'
 - version: '2.1.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
 - version: '2.1.0-coq-8.17'
@@ -77,8 +71,6 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-dev'
   repo: 'mathcomp/mathcomp'
-- version: 'coq-8.17'
-  repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.18'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-8.19'
@@ -89,9 +81,9 @@ tested_coq_opam_versions:
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "2.0" & < "2.3~") | (= "dev")}'
+    version: '{(>= "2.1" & < "2.3~") | (= "dev")}'
   description: |-
-    [MathComp ssreflect 2.0 or later](https://math-comp.github.io)
+    [MathComp ssreflect 2.1 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
   description: |-
@@ -122,9 +114,9 @@ dependencies:
     [Mczify](https://github.com/math-comp/mczify) 1.5.0 or later
 - opam:
     name: coq-mathcomp-algebra-tactics
-    version: '{>= "1.2.0"}'
+    version: '{>= "1.2.2"}'
   description: |-
-    [Algebra Tactics](https://github.com/math-comp/algebra-tactics) 1.2.0 or later
+    [Algebra Tactics](https://github.com/math-comp/algebra-tactics) 1.2.2 or later
 
 namespace: mathcomp.apery
 

theories/a_props.v

@@ -27,7 +27,7 @@ Local Open Scope ring_scope.
 
 (* Although the type of the values of a is the one of rationals, these *)
 (* values are all integer. *)
-Fact Qint_a (i : int)  : a i \is a Qint.
+Fact Qint_a (i : int)  : a i \is a Num.int.
 Proof. by apply: rpred_sum => ?; rewrite rpred_zify. Qed.
 
 (* The values of a are strictly positive at positive indexes. *)
@@ -305,18 +305,18 @@ suff im_hr j x : 0 <= j -> 0 < x -> x <= xp j -> hr j x <= xp (j + 1).
   move/(_ (eqxx _)): ihn => ler3x.
   have -> : n.+3 = Posz n.+2 + 1 :> int by rewrite -addn1 PoszD.
   have -> : QtoR (rho (Posz n.+2 + 1)) = hr n.+2 (QtoR (rho n.+2)).
-    rewrite rho_rec // h2hr // ; exact: lt_0_rho.
-  apply: le_trans (im_hr _ _ _ _ ler3x) _ => //.
-  rewrite RealAlg.ltr_to_alg; exact: lt_0_rho.
+    by rewrite rho_rec // h2hr; exact: lt_0_rho.
+  apply: le_trans (im_hr _ _ _ _ ler3x) _; first by [].
+    by rewrite RealAlg.ltr_to_alg lt_0_rho.
+  exact: le_refl. (* FIXME: done is too slow here *)
 move=> le0j lt0x /(hr_incr j _ _ le0j lt0x) {i le2i}.
 have -> : hr j (xp j) = xp j.
   apply/eqP; rewrite -subr_eq0 hr_p; last exact/lt0r_neq0/lt_0_xp.
   suff -> : p j (xp j) = 0 by rewrite mul0r.
   by rewrite fac_p // subrr mul0r oppr0.
 move=> h; apply: le_trans h _.
 suff xp_incr : xp j <= xp (j + 1) by [].
-rewrite /xp ler_pM2r; last first.
-  by rewrite invr_gt0 RealAlg.ltr_to_alg.
+rewrite /xp ler_pM2r; last by rewrite invr_gt0 RealAlg.ltr_to_alg.
 apply: lerD.
   by rewrite RealAlg.ler_to_alg rmorphD /=; apply: alpha_incr; rewrite ler0z.
 rewrite ler_sqrt; last by try apply/ltW; apply/deltap_pos/addr_ge0.

theories/b_props.v

@@ -51,17 +51,17 @@ Qed.
 (* This lemma is not in arithmetics.v becuse it uses type rat. *)
 
 Lemma iter_lcmn_mul_rat (r : rat) (n : nat) : `|denq r| <= n ->
-  (iter_lcmn n)%:Q * r \is a Qint.
+  (iter_lcmn n)%:Q * r \is a Num.int.
 Proof.
 move=> ledn; rewrite -[r]divq_num_den mulrA -rmorphM.
 by apply/Qint_dvdz/dvdz_mulr/iter_lcmn_div; rewrite // absz_gt0 denq_neq0.
 Qed.
 
 
 (* FIXME : still too much nat/int conversions, not so easy to do better *)
-Lemma Qint_l3b (n : nat) : 2%:Q * (l n)%:Q ^ 3 * b (Posz n) \is a Qint.
+Lemma Qint_l3b (n : nat) : 2%:Q * (l n)%:Q ^ 3 * b (Posz n) \is a Num.int.
 Proof.
-set goal_term := (X in X \is a Qint).
+set goal_term := (X in X \is a Num.int).
 have {goal_term} -> : goal_term =
   2%:Q * (l n)%:Q ^ 3 * ghn3 n * a n +
   2%:Q * (l n)%:Q ^ 3 * (\sum_(0 <= k < Posz n + 1 :> int) c n k * s n k).
@@ -76,7 +76,7 @@ move=> k /andP [/andP [le0k lekn] _]; rewrite mulrA mulr_sumr big_int_cond /=.
 apply/rpred_sum => m /andP [/andP [le1m lemk] _]; rewrite -mulrA cdM //.
 pose hardest_term := (l n)%:Q ^ 3 / (m%:Q ^ 3 * (binomialz k m)%:Q ^ 2).
 set other_term := (X in _ * _ * _ * X).
-set goal_term := (X in X \is a Qint).
+set goal_term := (X in X \is a Num.int).
 have {goal_term} -> : goal_term = (-1) ^ (m + 1) * other_term * hardest_term.
   rewrite /goal_term /hardest_term; field.
   rewrite !intr_eq0 lt0r_neq0 ?binz_gt0; lia.

theories/binomialz.v

@@ -214,10 +214,10 @@ Qed.
 
 (* Below, older results, possibly needing revision. *)
 Lemma binz_Znat_gt0 (n k : int) :
-  n \is a Znat -> k \is a Znat -> k <= n -> 0 < binomialz n k.
+  n \is a Num.nat -> k \is a Num.nat -> k <= n -> 0 < binomialz n k.
 Proof. by move=> /ZnatP[{}n ->] /ZnatP[{}k ->] le_kn; rewrite binz_gt0. Qed.
 
-Lemma binznSn (n : int) : n \is a Znat -> binomialz n (n + 1) = 0.
+Lemma binznSn (n : int) : n \is a Num.nat -> binomialz n (n + 1) = 0.
 Proof. by case/ZnatP => ? ->; rewrite -PoszD binz_nat_nat bin_small ?addn1. Qed.
 
 

theories/z3irrational.v

@@ -1,4 +1,4 @@
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect all_algebra archimedean.
 From mathcomp Require Import bigenough cauchyreals.
 Require Import extra_mathcomp extra_cauchyreals.
 Require Import tactics shift bigopz arithmetics seq_defs.
@@ -303,7 +303,7 @@ pose_big_enough n.
   have h_lt1 : sigma_Q n < 1 / 2%:Q.
     apply/lt_creal_cst; rewrite sigma_QP; apply: MP; raise_big_enough.
   suff : 1 <= sigma_Q n by apply/negP; rewrite -ltNge; apply: lt_trans h_lt1 _.
-  suff /QintP [z zP] : sigma_Q n \is a Qint.
+  suff /intrP [z zP] : sigma_Q n \is a Num.int.
     by move: h_pos; rewrite zP ler1z -gtz0_ge1 ltr0z; apply.
   rewrite /sigma_Q mulrDr mulrN; apply/rpredB/Qint_l3b.
   rewrite -mulrA; apply: rpredM (rpred_int _ _) _.