Long match of `Sum`s

Stream: lean4

[Bolton Bailey]

I have the following code matching a type constructed from a lot of Sums

def crsElemsI (idx : Unit ⊕ Unit ⊕ Unit ⊕ Fin n_var ⊕ Fin (n_var - 1) ⊕ Fin n_stmt ⊕ Fin n_wit) : Nat :=
  match idx with
    | Sum.inl _ => 0
    | Sum.inr (Sum.inl _) => 1
    | Sum.inr (Sum.inr (Sum.inl _)) => 2
    | Sum.inr (Sum.inr (Sum.inr (Sum.inl _))) => 3
    | Sum.inr (Sum.inr (Sum.inr (Sum.inr (Sum.inl i)))) => i
    | Sum.inr (Sum.inr (Sum.inr (Sum.inr (Sum.inr (Sum.inl _))))) => 17
    | Sum.inr (Sum.inr (Sum.inr (Sum.inr (Sum.inr (Sum.inr i))))) => i

Is there any way to write this without quadratically many characters in the number of ⊕? Or a way of generating the cases automatically?

[Damiano Testa]

How do you choose the output? Why does it change from being the number of inr to something else?

[Bolton Bailey]

The output for each case is a particular hard coded value set by the protocol I am analyzing. I currently am defining a type using this sequence of Sums so that I can capture this particular index space of 3 + n_var + (n_var-1) + n_stmt + n_wit values. I could make this just a list of this length, but then it will be more complicated to map which index corresponds to which index of the list.

[Bolton Bailey]

Basically , the adversary is allowed to provide a vector of this length 3 + n_var + (n_var-1) + n_stmt + n_wit, and so I would like to provide a type for vectors of this length, while still respecting the structure of which elements of the vector are conceptually grouped together.

[Bolton Bailey]

Damiano Testa said:

How do you choose the output? Why does it change from being the number of inr to something else?

What I wrote above is not my actual example, this is an MWE designed to import as little as possible. In reality the output type should be a type of MVPolynomials. The critical thing is that it's different for each case, and potentially depends on the subindex i

[Eric Wieser]

Is there any way to write this without quadratically many characters in the number of ⊕?

Yes, nest matches linearly

[Eric Wieser]

def crsElemsI  : Unit ⊕ Unit ⊕ Unit ⊕ Fin n_var ⊕ Fin (n_var - 1) ⊕ Fin n_stmt ⊕ Fin n_wit → Nat :=
  Sum.elim (fun _ => 0) <|
  Sum.elim (fun _ => 1) <|
  Sum.elim (fun _ => 2) <|
  Sum.elim (fun _ => 3) <|
  Sum.elim (fun _ => 1) <|
  Sum.elim (fun _ => 17) <| fun i => i

[Bolton Bailey]

Eric Wieser said:

Is there any way to write this without quadratically many characters in the number of ⊕?

Yes, nest matches linearly

Good point. I suppose I thought the technically-styled version of that would indent each line once more than the last and use a quadratic number of whitespace characters, but this version looks very nice!