Tactic to strip names of current goal

Stream: Is there code for X?

[Ayhon]

I like using case _ => to handle disjunctions in my proofs. However, sometimes tactics like apply introduce extra names to the main goal, even when there is only one goal resulting from the application. Is there a way to strip these?

For instance

example (f: Nat → Nat)
  (f_inj: ∀ {x y}, f x = f y → x = y)
  (a b : Nat)
: a = b
:= by
  apply f_inj
  -- The goal is now named `a`
  sorry

[Ayhon]

This is annoying because then, for instance, tactics like split prepend this name to the cases produced, and you need to specify it when using case.

example (f: Nat → Nat)
  (f_inj: ∀ {x y}, f x = f y → x = y)
  (a b : Nat)(cond: Bool)
: (if cond then a else a) = b
:= by
  apply f_inj
  split
  case isTrue h => sorry -- Complains that there is no `isTrue` case, but `a.isTrue` exists.
  case isFalse h => sorry

[Edward van de Meent]

you could use a focussing dot instead, right?

[Ayhon]

Yes, but then I lose the ability to name the hypothesis introduced different names (admittedly, not what happens in my current example)

[Ayhon]

I also like the idea of having the names of the different cases made explicit, but that's just what I'm used to, not sure if it's idiomatic or not.

[Edward van de Meent]

ah, i misunderstood your question. it's not that goals get names, and you want to remove the names so that case _ => matches it (presuming that that only matches "unnamed" goals, which isn't the case). Instead it is that if your goal is named foo and a tactic expands it to foo.bar, case bar => fails

[Ayhon]

Edward van de Meent said:

if your goal is named foo and a tactic expands it to foo.bar, case bar => fails

Precisely

[Ayhon]

More generally, I've observed that with custom tactics which apply a bunch of lemmas, the name of the goal ends up being quite complicated.

[Edward van de Meent]

i suppose maybe it could be considered useful if case foo => matches any some_namespaces.foo instead

[Mario Carneiro]

My recollection of @Kyle Miller 's explanation of the behavior of case is that it should work here even if the name of the goal is a.isTrue and the case says isTrue

[Mario Carneiro]

it already looks for prefixes and suffixes of the provided name

[Ayhon]

My latest code snippet shows that an error happens:

Case tag 'isTrue' not found.

Available tags:
  'a.isTrue._@.external:file:///project/mathlib-demo.lean._hyg.11',
  'a.isFalse._@.external:file:///project/mathlib-demo.lean._hyg.11'

[Mario Carneiro]

oh but what is that external thing?

[Ayhon]

:shrug:

[Ayhon]

Maybe it's another issue then
image.png

[Mario Carneiro]

and why is there a URL in the name :astonished:

[Ayhon]

In "Mathlib stable" it doesn't show the URL
image.png

[Edward van de Meent]

i imagine that's to do with how the live.lean environment is setup?

[Ayhon]

Edward van de Meent said:

i imagine that's to do with how the live.lean environment is setup?

At least it's also related to Mathlib or Lean versions, since changing the mode in the selector makes the URL go away.

[Mario Carneiro]

On my local test setup I get:

Available tags: 'a.isTrue._@.Mathlib.Test._hyg.11', 'a.isFalse._@.Mathlib.Test._hyg.11'

so it doesn't matter too much, I think the middle section is the name of the current module and the live.lean setup is setting it to a URL which is fine but weird

[Ayhon]

But then, it's failing because this name is being introduced by a tactic, and therefore the actual "relevant" part of the name is hidden by the hygenic suffix?

Doesn't make sense though, I see a call to eraseMacroScopes in getCaseGoals

[Mario Carneiro]

I think the problem is that the name of the goal after apply is not a, it is a hygienic a, which has a as a prefix which is why case a works, but appending isTrue to it results in a hygienic a.isTrue and now isTrue is neither prefix nor suffix of the true name of the goal

[Mario Carneiro]

Ayhon said:

Doesn't make sense though, I see a call to eraseMacroScopes in getCaseGoals

That's only on the needle, not the haystack

[Ayhon]

Yes, I see

[Ayhon]

A possible fix would then be changing findTag? to the following

private def findTag? (mvarIds : List MVarId) (tag : Name) : TacticM (Option MVarId) := do
  match (← mvarIds.findM? fun mvarId => return tag == (← mvarId.getDecl).userName.eraseMacroScopes) with
  | some mvarId => return mvarId
  | none =>
  match (← mvarIds.findM? fun mvarId => return tag.isSuffixOf (← mvarId.getDecl).userName.eraseMacroScopes) with
  | some mvarId => return mvarId
  | none => mvarIds.findM? fun mvarId => return tag.isPrefixOf (← mvarId.getDecl).userName.eraseMacroScopes

or, well, since eraseMacroScopes doesn't seem to be a free operation, cache that before potentially traversing it 3 times, idk.

[Ayhon]

In the meantime it seems like doing refine f_inj ?_ doesn't give a new name to the goal.

[Aaron Liu]

I guess you could refine ?my.better.goal.name

[Ayhon]

Aaron Liu said:

I guess you could refine ?my.better.goal.name

Yes, but that doesn't allow me to choose "unnamed", I don't think. refine ?_ results in x

[Ayhon]

Admitedly, it's interesting that apply f_inj; refine ?_ does not have the same behaviour as refine f_inj ?_.

[Aaron Liu]

There should be a way to clear the goal name

[Aaron Liu]

import Lean

/--
Replaces the tag of the main goal by `[anonymous]`.
-/
elab (name := clearGoalName) "clear_goal_name" : tactic => do
  let goal ← Lean.Elab.Tactic.getMainGoal
  goal.setTag .anonymous