structure bug?

Stream: general

[François G. Dorais]

This fails to generate foo.mk.inj_eq:

structure foo {α : Type} (β : α → α → Type) := (bar : Π (a : α), β a a)

Seems like a bug to me. Any thoughts on a workaround?

Also, is it still good form to report bugs on the leanprover/lean Github? They're unlikely to get fixed until Lean 4 but there could be some use in reporting them.

PS: This is a MWE so def foo.bar {α : Type} (β : α → α → Type) := Π (a : α), β a a won't do for my use case.

[Kevin Buzzard]

I don't know the rules for what is guaranteed to be generated. If you get rec then you can make everything else yourself. I think there is very little point filling a bug, it won't be fixed in Lean 3 and Lean 4 is a complete rewrite

[Kevin Buzzard]

What is the theorem you want?

[François G. Dorais]

I want the structure itself. *.mk.inj_eq is an internal thing. I don't know how essential it is but I don't know how to prevent lean from trying to generate it.

[Kevin Buzzard]

I don't understand this question at all. I'm looking through the source code for any mention of mk.inj_eq

[Kevin Buzzard]

I see sigma.mk.inj_eq but that is defined in the code base

[Kevin Buzzard]

Oh!

[Rob Lewis]

That's an odd one. This works, but I have no idea why.

structure foo' {α : Type} (β : α → α → Type)
structure foo {α : Type} (β : α → α → Type) extends foo' β :=
(bar : Π (a : α), β a a)

[Kevin Buzzard]

The structure itself fails to compile!

[Kevin Buzzard]

I thought you were just complaining that an auxiliary lemma was not generated.

[Kevin Buzzard]

structure foo {α : Type} (β : α → α → Type) := (bar : Π (a : α), β a a) -- error
/-
failed to generate auxiliary lemma 'foo.mk.inj_eq'
nested exception message:
assumption tactic failed
state:
α : Type,
β : α → α → Type,
bar bar_1 : Π (a : α), β a a,
h : {bar := bar} = {bar := bar_1}
⊢ {bar := bar} = {bar := bar_1}
-/

[Kevin Buzzard]

man, that assumption tactic looked like it was going to work fine.

[Kevin Buzzard]

class foo {α : Type} (β : α → α → Type) := (bar : Π (a : α), β a a) -- works fine ;-)

[François G. Dorais]

Yep, it's disabled for classes, I just found this comment in lean/src/library/constructions/injective.h:

Generate injectivity lemmas *.inj, *.inj_arrow and *.inj_eq.
If gen_inj_eq is false, then *.inj_eq lemma is not generated.
The *.inj_eq lemma is used by the simplifier.
We don't generate it for classes because they can be expensive to generate and are rarely used in this case.

The bug is too deep in the code for me to figure out what's going on but I'd love to hear about it if someone knows.

@Rob Lewis Thanks! That's easier than I had imagined it would be.

[Rob Lewis]

The problem isn't specific to the structure command at all.

inductive  foo' {α : Type} (β : α → α → Type)
| mk : (Π (a : α), β a a) → foo'

The tactic that (I think) is failing is actually implemented in Lean. (https://github.com/leanprover/lean/blob/master/library/init/meta/interactive.lean#L1610) In principle one could poke around there and see what's going on. It's a little late for me to start messing with core though.