Dead names

Stream: mathlib4

[Patrick Massot]

I'm really glad Lean 4 doesn't let us use auto-generated names. This will make porting to Lean 5 much easier. I'm porting algebra.ring_quot and it's full of proof by induction using auto-generated names and this is a royal pain for porting (of course auto-generated names in Lean 4 are not only inaccessible, they are also different from the Lean 3 ones).

[Patrick Massot]

I have a question about Lean 4 induction tactic actually. How do you use induction foo with when constructors have implicit arguments?

[Jireh Loreaux]

Does @constructor_name not work?

[Patrick Massot]

In the case at hand I have

inductive Rel (r : R → R → Prop) : R → R → Prop
  | of ⦃x y : R⦄ (h : r x y) : Rel r x y
  | add_left ⦃a b c⦄ : Rel r a b → Rel r (a + c) (b + c)
  | mul_left ⦃a b c⦄ : Rel r a b → Rel r (a * c) (b * c)
  | mul_right ⦃a b c⦄ : Rel r b c → Rel r (a * b) (a * c)

And given h : Rel r a b, starting with

induction h with
  | of h' =>

doesn't let me specify more than one argument after or, but I clearly need more.

[Patrick Massot]

Thanks Jireh!

[Patrick Massot]

It makes sense in hindsight.

[Jireh Loreaux]

Indeed, but it's not the kind of thing we had in Lean 3, so I understand. When I first found I could do that I was very excited.

[Eric Wieser]

Patrick Massot said:

it's full of proof by induction using auto-generated names

Could you point to where this happens in the lean3 file?

[Jireh Loreaux]

things like @fun x y h => ... work also when the expected type is ∀ {x y} (h), ...

[Patrick Massot]

Eric, the proof I'm doing right now is https://github.com/leanprover-community/mathlib/blob/master/src/algebra/ring_quot.lean#L395-L403

[Patrick Massot]

There you can see things like h_h or h_ih...

[Patrick Massot]

But really, I didn't mean to shame whoever wrote this.

[Patrick Massot]

My point was really that Lean 4 is right here.

[Eric Wieser]

I just wanted to check that person who wrote it was me a long time ago and not a more recent me who should know better (it looks like those lines are mine, but thankfully old).

[Eric Wieser]

I blame the fact the the old induction tactic made it super annoying to name all the hypotheses because you couldn't group them by goal without the rarely-used case tactic (another point for Lean4)