Zulip Chat Archive

Stream: new members

Topic: unfolding repeating Pi


view this post on Zulip Jesse Michael Han (Sep 21 2018 at 15:11):

hello everyone! i'm trying to define the following inductive datatype:

constant A : Π n : nat, Type

inductive hewwo : Type
  | base : nat  hewwo
  | apply : Π n, A n  sorry

where the intended type of apply n f is hewwo → ... → hewwo, repeated n + 1 times.

I defined the following function:

definition repeat_Pi :   Type u  Type (u + 1)
  | 0 A := A
  | (nat.succ n) A := Π A, repeat_Pi n A

but Lean complains that the following:

inductive hewwo : Type
  | base : nat  hewwo
  | apply : Π n, A n  repeat_Pi n hewwo

(rightly) has an incorrect return type for hewwo.apply.

Is there a way to get Lean to treat repeat_Pi k A as being equal to A -> ... -> A?

(edit: got rid of punit and shifted indexing down by 1)

view this post on Zulip Simon Hudon (Sep 21 2018 at 19:46):

Is it intended that in:

...
  | (nat.succ n) A := Π A, repeat_Pi n A

you ignore A that you get as a parameter?

view this post on Zulip Simon Hudon (Sep 21 2018 at 19:49):

Sorry, that doesn't fix the issue.

You may need to reflect the repetition into the definition of hewwo:

inductive hewwo : nat  Type
  | base : nat  hewwo 0
  | apply (n) : A n  hewwo n  hewwo (succ n)

view this post on Zulip Reid Barton (Sep 21 2018 at 20:37):

@Jesse Michael Han I would just use the uncurried \Pi n, A n -> (fin n -> hewwo) -> hewwo instead.
I don't think you can do the thing you were trying to do.


Last updated: May 14 2021 at 13:24 UTC