Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix `simpl_rel` and notations, `{pred T}` alias, `nonPropType` interface #9995

Merged
merged 1 commit into from Apr 30, 2019

Conversation

@ggonthier
Copy link
Contributor

commented Apr 24, 2019

  • Changed definition of simpl_rel to T -> simpl_pred T, so that
    inE will now expand a \in r b, when r := [rel x y | R] to R{b/x, a/y}, as the expanding coercion is now only inserted in the last
    application.
    The old definition made it possible to have a simpl_rel >-> rel
    coercion that does not block expansion, but this can now be achieved
    more economically with the Arguments … /. annotation.
  • Deleted the [rel of P] notation which is no longer needed with
    the new simpl_rel definition, and was broken anyway.
  • Added relpre f R definition of functional preimage of a notation.
  • comp and idfun are now proper definitions, using the Arguments … /. annotation to specify simplification on application.
  • Added {pred T} syntax for the alias of pred T in the pred_sort
    coercion class; deprecated the pred_class alias: one should either
    use pred_sort in Coercion declarations, or {pred T} in type casts.
  • Simplified the predType structure by removing the redundant
    explicit mem_pred subfield, and replacing it with an interlocked
    projection; deprecated mkPredType, now an alias for PredType.
  • Added (and extensively documented) a nonPropType interface
    matching types that do not have sort Prop, and used it to remove
    the non-standard maximal implicits annotation on Some_inj introduced
    in #6911 by @anton-trunov.
  • Documented the design of the four structures used to control the
    matching of inE and related predicate rewriting lemmas.
  • Used only printing annotations to get rid of token concatenation
    hacks.
  • Fixed boolean and general if b return t then … notation so that
    b is bound in t. This is a minor source of incompatibility for
    misuses of this syntax when b is not bound in t, and (if b then …) : t should have been used instead.
  • Reserved all ssreflect, ssrfun and ssrbool notation at the top
    of the file, adding some printing boxes, and removing some spurious
    [pred .. => ..] reserved notation.
  • Fixed parsing precedence and format of <hidden n> notation, and
    declared and put it in an explicit ssr_scope. @gares check this is
    fine with you.

@ggonthier ggonthier requested a review from coq/ssreflect-maintainers as a code owner Apr 24, 2019

@gares

This comment has been minimized.

Copy link
Member

commented Apr 25, 2019

Mtac failure seem unrelated

@gares gares added this to the 8.11+beta1 milestone Apr 25, 2019

@gares
Copy link
Member

left a comment

Looks good to me. I'd love to have a test in test-suite for an instance of nonPropType (or, is Some_inj used as a view in the few ssr*.v files? it does not seem to)

Notes:

  • should nonPropType also non-unify with SProp? If so we should add a test for this (SProp needs a command line flags in order to be available, but in test-suite we can set flags on a per file basis, so it should be doable)
  • the universe(template) attribute needs to be clarified
  • the CHANGES file seems not to reflect the recent creation of the v8.10 branch (eg this PR adds lines in the Unreleased section, but this section contains things that should be in a 8.10 section CC @vbgl )
failure.
**)

#[universes(template)]

This comment has been minimized.

Copy link
@gares

gares Apr 25, 2019

Member

I'm wondering why the Structures are annotate with template

This comment has been minimized.

Copy link
@ggonthier

ggonthier Apr 25, 2019

Author Contributor

"Just to be on the safe side", mostly, as I'm not sure about the semantics of the annotation.
If these only are meaningful for types with Type parameters then these are indeed useless, but then the external_view type (shouldn't it be a Variant?) does have a template annotation. I suppose the annotation on test_of is almost certainly useless, since that Structure has no parameter or component in Type.

This comment has been minimized.

Copy link
@gares

gares Apr 25, 2019

Member

Cc @maximedenes @mattam82 (given #9918 they surely know better).

This comment has been minimized.

Copy link
@SkySkimmer

SkySkimmer Apr 25, 2019

Contributor

I added the annotation mechanically when I added the auto template warning, hoping to have a look at individual cases at some point. The warning was later disabled-by-default due to low value and false positives.
AFAIK template is only useful when there's a Type parameter (not component), or when you rely on automatic lowering.

Automatic lowering: this would work without the attribute

#[universes(notemplate)]
Inductive foo := .
Fail Check foo : Prop. (* error foo is in Type *)

I would say don't bother annotating new types. I would almost consider reverting the existing annotations but I don't feel it's worth the time to think about it.

@gares gares self-assigned this Apr 25, 2019

@ggonthier

This comment has been minimized.

Copy link
Contributor Author

commented Apr 25, 2019

I'm not sure about SProp; is it supposed to be included in Prop? In any case, I don't think this really matters for the intended use cases.
I can make the mechanism open-ended by adding intermediate delta layers before and/or after maybeProp. This would let users adjust the set of excluded types by defining new instances of test_of, perhaps even using an auxiliary Structure to pattern-match on the type itself, e.g., to specifically exclude reflect. I thought however that nonPropType was good enough for known use cases, and simpler to explain (implementation is a whole other story!).

@ggonthier

This comment has been minimized.

Copy link
Contributor Author

commented Apr 25, 2019

I'll see about adding something to test-suite. Some_inj is used in seq, but not as a view; indeed this use made me realise that putting non-standard implicits on Some_inj was a mistake, and got me thinking about finding another way to address the issue raised by @anton-trunov.

@ggonthier

This comment has been minimized.

Copy link
Contributor Author

commented Apr 25, 2019

I'm not sure what to do about CHANGES. I assumed this was a bit late for 8.10, so the "unreleased" category seemed fine for me, and that the owners of other items would see to their migration in the 8.10 subdivision?

@gares

This comment has been minimized.

Copy link
Member

commented Apr 25, 2019

I'm not sure what to do about CHANGES

I'll deal with this at merge time myself

I'm not sure about SProp; is it supposed to be included in Prop? In any case, I don't think this really matters for the intended use cases.

CC @SkySkimmer knows the detail. I think that the terms that live in SProp can live in Prop, but not the converse and that there is no cumulativity between the two sorts.
My intuition is that, as a user, SProp is like Prop but with more proof irrelevance. So some statements that today I put in Prop, maybe tomorrow I'll put them in SProp. Hence my question about notProp, since I'd expect it to also rule out SProp.

@SkySkimmer

This comment has been minimized.

Copy link
Contributor

commented Apr 25, 2019

There's an explicit lift from SProp to Prop but no implicit lift (cumulativity).
I don't really understand what the new thing is, but I think you'd get a typing error at some point if you tried to use it with SProp due to the non cumulativity. (perhaps needing to wait until Qed / unset https://coq.github.io/doc/master/refman/addendum/sprop.html#coq:opt.elaboration-strictprop-cumulativity)

@ggonthier

This comment has been minimized.

Copy link
Contributor Author

commented Apr 25, 2019

There's no chance of a delayed type error, because a type being accepted as a Prop causes the unification to fail. So if Coq allows an SProp to be assigned to a Prop evar, then nonPropType will also exclude SProp, regardless of whether this assignment would be rejected on Qed (it will never get to this, since the unification will have failed and the assignment discarded). If not, then nonPropType will accept SProps, so a separate (or extended) version would be needed to have that functionality.

@SkySkimmer

This comment has been minimized.

Copy link
Contributor

commented Apr 25, 2019

BTW please don't open branches on the Coq repo itself.

ggonthier added a commit to math-comp/odd-order that referenced this pull request Apr 27, 2019

robustness fixes for ssrbool update
Refactoring some fragile script lines to work with `predType`
refactoring following coq/coq#9995 `ssrbool` update.

ggonthier added a commit to math-comp/math-comp that referenced this pull request Apr 28, 2019

Generalise use of `{pred T}` from coq/coq#9995
Use `{pred T}` systematically for generic _collective_ boolean
predicate.
Use `PredType` to construct `predType` instances.
Instrument core `ssreflect` files to replicate these and other new
features introduces by coq/coq#9555 (`nonPropType` interface,
`simpl_rel` that simplifies with `inE`).
@gares

gares approved these changes Apr 29, 2019

Copy link
Member

left a comment

Look OK to me.

@gares

This comment has been minimized.

Copy link
Member

commented Apr 29, 2019

BTW please don't open branches on the Coq repo itself.

I'll delete the branch after merging, next time @ggonthier please use the fork button to obtain a copy of coq in you github namespace, eg github.com/ggconthier/coq, push your branch there and do the PR. I guess you already have a coq clone on your hard drive, I recommend (after you hit the fork button in coq/coq) you do the git gimmicks

git remote rename origin upstream
git remote add origin git@github.com:ggonthier/coq.git
git remote update

In this way the standard destination for a push (origin) points your your own space, rather than the official repo (upstream).

WRT this PR, I think we are good, If I hear nothing I'll merge later today.

FTR the nonProp thing solves a quite annoying issue @bgregoir has been reporting privately many times, I CC him here to make him aware of this.

@ggonthier

This comment has been minimized.

Copy link
Contributor Author

commented Apr 29, 2019

@gares, @SkySkimmer : thank you for the specific instructions. You might want to include those in coq/CONTRIBUTING.md, which at present quite literally instructs contributors to fork the main repository....
Regarding this PR, I've got an additional outstanding commit fixing a multiple-coercion issue that came up while I was propagating the interface change to MathComp (math-comp/math-comp#337).
As this commit also removes rather than deprecates two legacy ssrbool definitions (mkPredType and pred_class) I'm holding it until math-comp/math-comp#337 can be merged (it's still held up by minor v8.7 compatibility issues, which I hope to clear up today).
Finally, CONTRIBUTING.md say I should add myself to CREDITS; I'm already in there, but the dates are wrong, so I guess I'll just fix that?

@Zimmi48

This comment has been minimized.

Copy link
Member

commented Apr 29, 2019

which at present quite literally instructs contributors to fork the main repository

You may be confusing "fork" and "clone" but the instruction of forking the repository is indeed what we request from contributors and what @gares just explained above. We may need to clarify further what that means.

Finally, CONTRIBUTING.md say I should add myself to CREDITS; I'm already in there, but the dates are wrong, so I guess I'll just fix that?

Yes, if you don't mind. Note though that because not many people actually follow this advice, we will probably switch to another setup wrt CREDITS in the future.

@gares

This comment has been minimized.

Copy link
Member

commented Apr 29, 2019

I'm holding it until

OK, then just ping me back when things are set.

ggonthier added a commit to ggonthier/finmap that referenced this pull request Apr 29, 2019

Compatibility with ssrbool update coq/coq#9995
Removed internal `mem_pred` sigma-types from undocumented subclasses of
`predType`, so that `finmap` will be compatible with coq/coq#9995 and
more generally with math-comp/math-comp#337, which eliminate these from
`predType` and `PredType`, respectively.
   Caveat: at the time of testing this PR I got compile errors for
non-uniform coercions in `set.Semiset` and `set.set`. These seem
unrelated to this PR so I have left them in, assuming they somehow pass
in the `fin map` compilation setup.

ggonthier added a commit to math-comp/math-comp that referenced this pull request Apr 29, 2019

@ggonthier ggonthier force-pushed the fix-simpl-rel branch from 3001c0e to ab73036 Apr 29, 2019

@ggonthier

This comment has been minimized.

Copy link
Contributor Author

commented Apr 29, 2019

@gares: completed, squashed and rebased; hopefully CI holds (math-comp itself was also updated).

ggonthier added a commit to ggonthier/finmap that referenced this pull request Apr 29, 2019

forward and backward compatibility
Added `mathcomp/ssrbool` shim so `finmap` should compile with both
mathcomp 1.8.0 and dev, and replaced reference to `sort_of_simpl_pred`
coercion with `pred_of_simpl` which will replace it in coq/coq#9995.

ggonthier added a commit to ggonthier/finmap that referenced this pull request Apr 29, 2019

Compatibility with ssrbool update coq/coq#9995
Removed internal `mem_pred` sigma-types from undocumented subclasses of
`predType`, so that `finmap` will be compatible with coq/coq#9995 and
more generally with math-comp/math-comp#337, which eliminate these from
`predType` and `PredType`, respectively.

Added `mathcomp/ssrbool` shim so `finmap` should compile with both
mathcomp 1.8.0 and dev, and replaced reference to `sort_of_simpl_pred`
coercion with `pred_of_simpl` which will replace it in coq/coq#9995.
fix `simpl_rel` and notations, `{pred T}` alias, `nonPropType` interface
** Changed definition of `simpl_rel` to `T -> `simpl_pred T`, so that
`inE` will now expand `a \in r b`, when `r := [rel x y | R]` to `R{b/x,
a/y}`, as the expanding coercion is now only inserted in the _last_
application.
The old definition made it possible to have a `simpl_rel >-> rel`
coercion that does not block expansion, but this can now be achieved
more economically with the `Arguments … /.` annotation.
**  Deleted the `[rel of P]` notation which is no longer needed with
the new `simpl_rel` definition, and was broken anyway.
** Added `relpre f R` definition of functional preimage of a notation.
** `comp` and `idfun` are now proper definitions, using the `Arguments
… /.` annotation to specify simplification on application.
** Added `{pred T}` syntax for the alias of `pred T` in the `pred_sort`
coercion class; deleted the `pred_class` alias: one should either
use `pred_sort` in `Coercion` declarations, or `{pred T}` in type casts.
Used `{pred T}` as appropriate in localised predicate (`{in …, …}`) theory.
Extended and corrected `pred` coercion internal documentation.
** Simplified the `predType` structure by removing the redundant
explicit `mem_pred` subfield, and replacing it with an interlocked
projection; deleted `mkPredType`, now replaced by `PredType`.
** Added (and extensively documented) a `nonPropType` interface
matching types that do _not_ have sort `Prop`, and used it to remove
the non-standard maximal implicits annotation on `Some_inj` introduced
in #6911 by @anton-trumov; included `test-suite` entry for `nonPropType`.
** Documented the design of the four structures used to control the
matching of `inE` and related predicate rewriting lemmas; added `test-suite`
entry covering the `pred` rewriting control idioms.
** Used `only printing` annotations to get rid of token concatenation
hacks.
** Fixed boolean and general `if b return t then …` notation so that
`b` is bound in `t`. This is a minor source of incompatibility for
misuses of this syntax when `b` is _not_ bound in `t`, and `(if b then
…) : t` should have been used instead.
** Reserved all `ssreflect`, `ssrfun` and `ssrbool` notation at the top
of the file, adding some printing boxes, and removing some spurious
`[pred .. => ..]` reserved notation.
** Fixed parsing precedence and format of `<hidden n>` notation, and
declared and put it in an explicit `ssr_scope`.
** Used module-and-functor idiom to ensure that the `simpl_pred T >-
pred T` _and_ `simpl_pred T >-> {pred T}` coercions are realised by the
_same_ Gallina constant.
** Updated `CREDITS`.
The policy implied by this PR: that `{pred T}` should systematically
be used as the generic collective predicate type, was implemented in MathComp
math-comp/math-comp#237. As a result  `simpl_pred >-> pred_sort` coercions
became more frequent, as it turned out they were not, as incorrectly stated
in `ssrbool` internal comments, impossible: while the `simplPredType`
canonical instance does solve all `simpl_pred T =~= pred_sort ?pT`
instances, it does _not_ solve `simpl_pred T =~= {pred T}`, and so the
coercion will be used in that case. However it appeared that having two
different coercion constants confused the SSReflect keyed matching
heuristic, hence the fix introduced here. This has entailed some
rearrangement of `ssrbool`: the large  `Predicates` section had to be
broken up as the module-functor idiom for aliasing coercions cannot be
used inside a section.

@ggonthier ggonthier force-pushed the fix-simpl-rel branch from ab73036 to 7875955 Apr 30, 2019

@gares

This comment has been minimized.

Copy link
Member

commented Apr 30, 2019

Are we good? (I see you said go, but then pushed again)

CohenCyril added a commit to math-comp/finmap that referenced this pull request Apr 30, 2019

@gares gares merged commit 7875955 into master Apr 30, 2019

8 checks passed

GitLab CI pipeline Pipeline completed on GitLab CI
Details
Pull request checks Passed.
Details
coq.coq Build #20190430.5 succeeded
Details
coq.coq (Windows) Windows succeeded
Details
coq.coq (macOS) macOS succeeded
Details
doc:ml-api:odoc: ml-api artifact Link to ml-api build artifact.
Details
doc:refman: refman artifact Link to refman build artifact.
Details
doc:refman: stdlib artifact Link to stdlib build artifact.
Details

gares added a commit that referenced this pull request Apr 30, 2019

Merge PR #9995: fix `simpl_rel` and notations, `{pred T}` alias, `non…
…PropType` interface

Ack-by: SkySkimmer
Reviewed-by: gares
Ack-by: ggonthier

@ejgallego ejgallego deleted the fix-simpl-rel branch Apr 30, 2019

vbgl added a commit to vbgl/coq that referenced this pull request Apr 30, 2019

@Zimmi48 Zimmi48 referenced this pull request Apr 30, 2019

Merged

Credits for 8.10 #9939

@Zimmi48 Zimmi48 modified the milestones: 8.11+beta1, 8.10+beta1 May 4, 2019

@Zimmi48 Zimmi48 added this to Shipped in 8.10+beta1 in Coq 8.10 May 4, 2019

thery added a commit to thery/math-comp that referenced this pull request Jul 10, 2019

Generalise use of `{pred T}` from coq/coq#9995
Use `{pred T}` systematically for generic _collective_ boolean
predicate.
Use `PredType` to construct `predType` instances.
Instrument core `ssreflect` files to replicate these and other new
features introduces by coq/coq#9555 (`nonPropType` interface,
`simpl_rel` that simplifies with `inE`).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.