Mutual records + inductives

Stream: lean4

[Siddharth Bhat]

I would like to be able to write definitions where we have mutual dependences between records and inductives, which lean does not allow today/ An example is:

mutual

-- | allow structures in mutual inductive blocks.
structure Foo where
  int: Int
  bar: Bar

inductive Bar where
| mk: Bar
| foo: Foo -> Bar
end


#print Foo
#print Bar
def fooBar : Foo := { int := 0, bar := (Bar.mk) }
#check fooBar

I have a patch here that extends Lean4's logic of elaborating mutual definitions to produce the output:

inductive Foo.{u_1} : Type u_1
number of parameters: 0
constructors:
Foo.mk : Int → Bar → Foo

inductive Bar.{u_1} : Type u_1
number of parameters: 0
constructors:
Bar.mk : Bar
Bar.foo : {Foo : Sort u_1} → Foo → Bar

fooBar : Foo

However, the implementation seems to fail on some tests (as noted in the comment: https://github.com/bollu/lean4/pull/6#issuecomment-1136566982). I would love to have some help to getting this bug-fixed. Unfortunately, I'm not sure what the source of the problem is. I'm hoping those with more familiarity of the compiler internals could help, so I can make this a real PR against lean4!

[Arthur Paulino]

@Siddharth Bhat this is related: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/mutual.20inductive.20and.20structure

[Sebastian Ullrich]

@Siddharth Bhat I think you are severely underestimating the complexity of this issue. Simply elaborating all inductives of the mutual block followed by each structure (separately), as you are doing right now, will not work. You would need to put everything together into a single declaration of mutual inductives, which would presumably require significant changes in the structure elaboration code.

[Sebastian Ullrich]

Bar.foo : {Foo : Sort u_1} → Foo → Bar

Note that Foo was auto-quantified here, the types are not actually mutually dependent

[Siddharth Bhat]

Ah, thanks! :)