MathComp 2 boilerplate

[palmskog]

No description provided.

[palmskog]

@chdoc as shown here, the changes from #10 work fine with Coq 8.16 to 8.17 and MathComp 2.0.0 to 2.2.0. The project fails on Coq 8.18 and later, but this is related to setoid rewriting and (I believe) unrelated to MathComp 2. Do you think this is sufficient for merging #10?

[palmskog]

For the record, I think everyone in the MathComp community is nearly all in on MathComp 2 these days, with only a few stragglers like FCSL PCM yet to be ported.

[palmskog]

Just confirmed the error is the same on Coq 8.18.0 and MathComp 1.19.0 as with MathComp 2.X:

File "./theories/libs/sltype.v", line 145, characters 33-59:
Error:
setoid rewrite failed: Unable to satisfy the following constraints:
UNDEFINED EVARS:
 ?X1876==[form ssub decompP F ssub_F
           (LF:=[fset C in powerset F | literalC C]) C IH inU s inC nL S S1
           S2 S3 S4 |- Relation_Definitions.relation form]
           (internal placeholder) {?r}
 ?X1877==[form ssub decompP F ssub_F
           (LF:=[fset C in powerset F | literalC C]) C IH inU s inC nL S S1
           S2 S3 S4 |- Relation_Definitions.relation form]
           (internal placeholder) {?r0}
 ?X1878==[form ssub decompP F ssub_F
           (LF:=[fset C in powerset F | literalC C]) C IH inU s inC nL S S1
           S2 S3 S4 (do_subrelation:=Morphisms.do_subrelation) |-
           Morphisms.Proper
             (Morphisms.respectful
                (fun x y : form =>
                 (let (T, mprv, Imp, _, _, _) as m return (m -> Prop) :=
                    let (msort, Bot', _) := slp_form form in msort in
                  mprv) (x <--> y)) (Morphisms.respectful ?r0 ?r))
             (Imp_op (m:=form))] (internal placeholder) {?p}
 ?X1879==[form ssub decompP F ssub_F
           (LF:=[fset C in powerset F | literalC C]) C IH inU s inC nL S S1
           S2 S3 S4 |- Morphisms.ProperProxy ?r0 (\or_(D<-base LF C) [af D])]
           (internal placeholder) {?p0}
 ?X1880==[form ssub decompP F ssub_F
           (LF:=[fset C in powerset F | literalC C]) C IH inU s inC nL S S1
           S2 S3 S4 (do_subrelation:=Morphisms.do_subrelation) |-
           Morphisms.Proper
             (Morphisms.respectful ?r (Basics.flip Basics.impl))
             (mprv (m:=form))] (internal placeholder) {?p1}
TYPECLASSES:?X1876 ?X1877 ?X1878 ?X1879 ?X1880
SHELF:||
FUTURE GOALS STACK:?X1880 ?X1879 ?X1878 ?X1877 ?X1876||

[chdoc]

@chdoc as shown here, the changes from #10 work fine with Coq 8.16 to 8.17 and MathComp 2.0.0 to 2.2.0. The project fails on Coq 8.18 and later, but this is related to setoid rewriting and (I believe) unrelated to MathComp 2. Do you think this is sufficient for merging #10?

Thank you for investigating this! Is the plan now to merge this PR (which implicitly merges #10 )? If so, please go ahead!

Just confirmed the error is the same on Coq 8.18.0 and MathComp 1.19.0 as with MathComp 2.X:

I was afraid something like this was going to happen eventually. Setoid rewriting was always brittle, but I didn't really see a way to avoid it for this project. In fact, I am surprised it took is long.

Are/were there other developments in community that ran against changes in setoid rewriting in Coq 8.18? Without any indication as to what change causes his breakage, I'm not sure I will ever summon the motivation to fix this.

[palmskog]

@chdoc I think I found the "offending" change in 8.18:

Changed: The RewriteRelation type class is now used to declare relations inferable by the setoid_rewrite tactic to construct Proper instances. This can break developments that relied on existing Reflexive instances to infer relations. The fix is to simply add a (backwards compatible) RewriteRelation declaration for the relation. This change allows to set stricter modes on the relation type classes Reflexive, Symmetric, etc. (#13969, fixes #7916, by Matthieu Sozeau).

Here is how it was fixed in relation-algebra, for example: https://github.com/damien-pous/relation-algebra/pull/32/files

[palmskog]

Actually, I think that change is too old, but this one isn't:

Fixed: untypable proof states generated by setoid_rewrite, which may cause some backwards-incompatibilities (#17304, fixes #17295, by Lasse Blaauwbroek).

[chdoc]

Too bad, I was just about to write:

If this is indeed the case, the fix may be as simple as adding something like:

#[export] Instance mImpPrv_rw (mS : mSystem) : RewriteRelation (@mImpPrv mS) := {}.
#[export] Instance EqvPrv_rw (mS : mSystem) : RewriteRelation (@EqvPrv mS) := {}.

somewhere around the other instance declarations in modular_hilbert.v.

[palmskog]

@chdoc I figured it out, it's actually coq/coq#16258 - PR incoming.