Equality problems when extending binary operation to n-ary

Stream: new members

[Cosmo Viola]

I'm working with a binary operation on structures that carry both a type and functons with that type as a domain. I'm trying to extend that binary operation to an n-ary operation, but I'm running into dependent type problems when trying to calculate closed forms for the fields of the resulting structure. Here's a minimized example demonstrating the problem:

import Mathlib.Data.Fintype.Basic

structure ex where
  σ : Type
  f : σ → Nat

def prodEx (s1 s2 : ex) : ex where
  σ := s1.σ × s2.σ
  f := fun (σ1, σ2) => s1.f σ1 + s2.f σ2

def prodNEx {n : Nat} (tup : Fin n → ex) : ex :=
  match n with
  | 0 => {σ := PUnit, f := fun _ => 0}
  | 1 => (tup 0)
  | _ + 2 => prodEx (tup 0) (prodNEx (Fin.tail tup))

def prodNTypes {n : Nat} (XArr : Fin n → Type) :=
  match n with
  | 0 => PUnit
  | 1 => XArr 0
  | _ + 2 => (XArr 0) × (prodNTypes (Fin.tail XArr))

theorem prodNExSigma {n : Nat} (tup : Fin (n + 1) → ex) :
    (prodNEx tup).σ = prodNTypes (fun i => (tup i).σ) := by {
  induction n
  case zero =>
    rfl
  case succ n h =>
    simp [prodNEx, prodNTypes, prodEx]
    rw [h]
    aesop
}

def prodNFs {n : Nat} (tupσ : Fin n → Type) (tupF : (i : Fin n) → (tupσ i) → Nat) : (prodNTypes tupσ) → Nat:=
  match n with
  | 0 => fun (_ : PUnit) => 0
  | 1 => (tupF 0)
  | _ + 2 => fun (σ1, σ2) => (tupF 0 σ1) + (prodNFs (Fin.tail tupσ) (Fin.tail tupF) σ2)

theorem prodNExF {n : Nat} (tup : Fin (n + 1) → ex) :
    (prodNEx tup).f = fun σ => prodNFs (fun i => (tup i).σ) (fun i => (tup i).f) (prodNExSigma tup ▸ σ) := by {
  induction n
  case zero =>
    aesop
  case succ =>
    simp [prodNFs]
    sorry
}

The σ field of prodNEx tup is tup 0 × (tup 1 × ...). As far as I can tell, this specific n-ary product isn't well supported in mathlib, so I define prodNTypes, which translates a tuple into one. This allows me to prove a theorem calculating (prodNEx tup).σ. However, to calculate (prodNEx tup).f, we need to translate an element of type (prodNEx tup).σ to type prodNTypes (fun i => (tup i).σ). As a result, in the succ case of prodNExF, we end up matching on an equality proof, and I'm unsure of how to make progress. I know that in general working with equalities of types is painful. Is there a good way to prove these goals in Lean? I know in many cases it's recommended to use isomorphisms instead of equalities, such as with Fin.cast. Should I be constructing an isomorphism between these types and using that instead of the equality I prove?

[Eric Paul]

This might not be helpful, but using split lets you make progress on the match. Things still do seem difficult to work with.

theorem prodNExF {n : Nat} (tup : Fin (n + 1) → ex) :
    (prodNEx tup).f = fun σ => prodNFs (fun i => (tup i).σ) (fun i => (tup i).f) (prodNExSigma tup ▸ σ) := by
  induction n
  case zero =>
    aesop
  case succ n ih =>
    simp [prodNFs]
    ext z
    split
    rename_i a b c d
    simp [prodNEx, prodEx, ih]
    sorry