diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index c8a1815..4705a8c 100644 --- a/.github/workflows/docker-action.yml +++ b/.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 diff --git a/README.md b/README.md index 542796e..a5e8964 100644 --- a/README.md +++ b/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) diff --git a/coq-comp-dec-modal.opam b/coq-comp-dec-modal.opam index 6a0a4fc..2a0b8d9 100644 --- a/coq-comp-dec-modal.opam +++ b/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: [ diff --git a/meta.yml b/meta.yml index c66be64..07ed94b 100644 --- a/meta.yml +++ b/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 diff --git a/theories/CPDL/PDL_def.v b/theories/CPDL/PDL_def.v index 57f2907..af7a723 100644 --- a/theories/CPDL/PDL_def.v +++ b/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 diff --git a/theories/CTL/CTL_def.v b/theories/CTL/CTL_def.v index ca15a56..c8b7ce6 100644 --- a/theories/CTL/CTL_def.v +++ b/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 diff --git a/theories/CTL/dags.v b/theories/CTL/dags.v index 0a906b0..5e2dd86 100644 --- a/theories/CTL/dags.v +++ b/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. diff --git a/theories/CTL/demo.v b/theories/CTL/demo.v index 279e466..8e13b44 100644 --- a/theories/CTL/demo.v +++ b/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. diff --git a/theories/CTL/gen_def.v b/theories/CTL/gen_def.v index fe9b532..b794bae 100644 --- a/theories/CTL/gen_def.v +++ b/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). diff --git a/theories/K/K_def.v b/theories/K/K_def.v index e44cb4d..5045e64 100644 --- a/theories/K/K_def.v +++ b/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 diff --git a/theories/Kstar/Kstar_def.v b/theories/Kstar/Kstar_def.v index 0125ecb..4e9ecfe 100644 --- a/theories/Kstar/Kstar_def.v +++ b/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 diff --git a/theories/Kstar/gen_def.v b/theories/Kstar/gen_def.v index d07babc..e4f1858 100644 --- a/theories/Kstar/gen_def.v +++ b/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). diff --git a/theories/PDL/PDL_def.v b/theories/PDL/PDL_def.v index ec7110b..02f05fa 100644 --- a/theories/PDL/PDL_def.v +++ b/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 diff --git a/theories/libs/fset.v b/theories/libs/fset.v index 757edb7..e09dbc3 100644 --- a/theories/libs/fset.v +++ b/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).