Merge pull request #11 from coq-community/mc2

MathComp 2 boilerplate

.github/workflows/docker-action.yml

@@ -19,19 +19,21 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp-dev:coq-dev'
-          - 'mathcomp/mathcomp:1.14.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.13.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.12.0-coq-8.13'
-          - 'mathcomp/mathcomp:1.11.0-coq-8.12'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.16'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.16'
+          - 'mathcomp/mathcomp:2.0.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.0.0-coq-8.16'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-comp-dec-modal.opam'
           custom_image: ${{ matrix.image }}
 
+
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme
 # https://github.com/erikmd/docker-coq-github-action-demo

README.md

@@ -11,8 +11,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [![coqdoc][coqdoc-shield]][coqdoc-link]
 [![DOI][doi-shield]][doi-link]
 
-[docker-action-shield]: https://github.com/coq-community/comp-dec-modal/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/coq-community/comp-dec-modal/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/coq-community/comp-dec-modal/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/coq-community/comp-dec-modal/actions/workflows/docker-action.yml
 
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
 [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md
@@ -52,9 +52,10 @@ of said algorithm.
 - Coq-community maintainer(s):
   - Christian Doczkal ([**@chdoc**](https://github.com/chdoc))
 - License: [CeCILL-B](LICENSE)
-- Compatible Coq versions: 8.12 or later
+- Compatible Coq versions: 8.16 and 8.17
 - Additional dependencies:
-  - [MathComp](https://math-comp.github.io) 1.11.0 or later (`ssreflect` suffices)
+  - [MathComp](https://math-comp.github.io) 2.0 or later (`ssreflect` suffices)
+  - [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) 1.6.0 or later
 - Coq namespace: `CompDecModal`
 - Related publication(s):
   - [A Machine-Checked Constructive Metatheory of Computation Tree Logic](https://www.ps.uni-saarland.de/static/doczkal-diss/index.php) doi:[10.22028/D291-26649](https://doi.org/10.22028/D291-26649)

coq-comp-dec-modal.opam

@@ -32,8 +32,9 @@ of said algorithm.
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.12" & < "8.16~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "1.11" & < "1.15~") | (= "dev")}
+  "coq" {>= "8.16" & < "8.18"}
+  "coq-mathcomp-ssreflect" {>= "2.0"}
+  "coq-hierarchy-builder" {>= "1.6.0"}
 ]
 
 tags: [

meta.yml

@@ -52,31 +52,37 @@ license:
   identifier: CECILL-B
 
 supported_coq_versions:
-  text: 8.12 or later
-  opam: '{(>= "8.12" & < "8.16~") | (= "dev")}'
+  text: 8.16 and 8.17
+  opam: '{>= "8.16" & < "8.18"}'
 
 tested_coq_opam_versions:
-- version: 'coq-dev'
-  repo: 'mathcomp/mathcomp-dev'
-- version: '1.14.0-coq-8.15'
+- version: '2.2.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
-- version: '1.13.0-coq-8.14'
+- version: '2.2.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
-- version: '1.12.0-coq-8.13'
+- version: '2.1.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
-- version: '1.11.0-coq-8.12'
+- version: '2.1.0-coq-8.16'
+  repo: 'mathcomp/mathcomp'
+- version: '2.0.0-coq-8.17'
+  repo: 'mathcomp/mathcomp'
+- version: '2.0.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
 
 # “At 01:42 on Sunday.”
 ci_cron_schedule: '42 1 * * 0'
-    
+
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "1.11" & < "1.15~") | (= "dev")}'
-  nix: ssreflect
+    version: '{>= "2.0"}'
+  description: |-
+    [MathComp](https://math-comp.github.io) 2.0 or later (`ssreflect` suffices)
+- opam:
+    name: coq-hierarchy-builder
+    version: '{>= "1.6.0"}'
   description: |-
-    [MathComp](https://math-comp.github.io) 1.11.0 or later (`ssreflect` suffices)
+    [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) 1.6.0 or later
 
 namespace: CompDecModal
 

theories/CPDL/PDL_def.v

@@ -1,5 +1,6 @@
 (* (c) Copyright Christian Doczkal and Joachim Bard                       *)
 (* Distributed under the terms of the CeCILL-B license                    *)
+From HB Require Import structures.
 Require Import Relations Lia Setoid Morphisms.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs 
@@ -96,13 +97,10 @@ Proof with case => /=; try (constructor; discriminate).
   - move => p IHp... move => q. apply: (iffP (IHp _)); congruence.
 Qed.
 End Eq.
-
-Definition form_eqMixin := EqMixin (fst Eq.form_prog_dec).
-Canonical Structure form_eqType := Eval hnf in @EqType form form_eqMixin.
 
-Definition prog_eqMixin := EqMixin (snd Eq.form_prog_dec).
-Canonical Structure prog_eqType := Eval hnf in @EqType prog prog_eqMixin.
+HB.instance Definition _ := hasDecEq.Build form (fst Eq.form_prog_dec).
 
+HB.instance Definition _ := hasDecEq.Build prog (snd Eq.form_prog_dec).
 
 (** To use formulas and other types built around formulas as base type
 for the finite set libaray, we need to show that formulas are
@@ -166,12 +164,7 @@ End formChoice.
 
 (** Note that we only need the [choiceType] and [countType] instances for formulas *)
 
-Definition form_countMixin := PcanCountMixin formChoice.picklefP.
-Definition form_choiceMixin := CountChoiceMixin form_countMixin.
-Canonical Structure form_ChoiceType := Eval hnf in ChoiceType form form_choiceMixin.
-Canonical Structure form_CountType := Eval hnf in CountType form form_countMixin.
-
-
+HB.instance Definition _ : isCountable form := PCanIsCountable formChoice.picklefP.
 
 (** ** Models
 

theories/CTL/CTL_def.v

@@ -1,5 +1,6 @@
 (* (c) Copyright Christian Doczkal, Saarland University                   *)
 (* Distributed under the terms of the CeCILL-B license                    *)
+From HB Require Import structures.
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs
@@ -211,8 +212,7 @@ Inductive form :=
 Lemma eq_form_dec (s t : form) : { s = t} + { s <> t}.
 Proof. decide equality; apply eq_comparable. Qed.
 
-Definition form_eqMixin := EqMixin (compareP eq_form_dec).
-Canonical Structure form_eqType := Eval hnf in @EqType form form_eqMixin.
+HB.instance Definition _ := hasDecEq.Build form (compareP eq_form_dec).
 
 (** To use formulas and other types built around formulas as base type
 for the finite set libaray, we need to show that formulas are
@@ -250,10 +250,7 @@ Module formChoice.
   Proof. move => s. by elim: s => //= [s -> t ->| s -> | s -> t -> | s -> t -> ]. Qed.
 End formChoice.
 
-Definition form_countMixin := PcanCountMixin formChoice.pickleP.
-Definition form_choiceMixin := CountChoiceMixin form_countMixin.
-Canonical Structure form_ChoiceType := Eval hnf in ChoiceType form form_choiceMixin.
-Canonical Structure form_CountType := Eval hnf in CountType form form_countMixin.
+HB.instance Definition _ : isCountable form := PCanIsCountable formChoice.pickleP.
 
 (** ** Models
 

theories/CTL/dags.v

@@ -77,7 +77,7 @@ Arguments restrict [T P] Tp e x y.
 Lemma connect_subtype (T : finType) (x0 : T) (e : rel T) (Tp : subFinType (connect e x0)) :
   forall x p, connect (restrict Tp e) (Sub x0 p) x.
 Proof.
-  move => x. case: (SubP x) => {x} - x Px. 
+  move => x. case: (SubP x) => {x} - x Px.
   case/connectP : Px (Px) => pth. elim/last_ind: pth x => [x _ -> Px /= p|pth y IH x /=].
   - by rewrite (bool_irrelevance p Px) connect0.
   - rewrite rcons_path last_rcons.

theories/CTL/demo.v

@@ -615,7 +615,8 @@ Section ModelConstruction.
       forall y, MRel (Mstate (root (Frag (next p.1, SeqSub (label x) (label_DF lf))))) y <->
                 MRel (Mstate x) y.
   Proof.
-    move => [p' y]. rewrite /MRel /Mstate (negbTE (root_internal _)) [_ && _]/= orbF.
+    move => [p' y]. rewrite /MRel /Mstate (negbTE (root_internal _)) [_ && _]/=.
+    rewrite [in X in X <-> _]orbF.
     split => [le|/orP [le|H]].
     - move: (liftE le) => ?;subst. rightb. rewrite lf /= !eqxx. by rewrite lift_eq in le.
     - move: (liftE le) => ?;subst. rewrite lift_eq in le.

theories/CTL/gen_def.v

@@ -1,5 +1,6 @@
 (* (c) Copyright Christian Doczkal, Saarland University                   *)
 (* Distributed under the terms of the CeCILL-B license                    *)
+From HB Require Import structures.
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs
@@ -26,8 +27,7 @@ Inductive annot :=
 Lemma eq_annot_dec (E1 E2 : annot) : {E1 = E2} + {E1 <> E2}.
 Proof. decide equality; apply: eq_comparable. Qed.
 
-Definition annot_eqMixin := EqMixin (compareP eq_annot_dec).
-Canonical Structure annot_eqType := Eval hnf in @EqType annot annot_eqMixin.
+HB.instance Definition _ := hasDecEq.Build annot (compareP eq_annot_dec).
 
 Definition aR (E : annot) := if E is aAXU (p, H) then aAU (p,H) else aVoid.
 
@@ -57,11 +57,7 @@ Module Annot.
   Proof. move => s. case: s => //= p; by rewrite pickleK. Qed.
 End Annot.
 
-
-Definition annot_countMixin := PcanCountMixin (Annot.pickleP).
-Definition annot_choiceMixin := CountChoiceMixin annot_countMixin.
-Canonical Structure annot_choiceType := Eval hnf in ChoiceType annot annot_choiceMixin.
-Canonical Structure annot_CountType := Eval hnf in CountType annot annot_countMixin.
+HB.instance Definition _ : isCountable annot := PCanIsCountable Annot.pickleP.
 
 Implicit Types (C : clause) (E : annot).
 

theories/K/K_def.v

@@ -1,5 +1,6 @@
 (* (c) Copyright Christian Doczkal, Saarland University                   *)
 (* Distributed under the terms of the CeCILL-B license                    *)
+From HB Require Import structures.
 Require Import Relations.
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
@@ -27,8 +28,7 @@ Inductive form :=
 Lemma eq_form_dec (s t : form) : { s = t} + { s <> t}.
 Proof. decide equality; apply eq_comparable. Qed.
 
-Definition form_eqMixin := EqMixin (compareP eq_form_dec).
-Canonical Structure form_eqType := Eval hnf in @EqType form form_eqMixin.
+HB.instance Definition _ := hasDecEq.Build form (compareP eq_form_dec).
 
 (** To use formulas and other types built around formulas as base type
 for the finite set libaray, we need to show that formulas are
@@ -60,10 +60,7 @@ Module formChoice.
   Proof. move => s. by elim: s => //= [s -> t ->| s -> ]. Qed.
 End formChoice.
 
-Definition form_countMixin := PcanCountMixin formChoice.pickleP.
-Definition form_choiceMixin := CountChoiceMixin form_countMixin.
-Canonical Structure form_ChoiceType := Eval hnf in ChoiceType form form_choiceMixin.
-Canonical Structure form_CountType := Eval hnf in CountType form form_countMixin.
+HB.instance Definition _ : isCountable form := PCanIsCountable formChoice.pickleP.
 
 (** ** Models
 

theories/Kstar/Kstar_def.v

@@ -1,5 +1,6 @@
 (* (c) Copyright Christian Doczkal, Saarland University                   *)
 (* Distributed under the terms of the CeCILL-B license                    *)
+From HB Require Import structures.
 Require Import Relations.
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
@@ -87,8 +88,7 @@ Inductive form :=
 Lemma eq_form_dec (s t : form) : { s = t} + { s <> t}.
 Proof. decide equality; apply eq_comparable. Qed.
 
-Definition form_eqMixin := EqMixin (compareP eq_form_dec).
-Canonical Structure form_eqType := Eval hnf in @EqType form form_eqMixin.
+HB.instance Definition _ := hasDecEq.Build form (compareP eq_form_dec).
 
 (** To use formulas and other types built around formulas as base type
 for the finite set libaray, we need to show that formulas are
@@ -122,10 +122,7 @@ Module formChoice.
   Proof. move => s. by elim: s => //= [s -> t ->| s -> | s -> ]. Qed.
 End formChoice.
 
-Definition form_countMixin := PcanCountMixin formChoice.pickleP.
-Definition form_choiceMixin := CountChoiceMixin form_countMixin.
-Canonical Structure form_ChoiceType := Eval hnf in ChoiceType form form_choiceMixin.
-Canonical Structure form_CountType := Eval hnf in CountType form form_countMixin.
+HB.instance Definition _ : isCountable form := PCanIsCountable formChoice.pickleP.
 
 (** ** Models 
 

theories/Kstar/gen_def.v

@@ -1,5 +1,6 @@
 (* (c) Copyright Christian Doczkal, Saarland University                   *)
 (* Distributed under the terms of the CeCILL-B license                    *)
+From HB Require Import structures.
 Require Import Relations.
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
@@ -26,8 +27,7 @@ Inductive annot :=
 Lemma eq_annot_dec (E1 E2 : annot) : {E1 = E2} + {E1 <> E2}.
 Proof. decide equality; apply: eq_comparable. Qed.
 
-Definition annot_eqMixin := EqMixin (compareP eq_annot_dec).
-Canonical Structure annot_eqType := Eval hnf in @EqType annot annot_eqMixin.
+HB.instance Definition _ := hasDecEq.Build annot (compareP eq_annot_dec).
 
 Module Annot.
   Definition pickle A :=
@@ -51,11 +51,7 @@ Module Annot.
   Proof. move => s. case: s => //= p; by rewrite pickleK. Qed.
 End Annot.
 
-
-Definition annot_countMixin := PcanCountMixin (Annot.pickleP).
-Definition annot_choiceMixin := CountChoiceMixin annot_countMixin.
-Canonical Structure annot_choiceType := Eval hnf in ChoiceType annot annot_choiceMixin.
-Canonical Structure annot_CountType := Eval hnf in CountType annot annot_countMixin.
+HB.instance Definition _ : isCountable annot := PCanIsCountable Annot.pickleP.
 
 Implicit Types (S H : {fset clause}) (C D E : clause) (a : annot) (Ca : clause * annot).
 

theories/PDL/PDL_def.v

@@ -1,5 +1,6 @@
 (* (c) Copyright Christian Doczkal and Joachim Bard                       *)
 (* Distributed under the terms of the CeCILL-B license                    *)
+From HB Require Import structures.
 Require Import Relations Lia Setoid Morphisms.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs 
@@ -92,13 +93,10 @@ Proof with case => /=; try (constructor; discriminate).
   - move => s IHs... move => t. apply: (iffP (IHs _)); congruence.
 Qed.
 End Eq.
-
-Definition form_eqMixin := EqMixin (fst Eq.form_prog_dec).
-Canonical Structure form_eqType := Eval hnf in @EqType form form_eqMixin.
 
-Definition prog_eqMixin := EqMixin (snd Eq.form_prog_dec).
-Canonical Structure prog_eqType := Eval hnf in @EqType prog prog_eqMixin.
+HB.instance Definition _ := hasDecEq.Build form (fst Eq.form_prog_dec).
 
+HB.instance Definition _ := hasDecEq.Build prog (snd Eq.form_prog_dec).
 
 (** To use formulas and other types built around formulas as base type
 for the finite set libaray, we need to show that formulas are
@@ -160,12 +158,7 @@ End formChoice.
 
 (** Note that we only need the [choiceType] and [countType] instances for formulas *)
 
-Definition form_countMixin := PcanCountMixin formChoice.picklefP.
-Definition form_choiceMixin := CountChoiceMixin form_countMixin.
-Canonical Structure form_ChoiceType := Eval hnf in ChoiceType form form_choiceMixin.
-Canonical Structure form_CountType := Eval hnf in CountType form form_countMixin.
-
-
+HB.instance Definition _ : isCountable form := PCanIsCountable formChoice.picklefP.
 
 (** ** Models
 

theories/libs/fset.v

@@ -1,5 +1,6 @@
 (* (c) Copyright Christian Doczkal, Saarland University                   *)
 (* Distributed under the terms of the CeCILL-B license                    *)
+From HB Require Import structures.
 Require Import Recdef.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs Require Import edone bcase base.
@@ -93,19 +94,15 @@ Section FinSets.
   Definition fset_of of phant T := fset_type.
   Identity Coercion type_of_fset_of  : fset_of >-> fset_type.
 
-  Canonical Structure fset_subType := [subType for elements by fset_type_rect].
-  Canonical Structure fset_eqType := EqType _ [eqMixin of fset_type by <:].
+  HB.instance Definition _ := [isSub for elements by fset_type_rect].
+  HB.instance Definition _ := [Choice of fset_type by <:].
   Canonical Structure fset_predType := PredType (fun (X : fset_type) x => nosimpl x \in elements X).
-  Canonical Structure fset_choiceType := Eval hnf in ChoiceType _ [choiceMixin of fset_type by <:].
 End FinSets.
 
 (** Additional Canonical Structures in case T is a countType. 
 This allows sets of sets of countTypes *)
 
-Canonical Structure fset_countType (T : countType) :=
-  Eval hnf in CountType _ [countMixin of fset_type T by <:].
-Canonical Structure fset_subCountType (T : countType) :=
-  Eval hnf in [subCountType of fset_type T].
+HB.instance Definition _ (T : countType) := [Countable of fset_type T by <:].
 
 (** Notation for fsets using Phant to allow the type checker to infer
 the Caonical Structure for the element type *)
@@ -687,10 +684,11 @@ Proof.
   move => x. by rewrite !inE mem_filter andbC.
 Qed.
 
-Canonical Structure fsetU_law (T : choiceType) := 
-  Monoid.Law (@fsetUA T) (@fset0U T) (@fsetU0 T).
-Canonical Structure fsetU_comlaw (T : choiceType) := 
-  Monoid.ComLaw (@fsetUC T).
+HB.instance Definition _ (T : choiceType) :=
+  Monoid.isLaw.Build {fset T} fset0 fsetU (@fsetUA T) (@fset0U T) (@fsetU0 T).
+
+HB.instance Definition _ (T : choiceType) :=
+  SemiGroup.isCommutativeLaw.Build _ fsetU (@fsetUC T).
 
 Notation "\bigcup_( x 'in' X | P )  F" := 
   (\big[fsetU/fset0]_(x <- elements X | P) F) (at level 41).