Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: No-confusion for generalised inductive types


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 13 2020 at 14:14):

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

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Sep 13 2020 at 14:23):

I think you can just skip to step 2

view this post on Zulip Mario Carneiro (Sep 13 2020 at 14:24):

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

view this post on Zulip Mario Carneiro (Sep 13 2020 at 14:24):

proving injectivity is more complicated

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Sep 13 2020 at 14:25):

The real front end no_confusion should support both cases


Last updated: May 09 2021 at 22:13 UTC