Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: No-confusion for generalised inductive types

Jannis Limperg (Sep 13 2020 at 12:32):

For generalised (nested or mutual) inductive types, Lean apparently does not generate the associated no-confusion principle. However, it seems like I can get around this by reducing an equation C = D, where C and D are different constructors of the generalised inductive type, to an equation C' = D' between constructors of the type that the kernel sees. Then I can apply that type's no-confusion principle.

Can anyone confirm or deny that this construction is sound?

Jannis Limperg (Sep 13 2020 at 12:35):

Example:

inductive rose : Type
| tip : rose
| node : list rose → rose

#print rose.no_confusion -- does not exist

#print _nest_1_1._nest_1_1.rose._mut_.no_confusion -- does exist

example (rs : list rose) (h : rose.tip = rose.node rs) : false :=
begin
  refine _nest_1_1._nest_1_1.rose._mut_.no_confusion h
end

Mario Carneiro (Sep 13 2020 at 14:13):

What do you mean? Of course the theorem is true, or else it wouldn't be a proper definition of the generalized inductive type in the first place

Mario Carneiro (Sep 13 2020 at 14:14):

but the framework doesn't prove the theorem because it wasn't implemented

Mario Carneiro (Sep 13 2020 at 14:15):

plus, you just proved it so you should have some reasonable confidence that the theorem is true :)

Jannis Limperg (Sep 13 2020 at 14:23):

The question is, given any generalised inductive type I and equation C = D : I with C and D different constructors of I, can I use the following tactic to prove false:

  • Unfold C until I get a constructor of some non-generalised inductive type J (which internally represents I).
  • Apply J's no-confusion lemma.

This seems to work on the examples, but I don't know much about the translation so I'm not sure if this method always succeeds.

Mario Carneiro (Sep 13 2020 at 14:23):

I think you can just skip to step 2

Mario Carneiro (Sep 13 2020 at 14:24):

This will work as long as you are only proving distinct constructors distinct

Mario Carneiro (Sep 13 2020 at 14:24):

proving injectivity is more complicated

Jannis Limperg (Sep 13 2020 at 14:25):

All right, thanks! Injectivity lemmas for the constructors of generalised inductives are provided by Lean, so I'm good on that front.

Mario Carneiro (Sep 13 2020 at 14:25):

The real front end no_confusion should support both cases

Last updated: Dec 20 2023 at 11:08 UTC