Updating to rocq9.2/mathcomp2.6

.github/workflows/docker-action.yml

@@ -18,8 +18,7 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0'
-          - 'mathcomp/mathcomp:2.5.0-rocq-prover-9.1'
+          - 'mathcomp/mathcomp:2.6.0-rocq-prover-9.2'
           - 'mathcomp/mathcomp-dev:rocq-prover-dev'
       fail-fast: false
     steps:

README.md

@@ -29,9 +29,9 @@ This library relies on propositional and functional extentionality axioms.
   - Anton Trunov
   - Alexander Gryzlov
 - License: [Apache-2.0](LICENSE)
-- Compatible Rocq/Coq versions: 9.0 or later
+- Compatible Rocq/Coq versions: 9.2 or later
 - Additional dependencies:
-  - [MathComp ssreflect 2.4 or later](https://math-comp.github.io)
+  - [MathComp ssreflect 2.6 or later](https://math-comp.github.io)
   - [Hierarchy Builder 1.7.0 or later](https://github.com/math-comp/hierarchy-builder)
   - [MathComp algebra](https://math-comp.github.io)
 - Rocq/Coq namespace: `pcm`

_CoqProject

@@ -2,11 +2,8 @@
 -arg -w -arg -notation-overridden
 -arg -w -arg -redundant-canonical-projection
 -arg -w -arg -HB.no-new-instance
--arg -w -arg -notation-for-abbreviation
-# release-specific args
--arg -w -arg -notation-incompatible-prefix # specific to coq8.20.0 
--arg -w -arg -deprecated-from-Coq # specific to coq8.21 
--arg -w -arg -deprecated-dirpath-Coq # specific to coq8.21 
+-arg -w -arg -ambiguous-paths
+-arg -w -arg -rewrite-rw
 
 core/options.v
 core/axioms.v

coq-fcsl-pcm.opam

@@ -10,7 +10,7 @@ dev-repo: "git+https://github.com/imdea-software/fcsl-pcm.git"
 bug-reports: "https://github.com/imdea-software/fcsl-pcm/issues"
 license: "Apache-2.0"
 
-synopsis: "Coq library of Partial Commutative Monoids"
+synopsis: "Rocq library of Partial Commutative Monoids"
 description: """
 The PCM library provides a formalisation of Partial Commutative Monoids (PCMs),
 a common algebraic structure used in separation logic for verification of
@@ -25,10 +25,10 @@ This library relies on propositional and functional extentionality axioms."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" { (>= "9.0" & < "9.2~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.6~") | (= "dev") }
-  "coq-hierarchy-builder" { (>= "1.7.0" & < "1.11~") | (= "dev") }
-  "coq-mathcomp-algebra" 
+  "coq" { (>= "9.2" & < "9.3~") | (= "dev") }
+  "rocq-mathcomp-ssreflect" { (>= "2.6.0" & < "2.7~") | (= "dev") }
+  "rocq-hierarchy-builder" { (>= "1.7.0" & < "1.11~") | (= "dev") }
+  "rocq-mathcomp-algebra" 
 ]
 
 tags: [

core/auto.v

@@ -30,7 +30,7 @@ From pcm Require Import options prelude.
 (*                                                                        *)
 (* Second, in some symmetric cancellation problems, e.g., dom_eq e1 e2,   *)
 (* we *want* to remove only one occurrence from e2 for each component in  *)
-(* e1. Otherwise, we will not produce a sound reduction. E.g.,            *)
+(* e1. Otherewriteise, we will not produce a sound reduction. E.g.,            *)
 (* dom (x \+ x) (x \+ x) is valid, since both expressions are undef.      *)
 (* However, after removing x from the left side, and both x's from the    *)
 (* right side, we get dom x Unit, which is not valid.                     *)
@@ -63,6 +63,10 @@ Variable A : Type.
 
 Structure tagged_elem := XTag {xuntag :> A}.
 
+(* DEVCOMMENT *)
+(* remove? *)
+(* Local Coercion untag : tagged_elem >-> A. *)
+(* /DEVCOMMENT *)
 
 Definition extend_tag := XTag.
 Definition recurse_tag := extend_tag.

core/autouniq.v

@@ -14,7 +14,8 @@ limitations under the License.
 From HB Require Import structures.
 From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat seq eqtype.
-From pcm Require Import options prelude auto.
+From pcm Require Import options prelude.
+From pcm Require Export auto.
 
 (**********************************************************)
 (**********************************************************)
@@ -378,8 +379,8 @@ Module UniqX.
 Section UniqX.
 Variable A : eqType.
 Implicit Types (j : ctx A) (ts : seq term).
-Notation form := Syntactify.form.
-Notation untag := Syntactify.untag.
+Abbreviation form := Syntactify.form.
+Abbreviation untag := Syntactify.untag.
 
 Structure packed_map (m : seq A) := Pack {unpack : seq A}.
 Canonical equate (m : seq A) := Pack m m.
@@ -412,8 +413,8 @@ Canonical start.
 Section Exports.
 Variable A : eqType.
 Implicit Types (j : ctx A) (ts : seq term).
-Notation form := Syntactify.form.
-Notation untag := Syntactify.untag.
+Abbreviation form := Syntactify.form.
+Abbreviation untag := Syntactify.untag.
 
 (* main lemma *)
 (* boolean component of rform is set to true *)
@@ -442,8 +443,8 @@ Module NeqX.
 Section NeqX.
 Variable A : eqType.
 Implicit Types (j : ctx A) (ts : seq term).
-Notation form := Syntactify.form.
-Notation untag := Syntactify.untag.
+Abbreviation form := Syntactify.form.
+Abbreviation untag := Syntactify.untag.
 
 Structure packed_elem (x : A) := Pack {unpack : A}.
 Canonical equate m := Pack m m.
@@ -485,8 +486,8 @@ Canonical start.
 Section Exports.
 Variable A : eqType.
 Implicit Types (j : ctx A) (ts : seq term).
-Notation form := Syntactify.form.
-Notation untag := Syntactify.untag.
+Abbreviation form := Syntactify.form.
+Abbreviation untag := Syntactify.untag.
 
 (* main lemma *)
 Lemma neqO n m i keys2 ts1 (f : form (empx A) i ts1) 
@@ -523,8 +524,8 @@ Module NotinX.
 Section NotinX.
 Variable A : eqType.
 Implicit Types (j : ctx A) (ts : seq term).
-Notation form := Syntactify.form.
-Notation untag := Syntactify.untag.
+Abbreviation form := Syntactify.form.
+Abbreviation untag := Syntactify.untag.
 
 Structure packed_map (x : seq A) := Pack {unpack : seq A}.
 Canonical equate m := Pack m m.
@@ -563,8 +564,8 @@ Canonical start.
 Section Exports.
 Variable A : eqType.
 Implicit Types (j : ctx A) (ts : seq term).
-Notation form := Syntactify.form.
-Notation untag := Syntactify.untag.
+Abbreviation form := Syntactify.form.
+Abbreviation untag := Syntactify.untag.
 
 (* main lemma *)
 Lemma notinO n m i keys2 ts1 (f : form (empx A) i ts1) 
@@ -602,11 +603,11 @@ Lemma uniqX' (A : eqType) i ts1 (f1 : Syntactify.form (empx A) i ts1) :
              uniq (UniqX.unpack (UniqX.pivot g))) * 
           (forall n keys2 (x : xfind (keyx i) keys2 n),
              ((forall m (y : NeqX.rform (Context keys2 (varx i)) ts1 n m true),
-               xuntag x == NeqX.unpack (NeqX.pivot y) = false) * 
+               (xuntag x == NeqX.unpack (NeqX.pivot y)) = false) * 
              (forall m (y : NotinX.rform (Context keys2 (varx i)) ts1 n m true),
-               xuntag x \in NotinX.unpack (NotinX.pivot y) = false))).
+               (xuntag x \in NotinX.unpack (NotinX.pivot y)) = false))).
 Proof. 
-by move=>U; split; [|split]=>*; first by [apply: uniqO U];
+by move=>U; split; [|split]; move=>*; first by [apply: uniqO U];
 apply/negbTE; [apply: neqO U|apply: notinO U].
 Qed.
 
@@ -616,3 +617,8 @@ Definition uniqX {A i ts1 f1} U :=
   (mem_rcons, mem_cat, inE, negb_or, rcons_uniq, cat_uniq, andbT, orbF, 
    @uniqX' A i ts1 f1 U).
 
+Lemma test (A : eqType) (s1 s2 : seq A) (x : A) :
+        uniq (rcons s1 x ++ s2) -> 
+        x \in s1 -> 
+        false.
+Proof. by move=>U; rewrite (uniqX U). Abort.

core/axioms.v

@@ -21,7 +21,8 @@ limitations under the License.
 (* Jonh Major equality via equality cast.                                     *)
 (******************************************************************************)
 
-From Stdlib Require Import ssreflect ssrfun Eqdep ClassicalFacts.
+From Corelib Require Import ssreflect ssrfun.
+From Stdlib Require Import Eqdep ClassicalFacts.
 From mathcomp Require Import eqtype.
 From pcm Require Import options.
 
@@ -40,7 +41,7 @@ Axiom fext : forall A (B : A -> Type) (f1 f2 : forall x, B x),
 Lemma pf_irr (P : Prop) (p1 p2 : P) : p1 = p2.
 Proof. by apply/ext_prop_dep_proof_irrel_cic/@pext. Qed.
 
-Lemma sval_inj A P : injective (@sval A P).
+Lemma inj_sval A P : injective (@sval A P).
 Proof.
 move=>[x Hx][y Hy] /= H; move: Hx Hy; rewrite H=>*.
 congr exist; apply: pf_irr.
@@ -55,50 +56,31 @@ Proof. by apply: fext. Qed.
 Lemma comp1f A B (f : A -> B) : f = id \o f.
 Proof. by apply: fext. Qed.
 
-(*****************************************)
-(* Cast and John Major Equality via cast *)
-(*****************************************)
+(********)
+(* Cast *)
+(********)
 
 (* depends on StreicherK axiom *)
 
 Section Cast.
 Variable (T : Type) (interp : T -> Type).
 
-Definition cast A B (pf : A = B) (v : interp B) : interp A :=
-  ecast _ _ (esym pf) v.
+Definition cast A B (pf : A = B) (v : interp A) : interp B :=
+  ecast _ _ pf v.
 
 Lemma eqc A (pf : A = A) (v : interp A) : cast pf v = v.
 Proof. by move: pf; apply: Streicher_K. Qed.
 
-Definition jmeq A B (v : interp A) (w : interp B) := exists pf, v = cast pf w.
-
-Lemma jm_refl A (v : interp A) : jmeq v v.
-Proof. by exists (erefl _); rewrite eqc. Qed.
-
-Lemma jm_sym A B (v : interp A) (w : interp B) : jmeq v w -> jmeq w v.
-Proof. by case=>? ->; subst B; rewrite eqc; apply: jm_refl. Qed.
-
-Lemma jm_trans A B C (u : interp A) (v : interp B) (w : interp C) :
-        jmeq u v -> jmeq v w -> jmeq u w.
-Proof. by case=>? -> [? ->]; subst B C; rewrite !eqc; apply: jm_refl. Qed.
-
-Lemma jmE A (v w : interp A) : jmeq v w <-> v = w.
-Proof. by split=>[[?]|] ->; [rewrite eqc | apply: jm_refl]. Qed.
-
-Lemma castE A B (pf1 pf2 : A = B) (v1 v2 : interp B) :
+Lemma castE A B (pf1 pf2 : A = B) (v1 v2 : interp A) :
         v1 = v2 <-> cast pf1 v1 = cast pf2 v2.
 Proof. by subst B; rewrite !eqc. Qed.
 
 End Cast.
 
 Arguments cast {T} interp [A][B] pf v.
-Arguments jmeq {T} interp [A][B] v w.
-
-#[export] Hint Resolve jm_refl : core.
 
 (* special notation for the common case when interp = id *)
-Notation icast pf v := (@cast _ id _ _ pf v).
-Notation ijmeq v w := (@jmeq _ id _ _ v w).
+Abbreviation icast pf v := (@cast _ id _ _ pf v).
 
 (* in case of eqTypes StreicherK not needed *)
 Section EqTypeCast.
@@ -107,7 +89,6 @@ Lemma eqd a (pf : a = a) (v : interp a) : cast interp pf v = v.
 Proof. by rewrite eq_axiomK. Qed.
 End EqTypeCast.
 
-
 (* type dynamic is sigT *)
 
 Section Dynamic.
@@ -116,20 +97,36 @@ Variables (A : Type) (P : A -> Type).
 (** eta expand definitions to prevent universe inconsistencies when using
     the injectivity of constructors of datatypes depending on [[dynamic]] *)
 
-Definition dynamic := sigT P.
+Definition dynamic := sigT [eta P].
 Definition dyn := existT P.
 Definition dyn_tp := @projT1 _ P.
 Definition dyn_val := @projT2 _ P.
 Definition dyn_eta := @sigT_eta _ P.
-Definition dyn_injT := @eq_sigT_fst _ P.
-Definition dyn_inj := @inj_pair2 _ P.
-
+Definition inj_dynT := @eq_sigT_fst _ P.
+Definition inj_dyn := @inj_pair2 _ P.
 End Dynamic.
 
-Prenex Implicits dyn_tp dyn_val dyn_injT dyn_inj.
+Prenex Implicits dyn_tp dyn_val inj_dynT inj_dyn.
 Arguments dyn {T} interp {A} _ : rename.
-Notation idyn v := (@dyn _ id _ v).
+Abbreviation idyn v := (@dyn _ id _ v).
+
+(* Tagging *)
+
+Abbreviation Tag := (@existT _ _).
+Definition inj_tagT := @eq_sigT_fst.
+Definition inj_tagK := @inj_pair2.
+Prenex Implicits inj_tagT inj_tagK.
+
+(* Because of a bug in inversion and injection tactics *)
+(* we occasionally have to destruct pairs by hand, else we *)
+(* lose the second equation. *)
+Lemma inj_pair A B (a1 a2 : A) (b1 b2 : B) :
+         (a1, b1) = (a2, b2) -> 
+         (a1 = a2) * (b1 = b2).
+Proof. by case. Qed.
+
+Arguments inj_pair {A B a1 a2 b1 b2}.
+
+Definition inj_some := @Some_inj.
+Prenex Implicits inj_some.
 
-Lemma dynE (A B : Type) interp (v : interp A) (w : interp B) :
-        jmeq interp v w <-> dyn interp v = dyn interp w.
-Proof. by split=>[[pf ->]|[pf]]; subst B; [rewrite !eqc | move/dyn_inj=>->]. Qed.