feat(Tactic): upstream @[mk_iff] from mathlib#1854
Conversation
github-actions
Bot
added
the
awaiting-review
|
I would be happy (and it might be desirable) to add e.g. its usage for IsChain in practice (and other inductive props - your examples seem good). |
Move `MVarId.existsi` from `Batteries.Lean.Meta.Basic` (its only user is `MkIff`) into `Batteries/Tactic/MkIff.lean`, so the foundational `Meta.Basic` no longer publicly imports the elaborator/tactic framework. Restore its original imports. Update the `mk_iff` docstrings from the non-existent `List.Chain` to the real `List.IsChain` output, and switch the `Shape` example to `ReflTransGen` (which actually exhibits variable elimination). Drop the dead `open` in `Lean.Name`. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
Mathlib CI status (docs):
|
- Replace hand-rolled `List.init`, `mkAndList`/`mkOrList`/`mkOpList`, and the `refine`/`evalTactic`-based `existsi`/`splitThenConstructor` with core `List.dropLast`, `mkAndN`, `MVarId.existsIntro`, and `MVarId.constructor`, dropping the now-dead `Lean.Elab.Tactic.Basic` import. - Add `Lean.mkOrN` (mirroring core `mkAndN`) and `Lean.Meta.mkExistsFVars` (the existential analogue of `mkForallFVars`) as the only exported helpers. - Use resolved (``) constant names throughout for compile-time checking. - Invert section visibility: default-private `meta section` with `public` only on the two helpers and the `mk_iff` syntax/attribute surface, instead of `public meta section` plus eleven `private` markers. - camelCase locals, drop the stale universe-names TODO. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
I had a bit of a think after digging into the file and with some Claude aid tried a refactor. What I'd like to do is avoid duplication with Core. Having said that - in fact the elephant in the room is that Lean.Meta.MkIffOfInductiveProp exists in Core. But it doesn't actually export the command or the attribute - just the essential plumbing. (And it also has some of the redundancy I've got rid of here.) I think the best strategy here - given that file already exists in Core - is that we consider a change to Core. Ideally they'd refactor as I have here - but at minimum mkIffOfInductivePropImpl should be made public, I think. Then we could add the command and attribute here in Batteries. |
|
Mathlib CI status (docs):
|
|
But the version in core does not properly decapitalise the iff lemma name, right? |
Well, I think the decapitalization happens in the part that Core just doesn't have. I think its mkIffOfInductivePropImpl is the same - or nearly. It's a weird state of affairs. |
|
I am interested in things moving forward. Although a core change is possibly the better long term solution, is there any downside to just moving the code from mathlib to batteries for now? Btw I have fixed the relevant batteries-pr-testing branch but I am waiting on someone to merge the fixes: leanprover-community/mathlib4-nightly-testing#247 |
|
That is the nightly tests for 1853, not 1854. |
|
Mathlib CI status (docs):
|
|
One more adaptation PR: leanprover-community/mathlib4-nightly-testing#248 Also brought up exposing |
|
I think in principle I feel this is good to merge. I'd hope that if we do expose this in Core we can upstream the improvements this PR makes to there. |
|
Mathlib CI status (docs):
|
|
Mathlib CI status (docs):
|
|
I've altered the namespaces to match what Core does and made public the thing we want them to make public - that should make further upstreaming to Core more or less drag and drop. |
|
You look like you're still have issues with Mathlib though I have to assume this is some kind of imports bug? |
|
I just checked and the breakage is completely unrelated to this PR. I assume this is because no one has yet adapted mathlib to recent changes in core |
|
Fiddlesticks. I assume it'll catch up but it'll hold this for now. Sorry. |
|
Mathlib CI status (docs):
|
| public section | ||
|
|
||
| /-- Decapitalize the last component of a name. -/ | ||
| def Lean.Name.decapitalize (n : Name) : Name := |
There was a problem hiding this comment.
Can we fix this?
#eval Lean.Name.decapitalize `Test.Me.That'sLife == `Test.Me.that'sLife -- true
#eval Lean.Name.decapitalize `Test.Me.Ç'estLaVie == `Test.Me.ç'estLaVie -- false3 participants
Motivated by #1853.