[Merged by Bors] - refactor(library/init/meta/*): refactor case tags #228
Conversation
|
I can't test these changes with mathlib right now because there's no branch that builds against Lean master, but last I checked, the resulting breakage was relatively minor. |
For the record, the branch that builds with mathlib is called |
|
|
||
| open name (mk_string mk_numeral) | ||
|
|
||
| instance : has_to_string case_tag := |
There was a problem hiding this comment.
Please also add has_repr, has_to_tactic_format, and has_format.
There was a problem hiding this comment.
There seems to be no instance has_repr name (which blocks has_repr case_tag). Is this intentional?
There was a problem hiding this comment.
I think the intention behind the repr/to_string split is that repr should output "valid" Lean code, and to_string a "Human-readable" version. But we are missing lots of instances because of this stringification class inflation. Practically speaking, it's really frustrating even if only some of the instances are missing because you need all of them. For example, #eval want has_repr, pp wants has_to_tactic_format, etc.
So yes, please add has_repr name. And add has_repr case_tag no matter whether there is a has_repr name or not. (I would have been ok with instance : has_repr case_tag := ⟨to_string⟩.)
There was a problem hiding this comment.
I get the repr/to_string split; there's a semantic difference there. What I think is unnecessary is has_format/to_string. If format wasn't meta -- and I don't see why it should be -- to_string could be subsumed by has_format.
Anyway, I'll add the has_repr instances.
There was a problem hiding this comment.
Oh, I hit the merge button a bit too early.
BTW, to_string is not subsumed by to_fmt. There is no has_to_string instance using has_to_format.
There was a problem hiding this comment.
Yes, my point was that to_string could be subsumed by to_fmt if has_format wasn't meta, because to_format and to_string serve the same purpose (human-friendly printing).
There was a problem hiding this comment.
👍 for adding a low-priority instance converting from has_to_format to has_to_string.
|
|
||
| Additionally, the form | ||
| ``` | ||
| case C : N₀ ... Nₙ {...} |
There was a problem hiding this comment.
This is just my personal opinion, but I find this syntax abhorrent and deeply offensive to my sense of beauty. IMHO case should require the user to provide explicit argument names, and the case syntax should mirror the constructor. That is, something like this:
case cons x xs, succ y { ... }Bonus points if I could write:
case x::xs, y+1 { ... }There was a problem hiding this comment.
I really like this suggestion actually. This would also force me to properly support chains of cases x; cases y; induction z. (At the moment, these are only properly supported if you put a with_cases around them.) Maybe I'll do a follow-up PR which adds this as alternative syntax.
There was a problem hiding this comment.
I agree, this can go in a follow-up PR, if you want. I just wanted to vent.
Okay, I can cherry-pick this PR and my previous PR, which this one depends on, on top of the v3.11.0 tag. That's actually not terrible. Building mathlib now. (I've also started a Zulip discussion about an alternative approach.) Also, thanks for the prompt review! I'll go through your comments now. |
|
mathlib diff for this PR is indeed very small (+/- 13). |
|
bors merge |
This is a redesign of case tags as discussed [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Case.20tags). Major changes: - The new file `library/init/meta/case_tag.lean` defines what a case tag is and how it is rendered, parsed and matched. Previously, this stuff was spread all over `init.meta.interactive`. The implementation is also mostly new, but the internal representation of goal tags (as a list of names) remains unchanged. - Case tags generated by `cases` and `induction` now contain the unique names of hypotheses introduced by these tactics. This information is used by the `case ... : x y z {}` form to determine which hypotheses should be renamed. Previously, `case` would parse the result term to do this, so it was very tightly coupled to the implementation of `cases`/`induction`. (`with_cases` generates case tags of a different form; these remain unchanged except for some cosmetics.) - `case` now matches case tags purely syntactically: `case n0 ... nN` looks for exactly one goal with tag `m0 ... mM n0' ... nN'` where the `ni` are suffixes of the `ni'`. The old implementation would first look for a goal `n0 ... nN m0 ... mM` (where the given names are a *prefix* of the goal tag, not a *suffix*). If no such goal was found, it would attempt to resolve the names `ni` as constructor names and repeat the matching with the resolved names.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
## Changes to bracket notation
* `{a}` now requires an instance `has_singleton`;
* `insert a ∅ = {a}` is called `insert_emptyc_eq`, provided by an `is_lawful_singleton` instance;
* `a ∈ ({b} : set α)` is now defeq `a = b`, not `a = b ∨ false`;
* `({a} : set α)` is no longer defeq `insert a ∅`;
* `({a} : finset α)` now means `⟨⟨[a]⟩, _⟩` (used to be called `finset.singleton a`), not `insert a ∅`;
* removed `finset.singleton`;
* `{a, b}` is now `insert a {b}`, not `insert b {a}`.
* `finset.univ : finset bool` is now `{tt, ff}`;
* `(({a} : finset α) : set α)` is no longer defeq `{a}`.
## Tactic `norm_num`
The interactive tactic `norm_num` was recently rewritten in Lean. The non-interactive `tactic.norm_num` has been removed in Lean 3.12 so that we can migrate the algebraic hierarchy to mathlib in 3.13.
## Tactic combinators
leanprover-community/lean#212 renames a bunch of tactic combinators. We change to using the new names.
## Tactic `case`
leanprover-community/lean#228 slightly changes the semantics of the `case` tactic. We fix the resulting breakage to be conform the new semantics.
Co-authored-by: Jannis Limperg <jannis@limperg.de>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
## Changes to bracket notation
* `{a}` now requires an instance `has_singleton`;
* `insert a ∅ = {a}` is called `insert_emptyc_eq`, provided by an `is_lawful_singleton` instance;
* `a ∈ ({b} : set α)` is now defeq `a = b`, not `a = b ∨ false`;
* `({a} : set α)` is no longer defeq `insert a ∅`;
* `({a} : finset α)` now means `⟨⟨[a]⟩, _⟩` (used to be called `finset.singleton a`), not `insert a ∅`;
* removed `finset.singleton`;
* `{a, b}` is now `insert a {b}`, not `insert b {a}`.
* `finset.univ : finset bool` is now `{tt, ff}`;
* `(({a} : finset α) : set α)` is no longer defeq `{a}`.
## Tactic `norm_num`
The interactive tactic `norm_num` was recently rewritten in Lean. The non-interactive `tactic.norm_num` has been removed in Lean 3.12 so that we can migrate the algebraic hierarchy to mathlib in 3.13.
## Tactic combinators
leanprover-community/lean#212 renames a bunch of tactic combinators. We change to using the new names.
## Tactic `case`
leanprover-community/lean#228 slightly changes the semantics of the `case` tactic. We fix the resulting breakage to be conform the new semantics.
Co-authored-by: Jannis Limperg <jannis@limperg.de>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
## Changes to bracket notation
* `{a}` now requires an instance `has_singleton`;
* `insert a ∅ = {a}` is called `insert_emptyc_eq`, provided by an `is_lawful_singleton` instance;
* `a ∈ ({b} : set α)` is now defeq `a = b`, not `a = b ∨ false`;
* `({a} : set α)` is no longer defeq `insert a ∅`;
* `({a} : finset α)` now means `⟨⟨[a]⟩, _⟩` (used to be called `finset.singleton a`), not `insert a ∅`;
* removed `finset.singleton`;
* `{a, b}` is now `insert a {b}`, not `insert b {a}`.
* `finset.univ : finset bool` is now `{tt, ff}`;
* `(({a} : finset α) : set α)` is no longer defeq `{a}`.
## Tactic `norm_num`
The interactive tactic `norm_num` was recently rewritten in Lean. The non-interactive `tactic.norm_num` has been removed in Lean 3.12 so that we can migrate the algebraic hierarchy to mathlib in 3.13.
## Tactic combinators
leanprover-community/lean#212 renames a bunch of tactic combinators. We change to using the new names.
## Tactic `case`
leanprover-community/lean#228 slightly changes the semantics of the `case` tactic. We fix the resulting breakage to be conform the new semantics.
Co-authored-by: Jannis Limperg <jannis@limperg.de>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
This is a redesign of case tags as discussed on Zulip. Major changes:
library/init/meta/case_tag.leandefines what a case tag is and how it is rendered, parsed and matched. Previously, this stuff was spread all overinit.meta.interactive. The implementation is also mostly new, but the internal representation of goal tags (as a list of names) remains unchanged.casesandinductionnow contain the unique names of hypotheses introduced by these tactics. This information is used by thecase ... : x y z {}form to determine which hypotheses should be renamed. Previously,casewould parse the result term to do this, so it was very tightly coupled to the implementation ofcases/induction. (with_casesgenerates case tags of a different form; these remain unchanged except for some cosmetics.)casenow matches case tags purely syntactically:case n0 ... nNlooks for exactly one goal with tagm0 ... mM n0' ... nN'where theniare suffixes of theni'. The old implementation would first look for a goaln0 ... nN m0 ... mM(where the given names are a prefix of the goal tag, not a suffix). If no such goal was found, it would attempt to resolve the namesnias constructor names and repeat the matching with the resolved names.