confused about equality of type indices

Stream: lean4

[Jesse Slater]

I am working with heterogeneous lists and I am confused about when an HList parametrized by a List l can be coerced to be parametrized by l' = l. I don't understand why cons_split_snd is a problem when cons_split_fst and cons_split_snd' are fine. Is there a way I can get cons_split_snd to work without the let?

inductive HList {α : Type} (β : α → Type) : List α → Type
  | nil : HList β []
  | cons : β a → HList β as → HList β (a::as)

def HList.split (bs : HList β (las ++ ras)) : HList β las × HList β ras :=
  match las, bs with
  | [], rbs => (nil, rbs)
  | _ :: _, cons b bs => bs.split.map (cons b ·) id

theorem HList.cons_split_fst
  {α : Type} {a : α} {β : α → Type} {b : β a} {las ras : List α} {bs : HList β (las ++ ras)}
  : (cons b bs).split.fst = cons b bs.split.fst := by -- works
  rfl

theorem HList.cons_split_snd
  {α : Type} {a : α} {β : α → Type} {b : β a} {las ras : List α} {bs : HList β (las ++ ras)}
  : (cons b bs).split.snd = bs.split.snd := by -- application type mismatch
  rfl

theorem HList.cons_split_snd'
  {α : Type} {a : α} {β : α → Type} {b : β a} {las ras : List α} {bs : HList β (las ++ ras)}
  : let bs' : HList β ((a :: las) ++ ras) := cons b bs
    bs'.split.snd = bs.split.snd := by -- works
    rfl

[Jesse Slater]

Somewhat related follow up: I want to prove HList append is associative. My understanding is that since (a ++ b ++ c) is not definitionally equal to (a ++ (b ++ c)) for lists, HList.append_assoc requires a cast, which is not ideal. Is there any way to avoid the cast?

inductive HList {α : Type} (β : α → Type) : List α → Type
  | nil : HList β []
  | cons : β a → HList β as → HList β (a::as)
infixr:67 " ::ₕ " => HList.cons

def HList.append : HList β las → HList β ras → HList β (las ++ ras)
  | nil,        rbs => rbs
  | lb ::ₕ lbs, rbs => lb ::ₕ (lbs.append rbs)

instance HList.instHAppend : HAppend (HList β las) (HList β ras) (HList β (las ++ ras)) where
  hAppend := HList.append

theorem HList.append_assoc
  {as₁ as₂ as₃ : List α} (hl₁ : HList β as₁) (hl₂ : HList β as₂) (hl₃ : HList β as₃)
  : hl₁ ++ hl₂ ++ hl₃ = hl₁ ++ (hl₂++ hl₃) := by sorry -- type mismatch

def HList.cast {as as' : List α} (eq : as = as') (hl : HList β as) : HList β as' := by
  subst eq
  exact hl

theorem HList.cons_cast
  {a : α} {b : β a} {as as' : List α} {eq : as = as'} {bs : HList β as}
  : b ::ₕ bs.cast eq = (b ::ₕ bs).cast ((List.cons_inj_right a).mpr eq) := by
  subst eq
  rfl

theorem HList.cons_append
  {a : α} {b : β a} {as₁ as₂ : List α} {hl₁ : HList β as₁} {hl₂ : HList β as₂}
  : b ::ₕ hl₁ ++ hl₂ = b ::ₕ (hl₁ ++ hl₂) := by
  rfl

theorem HList.append_assoc'
  {as₁ as₂ as₃ : List α} (hl₁ : HList β as₁) (hl₂ : HList β as₂) (hl₃ : HList β as₃)
  : hl₁ ++ hl₂ ++ hl₃ = (hl₁ ++ (hl₂++ hl₃)).cast (List.append_assoc as₁ as₂ as₃).symm := by -- works
  induction hl₁
  case nil => rfl
  case cons a as b bs ih =>
    rw [cons_append, cons_append, ih]
    exact cons_cast

[James Gallicchio]

My impression is that the standard way to avoid cast is to introduce a specialization of cast for types that frequently need cast, as you do here. HList.cast should be much less problematic than cast. Your associativity lemma is already as clean as it can be!

[James Gallicchio]

As for your first question, I think the reason cons_split_fst works is because the RHS helps the LHS infer the las and ras arguments for split. We can explicitly pass those the las arg and cons_split_snd works:

theorem HList.cons_split_snd
  {α : Type} {a : α} {β : α → Type} {b : β a} {las ras : List α} {bs : HList β (las ++ ras)}
  : ((cons b bs).split (las := a::las)).snd = bs.split.snd := by
  rfl

[James Gallicchio]

Leaving las and ras implicit in HList.split is probably a footgun. For example if lean is asked to unify [a,b] = ?las ++ ?ras, what do you expect the behavior to be? There are multiple reasonable ways Lean could unify it. Instead, make at least one of las and ras explicit, so that the caller must make their expectation clear.

[Jesse Slater]

Thank you!