mutual inductive and structure

Stream: lean4

[Arthur Paulino]

Are there plans (or is it even possible) to allow mutual declaration of inductive types and structures in the same block?

Something like this:

mutual
  inductive Foo
  | bar : Bar → Foo

  structure Bar where
    foo : Foo
end

[Chris B]

The example looks like it violates the rule that structures can't be recursive.

[Chris B]

I think you have to make Bar just a vanilla (mutual) inductive.

[Gabriel Barreto]

Aren't structures morally equivalent to inductives of a single constructor?

At any rate, there's an equivalent and valid definition

structure Bar (Foo : Type) where
  foo : Foo

inductive Foo
| bar : Bar Foo → Foo

which is a bit weird to me, since this sort of nesting is justified because it is equivalent to a mutual block, which in turn is equivalent, with a bit of cleverness, to a single inductive family, so these are all conservative extensions of the language. It seems like there's a mismatch in this case

[Chris B]

Gabriel Barreto said:

Aren't structures morally equivalent to inductives of a single constructor?

I guess it depends on how you define moral equivalence; the "not recursive" proviso is the other half of what makes a structure. The kernel has special support for structure projections and structures add inheritance into the mix via extends, so there are some concrete differences.

[Marcus Rossel]

@Gabriel Barreto
For example:

inductive A : Prop
  | intro (n : Nat) (h: n > 0) : A

... will work, but:

structure A : Prop where
  n : Nat
  h : n > 0

... would try to create a projection for n which it can't because that would escape Prop.