From df9abf505fde57cb80d080a1182f63fec19e6f28 Mon Sep 17 00:00:00 2001 From: thery Date: Wed, 1 Jul 2026 15:21:50 +0200 Subject: [PATCH] update for 2.5 --- .github/workflows/docker-action.yml | 5 +-- .../section6.v | 4 +-- .../tutorial_Gonthier_LeRoux.v | 3 +- README.md | 29 +++------------ SummerSchoolSophia/lesson5.v | 9 ++++- SummerSchoolSophia/lesson7.v | 36 +++++++++---------- SummerSchoolSophia/lesson8.v | 18 +++++----- coq-tutorial_material.opam | 4 +-- meta.yml | 12 +++---- 9 files changed, 55 insertions(+), 65 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 5d6a370..c94185a 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -9,6 +9,7 @@ on: pull_request: branches: - '**' + workflow_dispatch: jobs: build: @@ -17,10 +18,10 @@ jobs: strategy: matrix: image: - - 'mathcomp/mathcomp:2.1.0-coq-8.18' + - 'mathcomp/mathcomp:2.5.0-rocq-prover-9.1' fail-fast: false steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - uses: coq-community/docker-coq-action@v1 with: opam_file: 'coq-tutorial_material.opam' diff --git a/AnIntroductionToSmallScaleReflectionInCoq/section6.v b/AnIntroductionToSmallScaleReflectionInCoq/section6.v index 234e5e3..afd8f74 100644 --- a/AnIntroductionToSmallScaleReflectionInCoq/section6.v +++ b/AnIntroductionToSmallScaleReflectionInCoq/section6.v @@ -21,7 +21,6 @@ Lemma tuto_unit_enumP : Finite.axiom [:: tt]. Proof. by case. Qed. #[verbose] HB.instance Definition _ := isFinite.Build unit1 tuto_unit_enumP. - (******************************************************************************) (* Exercise 6.1.2 *) (******************************************************************************) @@ -79,7 +78,8 @@ Qed. (* Exercise 6.1.4 *) (******************************************************************************) -Check UniqFinMixin. + +Check Finite.uniq_enumP. Definition tuto_prod_enum (T1 T2 : finType) : seq (T1 * T2) := foldr (fun x1 => cat (map (pair x1) (enum T2))) [::] (enum T1). diff --git a/AnSsreflectTutorial/tutorial_Gonthier_LeRoux.v b/AnSsreflectTutorial/tutorial_Gonthier_LeRoux.v index b8d1bb3..06276a3 100644 --- a/AnSsreflectTutorial/tutorial_Gonthier_LeRoux.v +++ b/AnSsreflectTutorial/tutorial_Gonthier_LeRoux.v @@ -1,3 +1,5 @@ + +Require PeanoNat. From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat div. (*****************************************************************************) @@ -223,7 +225,6 @@ Lemma concrete_plus_bis : 16 + 64 = 80. Proof. (* simpl. *) by []. Qed. Print mult. - Print le. Lemma concrete_le : le 1 3. diff --git a/README.md b/README.md index bc92584..edc4be9 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/math-comp/tutorial_material/workflows/Docker%20CI/badge.svg?branch=master -[docker-action-link]: https://github.com/math-comp/tutorial_material/actions?query=workflow:"Docker%20CI" +[docker-action-shield]: https://github.com/math-comp/tutorial_material/actions/workflows/docker-action.yml/badge.svg?branch=master +[docker-action-link]: https://github.com/math-comp/tutorial_material/actions/workflows/docker-action.yml @@ -27,30 +27,9 @@ It contains - Author(s): - Laurent Théry - License: [MIT License](LICENSE) -- Compatible Coq versions: 8.18 or later - Additional dependencies: - - [MathComp ssreflect 2.1 or later](https://math-comp.github.io) -- Coq namespace: `tutorial_material` + - [MathComp ssreflect 2.5 or later](https://math-comp.github.io) +- Rocq/Coq namespace: `tutorial_material` - Related publication(s): none ## Building and installation instructions - -The easiest way to install the latest released version of tutorial_material -is via [OPAM](https://opam.ocaml.org/doc/Install.html): - -```shell -opam repo add coq-released https://coq.inria.fr/opam/released -opam install coq-tutorial_material -``` - -To instead build and install manually, do: - -``` shell -git clone https://github.com/math-comp/tutorial_material.git -cd tutorial_material -make # or make -j -make install -``` - - - diff --git a/SummerSchoolSophia/lesson5.v b/SummerSchoolSophia/lesson5.v index c9cb7e9..c3f7819 100644 --- a/SummerSchoolSophia/lesson5.v +++ b/SummerSchoolSophia/lesson5.v @@ -115,8 +115,10 @@ Proof. apply: (iffP idP). elim: n m => [|n IH] m; case: m => // m Hm. by rewrite (IH m Hm). +(* move=> def_n; rewrite {}def_n. Undo. +*) move=> ->. (* move + rewrie + clear idiom *) by elim: m. Qed. @@ -148,8 +150,10 @@ About andP. Lemma example n m k : k <= n -> (n <= m) && (m <= k) -> n = k. Proof. +(* move=> lekn /andP H; case: H => lenm lemk. Undo. +*) move=> lekn /andP[lenm lemk]. (* view + case idiom *) Abort. @@ -220,7 +224,8 @@ by case split. #
# *) -Print Bool.reflect. + +Print reflect. About andP. Lemma example_spec a b : a && b ==> (a == b). @@ -282,8 +287,10 @@ About prime_gt1. Lemma example_2 x y : prime x -> odd y -> 2 < y + x. Proof. +(* move/prime_gt1 => x_gt_1. (* view through prime_gt1 *) Undo. +*) move/prime_gt1/ltnW. Abort. diff --git a/SummerSchoolSophia/lesson7.v b/SummerSchoolSophia/lesson7.v index 3e65a87..9ce4c78 100644 --- a/SummerSchoolSophia/lesson7.v +++ b/SummerSchoolSophia/lesson7.v @@ -132,23 +132,23 @@ Type inference *) -Check [eqType of bool]. +Check (Equality.clone _ bool). -Fail Check [eqType of bool -> bool]. +Fail Check (Equality.clone _ (bool -> bool)). -Check [eqType of {ffun bool -> bool}]. +Check (Equality.clone _ {ffun bool -> bool}). -Check [eqType of nat]. +Check (Equality.clone _ nat). -Fail Check [eqType of nat -> nat]. +Fail Check (Equality.clone _ (nat -> nat)). -Check [eqType of {ffun 'I_256 -> nat}]. +Check (Equality.clone _ {ffun 'I_256 -> nat}). -Check [eqType of seq nat]. +Check (Equality.clone _ (seq nat)). -Fail Check [eqType of seq (nat -> nat)]. +Fail Check (Equality.clone _ (seq (nat -> nat))). -Check [eqType of seq {ffun 'I_256 -> nat}]. +Check (Equality.clone _ {ffun 'I_256 -> nat}). (** #
# @@ -281,21 +281,21 @@ Variable chT : choiceType. Check (@sigW chT). -Check [eqType of chT]. +Check (Equality.clone _ chT). Variable coT : countType. -Check [countType of nat]. -Check [choiceType of coT]. -Check [choiceType of nat * nat]. -Check [choiceType of seq coT]. +Check (Countable.clone _ nat). +Check (Choice.clone _ coT). +Check (Choice.clone _ (nat * nat)%type). +Check (Choice.clone _ (seq coT)). Variable fT : finType. -Check [finType of bool]. -Check [finType of 'I_10]. -Check [finType of {ffun 'I_10 -> fT}]. -Check [finType of bool * bool]. +Check (Finite.clone _ bool). +Check (Finite.clone _ 'I_10). +Check (Finite.clone _ {ffun 'I_10 -> fT}). +Check (Finite.clone _ (bool * bool)%type). End Interfaces. diff --git a/SummerSchoolSophia/lesson8.v b/SummerSchoolSophia/lesson8.v index ae1893f..022046f 100644 --- a/SummerSchoolSophia/lesson8.v +++ b/SummerSchoolSophia/lesson8.v @@ -104,8 +104,10 @@ Proof. by case: t => s /= /eqP. Qed. Example seq_on_tuple (n : nat) (t : n .-tuple nat) : size (rev [seq 2 * x | x <- rev t]) = size t. Proof. +(* by rewrite map_rev revK size_map. Undo. +*) rewrite size_tuple. Fail rewrite size_tuple. Abort. @@ -181,7 +183,7 @@ that means we can craft an eqType. HB.instance Definition _ (n : nat) T := [isSub for (@tval n T)]. HB.instance Definition _ n (T : eqType) := [Equality of n .-tuple T by <:]. -Check [eqType of 3.-tuple nat]. +Check (Equality.clone _ (3.-tuple nat)). Example test_eqtype (x y : 3.-tuple nat) : x == y -> True. Proof. @@ -199,8 +201,8 @@ many other "promotions" #
# *) -Check [finType of 3.-tuple bool]. -Fail Check [finType of 3.-tuple nat]. +Check (Finite.clone _ (3.-tuple bool)). +Fail Check (Finite.clone _ (3.-tuple nat)). (** #
# @@ -213,8 +215,8 @@ numbers smaller than n. *) Print ordinal. -Check [eqType of 'I_3]. -Check [finType of 'I_3]. +Check (Equality.clone _ 'I_3). +Check (Finite.clone _ 'I_3). About tnth. (* like the safe nth function for vectors *) @@ -230,11 +232,11 @@ Check {set 'I_4} : Type. Check forall a : {set 'I_4}, (a == set0) || (1 < #| a | < 4). Print set_type. Check {ffun 'I_4 -> bool} : Type. -Check [eqType of #| 'I_4 | .-tuple bool]. -Check [finType of #| 'I_4 | .-tuple bool]. +Check (Equality.clone _ (#| 'I_4 | .-tuple bool)). +Check (Finite.clone _ (#| 'I_4 | .-tuple bool)). Check {ffun 'I_4 * 'I_6 -> nat} : Type. -Check [eqType of {ffun 'I_4 * 'I_6 -> nat}] : Type. +Check (Equality.clone _ {ffun 'I_4 * 'I_6 -> nat}) : Type. From mathcomp Require Import all_algebra. Open Scope ring_scope. diff --git a/coq-tutorial_material.opam b/coq-tutorial_material.opam index 176d832..b844d87 100644 --- a/coq-tutorial_material.opam +++ b/coq-tutorial_material.opam @@ -25,8 +25,8 @@ It contains build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "coq" {(>= "8.18")} - "coq-mathcomp-ssreflect" {(>= "2.1.0")} + "coq" + "coq-mathcomp-ssreflect" {(>= "2.5.0")} ] tags: [ diff --git a/meta.yml b/meta.yml index dbf00bc..a825897 100644 --- a/meta.yml +++ b/meta.yml @@ -33,19 +33,19 @@ license: fullname: MIT License identifier: MIT -supported_coq_versions: - text: '8.18 or later' - opam: '{(>= "8.18")}' +supported_rocq_versions: + text: '9.1 or later' + opam: '{(>= "9.1")}' dependencies: - opam: name: coq-mathcomp-ssreflect - version: '{(>= "2.1.0")}' + version: '{(>= "2.5.0")}' description: |- - [MathComp ssreflect 2.1 or later](https://math-comp.github.io) + [MathComp ssreflect 2.5 or later](https://math-comp.github.io) tested_coq_opam_versions: -- version: '2.1.0-coq-8.18' +- version: '2.5.0-rocq-prover-9.1' repo: 'mathcomp/mathcomp' namespace: tutorial_material