mutual recursive induction and def

Stream: new members

[kana]

def f : t -> Type := match ...
inductive t : bool -> Type
| y : t false
| x : forall (a : t) -> f a -> t true

is it possible to define such thing?

[Mario Carneiro]

can you make a #mwe?

[Mario Carneiro]

This is an inductive-recursive type, and the answer is no, at least not directly

[Mario Carneiro]

but it might be possible to refactor the recursive function into an inductive relation, and then you can do it by mutual induction

[Mario Carneiro]

Your sketch doesn't typecheck, because t is not a type but you wrote forall (a : t)

[kana]

It is not mwe, because I don't know how to make it workable

inductive type
| u -- u means type of type
| unit
open type

inductive term : type → Type
| type : type → term u -- injection of types into terms
| tt : term unit
| the : ∀(α : term u), term (from_type α) → term (from_type α)
open term

def from_type : term u → type
| (term.type x) := x
| (term.the _ x) := from_type x

[Mario Carneiro]

You can encode this much using a well-formedness predicate on terms:

inductive type
| u
| unit
open type

inductive term : type → Type
| type : type → term u
| tt : term unit
| the : ∀ (β : type) (α : term u), term β → term u

def from_type : ∀ {α}, term α → option type
| _ (term.type x) := some x
| _ term.tt := none
| _ (term.the β _ _) := some β

def term.wf : ∀ {α}, term α → Prop
| _ (term.the β α x) := from_type x = some β ∧ α.wf ∧ x.wf
| _ (term.type _) := true
| _ term.tt := true

def wfterm (α : type) : Type := { t : term α // t.wf }

[kana]

Thanks!