From c2d3cbd83ffa13e7b3d7de4a5c490b503b8688e9 Mon Sep 17 00:00:00 2001 From: thery Date: Wed, 18 Dec 2024 11:37:00 +0100 Subject: [PATCH] mathcomp 2.3.0 --- .github/workflows/docker-action.yml | 4 ++-- README.md | 12 ++++++------ coq-hanoi.opam | 8 ++++---- extra.v | 14 +++++++------- meta.yml | 18 +++++++++--------- phi.v | 6 +++--- rhanoi4.v | 4 ++-- triangular.v | 4 ++-- 8 files changed, 35 insertions(+), 35 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index b546932..49e4abb 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -17,10 +17,10 @@ jobs: strategy: matrix: image: - - 'mathcomp/mathcomp:2.1.0-coq-8.18' + - 'mathcomp/mathcomp:2.3.0-coq-8.19' fail-fast: false steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - uses: coq-community/docker-coq-action@v1 with: opam_file: 'coq-hanoi.opam' diff --git a/README.md b/README.md index 7824b34..83c8e7d 100644 --- a/README.md +++ b/README.md @@ -6,8 +6,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener [![Docker CI][docker-action-shield]][docker-action-link] -[docker-action-shield]: https://github.com/thery/hanoi/workflows/Docker%20CI/badge.svg?branch=master -[docker-action-link]: https://github.com/thery/hanoi/actions?query=workflow:"Docker%20CI" +[docker-action-shield]: https://github.com/thery/hanoi/actions/workflows/docker-action.yml/badge.svg?branch=master +[docker-action-link]: https://github.com/thery/hanoi/actions/workflows/docker-action.yml @@ -43,11 +43,11 @@ An interactive version of the library is available - Author(s): - Laurent Théry - License: [MIT License](LICENSE) -- Compatible Coq versions: 8.18 or later +- Compatible Coq versions: 8.19 or later - Additional dependencies: - - [MathComp ssreflect 2.1 or later](https://math-comp.github.io) - - [MathComp algebra 2.1 or later](https://math-comp.github.io) - - [MathComp finmap 2.0 or later](https://github.com/math-comp/finmap) + - [MathComp ssreflect 2.3 or later](https://math-comp.github.io) + - [MathComp algebra 2.3 or later](https://math-comp.github.io) + - [MathComp finmap 2.1 or later](https://github.com/math-comp/finmap) - [MathComp bigenough 1.0.1 or later](https://github.com/math-comp/finmap) - Coq namespace: `hanoi` - Related publication(s): none diff --git a/coq-hanoi.opam b/coq-hanoi.opam index 297cbdc..0bf8b0a 100644 --- a/coq-hanoi.opam +++ b/coq-hanoi.opam @@ -41,10 +41,10 @@ An interactive version of the library is available build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "coq" {(>= "8.18")} - "coq-mathcomp-ssreflect" {(>= "2.1.0")} - "coq-mathcomp-algebra" {(>= "2.1.0")} - "coq-mathcomp-finmap" {(>= "2.0.0")} + "coq" {(>= "8.19")} + "coq-mathcomp-ssreflect" {(>= "2.3.0")} + "coq-mathcomp-algebra" {(>= "2.3.0")} + "coq-mathcomp-finmap" {(>= "2.1.0")} "coq-mathcomp-bigenough" {(>= "1.0.1")} ] diff --git a/extra.v b/extra.v index 4a23001..5a945d4 100644 --- a/extra.v +++ b/extra.v @@ -1,14 +1,15 @@ -From mathcomp Require Import all_ssreflect finmap. - -Set Implicit Arguments. -Unset Strict Implicit. - (******************************************************************************) (* *) (* Extra theorems and definitions *) (* *) (******************************************************************************) +From mathcomp Require Import all_ssreflect finmap. + +Set Implicit Arguments. +Unset Strict Implicit. + + (******************************************************************************) (* *) (* Extra theorems about lists *) @@ -250,10 +251,9 @@ Lemma s2f_setT n : s2f (setT : {set 'I_n}) = sint 0 n. Proof. apply/fsetP => i; rewrite mem_sint /=. apply/imfsetP/idP => /= [[j _ -> //]| iLn]. -by exists (Ordinal iLn). +by exists (Ordinal iLn); rewrite //= inE. Qed. - Lemma s2fD n (s1 s2 : {set 'I_n}) : s2f (s1 :\: s2) = s2f s1 `\` s2f s2. Proof. apply/fsetP => j; rewrite !inE. diff --git a/meta.yml b/meta.yml index ede3564..7c72939 100644 --- a/meta.yml +++ b/meta.yml @@ -50,25 +50,25 @@ license: identifier: MIT supported_coq_versions: - text: '8.18 or later' - opam: '{(>= "8.18")}' + text: '8.19 or later' + opam: '{(>= "8.19")}' dependencies: - opam: name: coq-mathcomp-ssreflect - version: '{(>= "2.1.0")}' + version: '{(>= "2.3.0")}' description: |- - [MathComp ssreflect 2.1 or later](https://math-comp.github.io) + [MathComp ssreflect 2.3 or later](https://math-comp.github.io) - opam: name: coq-mathcomp-algebra - version: '{(>= "2.1.0")}' + version: '{(>= "2.3.0")}' description: |- - [MathComp algebra 2.1 or later](https://math-comp.github.io) + [MathComp algebra 2.3 or later](https://math-comp.github.io) - opam: name: coq-mathcomp-finmap - version: '{(>= "2.0.0")}' + version: '{(>= "2.1.0")}' description: |- - [MathComp finmap 2.0 or later](https://github.com/math-comp/finmap) + [MathComp finmap 2.1 or later](https://github.com/math-comp/finmap) - opam: name: coq-mathcomp-bigenough version: '{(>= "1.0.1")}' @@ -77,7 +77,7 @@ dependencies: tested_coq_opam_versions: -- version: '2.1.0-coq-8.18' +- version: '2.3.0-coq-8.19' repo: 'mathcomp/mathcomp' namespace: hanoi diff --git a/phi.v b/phi.v index af75f5f..cbb90f2 100644 --- a/phi.v +++ b/phi.v @@ -116,7 +116,7 @@ Lemma gminE n : n = gmin n + troot n. Proof. case: n => //= n. rewrite {1}[n.+1]tmodE /gmin. -case: troot (troot_gt0 (isT : 0 < n.+1)) => //= t _. +case: troot (troot_gt0 (isT : 0 < n.+1)) => // t _. by rewrite deltaS addnAC. Qed. @@ -139,7 +139,7 @@ have mLt : tmod n < troot n by rewrite ltn_neqAle mDt tmod_le. rewrite subn1. apply/eqP; rewrite /gmin trootE. case: n {mDt}mLt => // [] [|] // n mLt. -case: troot mLt => //= t mLt. +case: troot mLt => // t mLt. by rewrite leq_addr deltaS ltn_add2l. Qed. @@ -224,7 +224,7 @@ rewrite (leq_trans (_ : _ <= gmin n.+1 + troot m)) //. rewrite -ltnS -addnS. rewrite /gmin {3}[n.+1]tmodE addnAC leq_add2r. have : 0 < troot n.+1 by apply troot_gt0. -case E : troot => [|t] _ //=. +case E : troot => [|t] _ //; rewrite [X in X <= _]/=. rewrite deltaS -E leq_add2l. by apply: gmin_root_lt. Qed. diff --git a/rhanoi4.v b/rhanoi4.v index 9bfb193..73796b5 100644 --- a/rhanoi4.v +++ b/rhanoi4.v @@ -984,10 +984,10 @@ have duz2_leq : psi (s2f E `&` `[T]) + psi (s2f A) + 2 ^ K.-1 < `d[u,z2]_rmove. rewrite -oprojE; case: (Hnz (z0 (oproj (enum_val i)))) => // /eqP. - rewrite -[_ == z0s N]negbK; case/negP. apply: (move_on_toplDr z0Mz0s) => //=. - by rewrite -{8}[n](subnK TLN) leq_add2r subnS ltnW. + by rewrite -[X in _ <= X](subnK TLN) leq_add2r subnS ltnW. - rewrite -[_ == p0]negbK; case/negP; rewrite -z0N0. apply: (move_on_toplDl z0Mz0s) => //=. - by rewrite -{8}[n](subnK TLN) ltn_add2r subnS. + by rewrite -[X in _ < X](subnK TLN) ltn_add2r subnS. rewrite -[_ == np3]negbK; case/negP. apply: memE''. have := mem_last u z0sb; rewrite -/z0 gE' !inE !mem_cat. diff --git a/triangular.v b/triangular.v index f9319c1..a50a39a 100644 --- a/triangular.v +++ b/triangular.v @@ -72,7 +72,7 @@ Proof. by case: n => // n _; rewrite deltaS addnS ltnS leq_addr. Qed. Lemma deltaE n : delta n = \sum_(i < n.+1) i. Proof. elim: n => [|n IH]; first by rewrite big_ord_recl big_ord0. -by rewrite big_ord_recr /= -IH deltaS. +by rewrite big_ord_recr -IH deltaS. Qed. Compute zip (iota 0 11) (map delta (iota 0 11)). @@ -303,7 +303,7 @@ case: p => a b. rewrite /tpair /pairt /= /tmod. have ->: ∇(Δ(a + b) + b) = a + b. apply/eqP. - rewrite trootE leq_addr /= deltaS. + rewrite trootE leq_addr deltaS. by rewrite addnS ltnS addnCA leq_addl. by rewrite [delta _ + _]addnC !addnK. Qed.