Zulip Chat Archive

Stream: general

Topic: nested inductive type


view this post on Zulip Björn Fischer (Apr 29 2019 at 09:17):

Is it possible to define a nested inductive type on a vector-like structure instead of lists?

inductive expression : Type
| a {dim : } (idx : vector (expression) dim) /- omitted constraints on dim -/ : expression
| b : expression

I get the following error: nested occurrence [...] contains variables that are not parameters.

view this post on Zulip Chris Hughes (Apr 29 2019 at 09:21):

I think this is an inductive recursive type, since it depends on the length function for lists. I don't think this is possible.

view this post on Zulip Mario Carneiro (Apr 29 2019 at 09:33):

This isn't an inductive recursive, but it's not a supported nested inductive. The easiest solution is to use fin dim -> expression instead of vector expression dim

view this post on Zulip Björn Fischer (Apr 29 2019 at 11:21):

That works. Thanks!

view this post on Zulip Björn Fischer (May 14 2019 at 13:49):

Follow up question:
If I want to define a recursive function over expressions like so:

def f : expression -> N
| (a idx) := 1 + ((vector.of_fn idx).map f).sum
| b ...
using_well_founded {rel_tac := λ_ _, `[exact ⟨_, measure_wf (λ e, expression_size e)] }

I have to proof that the function application is decreasing for some arbitrary expression e, i.e. expression_size e < expression_size (a idx). However I don't have a proof that e comes from idx, ergo I cannot proof it.
The only way around that I can think of is to use the recursor directly. Is there a more convenient way?
(I left out some details, expression is actually indexed over types)

view this post on Zulip Chris Hughes (May 14 2019 at 15:30):

This is probably easier to define using expression.rec_on

def f (e : expression) :  :=
expression.rec_on e
  (λ n idx f,  (vector.of_fn f).1.sum + 1)
  _

Last updated: May 10 2021 at 16:20 UTC