Zulip Chat Archive

Stream: lean4

Topic: subscript uparrow


view this post on Zulip Jason Gross (Mar 05 2021 at 22:37):

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

view this post on Zulip Bryan Gin-ge Chen (Mar 05 2021 at 22:41):

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

view this post on Zulip Jason Gross (Mar 05 2021 at 22:46):

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...

view this post on Zulip Sebastian Ullrich (Mar 05 2021 at 22:56):

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...

view this post on Zulip Brandon Brown (May 05 2021 at 01:13):

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?

view this post on Zulip Brandon Brown (May 05 2021 at 01:27):

(deleted)

view this post on Zulip Sebastian Ullrich (May 05 2021 at 06:33):

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).

view this post on Zulip Sebastian Ullrich (May 05 2021 at 06:34):

The alternative we did not mention in the course is

set_option tactic.hygienic false

as well as the unhygienic tactic combinator


Last updated: May 18 2021 at 23:14 UTC