induction fails

Stream: general

[Violeta Hernández]

Here's something weird I found. If you make an alias of list.perm.rec_on, theinduction tactic suddenly complains about it.

import data.list.perm

alias list.perm.rec_on ← list.perm.rec_on'

-- Works
example {α} {l₁ l₂ : list α} (h : l₁ ~ l₂) : true :=
by induction h using list.perm.rec_on; trivial

-- invalid user defined recursor, type of the major premise 'ᾰ' does not contain the recursor index 'ᾰ'
example {α} {l₁ l₂ : list α} (h : l₁ ~ l₂) : true :=
by induction h using list.perm.rec_on'; trivial

[David Renshaw]

I wonder if this has to do with @[elab_as_eliminator]

[Violeta Hernández]

Something similar happens with relation.trans_gen.rec_on.

import logic.relation

alias relation.trans_gen.rec_on ← relation.trans_gen.rec_on'

-- Works
example {α} {x y : α} {r : α → α → Prop} (h : relation.trans_gen r x y) : true :=
by induction h using relation.trans_gen.rec_on; trivial

-- invalid user defined recursor, type of the major premise 'ᾰ' must be for the form (I ...), where I is a constant
example {α} {x y : α} {r : α → α → Prop} (h : relation.trans_gen r x y) : true :=
by induction h using relation.trans_gen.rec_on'; trivial

[David Renshaw]

hm... attribute [elab_as_eliminator] list.perm.rec_on' does not seem to help.

[Violeta Hernández]

@Mario Carneiro might have an idea of what's going on

[Mario Carneiro]

induction using doesn't really work in lean 3, you should just use refine

[Mario Carneiro]

but you should make an issue to track it since it's hard to remember whhat goes wrong

[Violeta Hernández]

Would it be worthwhile to kill induction using in mathlib?

[Violeta Hernández]

I wanted to test out redefining list.perm as the transitive closure of the "at most one swap" relation, which gives a more general induction principle, but this change causes more trouble than it would otherwise due to induction using now failing...

[Ruben Van de Velde]

It works perfectly well in nearly all cases, in my experience

[Violeta Hernández]

I thought that as well, but I've found a total of three fail cases in the past two or so weeks

[Eric Wieser]

Does alias even work well for data? I thought we only ever used it for theorems

[Mario Carneiro]

it works fine for def and theorem, not so much for inductive

[Mario Carneiro]

well, for def it probably won't copy the definitional equation, resulting in poor rw behavior