# 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: May 09 2021 at 22:13 UTC