From c63c5cdca2459f3db00e865f64c093e9f3bd56a7 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Tue, 12 Nov 2024 15:31:24 +0100 Subject: [PATCH 1/4] Adapt to MC2 --- .github/workflows/docker-action.yml | 24 +++++-- README.md | 9 +-- coq-lemma-overloading.opam | 5 +- meta.yml | 47 +++++++++---- theories/auto.v | 6 +- theories/cancel.v | 6 +- theories/cancel2.v | 6 +- theories/cancelCTC.v | 6 +- theories/cancelD.v | 6 +- theories/domains.v | 6 +- theories/finmap.v | 13 ++-- theories/heaps.v | 17 ++--- theories/hprop.v | 6 +- theories/indom.v | 6 +- theories/indomCTC.v | 6 +- theories/llistR.v | 6 +- theories/noalias.v | 6 +- theories/noaliasBT.v | 6 +- theories/noaliasCTC.v | 6 +- theories/ordtype.v | 103 ++++++++-------------------- theories/perms.v | 6 +- theories/prefix.v | 3 +- theories/prelude.v | 3 +- theories/rels.v | 38 +++++----- theories/stlog.v | 6 +- theories/stlogCTC.v | 6 +- theories/stlogR.v | 6 +- theories/stmod.v | 10 ++- theories/stsep.v | 6 +- theories/terms.v | 6 +- theories/xfind.v | 6 +- theories/xfindCTC.v | 6 +- 32 files changed, 166 insertions(+), 232 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 0503060..69e1b0f 100644 --- a/.github/workflows/docker-action.yml +++ b/.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 diff --git a/README.md b/README.md index 264103c..39bec7b 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/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) diff --git a/coq-lemma-overloading.opam b/coq-lemma-overloading.opam index aee03f9..71aeb56 100644 --- a/coq-lemma-overloading.opam +++ b/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: [ diff --git a/meta.yml b/meta.yml index 7e78b56..5185697 100644 --- a/meta.yml +++ b/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 diff --git a/theories/auto.v b/theories/auto.v index c72a168..cfe36cc 100644 --- a/theories/auto.v +++ b/theories/auto.v @@ -15,10 +15,8 @@ along with this program. If not, see . *) -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. diff --git a/theories/cancel.v b/theories/cancel.v index 43a98f8..b0e1762 100644 --- a/theories/cancel.v +++ b/theories/cancel.v @@ -15,10 +15,8 @@ along with this program. If not, see . *) -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. diff --git a/theories/cancel2.v b/theories/cancel2.v index 07f095d..f106424 100644 --- a/theories/cancel2.v +++ b/theories/cancel2.v @@ -15,10 +15,8 @@ along with this program. If not, see . *) -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. diff --git a/theories/cancelCTC.v b/theories/cancelCTC.v index 0e22bbb..a2855e1 100644 --- a/theories/cancelCTC.v +++ b/theories/cancelCTC.v @@ -15,10 +15,8 @@ along with this program. If not, see . *) -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. diff --git a/theories/cancelD.v b/theories/cancelD.v index 8d87778..46cda50 100644 --- a/theories/cancelD.v +++ b/theories/cancelD.v @@ -15,10 +15,8 @@ along with this program. If not, see . *) -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. diff --git a/theories/domains.v b/theories/domains.v index ee514c1..7154c51 100644 --- a/theories/domains.v +++ b/theories/domains.v @@ -15,10 +15,8 @@ along with this program. If not, see . *) -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. diff --git a/theories/finmap.v b/theories/finmap.v index 368dffc..1381313 100644 --- a/theories/finmap.v +++ b/theories/finmap.v @@ -15,10 +15,9 @@ along with this program. If not, see . *) -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. diff --git a/theories/heaps.v b/theories/heaps.v index 26d6449..e94f3cc 100644 --- a/theories/heaps.v +++ b/theories/heaps.v @@ -15,12 +15,10 @@ along with this program. If not, see . *) -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 @@ Definition eq_ptr (x y : ptr) := 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 @@ Proof. by case=>x [y][z]; apply: ltn_trans. Qed. 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 *) diff --git a/theories/hprop.v b/theories/hprop.v index f85b3fc..5e56dbd 100644 --- a/theories/hprop.v +++ b/theories/hprop.v @@ -15,10 +15,8 @@ along with this program. If not, see . *) -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. diff --git a/theories/indom.v b/theories/indom.v index 32c84ff..ea5ed72 100644 --- a/theories/indom.v +++ b/theories/indom.v @@ -15,10 +15,8 @@ along with this program. If not, see . *) -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. diff --git a/theories/indomCTC.v b/theories/indomCTC.v index 46cc3c9..afe1789 100644 --- a/theories/indomCTC.v +++ b/theories/indomCTC.v @@ -15,10 +15,8 @@ along with this program. If not, see . *) -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. diff --git a/theories/llistR.v b/theories/llistR.v index 5d7dd09..e2b37c9 100644 --- a/theories/llistR.v +++ b/theories/llistR.v @@ -15,10 +15,8 @@ along with this program. If not, see . *) -From mathcomp -Require Import ssreflect ssrbool eqtype seq ssrfun. -From LemmaOverloading -Require Import heaps rels hprop stmod stsep stlogR. +From mathcomp Require Import ssreflect ssrbool eqtype seq ssrfun. +From LemmaOverloading Require Import heaps rels hprop stmod stsep stlogR. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/noalias.v b/theories/noalias.v index 69e4439..bbbaf69 100644 --- a/theories/noalias.v +++ b/theories/noalias.v @@ -15,10 +15,8 @@ along with this program. If not, see . *) -From mathcomp -Require Import ssreflect ssrbool seq eqtype. -From LemmaOverloading -Require Import heaps. +From mathcomp Require Import ssreflect ssrbool seq eqtype. +From LemmaOverloading Require Import heaps. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/noaliasBT.v b/theories/noaliasBT.v index 57dd444..3a718d9 100644 --- a/theories/noaliasBT.v +++ b/theories/noaliasBT.v @@ -15,10 +15,8 @@ along with this program. If not, see . *) -From mathcomp -Require Import ssreflect ssrbool seq eqtype. -From LemmaOverloading -Require Import heaps noalias. +From mathcomp Require Import ssreflect ssrbool seq eqtype. +From LemmaOverloading Require Import heaps noalias. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/noaliasCTC.v b/theories/noaliasCTC.v index 45002af..3156ff4 100644 --- a/theories/noaliasCTC.v +++ b/theories/noaliasCTC.v @@ -15,10 +15,8 @@ along with this program. If not, see . *) -From mathcomp -Require Import ssreflect ssrbool seq eqtype. -From LemmaOverloading -Require Import heaps. +From mathcomp Require Import ssreflect ssrbool seq eqtype. +From LemmaOverloading Require Import heaps. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/ordtype.v b/theories/ordtype.v index b42055c..4cfc005 100644 --- a/theories/ordtype.v +++ b/theories/ordtype.v @@ -15,81 +15,31 @@ along with this program. If not, see . *) -From mathcomp -Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq fintype. +From HB Require Import structures. +From mathcomp Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq fintype. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Module Ordered. +HB.mixin Record isTotalOrder T of Equality T := { + ord : rel T; + irr : irreflexive ord; + trans : transitive ord; + total : forall x y, [|| ord x y, x == y | ord y x]; +}. -Section RawMixin. +#[short(type="ordType")] +HB.structure Definition Order := { T of Equality T & isTotalOrder T }. -Structure mixin_of (T : eqType) := - Mixin {ordering : rel T; - _ : irreflexive ordering; - _ : transitive ordering; - _ : forall x y, [|| ordering x y, x == y | ordering y x]}. +Arguments ord {s}. +Arguments irr {s}. +Arguments trans {s} [y x z]. -End RawMixin. - -(* the class takes a naked type T and returns all the *) -(* relatex mixins; the inherited ones and the added ones *) -Section ClassDef. - -Record class_of (T : Type) := Class { - base : Equality.class_of T; - mixin : mixin_of (EqType T base)}. - -Local Coercion base : class_of >-> Equality.class_of. - -Structure type : Type := Pack {sort : Type; _ : class_of sort; _ : Type}. -Local Coercion sort : type >-> Sortclass. - -Variables (T : Type) (cT : type). -Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c. -Definition clone c of phant_id class c := @Pack T c T. - -(* produce an ordered type out of the inherited mixins *) -(* equalize m0 and m by means of a phantom; will be exploited *) -(* further down in the definition of OrdType *) -Definition pack b (m0 : mixin_of (EqType T b)) := - fun m & phant_id m0 m => Pack (@Class T b m) T. - -Definition eqType := Eval hnf in EqType cT class. - -End ClassDef. - -Module Exports. -Coercion sort : type >-> Sortclass. -Coercion eqType : type >-> Equality.type. -Canonical Structure eqType. -Notation ordType := Ordered.type. -Notation OrdMixin := Mixin. -Notation OrdType T m := (@pack T _ m _ id). -Definition ord T : rel (sort T) := (ordering (mixin (class T))). -Notation "[ 'ordType' 'of' T 'for' cT ]" := (@clone T cT _ id) - (at level 0, format "[ 'ordType' 'of' T 'for' cT ]") : form_scope. -Notation "[ 'ordType' 'of' T ]" := (@clone T _ _ id) - (at level 0, format "[ 'ordType' 'of' T ]") : form_scope. -End Exports. -End Ordered. -Export Ordered.Exports. - -Prenex Implicits ord. +(* Prenex Implicits ord. *) Section Lemmas. Variable T : ordType. -Lemma irr : irreflexive (@ord T). -Proof. by case: T=>s [b [m]]. Qed. - -Lemma trans : transitive (@ord T). -Proof. by case: T=>s [b [m]]. Qed. - -Lemma total (x y : T) : [|| ord x y, x == y | ord y x]. -Proof. by case: T x y=>s [b [m]]. Qed. - Lemma nsym (x y : T) : ord x y -> ord y x -> False. Proof. by move=>E1 E2; move: (trans E1 E2); rewrite irr. Qed. @@ -120,9 +70,8 @@ Lemma irr_ltn_nat : irreflexive ltn. Proof. by move=>x; rewrite /= ltnn. Qed. Lemma trans_ltn_nat : transitive ltn. Proof. by apply: ltn_trans. Qed. Lemma total_ltn_nat : forall x y, [|| x < y, x == y | y < x]. Proof. by move=>*; case: ltngtP. Qed. - -Definition nat_ordMixin := OrdMixin irr_ltn_nat trans_ltn_nat total_ltn_nat. -Canonical Structure nat_ordType := OrdType nat nat_ordMixin. +HB.instance Definition _ := + isTotalOrder.Build nat irr_ltn_nat trans_ltn_nat total_ltn_nat. End NatOrd. Section ProdOrd. @@ -153,11 +102,16 @@ rewrite (eq_sym y1) -pair_eqE /= H1 /=. by move: (total x1 y1); rewrite H1. Qed. -Definition prod_ordMixin := OrdMixin irr_lex trans_lex total_lex. -Canonical Structure prod_ordType := Eval hnf in OrdType (K * T) prod_ordMixin. +HB.instance Definition _ := + isTotalOrder.Build (K * T)%type irr_lex trans_lex total_lex. End ProdOrd. Section FinTypeOrd. + +Definition fin_order (T : Type) := T. + +HB.instance Definition _ (T : eqType) := Equality.copy (fin_order T) T. + Variable T : finType. Definition ordf : rel T := @@ -176,12 +130,9 @@ have [H1 H2]: x \in enum T /\ y \in enum T by rewrite !mem_enum. by rewrite -(nth_index x H1) -(nth_index x H2) H eq_refl. Qed. -Definition fin_ordMixin := OrdMixin irr_ordf trans_ordf total_ordf. -End FinTypeOrd. +HB.instance Definition _ := + isTotalOrder.Build (fin_order T) irr_ordf trans_ordf total_ordf. -(* notation to let us write I_n instead of (ordinal_finType n) *) -Notation "[ 'fin_ordMixin' 'of' T ]" := - (fin_ordMixin _ : Ordered.mixin_of [eqType of T]) (at level 0). +End FinTypeOrd. -Definition ordinal_ordMixin n := [fin_ordMixin of 'I_n]. -Canonical Structure ordinal_ordType n := OrdType 'I_n (ordinal_ordMixin n). +HB.instance Definition _ (n : nat) := Order.copy 'I_n (fin_order 'I_n). diff --git a/theories/perms.v b/theories/perms.v index 9d3d259..403e04e 100644 --- a/theories/perms.v +++ b/theories/perms.v @@ -15,10 +15,8 @@ along with this program. If not, see . *) -From mathcomp -Require Import ssreflect ssrfun seq. -From LemmaOverloading -Require Import rels. +From mathcomp Require Import ssreflect ssrfun seq. +From LemmaOverloading Require Import rels. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/prefix.v b/theories/prefix.v index 95c31d6..679592b 100644 --- a/theories/prefix.v +++ b/theories/prefix.v @@ -15,8 +15,7 @@ along with this program. If not, see . *) -From mathcomp -Require Import ssreflect ssrfun ssrbool ssrnat seq. +From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/prelude.v b/theories/prelude.v index dacd130..aee3f3d 100644 --- a/theories/prelude.v +++ b/theories/prelude.v @@ -15,8 +15,7 @@ along with this program. If not, see . *) -From mathcomp -Require Import ssreflect ssrbool eqtype ssrfun seq. +From mathcomp Require Import ssreflect ssrbool eqtype ssrfun seq. Require Import Eqdep ClassicalFacts. Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/rels.v b/theories/rels.v index 2eb4b90..8161616 100644 --- a/theories/rels.v +++ b/theories/rels.v @@ -15,8 +15,7 @@ along with this program. If not, see . *) -From mathcomp -Require Import ssreflect ssrfun ssrbool seq. +From mathcomp Require Import ssreflect ssrfun ssrbool seq. Require Import Setoid. Set Implicit Arguments. Unset Strict Implicit. @@ -124,16 +123,17 @@ Notation "r1 *p r2" := (PredI r1 r2) (at level 45, right associativity) : rel_scope. Notation "[ 'Pred' : T | E ]" := (SimplPred (fun _ : T => E)) - (at level 0, format "[ 'Pred' : T | E ]") : fun_scope. + (at level 0, format "[ 'Pred' : T | E ]") : function_scope. Notation "[ 'Pred' x | E ]" := (SimplPred (fun x => E)) - (at level 0, x ident, format "[ 'Pred' x | E ]") : fun_scope. + (at level 0, x ident, format "[ 'Pred' x | E ]") : function_scope. Notation "[ 'Pred' x : T | E ]" := (SimplPred (fun x : T => E)) - (at level 0, x ident, only parsing) : fun_scope. + (at level 0, x ident, only parsing) : function_scope. Notation "[ 'Pred' x y | E ]" := (SimplPred (fun t => let: (x, y) := t in E)) - (at level 0, x ident, y ident, format "[ 'Pred' x y | E ]") : fun_scope. + (at level 0, x ident, y ident, format "[ 'Pred' x y | E ]") : + function_scope. Notation "[ 'Pred' x y : T | E ]" := (SimplPred (fun t : (T*T) => let: (x, y) := t in E)) - (at level 0, x ident, y ident, only parsing) : fun_scope. + (at level 0, x ident, y ident, only parsing) : function_scope. Definition repack_Pred T pT := let: PropPredType _ a mP := pT return {type of @PropPredType T for pT} -> _ in @@ -207,35 +207,35 @@ Notation "A <=p B" := (SubMem (Mem A) (Mem B)) (* Some notation for turning PredTypes into Pred or Simple Pred *) Notation "[ 'Mem' A ]" := (Pred_of_Simpl (Pred_of_Mem_Pred (Mem A))) - (at level 0, only parsing) : fun_scope. + (at level 0, only parsing) : function_scope. Notation "[ 'PredI' A & B ]" := (PredI [Mem A] [Mem B]) - (at level 0, format "[ 'PredI' A & B ]") : fun_scope. + (at level 0, format "[ 'PredI' A & B ]") : function_scope. Notation "[ 'PredU' A & B ]" := (PredU [Mem A] [Mem B]) - (at level 0, format "[ 'PredU' A & B ]") : fun_scope. + (at level 0, format "[ 'PredU' A & B ]") : function_scope. Notation "[ 'PredD' A & B ]" := (PredD [Mem A] [Mem B]) - (at level 0, format "[ 'PredD' A & B ]") : fun_scope. + (at level 0, format "[ 'PredD' A & B ]") : function_scope. Notation "[ 'PredC' A ]" := (PredC [Mem A]) - (at level 0, format "[ 'PredC' A ]") : fun_scope. + (at level 0, format "[ 'PredC' A ]") : function_scope. Notation "[ 'Preim' f 'of' A ]" := (Preim f [Mem A]) - (at level 0, format "[ 'Preim' f 'of' A ]") : fun_scope. + (at level 0, format "[ 'Preim' f 'of' A ]") : function_scope. Notation "[ 'Pred' x \In A ]" := [Pred x | x \In A] - (at level 0, x ident, format "[ 'Pred' x \In A ]") : fun_scope. + (at level 0, x ident, format "[ 'Pred' x \In A ]") : function_scope. Notation "[ 'Pred' x \In A | E ]" := [Pred x | (x \In A) /\ E] - (at level 0, x ident, format "[ 'Pred' x \In A | E ]") : fun_scope. + (at level 0, x ident, format "[ 'Pred' x \In A | E ]") : function_scope. Notation "[ 'Pred' x y \In A & B | E ]" := [Pred x y | (x \In A) /\ (y \In B) /\ E] (at level 0, x ident, y ident, - format "[ 'Pred' x y \In A & B | E ]") : fun_scope. + format "[ 'Pred' x y \In A & B | E ]") : function_scope. Notation "[ 'Pred' x y \In A & B ]" := [Pred x y | (x \In A) /\ (y \In B)] (at level 0, x ident, y ident, - format "[ 'Pred' x y \In A & B ]") : fun_scope. + format "[ 'Pred' x y \In A & B ]") : function_scope. Notation "[ 'Pred' x y \In A | E ]" := [Pred x y \In A & A | E] (at level 0, x ident, y ident, - format "[ 'Pred' x y \In A | E ]") : fun_scope. + format "[ 'Pred' x y \In A | E ]") : function_scope. Notation "[ 'Pred' x y \In A ]" := [Pred x y \In A & A] (at level 0, x ident, y ident, - format "[ 'Pred' x y \In A ]") : fun_scope. + format "[ 'Pred' x y \In A ]") : function_scope. Section Simplifications. Variables (T : Type) (pT : PredType T). diff --git a/theories/stlog.v b/theories/stlog.v index dbae01a..e4841d2 100644 --- a/theories/stlog.v +++ b/theories/stlog.v @@ -15,10 +15,8 @@ along with this program. If not, see . *) -From mathcomp -Require Import ssreflect ssrbool seq ssrfun. -From LemmaOverloading -Require Import heaps rels hprop stmod stsep. +From mathcomp Require Import ssreflect ssrbool seq ssrfun. +From LemmaOverloading Require Import heaps rels hprop stmod stsep. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/stlogCTC.v b/theories/stlogCTC.v index 471172b..a65ab9c 100644 --- a/theories/stlogCTC.v +++ b/theories/stlogCTC.v @@ -15,10 +15,8 @@ along with this program. If not, see . *) -From mathcomp -Require Import ssreflect ssrbool ssrfun. -From LemmaOverloading -Require Import heaps stmod stsep stlog. +From mathcomp Require Import ssreflect ssrbool ssrfun. +From LemmaOverloading Require Import heaps stmod stsep stlog. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/stlogR.v b/theories/stlogR.v index 564cfe3..cda0ff2 100644 --- a/theories/stlogR.v +++ b/theories/stlogR.v @@ -15,10 +15,8 @@ along with this program. If not, see . *) -From mathcomp -Require Import ssreflect ssrbool ssrfun. -From LemmaOverloading -Require Import heaps rels stmod stsep stlog. +From mathcomp Require Import ssreflect ssrbool ssrfun. +From LemmaOverloading Require Import heaps rels stmod stsep stlog. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/stmod.v b/theories/stmod.v index 9379ded..c4616eb 100644 --- a/theories/stmod.v +++ b/theories/stmod.v @@ -15,10 +15,9 @@ along with this program. If not, see . *) -From mathcomp -Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq. -From LemmaOverloading -Require Import prelude heaps rels hprop domains. +From HB Require Import structures. +From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq. +From LemmaOverloading Require Import prelude heaps rels hprop domains. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -38,8 +37,7 @@ move=>[x][y]//=; case: eqP=>[->|*];constructor=>//. by move=>[*]. Qed. -Canonical Structure exn_eqMixin := EqMixin eqexnP. -Canonical Structure exn_eqType := EqType exn exn_eqMixin. +HB.instance Definition _ := hasDecEq.Build exn eqexnP. (* Answer type *) Inductive ans (A : Type) : Type := Val of A | Exn of exn. diff --git a/theories/stsep.v b/theories/stsep.v index 2d6f9b9..9900b12 100644 --- a/theories/stsep.v +++ b/theories/stsep.v @@ -15,10 +15,8 @@ along with this program. If not, see . *) -From mathcomp -Require Import ssreflect ssrbool ssrnat ssrfun seq eqtype. -From LemmaOverloading -Require Import heaps rels hprop stmod. +From mathcomp Require Import ssreflect ssrbool ssrnat ssrfun seq eqtype. +From LemmaOverloading Require Import heaps rels hprop stmod. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/terms.v b/theories/terms.v index 7621636..27b1a32 100644 --- a/theories/terms.v +++ b/theories/terms.v @@ -15,10 +15,8 @@ along with this program. If not, see . *) -From mathcomp -Require Import ssreflect ssrbool ssrnat ssrfun eqtype seq. -From LemmaOverloading -Require Import prelude prefix perms heaps. +From mathcomp Require Import ssreflect ssrbool ssrnat ssrfun eqtype seq. +From LemmaOverloading Require Import prelude prefix perms heaps. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/xfind.v b/theories/xfind.v index 102e319..4cbac0c 100644 --- a/theories/xfind.v +++ b/theories/xfind.v @@ -15,10 +15,8 @@ along with this program. If not, see . *) -From mathcomp -Require Import ssreflect ssrnat seq. -From LemmaOverloading -Require Import prefix. +From mathcomp Require Import ssreflect ssrnat seq. +From LemmaOverloading Require Import prefix. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/xfindCTC.v b/theories/xfindCTC.v index fea2c0c..3a0a657 100644 --- a/theories/xfindCTC.v +++ b/theories/xfindCTC.v @@ -15,10 +15,8 @@ along with this program. If not, see . *) -From mathcomp -Require Import ssreflect ssrnat seq. -From LemmaOverloading -Require Import prefix. +From mathcomp Require Import ssreflect ssrnat seq. +From LemmaOverloading Require Import prefix. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. From 84fd7cef767b1c82b6b09e60abb5f10cf07543f6 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Wed, 13 Nov 2024 11:29:31 +0100 Subject: [PATCH 2/4] Add the #[export] attribute --- theories/cancelCTC.v | 5 ++++- theories/domains.v | 1 + theories/heaps.v | 5 +++++ theories/indomCTC.v | 3 +++ theories/noaliasCTC.v | 9 +++++++++ theories/perms.v | 1 + theories/prefix.v | 1 + theories/prelude.v | 2 ++ theories/rels.v | 2 ++ theories/stlog.v | 2 ++ theories/stlogCTC.v | 6 ++++++ theories/stmod.v | 1 + theories/stsep.v | 1 + theories/xfindCTC.v | 3 +++ 14 files changed, 41 insertions(+), 1 deletion(-) diff --git a/theories/cancelCTC.v b/theories/cancelCTC.v index a2855e1..f868587 100644 --- a/theories/cancelCTC.v +++ b/theories/cancelCTC.v @@ -34,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. @@ -44,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) : @@ -62,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. diff --git a/theories/domains.v b/theories/domains.v index 7154c51..3a23c0c 100644 --- a/theories/domains.v +++ b/theories/domains.v @@ -99,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) diff --git a/theories/heaps.v b/theories/heaps.v index e94f3cc..002f307 100644 --- a/theories/heaps.v +++ b/theories/heaps.v @@ -299,6 +299,7 @@ Qed. 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). @@ -633,6 +634,7 @@ Proof. by rewrite -lt0n addn1. Qed. Opaque fresh. +#[export] Hint Resolve dom_fresh fresh_null : core. (********) @@ -744,6 +746,7 @@ apply/subdomP=>[//||x in1]; first by apply negbT. by apply: (subdomQ H2) (subdomQ H1 in1). Qed. +#[export] Hint Resolve subdom_emp subdomPE : core. (***********) @@ -1177,6 +1180,7 @@ Notation "h1 =~ h2" := (loweq h1 h2) (at level 80). 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). @@ -1223,6 +1227,7 @@ Qed. 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) : diff --git a/theories/indomCTC.v b/theories/indomCTC.v index afe1789..b49f4aa 100644 --- a/theories/indomCTC.v +++ b/theories/indomCTC.v @@ -27,12 +27,14 @@ Class Indom (x : ptr) (h : heap) := Obligation Tactic := idtac. +#[export] Program Instance found : forall A x (v : A), Indom x (x:->v). Next Obligation. move=> A x v; rewrite defPt => xnull. by rewrite domPt !inE eq_refl xnull. Qed. +#[export] Program Instance found_left : forall x h1 h2 (xh1 : Indom x h1), Indom x (h1:+h2). Next Obligation. @@ -40,6 +42,7 @@ move=> x h1 h2 xh1 defh12; rewrite domUn !inE defh12. case: xh1 => xh1; by rewrite (xh1 (defUnl defh12)). Qed. +#[export] Program Instance found_right : forall x h1 h2 (xh2 : Indom x h2), Indom x (h1:+h2). Next Obligation. diff --git a/theories/noaliasCTC.v b/theories/noaliasCTC.v index 3156ff4..8e9f2c2 100644 --- a/theories/noaliasCTC.v +++ b/theories/noaliasCTC.v @@ -33,6 +33,7 @@ Class Scan (h : heap) := { seq_of : seq ptr ; scan : scan_axiom h seq_of }. +#[export] Program Instance scan_union h1 h2 (f1 : Scan h1) (f2 : Scan h2) : Scan (h1:+h2) | 2 := {| seq_of := @seq_of _ f1 ++ @seq_of _ f2 |}. Next Obligation. @@ -46,12 +47,14 @@ apply/allP=>x; move/H2=>H3; apply: (introN idP); move/H1=>H4. by case: defUn D=>// _ _; move/(_ _ H4); rewrite H3. Qed. +#[export] Program Instance scan_ptr A x (v : A) : Scan (x:->v) | 1 := {| seq_of := [:: x] |}. Next Obligation. rewrite /scan_axiom /= defPt => D; split=>//. by move=>y; rewrite inE; move/eqP=>->; rewrite domPt inE /= eq_refl D. Qed. +#[export] Program Instance scan_default h : Scan h | 10 := {| seq_of := [::] |}. Next Obligation. by move=>_; split. @@ -73,11 +76,13 @@ Abort. Class Search (x : ptr) (s : seq ptr) := { search : x \in s }. +#[export] Program Instance search_found x s : Search x (x :: s). Next Obligation. by rewrite inE eq_refl. Qed. +#[export] Program Instance search_recurse x y s (f : Search x s) : Search x (y :: s) | 5. Next Obligation. by case: f; rewrite inE=>->; rewrite orbT. @@ -95,18 +100,21 @@ Definition search2_axiom (x y : ptr) (s : seq ptr) := Class Search2 x y s := { search2 : search2_axiom x y s}. +#[export] Program Instance search2_foundx x y s (s1 : Search y s) : Search2 x y (x :: s). Next Obligation. case: s1=>s2; rewrite /search2_axiom !inE eq_refl. by rewrite s2 orbT; split=>//; case/andP=>H2 _; case: eqP s2 H2=>// -> ->. Qed. +#[export] Program Instance search2_foundy x y s (f : Search x s) : Search2 x y (y :: s). Next Obligation. case: f=>H1; rewrite /search2_axiom !inE eq_refl. by rewrite H1 orbT; split=>//; case/andP=>H2 _; case: eqP H1 H2=>// -> ->. Qed. +#[export] Program Instance search2_foundz x y z s (f : Search2 x y s) : Search2 x y (z :: s) | 1. Next Obligation. case: f=>[[H1 H2 H3]]. @@ -134,6 +142,7 @@ Qed. Arguments noaliasR [h x y sc s2]. +#[export] Hint Extern 20 (Search2 _ _ _) => progress simpl : typeclass_instances. Example ex_noalias x1 x2 : def (x2 :-> 1 :+ x1 :-> 2) -> x1 != x2. diff --git a/theories/perms.v b/theories/perms.v index 403e04e..b0945b2 100644 --- a/theories/perms.v +++ b/theories/perms.v @@ -256,5 +256,6 @@ Proof. by move=>*; rewrite !catA perm_cat2r. Qed. End Permutations. +#[export] Hint Resolve perm_refl perm_catC perm_cons_catCA perm_cons_catAC perm_catAC perm_catCA : core. diff --git a/theories/prefix.v b/theories/prefix.v index 679592b..c334b16 100644 --- a/theories/prefix.v +++ b/theories/prefix.v @@ -80,4 +80,5 @@ Qed. End Prefix. +#[export] Hint Resolve prefix_refl : core. diff --git a/theories/prelude.v b/theories/prelude.v index aee3f3d..28e2123 100644 --- a/theories/prelude.v +++ b/theories/prelude.v @@ -160,6 +160,7 @@ Proof. by move=>pf; rewrite eqc. Qed. End Coercions. +#[export] Hint Resolve jmeq_refl : core. Arguments jmeq T [A B] x y. Notation "a =jm b" := (jmeq id a b) (at level 50). @@ -207,6 +208,7 @@ Proof. by move=>pf; rewrite eqc2. Qed. End Coercions2. +#[export] Hint Resolve refl_jmeq2 : core. Arguments jmeq2 T [A1 A2 B1 B2] x y. diff --git a/theories/rels.v b/theories/rels.v index 8161616..ff9e785 100644 --- a/theories/rels.v +++ b/theories/rels.v @@ -289,6 +289,7 @@ Definition EqPredType_trans r2 r1 r3 := @EqPredType_trans' r1 r2 r3. Definition SubPredType_trans r2 r1 r3 := @SubPredType_trans' r1 r2 r3. End RelProperties. +#[export] Hint Resolve EqPredType_refl SubPredType_refl : core. (* Declaration of relations *) @@ -458,6 +459,7 @@ Proof. by move=>H x [H1 H2]; split; [|apply: H]. Qed. End SubMemLaws. +#[export] Hint Resolve subp_refl : core. Section ListMembership. diff --git a/theories/stlog.v b/theories/stlog.v index e4841d2..fc1d0aa 100644 --- a/theories/stlog.v +++ b/theories/stlog.v @@ -398,12 +398,14 @@ Prenex Implicits swp opn. Lemma blah (A : Type) (p : ptr) (l : A) : def (p :-> l) -> (p :-> l) \In p :--> l. Proof. by move=>H; apply/swp. Qed. +#[export] Hint Immediate blah : core. Lemma blah2 (A : Type) (v1 v2 : A) q : def (q :-> v1) -> v1 = v2 -> q :-> v1 \In q :--> v2. Proof. by move=>D E; apply/swp; rewrite E. Qed. +#[export] Hint Immediate blah2 : core. Ltac hauto := (do ?econstructor=>//; diff --git a/theories/stlogCTC.v b/theories/stlogCTC.v index a65ab9c..701b0e5 100644 --- a/theories/stlogCTC.v +++ b/theories/stlogCTC.v @@ -29,11 +29,13 @@ Arguments update1 [h1 h2 k1 k2]. Arguments update2 [h1 h2 k1 k2]. Arguments rest [h1 h2 k1 k2]. +#[export] Program Instance found_struct k1 k2 : Update k1 k2 k1 k2 | 1 := {| rest := empty |}. Next Obligation. by rewrite unh0. Qed. Next Obligation. by rewrite unh0. Qed. +#[export] Program Instance left_struct l h1 h2 k1 k2 (f : Update h1 h2 k1 k2) : Update (l :+ h1) (l :+ h2) k1 k2 | 2 := {| rest := (l :+ rest f) |}. @@ -46,6 +48,7 @@ have H : h2 = k2 :+ (rest f) by eapply (update2 f). by rewrite -unCA -H. Qed. +#[export] Program Instance right_struct l h1 h2 k1 k2 (f : Update h1 h2 k1 k2) : Update (h1 :+ l) (h2 :+ l) k1 k2 | 2 := {| rest := (rest f :+ l) |}. @@ -95,15 +98,18 @@ End EvalDeallocR. Class Find1 (h k : heap) := { rest1 : heap; heq1 : h = k :+ rest1}. +#[export] Program Instance ffound_struct1 k : Find1 k k | 1 := {| rest1 := empty|}. Next Obligation. by rewrite unh0. Qed. +#[export] Program Instance fleft_struct1 l r k (f : Find1 l k) : Find1 (l :+ r) k | 2 := {| rest1 := rest1 :+ r |}. Next Obligation. by rewrite unA -heq1. Qed. +#[export] Program Instance fright_struct1 l r k (f : Find1 r k) : Find1 (l :+ r) k | 2 := {| rest1 := l :+ rest1 |}. diff --git a/theories/stmod.v b/theories/stmod.v index c4616eb..a24e477 100644 --- a/theories/stmod.v +++ b/theories/stmod.v @@ -406,6 +406,7 @@ Definition conseq A (s1 s2 : spec A) := Lemma conseq_refl (A : Type) (s : spec A) : conseq s s. Proof. by []. Qed. +#[export] Hint Resolve conseq_refl : core. Section Consequence. diff --git a/theories/stsep.v b/theories/stsep.v index 9900b12..500b981 100644 --- a/theories/stsep.v +++ b/theories/stsep.v @@ -152,6 +152,7 @@ Local Notation conseq1 := Lemma conseq_refl A (s : spec A) : conseq1 A s s. Proof. by case: s=>s1 s2 i H; apply: frame0. Qed. +#[export] Hint Resolve conseq_refl : core. Section SepConseq. diff --git a/theories/xfindCTC.v b/theories/xfindCTC.v index 3a0a657..f2d0c33 100644 --- a/theories/xfindCTC.v +++ b/theories/xfindCTC.v @@ -34,15 +34,18 @@ Class XFind A (s : seq A) (e : A) := { Arguments XFind [A]. +#[export] Program Instance found_struct A (x:A) t : XFind (x :: t) x := {| seq_of := (x :: t); index_of := 0|}. Next Obligation. by split; [|apply: prefix_refl]. Qed. +#[export] Program Instance recurse_struct A (y:A) t e (f : XFind t e) : XFind (y :: t) e | 2 := {| seq_of := (y :: seq_of); index_of := index_of.+1|}. Next Obligation. by case:f=>r i /= [H1 H2]; split; [|apply/prefix_cons]. Qed. +#[export] Program Instance extend_struct A (x:A) : XFind [::] x := {| seq_of := [:: x]; index_of := 0|}. Next Obligation. by []. Qed. From 1fc1c8806a95bca640437ba2a8f4ee7786d84373 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Wed, 13 Nov 2024 14:44:46 +0100 Subject: [PATCH 3/4] Compatible with coq-master --- theories/prelude.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/prelude.v b/theories/prelude.v index 28e2123..147a041 100644 --- a/theories/prelude.v +++ b/theories/prelude.v @@ -15,8 +15,8 @@ along with this program. If not, see . *) -From mathcomp Require Import ssreflect ssrbool eqtype ssrfun seq. Require Import Eqdep ClassicalFacts. +From mathcomp Require Import ssreflect ssrbool eqtype ssrfun seq. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -71,7 +71,7 @@ Proof. by []. Qed. (* rewrite rule for propositional symmetry *) Lemma sym A (x y : A) : x = y <-> y = x. -Proof. by []. Qed. +Proof. by split. Qed. (* selecting a list element *) (* should really be in seq.v *) From 5e1d1235b077224a43bd34fce61b67252b9141ea Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Wed, 13 Nov 2024 15:22:15 +0100 Subject: [PATCH 4/4] Clean up some import lists --- theories/heaps.v | 6 +++--- theories/prelude.v | 4 ++-- theories/rels.v | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/theories/heaps.v b/theories/heaps.v index 002f307..8304c0a 100644 --- a/theories/heaps.v +++ b/theories/heaps.v @@ -15,11 +15,11 @@ along with this program. If not, see . *) +From Coq Require Import Eqdep. From HB Require Import structures. -From mathcomp Require Import ssreflect ssrfun ssrnat div ssrbool seq. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div. From LemmaOverloading Require Import prelude finmap ordtype. -From mathcomp Require Import path eqtype. -Require Import Eqdep. +From mathcomp Require Import path. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/prelude.v b/theories/prelude.v index 147a041..80bfd32 100644 --- a/theories/prelude.v +++ b/theories/prelude.v @@ -15,8 +15,8 @@ along with this program. If not, see . *) -Require Import Eqdep ClassicalFacts. -From mathcomp Require Import ssreflect ssrbool eqtype ssrfun seq. +From Coq Require Import Eqdep ClassicalFacts. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype seq. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/theories/rels.v b/theories/rels.v index ff9e785..5d2a091 100644 --- a/theories/rels.v +++ b/theories/rels.v @@ -15,8 +15,8 @@ along with this program. If not, see . *) +From Coq Require Import Setoid. From mathcomp Require Import ssreflect ssrfun ssrbool seq. -Require Import Setoid. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive.