search

imdea-software / fcsl-pcm

Partial Commutative Monoids
Apache License 2.0
25 stars 12 forks source link

[coq] Be explicit about the dependency on Setoid rules. #21

Closed ejgallego closed 4 years ago

ejgallego commented 4 years ago

A couple of files depend on Setoid rewriting implicitly.

As of today, Setoid rules are placed in scope by ssrnat, but IMO you should not rely on this behavior as ssrnat may stop requiring Setoid in the future.

The patch is fully backwards compatible.

ejgallego commented 4 years ago

Typical error if ssrnat doesn't pre-load Setoid is:

Error:
not a rewritable relation: ((mx _ \+ _ = mx _ -> (_ = _) * (_ = Unit)) /\
                            ((_ = _) * (_ = Unit) -> mx _ \+ _ = mx _))
in rule cancelMx
anton-trunov commented 4 years ago

Hi Emilio, thanks for bringing this up! There is an alternative fix, namely, we could remove ssrnat from the list of imports, since it turns out there is no real dependency here. What do you think?

anton-trunov commented 4 years ago

I guess that Setoid (or Morphisms) dependency comes from elsewhere then.

anton-trunov commented 4 years ago

Ah, I keep forgetting that this kind of dependency is transitive. mutex imports fcsl.pcm which imports mathcomp.ssrnat which indirectly exports Coq.Setoid hence the rewrite tactic is able to do setoid rewrites.

ejgallego commented 4 years ago

Ah, I keep forgetting that this kind of dependency is transitive. mutex imports fcsl.pcm which imports mathcomp.ssrnat which indirectly exports Coq.Setoid hence the rewrite tactic is able to do setoid rewrites.

Thanks Anton; indeed, this kind of implicit global effects are pretty weird and far from modular. IMHO it is good to start documenting them for the day we make them more explicit.