Stream: general

Topic: structure bug?

François G. Dorais (Feb 10 2019 at 20:22):

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 (Feb 10 2019 at 20:41):

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 (Feb 10 2019 at 20:41):

What is the theorem you want?

François G. Dorais (Feb 10 2019 at 20:45):

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 (Feb 10 2019 at 20:47):

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

Kevin Buzzard (Feb 10 2019 at 20:47):

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

Oh!

Rob Lewis (Feb 10 2019 at 20:49):

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 (Feb 10 2019 at 20:49):

The structure itself fails to compile!

Kevin Buzzard (Feb 10 2019 at 20:49):

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

Kevin Buzzard (Feb 10 2019 at 20:50):

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 (Feb 10 2019 at 20:51):

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

Kevin Buzzard (Feb 10 2019 at 21:08):

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


François G. Dorais (Feb 10 2019 at 21:18):

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 (Feb 10 2019 at 21:25):

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.

Last updated: May 14 2021 at 12:18 UTC