feat: refined variable behavior in proofs
#4814
Conversation
github-actions
bot
added
the
toolchain-available
semorrison
added
the
release-ci
Should this be "are instance-implicit variables and all referenced variables are included by these rules."? variable {R : Type*} [CommRing R] {M : Type*} [AddCommGroup M] [Module R M]If only one of (I would also love it if |
Makes sense to me, updated.
Would |
|
Yes, those would be equivalent. In Mathlib we are striving towards using |
@fpvandoorn, I've finally started looking at Mathlib under this PR (the I've already encountered a few places where is seems rather inconvenient for only using |
leanprover-community-mathlib4-bot
added
the
breaks-mathlib
|
Mathlib CI status (docs):
|
|
Re: looking at Mathlib on this PR. So far there are two classes of problems: typeclasses hypothesis being included which should not be (for which the new linter is really helpful), and variables with need an Fixing the first class of problems requires either adding sections to bound I propose that for anyone working on the Mathlib branch for this PR, we try to backport all the changes of the first form. A reasonable workflow seems to be:
(We have have following a similar workflow for the This is going to be a massive adaptation exercise to get this working, and I will need help to get it done. |
@Kha, I think this change may have not worked as intended. In Mathlib on lean-pr-testing-4814 I am seeing: failing with (I have no idea why in Mathlib the first argument of Let me know if you'd like a minimization of this. |
|
@Kha, another bug, where typeclass arguments that are included transitively can be included with multiplicity, apparently! Again on resulting in the signature where apparently Again, please let me know if you'd like an minimisation. |
|
And another problem, @Kha! We have places in Mathlib where people have add implicit arguments that could otherwise be automatically included instance arguments, on the principle that it is faster/better to find these by unification from later arguments that to redo typeclass search. Here's an example from Mathlib in It's perfectly okay on However on lean-pr-testing-4814, we get warning, because the signature becomes: I'm uncertain the best way to proceed here. Probably we ought to make the variable inclusion mechanism robust to this, and decline to include instance arguments if there are already there as implicit arguments. In this particular case it's fine to just remove them, but I don't think that is always going to be true. Again, let me know if you want a minimization. |
|
And more. :-) We may need to pull in typeclass arguments because they mention the type of an included argument, not just the argument itself. For example in Mathlib we have in Here Making matters worse, if we just change the theorem statement to then we get the incorrect warning: I can work around this by just not making it a section variable at all and instead including it directly in both theorems here. (As above with minimization. :-) |
We should probably not strive to do this immediately. Another thing we can consider is to have (in the long-term) no explicit variables, instead repeating those in each theorem statement. That should also reduce the number of |
Kha
changed the title
variable behavior in proofs
|
|
||
| Variable declarations have the same flexibility as regular function paramaters. In particular they | ||
| can be [explicit, implicit][binder docs], or [instance implicit][tpil classes] (in which case they | ||
| can be anonymous). This can be changed, for instance one can turn explicit variable `x` into an | ||
| implicit one with `variable {x}`. Note that currently, you should avoid changing how variables are | ||
| bound and declare new variables at the same time; see [issue 2789] for more on this topic. | ||
|
|
||
| In *theorem bodies* (i.e. proofs), variables are not included based on usage in order to ensure that |
There was a problem hiding this comment.
@david-christiansen I merged this version for now to avoid a stale update-stage0, but please feel free to refine!
There was a problem hiding this comment.
I think the text is perfectly fine as-is. I'll do a refinement pass when I get to that chapter of the manual.
This one is a bit awkward / done badly. I reordered theorems in order to avoid pulling in `SmoothManifoldWithCorners` unnecessarily, but I didn't preserve the section headings properly. :-(
Resolves #2452. For theorems, section variables are now conditionally included when elaborating the theorem body and sending the result to the kernel based on their use in the header; elaboration of the header is unchanged. Definitions as well are unchanged for now because the cost/benefit ratio is much less clear for them.
Specifically, section variables are included if they
includecommand in the current section,For porting, a new option
deprecated.oldSectionVarsis included to locally switch back to the old behavior.breaking change