From bfbc3d8e76fc8ba22bfa0a4711228b93ee501635 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 1 Jan 2024 17:27:13 +0900 Subject: [PATCH] compat with mathcomp >= 1.16 --- .github/workflows/docker-action.yml | 18 ++++++++----- README.md | 2 +- coq-robot.opam | 14 +++++----- derive_matrix.v | 19 +++----------- differential_kinematics.v | 4 +-- euclidean.v | 8 +++--- meta.yml | 40 +++++++++++++++++++---------- skew.v | 2 +- 8 files changed, 56 insertions(+), 51 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index ce2f37d..14fb1c3 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -17,12 +17,18 @@ jobs: strategy: matrix: image: - - 'mathcomp/mathcomp:1.13.0-coq-8.14' - - 'mathcomp/mathcomp:1.13.0-coq-8.15' - - 'mathcomp/mathcomp:1.14.0-coq-8.14' - - 'mathcomp/mathcomp:1.14.0-coq-8.15' - - 'mathcomp/mathcomp:1.15.0-coq-8.14' - - 'mathcomp/mathcomp:1.15.0-coq-8.15' + - 'mathcomp/mathcomp:1.16.0-coq-8.14' + - 'mathcomp/mathcomp:1.16.0-coq-8.15' + - 'mathcomp/mathcomp:1.16.0-coq-8.16' + - 'mathcomp/mathcomp:1.16.0-coq-8.17' + - 'mathcomp/mathcomp:1.16.0-coq-8.18' + - 'mathcomp/mathcomp:1.17.0-coq-8.15' + - 'mathcomp/mathcomp:1.17.0-coq-8.16' + - 'mathcomp/mathcomp:1.17.0-coq-8.17' + - 'mathcomp/mathcomp:1.17.0-coq-8.18' + - 'mathcomp/mathcomp:1.18.0-coq-8.16' + - 'mathcomp/mathcomp:1.18.0-coq-8.17' + - 'mathcomp/mathcomp:1.18.0-coq-8.18' fail-fast: false steps: - uses: actions/checkout@v2 diff --git a/README.md b/README.md index 322d8bd..f38ba8f 100644 --- a/README.md +++ b/README.md @@ -23,7 +23,7 @@ Mathematical Components library. - Cyril Cohen, Inria (initial) - Laurent Théry, Inria - License: [LGPL-2.1-or-later](LICENSE) -- Compatible Coq versions: Coq 8.14 to Coq 8.15 +- Compatible Coq versions: Coq 8.14 to Coq 8.18 - Additional dependencies: - [MathComp ssreflect](https://math-comp.github.io) - [MathComp fingroup](https://math-comp.github.io) diff --git a/coq-robot.opam b/coq-robot.opam index caad4fe..760c09c 100644 --- a/coq-robot.opam +++ b/coq-robot.opam @@ -19,13 +19,13 @@ Mathematical Components library.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "coq" { (>= "8.14" & < "8.16~") | (= "dev") } - "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.16~") } - "coq-mathcomp-fingroup" { (>= "1.13.0" & < "1.16~") } - "coq-mathcomp-algebra" { (>= "1.13.0" & < "1.16~") } - "coq-mathcomp-solvable" { (>= "1.13.0" & < "1.16~") } - "coq-mathcomp-field" { (>= "1.13.0" & < "1.16~") } - "coq-mathcomp-analysis" { (>= "0.5.0" & < "0.6~") } + "coq" { (>= "8.14" & < "8.19~") | (= "dev") } + "coq-mathcomp-ssreflect" { (>= "1.14.0" & < "1.19~") } + "coq-mathcomp-fingroup" { (>= "1.14.0" & < "1.19~") } + "coq-mathcomp-algebra" { (>= "1.14.0" & < "1.19~") } + "coq-mathcomp-solvable" { (>= "1.14.0" & < "1.19~") } + "coq-mathcomp-field" { (>= "1.14.0" & < "1.19~") } + "coq-mathcomp-analysis" { (>= "0.6.0" & < "0.7~") } "coq-mathcomp-real-closed" { (>= "1.1.3") } ] diff --git a/derive_matrix.v b/derive_matrix.v index 2efe6f1..35ea089 100644 --- a/derive_matrix.v +++ b/derive_matrix.v @@ -2,9 +2,9 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum rat. From mathcomp Require Import closed_field polyrcf matrix mxalgebra mxpoly zmodp. From mathcomp Require Import realalg complex fingroup perm. -From mathcomp.analysis Require Import boolp reals Rstruct classical_sets signed. -From mathcomp.analysis Require Import topology normedtype landau forms derive. -From mathcomp.analysis Require Import functions. +From mathcomp Require Import boolp reals Rstruct classical_sets signed. +From mathcomp Require Import topology normedtype landau forms derive. +From mathcomp Require Import functions. Require Import ssr_ext euclidean rigid skew. (******************************************************************************) @@ -22,19 +22,6 @@ Import Order.TTheory GRing.Theory Num.Def Num.Theory. Local Open Scope ring_scope. -(* NB: PR to analysis in progress *) -Lemma derive1_cst (R : numFieldType) (V : normedModType R) (k : V) t : - (cst k)^`() t = 0. -Proof. by rewrite derive1E derive_val. Qed. - -(* TODO: see coord_continuous in normedtype.v *) -Lemma coord_continuous (R : numDomainType) (K : normedModType R) m n i j : - continuous (fun M : 'M[K]_(m, n) => M i j). -Proof. -move=> /= M s /= /nbhs_normP => -[e e0 es]. -by apply/nbhs_ballP; exists e => //= N MN; exact/es/MN. -Qed. - Lemma mx_lin1N (R : ringType) n (M : 'M[R]_n) : mx_lin1 (- M) = -1 \*: mx_lin1 M :> ( _ -> _). Proof. by rewrite funeqE => v /=; rewrite scaleN1r mulmxN. Qed. diff --git a/differential_kinematics.v b/differential_kinematics.v index 7831a5b..5c0328c 100644 --- a/differential_kinematics.v +++ b/differential_kinematics.v @@ -2,8 +2,8 @@ From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum rat. From mathcomp Require Import closed_field polyrcf matrix mxalgebra mxpoly zmodp. From mathcomp Require Import realalg complex fingroup perm. -From mathcomp.analysis Require Import boolp reals Rstruct classical_sets signed. -From mathcomp.analysis Require Import topology normedtype landau forms derive. +From mathcomp Require Import boolp reals Rstruct classical_sets signed. +From mathcomp Require Import topology normedtype landau forms derive. From mathcomp Require Import functions. Require Import ssr_ext derive_matrix euclidean frame rot skew rigid. diff --git a/euclidean.v b/euclidean.v index e81b93a..710b42d 100644 --- a/euclidean.v +++ b/euclidean.v @@ -1625,16 +1625,16 @@ rewrite !coefD. rewrite [X in X + _ + _](_ : _ = M 0 0 * (M 2%:R 2%:R + M 1 1) + (M 1 1 * M 2%:R 2%:R - M 2%:R 1 * M 1 2%:R)); last first. rewrite coefM sum2E coefD coefX add0r coefN coefC [- _]/=. - rewrite subn0 coefD. + rewrite subn0 coefD coefB. rewrite coefM sum2E subn0 coefD coefX add0r coefN (_ : _`_0 = M 1 1); last by rewrite coefC. rewrite coefD coefX coefN coefC subr0 mulr1. rewrite coefD coefN coefX coefN coefC subr0 mul1r. rewrite subnn coefD coefX add0r coefN coefC [in X in - M 1 1 - X]/=. rewrite coefM sum2E coefC coefC mulr0 add0r coefC mul0r subr0. - rewrite coefD coefX coefN coefC subr0 mul1r. - rewrite coefD coefM sum1E coefD coefX add0r coefN coefC [in X in - X * _`_ _]/=. + rewrite coefD coefN coefC subr0 mul1r. + rewrite coefM sum1E coefD coefX add0r coefN coefC [in X in - X * _`_ _]/=. rewrite coefD coefX add0r coefN coefC mulrN !mulNr opprK. - rewrite coefN coefM sum1E coefC coefC [in X in M 1 1 * _ - X]/=. + rewrite coefM sum1E coefC coefC [in X in M 1 1 * _ - X]/=. by rewrite -opprB mulrN 2!opprK. rewrite [X in _ + X + _](_ : _ = - M 0 1 * M 1 0); last first. rewrite coefN coefM sum2E coefC [in X in X * _]/= subnn. diff --git a/meta.yml b/meta.yml index 9b72129..952d69d 100644 --- a/meta.yml +++ b/meta.yml @@ -30,52 +30,64 @@ license: file: LICENSE supported_coq_versions: - text: Coq 8.14 to Coq 8.15 - opam: '{ (>= "8.14" & < "8.16~") | (= "dev") }' + text: Coq 8.14 to Coq 8.18 + opam: '{ (>= "8.14" & < "8.19~") | (= "dev") }' tested_coq_opam_versions: -- version: '1.13.0-coq-8.14' +- version: '1.16.0-coq-8.14' repo: 'mathcomp/mathcomp' -- version: '1.13.0-coq-8.15' +- version: '1.16.0-coq-8.15' repo: 'mathcomp/mathcomp' -- version: '1.14.0-coq-8.14' +- version: '1.16.0-coq-8.16' repo: 'mathcomp/mathcomp' -- version: '1.14.0-coq-8.15' +- version: '1.16.0-coq-8.17' repo: 'mathcomp/mathcomp' -- version: '1.15.0-coq-8.14' +- version: '1.16.0-coq-8.18' repo: 'mathcomp/mathcomp' -- version: '1.15.0-coq-8.15' +- version: '1.17.0-coq-8.15' + repo: 'mathcomp/mathcomp' +- version: '1.17.0-coq-8.16' + repo: 'mathcomp/mathcomp' +- version: '1.17.0-coq-8.17' + repo: 'mathcomp/mathcomp' +- version: '1.17.0-coq-8.18' + repo: 'mathcomp/mathcomp' +- version: '1.18.0-coq-8.16' + repo: 'mathcomp/mathcomp' +- version: '1.18.0-coq-8.17' + repo: 'mathcomp/mathcomp' +- version: '1.18.0-coq-8.18' repo: 'mathcomp/mathcomp' dependencies: - opam: name: coq-mathcomp-ssreflect - version: '{ (>= "1.13.0" & < "1.16~") }' + version: '{ (>= "1.14.0" & < "1.19~") }' description: |- [MathComp ssreflect](https://math-comp.github.io) - opam: name: coq-mathcomp-fingroup - version: '{ (>= "1.13.0" & < "1.16~") }' + version: '{ (>= "1.14.0" & < "1.19~") }' description: |- [MathComp fingroup](https://math-comp.github.io) - opam: name: coq-mathcomp-algebra - version: '{ (>= "1.13.0" & < "1.16~") }' + version: '{ (>= "1.14.0" & < "1.19~") }' description: |- [MathComp algebra](https://math-comp.github.io) - opam: name: coq-mathcomp-solvable - version: '{ (>= "1.13.0" & < "1.16~") }' + version: '{ (>= "1.14.0" & < "1.19~") }' description: |- [MathComp solvable](https://math-comp.github.io) - opam: name: coq-mathcomp-field - version: '{ (>= "1.13.0" & < "1.16~") }' + version: '{ (>= "1.14.0" & < "1.19~") }' description: |- [MathComp field](https://math-comp.github.io) - opam: name: coq-mathcomp-analysis - version: '{ (>= "0.5.0" & < "0.6~") }' + version: '{ (>= "0.6.0" & < "0.7~") }' description: |- [MathComp analysis](https://github.com/math-comp/analysis) - opam: diff --git a/skew.v b/skew.v index 7334539..7701e07 100644 --- a/skew.v +++ b/skew.v @@ -607,7 +607,7 @@ move=> u0 /= k. rewrite inE eigenvalue_root_char -map_char_poly char_poly_spin. apply/rootP. case: ifPn => [|Hk]. -- rewrite inE => /orP [/eqP ->|]; first by rewrite /= horner_map !hornerE. +- rewrite inE => /orP [/eqP ->|]; first by rewrite /= horner_map/= !hornerE/= expr0n. rewrite inE => /orP [/eqP ->|]. eigenvalue_spin_eval_poly. simpc.