Nested pair types

Stream: lean4

[Wrenna Robson]

I have these somewhat cursed definitions.

abbrev PairRec (α : Type u) : ℕ → Type u
  | 0 => α
  | (n + 1) => PairRec α n × PairRec α n

instance instPairRecRepr [h : Repr α] : (n : ℕ) → Repr (PairRec α n)
  | 0 => h
  | (n + 1) => haveI := (instPairRecRepr n) ; inferInstance

abbrev SigmaPairRec (α : Type u) := (n : ℕ) × PairRec α n

What is a more idiomatic way to achieve the same thing? Essentially given a type α, I want to define the type which consists of: α, pairs in α × α, pairs in (α × α) × (α × α), and so on. Ideally I would not need to define a representation instance for this, it would derive all the obvious things in the obvious way.

[Kyle Miller]

Do you need it to be literally nested Prods? Defining a new inductive type is nice, except for the instances you might want to inherit from Prod.

inductive PairRec (α : Type u) : ℕ → Type u where
  | leaf : α → PairRec α 0
  | pair {n : Nat} (left right : PairRec α n) : PairRec α (n + 1)
  deriving Repr

(Do you need to define that Repr instance for your type? Locally, I'm not seeing that you do.)

[Wrenna Robson]

Well it's just convenient, and I wasn't successfully deriving it.

[Wrenna Robson]

I think your definition there is exactly equivalent to "type of perfect binary trees of level n", which makes sense as that's really what these nested pairs are in context.

[Wrenna Robson]

I was prototyping in Lean but unfortunately I really need to implement them in EasyCrypt which has a less expressive type system, so I don't think it will admit such a definition.