mathcomp 2.1

.github/workflows/docker-action.yml

@@ -17,7 +17,7 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.17.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.18'
       fail-fast: false
     steps:
       - uses: actions/checkout@v3

AnIntroductionToSmallScaleReflectionInCoq/section5.v

@@ -3,6 +3,7 @@
 (******************************************************************************)
 
 
+From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
 From mathcomp Require Import choice fintype  tuple finset.
 
@@ -13,8 +14,9 @@ Import Prenex Implicits.
 (******************************************************************************)
 (* Exercise 5.1.1                                                             *)
 (******************************************************************************)
+(* 2023 This has been updated to use HB *)
 
-Record zmodule_mixin (T : Type) : Type := ZmoduleMixin {
+HB.mixin Record IsZmodule T := {
   zero : T;
   opp : T -> T;
   add : T -> T -> T;
@@ -24,33 +26,28 @@ Record zmodule_mixin (T : Type) : Type := ZmoduleMixin {
   add0m : left_inverse zero opp add
 }.
 
-Record zmodule : Type := Zmodule {
-  carrier :> Type;
-  spec : zmodule_mixin carrier
-}.
-
-
-Definition bool_zmoduleMixin := ZmoduleMixin addbA addbC addFb addbb.
-
-
-Definition bool_zmodule := Zmodule bool_zmoduleMixin.
-
+#[short(type="zmodule")]
+HB.structure Definition Zmodule := { T of IsZmodule T }.
 
-Definition zmadd (Z : zmodule) := add (spec Z).
-
-Notation "x \+ y" :=    (@zmadd _ x y)(at level 50,left associativity).
+#[verbose]
+HB.instance Definition Bool_Zmodule :=
+  IsZmodule.Build bool addbA addbC addFb addbb.
 
+Notation "x \+ y" := (add x y)(at level 50,left associativity).
 
 (* We first need to prove that zmadd is associative and commutative *)
 (* The proof consists in breaking successivly the two nested records *)
 (*to recover all the ingredients present in the zmodule_mixin. Then *)
 (*the goal becomes trivial because the associative and commutative *)
 (*requirements were present in the spec. *)
-Lemma zmaddA : forall m : zmodule, associative (@zmadd m).
-Proof. by case=> Mc []. Qed.
+(* Update with HB, associativity and commutativity are available directly *)
+
+Lemma zmaddA : forall m : zmodule, associative (@add m).
+Proof. move=> m; apply: addA. Qed.
+
+Lemma zmaddC : forall m : zmodule, commutative (@add m).
+Proof. move=> m; apply: addC. Qed.
 
-Lemma zmaddC : forall m : zmodule, commutative (@zmadd m).
-Proof. by case=> Mc []. Qed.
 
 (* No we can conveniently prove the lemma *)
 (* The ssreflect rewrite tactic allows rewrite redex selection by *)
@@ -69,19 +66,24 @@ Qed.
 (*by the system, which is possibliy syntactically slightly different *)
 (*from the definition typed by the user (specially in the case of *)
 (*nested pattern matching *)
-Print nat_eqType.
-Print nat_eqMixin.
+
+HB.about hasDecEq.
+HB.about hasDecEq.eq_op.
+HB.about hasDecEq.eqP.
+
 Print eqn.
 Check @eqnP.
 
-Print bool_eqType.
-Print bool_eqMixin.
 Print eqb.
 Check @eqbP.
 
 (* Look for nat, bool, Equality.sort in the answer of the command: *)
 Print Canonical Projections.
 (* The equations stored after these declarations are respectively :
+eqn <- hasDecEq.eq_op ( ssrnat.HB_unnamed_factory_1 )
+BinNat.N.eqb <- hasDecEq.eq_op ( ssrnat.HB_unnamed_factory_3 )
+eqb <- hasDecEq.eq_op ( HB_unnamed_factory_4 )
+
 [ Equality.sort ? == nat  ] => ? = nat_eqType
 [ Equality.sort ? == bool ] => ? = bool_eqType
 *)

AnIntroductionToSmallScaleReflectionInCoq/section6.v

@@ -1,7 +1,9 @@
 (******************************************************************************)
 (* Solutions of exercises : Type inference by canonical structures            *)
 (******************************************************************************)
+(* This has been updated with HB *)
 
+From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
 From mathcomp Require Import choice fintype tuple finset.
 
@@ -13,10 +15,11 @@ Import Prenex Implicits.
 (* Exercise 6.1.1                                                             *)
 (******************************************************************************)
 
+Definition unit1 := unit.
 Lemma tuto_unit_enumP : Finite.axiom [:: tt]. Proof. by case. Qed.
 
-Definition tuto_unit_finMixin := FinMixin tuto_unit_enumP.
-Canonical Structure unit_finType := Eval hnf in FinType unit unit_finMixin.
+#[verbose]
+HB.instance Definition _ := isFinite.Build unit1 tuto_unit_enumP.
 
 
 (******************************************************************************)
@@ -369,8 +372,8 @@ Variable T : Type.
 Structure tuto_tuple_of  : Type := 
   TutoTuple {tuto_tval :> seq T; _ : size tuto_tval == n}.
 
-Canonical Structure tuple_subType :=
-  Eval hnf in [subType for tuto_tval].
+#[verbose]
+HB.instance Definition _ := [isSub for tuto_tval].
 
 End Def.
 
@@ -429,10 +432,9 @@ Section OrdinalSub.
 
 Variable n : nat.
 
-Inductive ordinal : predArgType := Ordinal m of m < n.
+Coercion nat_of_ord i := let: Ordinal m _ := i in m.
 
-Canonical Structure ordinal_subType :=
-  [subType for nat_of_ord].
+HB.instance Definition _ := [isSub of ordinal for nat_of_ord].
 
 End OrdinalSub.
 *)
@@ -452,15 +454,14 @@ Definition two := Ordinal (ltnSn 2).
 Check two.
 Eval compute in (val two).
 
-
 (* Orelse we can cast the definition with the expected type and use *)
 (*the generic subType constructor Sub *)
-Definition two' : [subType of 'I_3] := Sub 2 (ltnSn 3).
+Definition two' : (SubType.clone _ _ _ 'I_3) := Sub 2 (ltnSn 3).
 Check (two' : 'I_3).
 
 (* But in fact we only need to claim that the boolean test will *)
 (*evaluate to true, and let the system check that for us *)
-Definition two'' : [subType of 'I_3] := Sub 2 (refl_equal true).
+Definition two'' : (SubType.clone _ _ _ 'I_3) := Sub 2 (refl_equal true).
 Check two''.
 Eval compute in (val two'').
 
@@ -471,11 +472,9 @@ Inductive odds : Set := Odds x of (odd x).
 Definition nat_of_odds i := let: Odds m _ := i in m.
 
 (* And now the subType definition, which should declared as canonical *)
-Canonical Structure odds_subType :=
-  Eval hnf in [subType for nat_of_odds by odds_rect].
+#[verbose]
+HB.instance Definition _ := [isSub for nat_of_odds by odds_rect].
 
-(* Check that this require a canonical structure by replacing above
-Canonical Structure odds_subType := by Definition .... := *)
 Definition three : odds := Sub 3 (refl_equal true).
 
 (******************************************************************************)
@@ -486,14 +485,11 @@ Definition three : odds := Sub 3 (refl_equal true).
 (* WARNING : to be effective when the library where they are defined *)
 (*is loaded, canonical structures should be defined (or re-defined) *)
 (*outside sections... *)
-Definition odds_eqMixin := Eval hnf in [eqMixin of odds by <:].
-
-Canonical Structure odds_eqType := Eval hnf in EqType odds odds_eqMixin.
-
-Definition tuto_tuple_eqMixin := Eval hnf in [eqMixin of n.-tuple T by <:].
+#[verbose]
+HB.instance Definition _ := [Equality of odds by <:].
 
-Canonical Structure tuto_tuple_eqType :=
-  Eval hnf in EqType (n.-tuple T) tuto_tuple_eqMixin.
+#[verbose]
+HB.instance Definition _ := [Equality of n.-tuple T by <:].
 
 Lemma tuto_map_tnth_enum : forall (t : n.-tuple T),
    map (tnth t) (enum 'I_n) = t.

README.md

@@ -27,15 +27,23 @@ It contains
 - Author(s):
   - Laurent Théry
 - License: [MIT License](LICENSE)
-- Compatible Coq versions: 8.17 or later
+- Compatible Coq versions: 8.18 or later
 - Additional dependencies:
-  - [MathComp ssreflect 1.17 or later](https://math-comp.github.io)
+  - [MathComp ssreflect 2.1 or later](https://math-comp.github.io)
 - Coq namespace: `tutorial_material`
 - Related publication(s): none
 
 ## Building and installation instructions
 
-To build and install manually, do:
+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

Ssreflect15min/quesako.v

@@ -60,7 +60,7 @@ already require thinking a bit about data-structures and complexity. *)
 Close Scope Z_scope.
 
 (* E.g. unary numbes are not an option. *)
-Fail Eval compute in (10000 * 10000 : nat).
+Time Eval compute in (1000 * 1000 : nat).
 
 (* A reflection-based tactic replace explicit deduction steps, 
 logged in proof terms, with computational steps, checked by the kernel's 

SummerSchoolSophia/exercise8_solution.v

@@ -1,3 +1,4 @@
+From HB Require Import structures.
 From mathcomp Require Import all_ssreflect. 
 
 
@@ -76,22 +77,19 @@ Fail Check forall n m : odd_nat, n == m.
 
 (* Use the subtype machinery (that we used for tuples) in order
    to teach Coq that [odd_nat] is an [eqType] *)
-Canonical odd_subType :=
-(*D*)Eval hnf in [subType for oval].
-Definition odd_eqMixin :=
-(*D*)Eval hnf in [eqMixin of odd_nat by <:].
-Canonical odd_eqType :=
-(*D*)Eval hnf in EqType odd_nat odd_eqMixin.
+HB.instance Definition _ := 
+(*D*)  [isSub for oval].
+HB.instance Definition _ := 
+(*D*)[Equality of odd_nat by <:].
 
 (* Enjoy *)
 Check forall n m : odd_nat, n == m.
 
 (* Now do the same for [even_nat] *)
 Fail Check forall (n m : even_nat), m == n.
 
-(*D*)Canonical even_subType := Eval hnf in [subType for eval].
-(*D*)Definition even_eqMixin := Eval hnf in [eqMixin of even_nat by <:].
-(*D*)Canonical even_eqType := Eval hnf in EqType even_nat even_eqMixin.
+(*D*)HB.instance Definition _ := [isSub for eval].
+(*D*)HB.instance Definition _ :=  [Equality of even_nat by <:].
 
 Check forall (n m : even_nat), m == n.
 

SummerSchoolSophia/lesson7.v

@@ -76,7 +76,7 @@ Check true == false.
 
 Check (@eq_op _ true false).
 
-Check (@eq_op bool_eqType true false).
+Check (@eq_op (Equality.clone _ bool) true false).
 
 Check 3 == 4.
 

SummerSchoolSophia/lesson8.v

@@ -1,4 +1,4 @@
-
+From HB Require Import structures.
 From mathcomp Require Import all_ssreflect.
 
 Set Implicit Arguments.
@@ -34,12 +34,10 @@ Let's see another interface, the one of finite types
 #<div>#
 *)
 
-Print Finite.class_of. (* we extend choice with a mix in *)
-
-Print Finite.mixin_of. (* we mix in countable and two specific
-                          fields: an enumeration and an axiom *)
+HB.about Finite.
+HB.about isFinite.
 
-Print Finite.axiom.
+Print finite_axiom.
 Print count_mem.
 
 Eval lazy in count_mem 3 [:: 1;2;3;4;3;2;1].
@@ -94,7 +92,7 @@ Let's define the type of homogeneous tuples
 
 Module Tup.
 
-Record tuple_of n T := Tuple {
+Record tuple_of (n : nat) T := Tuple {
   tval  :> seq T;
   tsize :  size tval == n
 }.
@@ -180,10 +178,8 @@ that means we can craft an eqType.
 #<div>#
 *)
 
-
-Canonical tuple_subType n T := Eval hnf in [subType for (@tval n T)].
-Definition tuple_eqMixin n (T : eqType) := Eval hnf in [eqMixin of n .-tuple T by <:].
-Canonical tuple_eqType n (T : eqType) := Eval hnf in EqType (n .-tuple T) (tuple_eqMixin n T).
+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].
 

coq-tutorial_material.opam

@@ -25,8 +25,8 @@ It contains
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.17")}
-  "coq-mathcomp-ssreflect" {(>= "1.17.0")}
+  "coq" {(>= "8.18")}
+  "coq-mathcomp-ssreflect" {(>= "2.1.0")}
 ]
 
 tags: [

meta.yml

@@ -34,18 +34,18 @@ license:
   identifier: MIT
 
 supported_coq_versions:
-  text: '8.17 or later'
-  opam: '{(>= "8.17")}'
+  text: '8.18 or later'
+  opam: '{(>= "8.18")}'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "1.17.0")}'
+    version: '{(>= "2.1.0")}'
   description: |-
-    [MathComp ssreflect 1.17 or later](https://math-comp.github.io)
+    [MathComp ssreflect 2.1 or later](https://math-comp.github.io)
 
 tested_coq_opam_versions:
-- version: '1.17.0-coq-8.17'
+- version: '2.1.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
 
 namespace: tutorial_material