update for 2.5

.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'

AnIntroductionToSmallScaleReflectionInCoq/section6.v

@@ -18,10 +18,9 @@
 Definition unit1 := unit.
 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 @@
 (* 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).
@@ -372,7 +372,7 @@
 Structure tuto_tuple_of  : Type := 
   TutoTuple {tuto_tval :> seq T; _ : size tuto_tval == n}.
 
 #[verbose]
 HB.instance Definition _ := [isSub for tuto_tval].
 
 End Def.

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 @@
 Proof. (* simpl. *)  by []. Qed.
 
 Print mult.
-
 Print le.
 
 Lemma concrete_le : le 1 3.
@@ -238,7 +239,7 @@
 
 Print subn.
 
 Print subn_rec.
 
 Lemma concrete_big_leq : 0 <= 51.
 Proof. by []. Qed.

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 <number-of-cores-on-your-machine> 
-make install
-```
-
-
-

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.
 
 #<div>#
 *)
-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.

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}).
 
 (**
 #</div>#
@@ -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.
 

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"
 #<div>#
 *)
 
-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)).
 
 (**
 #<div/>#
@@ -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.

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: [

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