Mutually recursive inductive types

Stream: new members

[Sam Stites]

Hi all,
I'm trying to use Lean to do some language design and experimentation.

I'm just starting with an untyped lambda calculus which looks a little like:

constants (real : Type)

structure var := (Var : string)
structure fn  := (Fn : string)

inductive primval : Type
  | Real : real → primval
  | Bool : bool → primval
  | MyList : list myexpr → primval

inductive primop : Type
  | Op : string → primop

  -- number ops
  | Mul : primop
  | Sub : primop
  | Div : primop
  | Add : primop
  | GT : primop
  | LT  : primop

  -- bool ops
  | Or  : primop
  | And  : primop

inductive myexpr : Type
  | Primval : primval → myexpr
  | Primop : primop → myexpr
  | Let : var → myexpr → myexpr → myexpr
  | V : var → myexpr
  | F : fn → myexpr
  | If (pred : myexpr) : myexpr → myexpr → myexpr
  | Lambda (vs : list var) (body : myexpr)
  | App (op : myexpr) (args : list myexpr)

Unfortunately, MyList : list myexpr → primval doesn't have myexpr in scope -- I guess lean doesn't hoist definitions?

How would you go about doing this? Alternatively, is a resource on writing embedded DSLs in lean?

Oh, also, where is real?

[Kenny Lau]

```lean
[code goes here]
```

[Kenny Lau]

import data.real.basic

[Kenny Lau]

you can have mutual inductive types

[Reid Barton]

In this case, though, the path of least resistance is most likely to "inline" primval into myexpr, given that you use it only once

[Reid Barton]

(A list of any-values-whatsoever isn't so "primitive" anyways, is it?)

[Sam Stites]

Thanks @Kenny Lau! Am I doing something wrong here, then? This example fails to compile.

@Reid Barton I can't inline as I'm aiming for something slightly more complex.

[Reid Barton]

Check the section of TPIL on mutual inductive types

[Kevin Buzzard]

https://leanprover.github.io/theorem_proving_in_lean/induction_and_recursion.html#mutual-recursion

[Reid Barton]

they have their own syntax, and they are handled by translation into an indexed inductive type so they are less pleasant to handle

[Kevin Buzzard]

and https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html#mutual-and-nested-inductive-types

[Sam Stites]

Perfect! Thank you!

[Reid Barton]

don't say you weren't warned :smiling_devil:

[Jannis Limperg]

Not long ago, I asked @Gabriel Ebner a question about some mutual inductives and his answer was something along the lines of, "don't ever use them, they don't work". In that spirit: Has anyone actually used mutual inductives successfully?

[Reid Barton]

(At a high level, the situation is: the Lean kernel does not support mutually inductive types; so either you have to use mutual or manage the translation yourself, each with its own downsides)

[Reid Barton]

Apparently there is exactly one use in mathlib, in a file I've never looked at

[Reid Barton]

oh but they are mutually inductive Props, which probably makes life simpler

[Reid Barton]

Maybe they are usable if you only care about programming and not proving?

[Reid Barton]

Heh, these search results are also representative I think: https://github.com/flypitch/flypitch/search?q=mutual&unscoped_q=mutual

[Sam Stites]

Ultimately, I'm hoping to formally verify some DSLs so hopefully these don't fall apart too fast

[Reid Barton]

One use in a subdirectory old/, and a comment in the real code explaining that they are not convenient

[Scott Morrison]

Every attempt I've made to use them has worked at first, and them quickly led to despair (usually the definitional equations not being usable for some reason), and me asking the experts here "how do I write this without mutual inductives"?