Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adapt to math-comp/math-comp#1237 #23

Merged
merged 2 commits into from
Jul 8, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 0 additions & 4 deletions .github/workflows/docker-action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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'
Expand All @@ -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'
Expand Down
4 changes: 2 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
4 changes: 2 additions & 2 deletions coq-mathcomp-apery.opam
Original file line number Diff line number Diff line change
Expand Up @@ -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: [
Expand Down
16 changes: 4 additions & 12 deletions meta.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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'
Expand All @@ -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'
Expand All @@ -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: |-
Expand Down Expand Up @@ -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

Expand Down
12 changes: 6 additions & 6 deletions theories/a_props.v
Original file line number Diff line number Diff line change
Expand Up @@ -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. *)
Expand Down Expand Up @@ -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.
Expand Down
8 changes: 4 additions & 4 deletions theories/b_props.v
Original file line number Diff line number Diff line change
Expand Up @@ -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).
Expand All @@ -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.
Expand Down
4 changes: 2 additions & 2 deletions theories/binomialz.v
Original file line number Diff line number Diff line change
Expand Up @@ -214,10 +214,10 @@

(* 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.

Check warning on line 217 in theories/binomialz.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:coq-8.19)

Notation Num.nat is deprecated since mathcomp 2.1.0.

Check warning on line 217 in theories/binomialz.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.18)

Notation Num.nat is deprecated since mathcomp 2.1.0.

Check warning on line 217 in theories/binomialz.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.18)

Notation Num.nat is deprecated since mathcomp 2.1.0.

Check warning on line 217 in theories/binomialz.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:coq-dev)

Notation Num.nat is deprecated since mathcomp 2.1.0.

Check warning on line 217 in theories/binomialz.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:coq-8.18)

Notation Num.nat is deprecated since mathcomp 2.1.0.

Check warning on line 217 in theories/binomialz.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19)

Notation Num.nat is deprecated since mathcomp 2.1.0.

Check warning on line 217 in theories/binomialz.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19)

Notation Num.nat is deprecated since mathcomp 2.1.0.

Check warning on line 217 in theories/binomialz.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.17)

Notation Num.nat is deprecated since mathcomp 2.1.0.

Check warning on line 217 in theories/binomialz.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.17)

Notation Num.nat is deprecated since mathcomp 2.1.0.

Check warning on line 217 in theories/binomialz.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.16)

Notation Num.nat is deprecated since mathcomp 2.1.0.

Check warning on line 217 in theories/binomialz.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.16)

Notation Num.nat is deprecated since mathcomp 2.1.0.

Check warning on line 217 in theories/binomialz.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.17)

Notation Num.nat is deprecated since mathcomp 2.1.0.

Check warning on line 217 in theories/binomialz.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.17)

Notation Num.nat is deprecated since mathcomp 2.1.0.

Check warning on line 217 in theories/binomialz.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.16)

Notation Num.nat is deprecated since mathcomp 2.1.0.

Check warning on line 217 in theories/binomialz.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.16)

Notation Num.nat is deprecated since mathcomp 2.1.0.
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.


Expand Down
4 changes: 2 additions & 2 deletions theories/z3irrational.v
Original file line number Diff line number Diff line change
@@ -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.
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This change can be reverted when the support for MathComp 2.2 is dropped.

Require Import extra_mathcomp extra_cauchyreals.
Require Import tactics shift bigopz arithmetics seq_defs.
Expand Down Expand Up @@ -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 _ _) _.
Expand Down
Loading