List.getConsAppend_eq_getConsZipAppend, sort of?

Stream: Is there code for X?

[Malvin Gattinger]

I admit this theorem is ugly - it comes from an extract_goal :innocent: But maybe there are some lemmas already that make it easier to prove than my induction approach?

import Mathlib.Data.Fin.Basic

theorem get_eq_getzip {X Y : α} {i : Fin ((List.length (l ++ [Y])))} {h} :
  List.get (X :: (l ++ [Y])) (Fin.castSucc i) = (List.get ((x, X) :: List.zip δ (l ++ [Y])) ⟨i.val, h⟩).2 := by
  induction l
  case nil =>
    simp at i
    have : i = 0 := by simp_all; ext; simp_all
    simp_all
  case cons l ls IH =>
    simp_all
    -- ugly, maybe need a different IH here?
    sorry

[Malvin Gattinger]

Never mind, done. Discord has beaten Zulip for this one ;-)

[Malvin Gattinger]

Solution

import Mathlib.Data.Fin.Basic
import Mathlib.Data.List.Zip

theorem get_eq_getzip {X Y : α} {i : Fin ((List.length (l ++ [Y])))} {h} :
  List.get (X :: (l ++ [Y])) (Fin.castSucc i) = (List.get ((x, X) :: List.zip δ (l ++ [Y])) ⟨i.val, h⟩).2 := by
  -- special thanks to droplet739
  simp only [←List.zip_cons_cons]
  rw [List.get_zip]
  rfl