Fix compatibility with Coq 8.18 and later

.github/workflows/docker-action.yml

@@ -19,6 +19,8 @@ jobs:
     strategy:
       matrix:
         image:
+          - 'mathcomp/mathcomp:2.2.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.18'
           - 'mathcomp/mathcomp:2.2.0-coq-8.17'
           - 'mathcomp/mathcomp:2.2.0-coq-8.16'
           - 'mathcomp/mathcomp:2.1.0-coq-8.17'

README.md

@@ -52,7 +52,7 @@ of said algorithm.
 - Coq-community maintainer(s):
   - Christian Doczkal ([**@chdoc**](https://github.com/chdoc))
 - License: [CeCILL-B](LICENSE)
-- Compatible Coq versions: 8.16 and 8.17
+- Compatible Coq versions: 8.16 to 8.20
 - Additional dependencies:
   - [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

_CoqProject

@@ -3,7 +3,6 @@
 -arg -w -arg -notation-overridden
 -arg -w -arg -redundant-canonical-projection
 -arg -w -arg -notation-incompatible-format
--arg -w -arg -deprecated-instance-without-locality
 
 -Q theories CompDecModal
 

coq-comp-dec-modal.opam

@@ -32,7 +32,7 @@ of said algorithm.
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.16" & < "8.18"}
+  "coq" {>= "8.16" & < "8.21"}
   "coq-mathcomp-ssreflect" {>= "2.0"}
   "coq-hierarchy-builder" {>= "1.6.0"}
 ]

meta.yml

@@ -52,10 +52,14 @@ license:
   identifier: CECILL-B
 
 supported_coq_versions:
-  text: 8.16 and 8.17
-  opam: '{>= "8.16" & < "8.18"}'
+  text: 8.16 to 8.20
+  opam: '{>= "8.16" & < "8.21"}'
 
 tested_coq_opam_versions:
+- version: '2.2.0-coq-8.19'
+  repo: 'mathcomp/mathcomp'
+- version: '2.2.0-coq-8.18'
+  repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.16'

theories/CPDL/PDL_def.v

@@ -4,7 +4,7 @@ From HB Require Import structures.
 Require Import Relations Lia Setoid Morphisms.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs 
- Require Import edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac.
+ Require Import edone bcase fset base induced_sym modular_hilbert sltype rewrite_inequality fset_tac.
 
 Set Default Proof Using "Type".
 
@@ -323,7 +323,7 @@ End Hilbert.
   Lemma rNorm p s t : prv (s ---> t) -> prv ([p]s ---> [p]t).
   Proof. move => H. rule axN. exact: rNec. Qed.
 
-  Instance AX_mor (p : prog) : Proper (@mImpPrv prv_mSystem ==> @mImpPrv prv_mSystem) (fAX p).
+  #[export] Instance AX_mor (p : prog) : Proper (@mImpPrv prv_mSystem ==> @mImpPrv prv_mSystem) (fAX p).
   Proof. exact: rNorm. Qed.
 
   Lemma rStar_ind p u s : prv (u ---> [p]u) -> prv (u ---> s) -> prv (u ---> [p^*]s).
@@ -344,7 +344,7 @@ End Hilbert.
   Lemma rEXn p s t : prv (s ---> t) -> prv (EX p s ---> EX p t).
   Proof. move => H. rule ax_contraNN. apply: rNorm. by rule ax_contraNN. Qed.
 
-  Instance EX_mor (p : prog) : Proper (@mImpPrv prv_mSystem ==> @mImpPrv prv_mSystem) (EX p).
+  #[export] Instance EX_mor (p : prog) : Proper (@mImpPrv prv_mSystem ==> @mImpPrv prv_mSystem) (EX p).
   Proof. exact: rEXn. Qed.
 
   Lemma axDBD p s t : prv (EX p s ---> [p]t ---> EX p (s :/\: t)).

theories/CPDL/hilbert_ref.v

@@ -3,7 +3,7 @@
 Require Import Relations.
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
-From CompDecModal.libs Require Import edone bcase fset base modular_hilbert.
+From CompDecModal.libs Require Import edone bcase fset base induced_sym modular_hilbert.
 From CompDecModal.CPDL Require Import PDL_def demo.
 
 Set Default Proof Using "Type".

theories/CTL/gen_hsound.v

@@ -3,7 +3,7 @@
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs
- Require Import edone bcase fset base modular_hilbert sltype.
+ Require Import edone bcase fset base induced_sym modular_hilbert sltype.
 From CompDecModal.CTL
  Require Import CTL_def gen_def hilbert hilbert_hist.
 Import IC.

theories/CTL/hilbert_Eme90.v

@@ -3,7 +3,7 @@
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs
- Require Import edone bcase fset base modular_hilbert.
+ Require Import edone bcase fset base induced_sym modular_hilbert.
 From CompDecModal.CTL
  Require Import CTL_def hilbert.
 

theories/CTL/hilbert_LS.v

@@ -3,7 +3,7 @@
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs
- Require Import edone bcase fset base modular_hilbert.
+ Require Import edone bcase fset base induced_sym modular_hilbert.
 From CompDecModal.CTL
  Require Import CTL_def hilbert hilbert_hist.
 
@@ -202,4 +202,4 @@ Proof.
 Qed.       
 
 Lemma LS_sound s : LS.prv s -> prv s.
-Proof. elim => {s} *; eauto using prv,ERel,ARel,axARf,axERf,axAUcmp,axSer. Qed.
+Proof. elim => {s} *; eauto using prv,ERel,ARel,axARf,axERf,axAUcmp,axSer. Qed.

theories/CTL/hilbert_hist.v

@@ -3,7 +3,7 @@
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs
- Require Import edone bcase fset base modular_hilbert sltype.
+ Require Import edone bcase fset base induced_sym modular_hilbert sltype.
 From CompDecModal.CTL
  Require Import CTL_def hilbert.
 Import IC.

theories/CTL/hilbert_ref.v

@@ -4,7 +4,7 @@ Require Import Lia.
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs
- Require Import edone bcase fset base modular_hilbert sltype.
+ Require Import edone bcase fset base induced_sym modular_hilbert sltype.
 From CompDecModal.CTL
  Require Import CTL_def dags demo hilbert relaxed_pruning.
 Import IC.

theories/K/gentzen.v

@@ -4,7 +4,7 @@ Require Import Lia.
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs
- Require Import edone bcase fset base modular_hilbert sltype.
+ Require Import edone bcase fset base induced_sym modular_hilbert sltype.
 From CompDecModal.K
  Require Import K_def demo.
 

theories/K/hilbert_ref.v

@@ -4,7 +4,7 @@ Require Import Lia.
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs
- Require Import edone bcase fset base modular_hilbert sltype.
+ Require Import edone bcase fset base induced_sym modular_hilbert sltype.
 From CompDecModal.K
  Require Import K_def demo.
 

theories/Kstar/hilbert_ref.v

@@ -4,7 +4,7 @@ Require Import Relations Lia.
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs
- Require Import edone bcase fset base modular_hilbert sltype.
+ Require Import edone bcase fset base induced_sym modular_hilbert sltype.
 From CompDecModal.Kstar
  Require Import Kstar_def demo.
 

theories/PDL/PDL_def.v

@@ -4,7 +4,7 @@ From HB Require Import structures.
 Require Import Relations Lia Setoid Morphisms.
 From mathcomp Require Import all_ssreflect.
 From CompDecModal.libs 
- Require Import edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac.
+ Require Import edone bcase fset base induced_sym modular_hilbert sltype rewrite_inequality fset_tac.
 
 Set Default Proof Using "Type".
 
@@ -310,7 +310,7 @@ End Hilbert.
   Lemma rNorm p s t : prv (s ---> t) -> prv ([p]s ---> [p]t).
   Proof. move => H. rule axN. exact: rNec. Qed.
 
-  Instance AX_mor (p : prog) : Proper (@mImpPrv prv_mSystem ==> @mImpPrv prv_mSystem) (fAX p).
+  #[export] Instance AX_mor (p : prog) : Proper (@mImpPrv prv_mSystem ==> @mImpPrv prv_mSystem) (fAX p).
   Proof. exact: rNorm. Qed.
 
   Lemma rStar_ind p u s : prv (u ---> [p]u) -> prv (u ---> s) -> prv (u ---> [p^*]s).

theories/PDL/hilbert_ref.v

@@ -3,7 +3,7 @@
 Require Import Relations.
 Require Import mathcomp.ssreflect.ssreflect.
 From mathcomp Require Import all_ssreflect.
-From CompDecModal.libs Require Import edone bcase fset base modular_hilbert.
+From CompDecModal.libs Require Import edone bcase fset base induced_sym modular_hilbert.
 From CompDecModal.PDL Require Import PDL_def demo.
 
 Set Default Proof Using "Type".

theories/libs/edone.v

@@ -21,7 +21,6 @@ Ltac done := trivial; hnf in |- *; intros;
       | split
       | rewrite ?andbT ?andbF ?orbT ?orbF ]
     )
-    | case not_locked_false_eq_true; assumption
     | match goal with
         | H:~ _ |- _ => solve [ case H; trivial ]
       end

theories/libs/induced_sym.v

@@ -12,7 +12,7 @@ Require Import Setoid Morphisms Basics.
 Class InducedSym {T : Type} (P R : relation T) :=
   induced_iff : forall x y, R x y <-> P x y /\ P y x.
 
-Instance induced_sub {T : Type} (P R : relation T) :
+#[export] Instance induced_sub {T : Type} (P R : relation T) :
   InducedSym P R -> subrelation R P.
 Proof. firstorder. Qed.
 
@@ -45,22 +45,22 @@ Proof.
   firstorder.
 Qed.
 
-Instance induced_mor_p {T : Type} (P R : relation T) m :
+#[export] Instance induced_mor_p {T : Type} (P R : relation T) m :
   InducedSym P R -> Proper (P ==> P) m -> Proper (R ==> R) m.
 Proof. intros ind prop x y Rxy; induced_tac R. Qed.
 
-Instance induced_mor_n {T : Type} (P R : relation T) m :
+#[export] Instance induced_mor_n {T : Type} (P R : relation T) m :
   InducedSym P R -> Proper (P --> P) m -> Proper (R ==> R) m.
 Proof. intros ind prop x y Rxy; induced_tac R. Qed.
 
-Instance induced_mor_pp {T : Type} (P R : relation T) m :
+#[export] Instance induced_mor_pp {T : Type} (P R : relation T) m :
   InducedSym P R -> Proper (P ==> P ==> P) m -> Proper (R ==> R ==> R) m.
 Proof. intros ind prop x y Rxy x' y' Rxy'; induced_tac R. Qed.
 
-Instance induced_mor_pn {T : Type} (P R : relation T) m :
+#[export] Instance induced_mor_pn {T : Type} (P R : relation T) m :
   InducedSym P R -> Proper (P ==> P --> P) m -> Proper (R ==> R ==> R) m.
 Proof. intros ind prop x y Rxy x' y' Rxy'; induced_tac R. Qed.
 
-Instance induced_mor_np {T : Type} (P R : relation T) m :
+#[export] Instance induced_mor_np {T : Type} (P R : relation T) m :
   InducedSym P R -> Proper (P --> P ==> P) m -> Proper (R ==> R ==> R) m.
 Proof. intros ind prop x y Rxy x' y' Rxy'; induced_tac R. Qed.

theories/libs/modular_hilbert.v

@@ -102,14 +102,14 @@ Ltac Suff u := apply (mp2 (axS u _ _)).
 
 (** Enable Setoid rewriting for with provable implications *)
 
-Instance mImpPrv_rel (mS : mSystem) : PreOrder (@mImpPrv mS).
+#[export] Instance mImpPrv_rel (mS : mSystem) : PreOrder (@mImpPrv mS).
 Proof. split. exact: axI. exact: mImpPrv_trans. Qed.
 
-Instance mprv_mor (mS : mSystem) :
+#[export] Instance mprv_mor (mS : mSystem) :
   Proper ((@mImpPrv mS) ++> Basics.impl) (@mprv mS).
 Proof. move => x y H H'. mp; eassumption. Qed.
 
-Instance Imp_mor (mS : mSystem) :
+#[export] Instance Imp_mor (mS : mSystem) :
   Proper ((@mImpPrv mS) --> (@mImpPrv mS) ++> (@mImpPrv mS)) (@Imp mS).
 Proof.
   move => x' x X y y' Y. rewrite /mImpPrv in X Y *.
@@ -208,15 +208,15 @@ End PTheoryBase.
 
 (** Morphisms for defined locial operators *)
 
-Instance Neg_mor (pS : pSystem) :
+#[export] Instance Neg_mor (pS : pSystem) :
   Proper ((@mImpPrv pS) --> (@mImpPrv pS))(@Neg pS).
 Proof. rewrite /Neg; solve_proper. Qed.
 
-Instance And_mor (pS : pSystem) :
+#[export] Instance And_mor (pS : pSystem) :
   Proper ((@mImpPrv pS) ==> (@mImpPrv pS) ==> (@mImpPrv pS)) (@And pS).
 Proof. by rewrite /And; solve_proper. Qed.
 
-Instance Or_mor (pS : pSystem) :
+#[export] Instance Or_mor (pS : pSystem) :
   Proper ((@mImpPrv pS) ==> (@mImpPrv pS) ==> (@mImpPrv pS)) (@Or pS).
 Proof. by rewrite /Or; solve_proper. Qed.
 
@@ -243,35 +243,35 @@ Section EqiTheoryBase.
   Proof. exact: axAI. Qed.
 End EqiTheoryBase.
 
-Instance eqi_induced_symmety (pS : pSystem) : InducedSym (@mImpPrv pS) (@EqiPrv pS).
+#[export] Instance eqi_induced_symmety (pS : pSystem) : InducedSym (@mImpPrv pS) (@EqiPrv pS).
 Proof.
   move => s t. split => [H | [H1 H2]].
   split. by rule axEEl. by rule axEEr. by rule axEI.
 Qed.
 
-Instance induced_eqi (pS : pSystem) : Equivalence (@EqiPrv pS).
+#[export] Instance induced_eqi (pS : pSystem) : Equivalence (@EqiPrv pS).
 Proof. apply: induced_eqi. Qed.
 
 (** Short cut morphisms for faster equivalence rewrites *)
-Instance mprv_eqi_mor (pS : pSystem) :
+#[export] Instance mprv_eqi_mor (pS : pSystem) :
   Proper (@EqiPrv pS ==> iff) (@mprv pS).
 Proof. move => s t H. split. by rewrite -> H. by rewrite <- H. Qed.
 
-Instance Neg_Eqi_mor (pS : pSystem) :
+#[export] Instance Neg_Eqi_mor (pS : pSystem) :
   Proper ((@EqiPrv pS) ==> (@EqiPrv pS))(@Neg pS).
 Proof. rewrite /Neg; solve_proper. Qed.
 
-Instance And_Eqi_mor (pS : pSystem) :
+#[export] Instance And_Eqi_mor (pS : pSystem) :
   Proper ((@EqiPrv pS) ==> (@EqiPrv pS) ==> (@EqiPrv pS)) (@And pS).
 Proof. by rewrite /And; solve_proper. Qed.
 
-Instance Or_Eqi_mor (pS : pSystem) :
+#[export] Instance Or_Eqi_mor (pS : pSystem) :
   Proper ((@EqiPrv pS) ==> (@EqiPrv pS) ==> (@EqiPrv pS)) (@Or pS).
 Proof. by rewrite /Or; solve_proper. Qed.
 
 (** Rewriting below Equivalences *)
 
-Instance Eqi_mor (pS : pSystem) :
+#[export] Instance Eqi_mor (pS : pSystem) :
   Proper ((@EqiPrv pS) ==> (@EqiPrv pS) ==> (@EqiPrv pS)) (@Eqi pS).
 Proof. rewrite /Eqi. solve_proper. Qed.
 
@@ -518,20 +518,20 @@ Record kSystem := KSystem { psort   :> pSystem;
 Lemma rNorm (kS : kSystem) (s t : kS) : mprv (s ---> t) -> mprv (AX s ---> AX t).
 Proof. move => H. rule axN. exact: rNec. Qed.
 
-Instance AX_mor (kS : kSystem) : Proper ((@mImpPrv kS) ==> (@mImpPrv kS)) (@AX kS).
+#[export] Instance AX_mor (kS : kSystem) : Proper ((@mImpPrv kS) ==> (@mImpPrv kS)) (@AX kS).
 Proof. exact: rNorm. Qed.
 
 Definition EX (kS : kSystem) (s : kS) := ~~: AX (~~: s).
 
-Instance EX_mor (kS : kSystem) : Proper ((@mImpPrv kS) ==> (@mImpPrv kS)) (@EX kS).
+#[export] Instance EX_mor (kS : kSystem) : Proper ((@mImpPrv kS) ==> (@mImpPrv kS)) (@EX kS).
 Proof. move => x y H. rewrite /EX /mImpPrv. by rewrite -> H. Qed.
 
 (** Redundant Morphisms for Equivalence *)
 
-Instance AX_Eqi_mor (kS : kSystem) : Proper ((@EqiPrv kS) ==> (@EqiPrv kS)) (@AX kS).
+#[export] Instance AX_Eqi_mor (kS : kSystem) : Proper ((@EqiPrv kS) ==> (@EqiPrv kS)) (@AX kS).
 Proof. move => s t H. rewrite -> H. reflexivity. Qed.
 
-Instance EX_Eqi_mor (kS : kSystem) : Proper ((@EqiPrv kS) ==> (@EqiPrv kS)) (@EX kS).
+#[export] Instance EX_Eqi_mor (kS : kSystem) : Proper ((@EqiPrv kS) ==> (@EqiPrv kS)) (@EX kS).
 Proof. move => s t H. rewrite -> H. reflexivity. Qed.
 
 Section KTheory.
@@ -609,7 +609,7 @@ Section KStarTheory.
   Lemma rNormS s t : mprv (s ---> t) -> mprv (AG s ---> AG t).
   Proof. move/rNecS. apply: rMP. exact: axAGN. Qed.
 
-  Instance AG_mor : Proper ((@mImpPrv ksS) ==> (@mImpPrv ksS)) (@AG ksS).
+  #[export] Instance AG_mor : Proper ((@mImpPrv ksS) ==> (@mImpPrv ksS)) (@AG ksS).
   Proof. exact: rNormS. Qed.
 
   Lemma axAGEn s : mprv (~~: AG s ---> ~~: s :\/: ~~: AX (AG s)).
@@ -649,25 +649,25 @@ Definition ER {cS : ctlSystem} (s t : cS) := ~~: AU (~~: s) (~~: t).
 Definition EU {cS : ctlSystem} (s t : cS) := ~~: AR (~~: s) (~~: t).
 Notation "'EG' s" := (ER Bot s) (at level 8).
 
-Instance AU_mor (cS : ctlSystem) :
+#[export] Instance AU_mor (cS : ctlSystem) :
   Proper ((@mImpPrv cS) ==> (@mImpPrv cS) ==> (@mImpPrv cS))(@AU cS).
 Proof.
   move => x x' X y y' Y. rewrite /mImpPrv in X Y *.
   apply: rAU_ind. rewrite -> Y. exact: axAUI. rewrite -> X. exact: axAUf.
 Qed.
 
-Instance ER_mor (cS : ctlSystem) :
+#[export] Instance ER_mor (cS : ctlSystem) :
   Proper ((@mImpPrv cS) ==> (@mImpPrv cS) ==> (@mImpPrv cS))(@ER cS).
 Proof. rewrite /ER. solve_proper. Qed.
 
-Instance AR_mor (cS : ctlSystem) :
+#[export] Instance AR_mor (cS : ctlSystem) :
   Proper ((@mImpPrv cS) ==> (@mImpPrv cS) ==> (@mImpPrv cS))(@AR cS).
 Proof.
   move => x x' X y y' Y. rewrite /mImpPrv in X Y *.
   apply: rAR_ind. rewrite <- Y. exact: axARE. rewrite <- X. exact: axARu.
 Qed.
 
-Instance EU_mor (cS : ctlSystem) :
+#[export] Instance EU_mor (cS : ctlSystem) :
   Proper ((@mImpPrv cS) ==> (@mImpPrv cS) ==> (@mImpPrv cS))(@EU cS).
 Proof. rewrite /EU. solve_proper. Qed.