List.zipWith and List.ofFn

Stream: Is there code for X?

[Paige Thomas]

I was wondering if anyone might know how to prove this?

example
  {α β : Type}
  (f : α → α → β)
  (xs ys : List α)
  (h1 : xs.length = ys.length) :
  ∃ (n : Nat) (fn_xs fn_ys : Fin n → α),
    List.ofFn (fun i => f (fn_xs i) (fn_ys i)) = List.zipWith f xs ys ∧
    List.ofFn fn_xs = xs ∧
    List.ofFn fn_ys = ys := sorry

I've gotten as far as

example
  {α β : Type}
  (f : α → α → β)
  (xs ys : List α)
  (h1 : xs.length = ys.length) :
  ∃ (n : Nat) (fn_xs fn_ys : Fin n → α), List.ofFn (fun i => f (fn_xs i) (fn_ys i)) = List.zipWith f xs ys ∧ List.ofFn fn_xs = xs ∧ List.ofFn fn_ys = ys :=
  by
    apply Exists.intro (min xs.length ys.length)
    apply Exists.intro (fun i => xs[i])
    apply Exists.intro (fun i => ys[i])
    constructor
    · induction xs generalizing ys
      case _ =>
        cases ys
        case _ =>
          simp
        case _ ys_hd ys_tl =>
          simp at h1
      case _ xs_hd xs_tl xs_ih =>
        cases ys
        case _ =>
          simp at h1
        case _ ys_hd ys_tl =>
          simp only [List.zipWith]
          sorry
    · sorry

but I haven't made much progress past that.

[Paige Thomas]

import Batteries.Data.List
import Mathlib.Order.Basic
import Mathlib.Data.List.OfFn


example
  {α β : Type}
  (f : α → α → β)
  (xs ys : List α)
  (h1 : xs.length = ys.length) :
  ∃ (n : Nat) (fn_xs fn_ys : Fin n → α), List.ofFn (fun i => f (fn_xs i) (fn_ys i)) = List.zipWith f xs ys ∧ List.ofFn fn_xs = xs ∧ List.ofFn fn_ys = ys :=
  by
    apply Exists.intro (min xs.length ys.length)
    apply Exists.intro (fun i => xs[i])
    apply Exists.intro (fun i => ys[i])
    constructor
    · induction xs generalizing ys
      case _ =>
        cases ys
        case _ =>
          simp
        case _ ys_hd ys_tl =>
          simp at h1
      case _ xs_hd xs_tl xs_ih =>
        cases ys
        case _ =>
          simp at h1
        case _ ys_hd ys_tl =>
          simp only [List.zipWith]
          rw [← xs_ih]
          ext n z
          · simp
            induction n
            case _ =>
              simp
            case _ m ih =>
              simp
          · simp at h1
            exact h1
    · constructor
      · have s1 : ys.length = xs.length :=
        by
          symm
          exact h1

        simp_all only [min_self, Fin.getElem_fin, Fin.coe_cast]
        exact List.ofFn_getElem xs

      · simp_all only [min_self, Fin.getElem_fin, Fin.coe_cast]
        exact List.ofFn_getElem ys

Is there a simpler proof?

[Ilmārs Cīrulis]

Maybe like this:

import Mathlib

example
  {α β : Type}
  (f : α → α → β)
  (xs ys : List α)
  (h1 : xs.length = ys.length) :
  ∃ (n : Nat) (fn_xs fn_ys : Fin n → α), List.ofFn (fun i => f (fn_xs i) (fn_ys i)) = List.zipWith f xs ys ∧ List.ofFn fn_xs = xs ∧ List.ofFn fn_ys = ys :=
  by
    exists (xs.length), (fun i => xs[i]), (fun i => ys[i])
    refine ⟨?_, ?_, ?_⟩
    · induction xs generalizing ys with
      | nil => simp at *
      | cons head tail ih =>
        simp at *
        obtain ⟨ys_head, ys_tail, Hys⟩ := List.exists_cons_of_length_eq_add_one h1.symm
        subst ys
        simp
        exact ih ys_tail (Nat.succ_inj'.mp h1)
    · sorry
    . sorry

I left two last parts sorried.

[Ilmārs Cīrulis]

You have hypothesis h1: xs.length = ys.length, so there is no need to use min, in my opinion.

[Ilmārs Cīrulis]

The first sorry is solved by simp.

[Ilmārs Cīrulis]

And the second sorry is solved by simp [h1].

[Paige Thomas]

@Lessness Nice. Thank you!