subscript uparrow

Stream: lean4

[Jason Gross]

What does the purple subscript uparrow mean? (Apparently it's \textdied in Lean input mode...)
image.png

[Bryan Gin-ge Chen]

It's a cross: :cross:️. Those indicate names which are inaccessible by the user. See e.g. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Come.20on/near/226307180

[Jason Gross]

Thanks. The name isn't inaccessible to the user, though, it just doesn't exist in the context where Lean is performing unification, I think...

[Sebastian Ullrich]

The binding of the motive Gamma was inserted implicitly and is therefore inaccessible. Not sure about the unification error itself, it's too late for that here...

[Brandon Brown]

I'm having a similar issue with the cross, trying to prove the following (MWE):

inductive int where
| zero : int
| succ : int → int
| pred : int → int

protected def int.norm (a : int) : int :=
match a with
| int.zero => int.zero
| int.succ (int.pred a) => int.norm a
| int.pred (int.succ a) => int.norm a
| int.succ a => int.succ (int.norm a)
| int.pred a => int.pred (int.norm a)

#reduce int.zero |> int.succ |> int.pred |> int.succ |> int.pred |> int.norm
def intn := {x : int // x = (int.norm x)}

example (a : int): int.norm (int.succ a) = int.norm (int.norm (int.succ a)) := by
  induction a
  rfl

/- Tactic State:
case succ
a✝ : int
v_0✝ : int.norm (int.succ a✝) = int.norm (int.norm (int.succ a✝))
⊢ int.norm (int.succ (int.succ a✝)) = int.norm (int.norm (int.succ (int.succ a✝)))
-/

How I am supposed to prove this without having the variables accessible?

[Brandon Brown]

(deleted)

[Sebastian Ullrich]

See https://raw.githubusercontent.com/IPDSnelting/tba-2021/master/slides/lecture4.pdf#page=26, last slide and preceding slides. You can name them using either induction-with or case (recent nightly).

[Sebastian Ullrich]

The alternative we did not mention in the course is

set_option tactic.hygienic false

as well as the unhygienic tactic combinator