Zulip Chat Archive

Stream: new members

Topic: mutual recursive induction and def


view this post on Zulip kana (Mar 19 2021 at 22:34):

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?

view this post on Zulip Mario Carneiro (Mar 19 2021 at 22:36):

can you make a #mwe?

view this post on Zulip Mario Carneiro (Mar 19 2021 at 22:37):

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

view this post on Zulip Mario Carneiro (Mar 19 2021 at 22:37):

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

view this post on Zulip Mario Carneiro (Mar 19 2021 at 22:39):

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

view this post on Zulip kana (Mar 19 2021 at 22:43):

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

view this post on Zulip Mario Carneiro (Mar 19 2021 at 22:53):

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 }

view this post on Zulip kana (Mar 19 2021 at 23:13):

Thanks!


Last updated: May 08 2021 at 04:14 UTC