Adapt to MC2 and newer versions of Coq

.github/workflows/docker-action.yml

@@ -17,21 +17,31 @@ jobs:
     strategy:
       matrix:
         image:
+          - 'mathcomp/mathcomp:2.0.0-coq-8.16'
+          - 'mathcomp/mathcomp:2.0.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.0.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.16'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.16'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.20'
+          - 'mathcomp/mathcomp:2.2.0-coq-dev'
+          - 'mathcomp/mathcomp-dev:coq-8.18'
+          - 'mathcomp/mathcomp-dev:coq-8.19'
+          - 'mathcomp/mathcomp-dev:coq-8.20'
           - 'mathcomp/mathcomp-dev:coq-dev'
-          - 'mathcomp/mathcomp:1.13.0-coq-8.14'
-          - 'mathcomp/mathcomp:1.12.0-coq-8.13'
-          - 'mathcomp/mathcomp:1.12.0-coq-8.12'
-          - 'mathcomp/mathcomp:1.11.0-coq-8.12'
-          - 'mathcomp/mathcomp:1.10.0-coq-8.11'
-          - 'mathcomp/mathcomp:1.10.0-coq-8.10'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-lemma-overloading.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/lemma-overloading/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/coq-community/lemma-overloading/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/coq-community/lemma-overloading/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/coq-community/lemma-overloading/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
@@ -48,9 +48,10 @@ re-implementations for comparison.
 - Coq-community maintainer(s):
   - Anton Trunov ([**@anton-trunov**](https://github.com/anton-trunov))
 - License: [GNU General Public License v3.0 or later](LICENSE.md)
-- Compatible Coq versions: 8.10 or later (use releases for other Coq versions)
+- Compatible Coq versions: 8.16 or later (use releases for other Coq versions)
 - Additional dependencies:
-  - [MathComp](https://math-comp.github.io) 1.10.0 or later (`ssreflect` suffices)
+  - [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) 1.5.0 or later
+  - [MathComp](https://math-comp.github.io) 2.0.0 or later (`ssreflect` suffices)
 - Coq namespace: `LemmaOverloading`
 - Related publication(s):
   - [How to make ad hoc proof automation less ad hoc](https://software.imdea.org/~aleks/papers/lessadhoc/journal.pdf) doi:[10.1017/S0956796813000051](https://doi.org/10.1017/S0956796813000051)

coq-lemma-overloading.opam

@@ -25,8 +25,9 @@ re-implementations for comparison."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.10" & < "8.15~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "1.10" & < "1.14~") | (= "dev")}
+  "coq" {>= "8.16"}
+  "coq-hierarchy-builder" {>= "1.5.0"}
+  "coq-mathcomp-ssreflect" {>= "2.0"}
 ]
 
 tags: [

meta.yml

@@ -53,32 +53,55 @@ license:
   file: LICENSE.md
 
 supported_coq_versions:
-  text: 8.10 or later (use releases for other Coq versions)
-  opam: '{(>= "8.10" & < "8.15~") | (= "dev")}'
+  text: 8.16 or later (use releases for other Coq versions)
+  opam: '{>= "8.16"}'
 
 tested_coq_opam_versions:
-- version: 'coq-dev'
-  repo: 'mathcomp/mathcomp-dev'
-- version: '1.13.0-coq-8.14'
+- version: '2.0.0-coq-8.16'
+  repo: 'mathcomp/mathcomp'
+- version: '2.0.0-coq-8.17'
+  repo: 'mathcomp/mathcomp'
+- version: '2.0.0-coq-8.18'
+  repo: 'mathcomp/mathcomp'
+- version: '2.1.0-coq-8.16'
+  repo: 'mathcomp/mathcomp'
+- version: '2.1.0-coq-8.17'
+  repo: 'mathcomp/mathcomp'
+- version: '2.1.0-coq-8.18'
+  repo: 'mathcomp/mathcomp'
+- version: '2.2.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
-- version: '1.12.0-coq-8.13'
+- version: '2.2.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
-- version: '1.12.0-coq-8.12'
+- version: '2.2.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
-- version: '1.11.0-coq-8.12'
+- version: '2.2.0-coq-8.19'
   repo: 'mathcomp/mathcomp'
-- version: '1.10.0-coq-8.11'
+- version: '2.2.0-coq-8.20'
   repo: 'mathcomp/mathcomp'
-- version: '1.10.0-coq-8.10'
+- version: '2.2.0-coq-dev'
   repo: 'mathcomp/mathcomp'
+- version: 'coq-8.18'
+  repo: 'mathcomp/mathcomp-dev'
+- version: 'coq-8.19'
+  repo: 'mathcomp/mathcomp-dev'
+- version: 'coq-8.20'
+  repo: 'mathcomp/mathcomp-dev'
+- version: 'coq-dev'
+  repo: 'mathcomp/mathcomp-dev'
 
 dependencies:
+- opam:
+    name: coq-hierarchy-builder
+    version: '{>= "1.5.0"}'
+  description: |-
+    [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) 1.5.0 or later
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "1.10" & < "1.14~") | (= "dev")}'
+    version: '{>= "2.0"}'
   nix: ssreflect
   description: |-
-    [MathComp](https://math-comp.github.io) 1.10.0 or later (`ssreflect` suffices)
+    [MathComp](https://math-comp.github.io) 2.0.0 or later (`ssreflect` suffices)
 
 namespace: LemmaOverloading
 

theories/auto.v

@@ -15,10 +15,8 @@
     along with this program.  If not, see <http://www.gnu.org/licenses/>.
 *)
 
-From mathcomp
-Require Import ssreflect seq.
-From LemmaOverloading
-Require Import rels.
+From mathcomp Require Import ssreflect seq.
+From LemmaOverloading Require Import rels.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.

theories/cancel.v

@@ -15,10 +15,8 @@
     along with this program.  If not, see <http://www.gnu.org/licenses/>.
 *)
 
-From mathcomp
-Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype.
-From LemmaOverloading
-Require Import prelude prefix xfind heaps terms.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype.
+From LemmaOverloading Require Import prelude prefix xfind heaps terms.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.

theories/cancel2.v

@@ -15,15 +15,13 @@
     along with this program.  If not, see <http://www.gnu.org/licenses/>.
 *)
 
-From mathcomp
-Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype.
-From LemmaOverloading
-Require Import prelude prefix heaps terms.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype.
+From LemmaOverloading Require Import prelude prefix heaps terms.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Obligation Tactic := idtac.
 
 Set Printing Existential Instances.
 

theories/cancelCTC.v

@@ -15,10 +15,8 @@
     along with this program.  If not, see <http://www.gnu.org/licenses/>.
 *)
 
-From mathcomp
-Require Import ssreflect ssrbool ssrnat seq eqtype.
-From LemmaOverloading
-Require Import prelude heaps terms prefix xfindCTC.
+From mathcomp Require Import ssreflect ssrbool ssrnat seq eqtype.
+From LemmaOverloading Require Import prelude heaps terms prefix xfindCTC.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -36,6 +34,7 @@ Arguments Ast : clear implicits.
 
 
 (* pass output context of f1 as input of f2 *)
+#[export]
 Program Instance
   union_struct i j k t1 t2 h1 h2 (f1 : Ast i j t1 h1) (f2 : Ast j k t2 h2) :
   Ast i k (t1 ++ t2) (h1 :+ h2) | 3.
@@ -46,12 +45,14 @@ split; first by rewrite interp_cat (interp_subctx D1 S2).
 by rewrite valid_cat D2 andbT; apply: (valid_subctx S2).
 Qed.
 
+#[export]
 Program Instance empty_struct i :
   Ast i i [::] empty | 1.
 Next Obligation.
 split; by [|apply: subctx_refl|].
 Qed.
 
+#[export]
 Program Instance
   pts_struct A hs xs1 x (d : A)
            (f : XFind xs1 x) :
@@ -64,7 +65,7 @@ case: f=>[xs2 n /= [H P]]; split; first by rewrite /= H.
 by apply/andP; rewrite /= (onth_size H).
 Qed.
 
-
+#[export]
 Program Instance var_struct hs1 xs h (f : XFind hs1 h) :
   Ast (Context hs1 xs) (Context seq_of xs) [:: Var index_of] h | 1000.
 Next Obligation.

theories/cancelD.v

@@ -15,10 +15,8 @@
     along with this program.  If not, see <http://www.gnu.org/licenses/>.
 *)
 
-From mathcomp
-Require Import ssreflect ssrbool.
-From LemmaOverloading
-Require Import prelude xfind heaps cancel.
+From mathcomp Require Import ssreflect ssrbool.
+From LemmaOverloading Require Import prelude xfind heaps cancel.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.

theories/domains.v

@@ -15,10 +15,8 @@
     along with this program.  If not, see <http://www.gnu.org/licenses/>.
 *)
 
-From mathcomp
-Require Import ssreflect ssrbool ssrfun ssrnat eqtype.
-From LemmaOverloading
-Require Import rels prelude.
+From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype.
+From LemmaOverloading Require Import rels prelude.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -101,6 +99,7 @@ Proof. by case: T y x z=>S [[l b B R A Tr]] ? x y z; apply: (Tr). Qed.
 
 End Laws.
 
+#[export]
 Hint Resolve botP poset_refl : core.
 
 Add Parametric Relation (T : poset) : T (@Poset.leq T)

theories/finmap.v

@@ -15,10 +15,9 @@
     along with this program.  If not, see <http://www.gnu.org/licenses/>.
 *)
 
-From mathcomp
-Require Import ssreflect ssrbool eqtype ssrfun seq path.
-From LemmaOverloading
-Require Import ordtype prelude.
+From HB Require Import structures.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrfun seq path.
+From LemmaOverloading Require Import ordtype prelude.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -717,8 +716,6 @@ case: eqP; first by move/fmapE=>->; apply: ReflectT.
 by move=>H; apply: ReflectF; move/fmapE; move/H.
 Qed.
 
-Canonical Structure fmap_eqMixin := EqMixin feqP.
-Canonical Structure fmap_eqType := EqType (finMap K V) fmap_eqMixin.
-End EqType.
-
+HB.instance Definition _ := hasDecEq.Build (finMap K V) feqP.
 
+End EqType.

theories/heaps.v

@@ -15,12 +15,10 @@
     along with this program.  If not, see <http://www.gnu.org/licenses/>.
 *)
 
-From mathcomp
-Require Import ssreflect ssrfun ssrnat div ssrbool seq.
-From LemmaOverloading
-Require Import prelude finmap ordtype.
-From mathcomp
-Require Import path eqtype.
+From HB Require Import structures.
+From mathcomp Require Import ssreflect ssrfun ssrnat div ssrbool seq.
+From LemmaOverloading Require Import prelude finmap ordtype.
+From mathcomp Require Import path eqtype.
 Require Import Eqdep.
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -43,8 +41,7 @@
 Lemma eq_ptrP : Equality.axiom eq_ptr.
 Proof. by case=>x [y] /=; case: eqP=>[->|*]; constructor=>//; case. Qed.
 
-Definition ptr_eqMixin := EqMixin eq_ptrP.
-Canonical Structure ptr_eqType := EqType ptr ptr_eqMixin.
+HB.instance Definition _ := hasDecEq.Build ptr eq_ptrP.
 
 (* some pointer arithmetic: offsetting from a base *)
 
@@ -89,8 +86,8 @@
 Lemma ltn_ptr_total : forall x y : ptr, [|| ltn_ptr x y, x == y | ltn_ptr y x].
 Proof. by case=>x [y]; rewrite ptrE /=; case: ltngtP. Qed.
 
-Definition ptr_ordMixin := OrdMixin ltn_ptr_irr ltn_ptr_trans ltn_ptr_total.
-Canonical Structure ptr_ordType := OrdType ptr ptr_ordMixin.
+HB.instance Definition _ :=
+  isTotalOrder.Build ptr ltn_ptr_irr ltn_ptr_trans ltn_ptr_total.
 
 (*********)
 (* Heaps *)
@@ -131,14 +128,14 @@
 
 Definition empty := @Def (finmap.nil _ _) is_true_true.
 
 Definition upd h x d := nosimpl
   (if h is Def hs ns then
     if decP (@idP (x != null)) is left pf then
       Def (@upd_nullP _ _ d pf ns)
     else Undef
   else Undef).
 
 Definition dom h : pred ptr := nosimpl
   (if h is Def f _ then mem (supp f) else pred0).
 
 Definition free x h : heap :=
@@ -149,7 +146,7 @@
     if fnd x hs is Some d then d else dyn tt
   else dyn tt).
 
 Definition union2 h1 h2 := nosimpl
   (if (h1, h2) is (Def hs1 ns1, Def hs2 ns2) then
      if disj hs1 hs2 then
         Def (@un_nullP _ _ ns1 ns2)
@@ -302,6 +299,7 @@
 Lemma def0 : def empty.
 Proof. by []. Qed.
 
+#[export]
 Hint Resolve def0 : core.
 
 Lemma defU h x d : def (upd h x d) = (x != null) && (def h).
@@ -636,6 +634,7 @@
 
 Opaque fresh.
 
+#[export]
 Hint Resolve dom_fresh fresh_null : core.
 
 (********)
@@ -747,6 +746,7 @@
 by apply: (subdomQ H2) (subdomQ H1 in1).
 Qed.
 
+#[export]
 Hint Resolve subdom_emp subdomPE : core.
 
 (***********)
@@ -1180,6 +1180,7 @@
 Lemma low_refl h : h =~ h.
 Proof. by rewrite /loweq. Qed.
 
+#[export]
 Hint Resolve low_refl : core.
 
 Lemma low_sym h1 h2 : (h1 =~ h2) = (h2 =~ h1).
@@ -1226,6 +1227,7 @@
 Lemma lowPn A1 A2 (x : ptr) (v1 : A1) (v2 : A2) : x :-> v1 =~ x :-> v2.
 Proof. by apply/loweqP=>y; rewrite !ldomP !domPt. Qed.
 
+#[export]
 Hint Resolve lowPn : core.
 
 Lemma highPn A1 A2 (x1 x2 : ptr) (v1 : A1) (v2 : A2) :

theories/hprop.v

@@ -15,10 +15,8 @@
     along with this program.  If not, see <http://www.gnu.org/licenses/>.
 *)
 
-From mathcomp
-Require Import ssreflect ssrfun.
-From LemmaOverloading
-Require Import rels heaps.
+From mathcomp Require Import ssreflect ssrfun.
+From LemmaOverloading Require Import rels heaps.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.

theories/indom.v

@@ -15,10 +15,8 @@
     along with this program.  If not, see <http://www.gnu.org/licenses/>.
 *)
 
-From mathcomp
-Require Import ssreflect ssrbool ssrnat eqtype.
-From LemmaOverloading
-Require Import heaps.
+From mathcomp Require Import ssreflect ssrbool ssrnat eqtype.
+From LemmaOverloading Require Import heaps.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.