Renaming `split`

Stream: mathlib4

[Gabriel Ebner]

As you've probably noticed, core Lean has also defined a split tactic now. Of course, the new tactic does something completely different---split now seems to be a generalization of split_ifs.

In other words, we should rename the split (≈ constructor) tactic. Any suggestions for a new name?

[Johan Commelin]

First suggestions by a random thesaurus: rip, rent, snag, tear,

[Mario Carneiro]

intro

[Johan Commelin]

But split worked on the goal.

[Mario Carneiro]

intro also works on the goal

[Johan Commelin]

I think if you have P ∧ Q as goal, using intro to split it into pieces is weird from a semantic point of view.

[Mario Carneiro]

why is that? You are literally applying and.intro

[Mario Carneiro]

alternatively, we could just lean into constructor if the name isn't taken

[Mario Carneiro]

mk?

[Johan Commelin]

I think intro is a synonym for assume in my mind. Maybe I should decouple that.

[Johan Commelin]

destruct?

[Johan Commelin]

construct?

[Mario Carneiro]

it's a constructor, an introduction rule

[Mario Carneiro]

lambda is the introduction rule for pi, which is why intro is called that

[Mario Carneiro]

but it could easily(ish) be generalized to intro'ing arbitrary inductives too

[Mario Carneiro]

admittedly, everything gets turned around when working on the goal, so introduction patterns make type operators go away

[Gabriel Ebner]

Mario Carneiro said:

alternatively, we could just lean into constructor if the name isn't taken

Is there any difference between constructor and split besides split having a shorter name?

[Mario Carneiro]

constructor applies any of the constructors, not just the first

[Mario Carneiro]

but I don't find this difference in behavior particularly helpful since it's basically just rejecting some class of inputs that could be reasonably handled

[Mario Carneiro]

that is, if you made split an alias to constructor today mathlib would still build

[Johan Commelin]

Can we merge split and split_ifs? It's hard to beat split if it comes to meaningful tactic names: take the goal and split it into subgoals for me.

[Mario Carneiro]

split and split_ifs are completely different

[Johan Commelin]

Under the hood.

[Mario Carneiro]

no, they visibly have very different effects

[Mario Carneiro]

if you have (if a then b else c) /\ d then split turns the goal into if a then b else c and d and split_ifs turns the goal into b /\ d and c /\ d

[Gabriel Ebner]

Okay, I'm gonna remove split for now in favor of constructor: https://github.com/leanprover-community/mathlib4/pull/70
We can always set up a shorter alias if we find a better name.

[Johan Commelin]

@Mario Carneiro super_split could give me three goals: b, c, and d.

[Mario Carneiro]

no takers for mk? The golfers will love us

[Johan Commelin]

What I like about split is that it's a verb. constructor isn't.

[Johan Commelin]

mk is a vrb, I guess. mk s vrb, gss.

[Mario Carneiro]

constr, you get to decide whether it's abbreviating a noun or verb

[Mario Carneiro]

∧I

[Mario Carneiro]

If mk takes an optional (space-separated?) list of arguments, like use, I think it will be pretty convenient

[Johan Commelin]

It would replace rfn (aka refine), right?

[Mario Carneiro]

right

[Mario Carneiro]

I almost never use split normally

[Johan Commelin]

But it's very beginner-friendly. Which is why I'm sad to see it go.

[Mario Carneiro]

and_intro seems pretty friendly

[Johan Commelin]

You mean split_and?

[Mario Carneiro]

we could do that

[Johan Commelin]

But I think that you main point is that it would be nice to have a very cheap way to switch to term mode. exact is quite long for that.

[Mario Carneiro]

having ⟨ be an exact-shortcut would be nice

[Gabriel Ebner]

We could make ⟨?left, ?right⟩ a tactic, this should be unambiguous.

[Johan Commelin]

by puts you in tactic mode. How do you leave it? With as little chars as possible?

[Mario Carneiro]

did you know that lean 3 has exact-shortcuts too? There is only one though, and it is hard coded: calc

[Johan Commelin]

⟨ would work whenever there is a constructor that you want to use, right? But it's not the general thing.

[Mario Carneiro]

calc is not a tactic, but you don't need to write exact first by magic

[Johan Commelin]

calc even uses refine these dats (-;

[Mario Carneiro]

We can make most expr-starters be exact-shortcuts, except for identifiers, which are unfortunately quite common

[Mario Carneiro]

I don't think we should interpret an unknown tactic identifier as an exact-shortcut because that will cause forward compatibility problems

[Johan Commelin]

from is of course also a way to switch to term mode, in lean 3. But it's still 4 chars.

[Johan Commelin]

Would t or x be too cryptic?

[Mario Carneiro]

=

[Gabriel Ebner]

macro (priority := 0) t:term : tactic => `(tactic| exact $t)
example : True := by True.intro

[Johan Commelin]

That's the best solution, I guess.

[Gabriel Ebner]

I'm not sure if this too cryptic though.

[Mario Carneiro]

Like I said, I don't think that's a good idea because tactic names will now compete with variable and constant names. Think about ring for example

[Gabriel Ebner]

It's Ring, now.

[Mario Carneiro]

checkmate

[Johan Commelin]

But it's Ring in both cases, right?

[Mario Carneiro]

no, tactics are snake case

[Johan Commelin]

check_Mate

[Mario Carneiro]

It's also going to interact weirdly with tactic combinators

[Gabriel Ebner]

Is it any worse than exact, though?

[Mario Carneiro]

Not sure. I wouldn't be surprised if some parsing oddity shows up like with the - block syntax

[Mario Carneiro]

that said, I'm not really too much against the pattern. MM0 has had refine-shortcut exactly like this since the beginning

[Gabriel Ebner]

There is one unfortunate ambiguity though: by rfl

[Mario Carneiro]

luckily rfl means exact rfl in lean 4 so there is no problem

[Gabriel Ebner]

Don't forget about the nondeterministic tactics. :smile: It could also mean exact Iff.rfl.

[Gabriel Ebner]

It also breaks rw [l] at h. :shrug: https://github.com/leanprover-community/mathlib4/pull/71

[Mario Carneiro]

Did you set the priority right? Tactics should always win

[Gabriel Ebner]

I hope so. At least I tried priority := 0 and priority := low and it didn't make a difference.

[Mario Carneiro]

The set of leading tactic tokens is known to the system, right? Can we make a custom parser for "term, but where the first token is not a tactic token"

[Mario Carneiro]

that should also prevent parser issues where a syntactically incorrect tactic backtracks a lot and gets parsed as a term

[Gabriel Ebner]

If I remove the have above, then it works..

[Mario Carneiro]

what does the bad code look like?

[Gabriel Ebner]

lemma implies_of_if_pos {c t e : Prop} [Decidable c] (h : ite c t e) : c → t :=
by intro hc
   have hp : ite c t e = t := if_pos hc
   rwa [hp] at h

[Mario Carneiro]

I think it's treating have as a term

[Gabriel Ebner]

I agree, but I don't know why.

[Mario Carneiro]

it's a longer match?

[Mario Carneiro]

woe is us for making the tactic language look so much like the term language...

[Mac]

Mario Carneiro said:

that should also prevent parser issues where a syntactically incorrect tactic backtracks a lot and gets parsed as a term

:up: I tried a similar strategy in Papyrus. This will cause virtually all tactic syntax errors to turn into very hard to debug term errors. You need some kind of token to enter term mode. I plan on using # in papyrus, and I think it could be a good idea here as well.

[Mario Carneiro]

we already have such a token, it is exact

[Mac]

@Mario Carneiro yes but that, as mentioned, is quite long

[Johan Commelin]

I think I like the # suggestion. Writing ##ℕ for exact cardinal.mk ℕ will look a bit funny, but besides that, I think it's an excellent symbol for the job.

[Mario Carneiro]

I would put a space after it

[Mario Carneiro]

like # #ℕ

[Scott Morrison]

Is % a possibility? We are use foo and foo% as a naming scheme for analogous tactics and term-elaborators, so % is going to have a "this is a term" connotation already.

[Scott Morrison]

Shall we backport the decision to use constructor instead of split to mathlib3? If not, we'll need some special casing in mathport to handle the translation, which seems more trouble than it is worth.

[Alex J. Best]

Can you say a bit more about what special casing is needed? From reading this thread it just sounds like the name split in lean4 is taken by a different tactic, so split should be renamed to something else in Lean 4, but my understanding of the whole mathport process is that there is an automated source to source translation which handles a lot harder things than just simple renames already, is the goal to have no tactic renames in the process?

[Scott Morrison]

I was confused, special casing is trivial: I can (and will shortly) just change https://github.com/leanprover-community/mathport/blob/master/Mathport/Syntax/Translate/Tactic/Lean3.lean#L268 to say

@[trTactic split] def trSplit : TacM Syntax := `(tactic| constructor)

which should do it.

[Scott Morrison]

https://github.com/leanprover-community/mathport/pull/59