Thought I had to fight with HEq, but successfully dodged it

Stream: lean4

[Hirotaka Sato]

In my proof, I need a version of List.zipIdx whose indices are of Fin, so I implemented zipIdxFin.

Since it is sometimes cumbersome to have the Fin.isLt condition, I would also like to state that forgetting this condition results in the usual List.zipIdx.

However, in trying to prove this fact, I came across HEq:

1. Why does this even happen?
2. How can I either solve this issue or get around this?

import Mathlib.Data.Finset.Defs

/--
Same as `List.zipIdx`, but with `Fin` indices.
-/
def zipIdxFin {α} (l : List α) {m : Nat} (h_len : m = l.length) (n : Nat := 0) : List (α × Fin (m + n)) :=
 match hl : l, n with
  | [], _=> []
  | x :: xs, n =>
    let m' := xs.length
    let h_m : m = m' + 1 := by simp at h_len; grind only
    let head_isLt : n < m + n := by simp [h_m]
    let h_len' : m' = xs.length := by grind
    let rest : List (α × Fin (m' + (n + 1))) := zipIdxFin xs h_len' (n + 1)
    -- Now I need to convince that  `List (α × Fin (m' + (n + 1)))` is the same thing as `List (α × Fin (m' + 1 + n))`
    let cast : Fin (m' + (n + 1)) -> Fin (m + n) := fun ⟨ a, isLt' ⟩ =>
      let new_isLt : a < m + n := by
        rw [h_m, show m' + 1 + n = m' + (n + 1) from by ac_rfl]
        assumption
      ⟨ a, new_isLt ⟩
    (x, ⟨ n, head_isLt ⟩ ) :: rest.map (fun (x, i) => (x, cast i))

theorem zipIdxFin_forget_bound {α} {l : List α} {m : Nat} (h_len : m = l.length) (n : Nat := 0) :
  List.map (fun ⟨ a, ⟨ i, isLt ⟩ ⟩ => (a, i)) (zipIdxFin l h_len n) = List.zipIdx l n := by
  induction l generalizing m n with
  | nil =>
    unfold zipIdxFin
    simp [List.zipIdx]
  | cons x xs ih =>
    simp
    unfold zipIdxFin
    simp
    simp at h_len
    match m with
    | 0 => simp at h_len -- contradiction
    | m' + 1 =>
      simp at h_len
      have ih2 := ih h_len (n + 1)
      rw [← ih2]
      congr
      · exact h_len.symm
      · sorry
      · exact h_len.symm
      · sorry

[Hirotaka Sato]

Fortunately, simplifying the definition eliminated the HEq.

import Mathlib.Data.Finset.Defs

/--
Same as `List.zipIdx`, but with `Fin` indices.
-/
def zipIdxFin {α} (l : List α) {m : Nat} (h_len : m = l.length) (n : Nat := 0) : List (α × Fin (m + n)) :=
 match hl : l, n with
  | [], _=> []
  | x :: xs, n =>
    let h_m : m = xs.length + 1 := by simp at h_len; assumption
    let head_isLt : n < m + n := by simp [h_m]
    let rest : List (α × Fin (xs.length + (n + 1))) := zipIdxFin xs (by rfl) (n + 1)
    -- Now I need to convince that  `List (α × Fin (xs.length + (n + 1)))` is the same thing as `List (α × Fin (xs.length + 1 + n))`
    let cast : Fin (xs.length + (n + 1)) -> Fin (m + n) := fun ⟨ a, isLt' ⟩ =>
      let new_isLt : a < m + n := by
        rw [h_m, show xs.length + 1 + n = xs.length + (n + 1) from by ac_rfl]
        assumption
      ⟨ a, new_isLt ⟩
    (x, ⟨ n, head_isLt ⟩ ) :: rest.map (fun (x, i) => (x, cast i))

theorem zipIdxFin_forget_bound {α} {l : List α} {m : Nat} (h_len : m = l.length) (n : Nat := 0) :
  List.map (fun ⟨ a, ⟨ i, _isLt ⟩ ⟩ => (a, i)) (zipIdxFin l h_len n) = List.zipIdx l n := by
  induction l generalizing m n with
  | nil =>
    unfold zipIdxFin
    simp [List.zipIdx]
  | cons x xs ih =>
    simp
    unfold zipIdxFin
    simp
    simp at h_len
    have ih2 := ih (by rfl) (n + 1)
    rw [← ih2]
    congr

[pandaman]

Just before congr, the (zipIdxFin xs ⋯ (n + 1)) term on the left hand side has type List (α × Fin (xs.length + (n + 1))), while (zipIdxFin xs h_len (n + 1)) on the right hand side has type List (α × Fin (m' + (n + 1))). I guess this is where the HEq comes from.

Substituting m early helped:

theorem zipIdxFin_forget_bound {α} {l : List α} {m : Nat} (h_len : m = l.length) (n : Nat := 0) :
  List.map (fun ⟨ a, ⟨ i, isLt ⟩ ⟩ => (a, i)) (zipIdxFin l h_len n) = List.zipIdx l n := by
  induction l generalizing m n with
  | nil =>
    unfold zipIdxFin
    simp [List.zipIdx]
  | cons x xs ih =>
    subst m
    simp [zipIdxFin]
    rw [←ih rfl (n + 1)]
    simp

[pandaman]

That being said, I would just use List.zipIdx in code and List.snd_lt_of_mem_zipIdx in proofs.