List.Forall canonical unpacking

Stream: Is there code for X?

[Arnav Sabharwal]

Hello!

I have the following hypotheses:

l1 l2 : List Nat
h1 : List.Forall2 P l l1
h2 : List.Forall2 P l l2
Q : forall m, forall n1 n2, P m n1 -> P m n2 -> n1 = n2

I also know l1 and l2 happen to be of the same length. My goal is to prove l1 = l2, and I'm trying to avoid nested induction or dealing with List.get, if possible. What is the cleanest way to do this?

Thanks!

[Kevin Buzzard]

Can you make a #mwe ? Then it will be easier for people to help you.

[Robin Arnez]

I think the simplest approach would be induction on l:

import Batteries.Data.List.Basic

example (P : α → Nat → Prop) (l1 l2 : List Nat)
    (h1 : List.Forall₂ P l l1) (h2 : List.Forall₂ P l l2)
    (Q : ∀ m, ∀ n1 n2, P m n1 → P m n2 → n1 = n2) :
    l1 = l2 := by
  induction l generalizing l1 l2 with
  | nil => cases h1; cases h2; rfl
  | cons x t ih =>
    obtain _ | @⟨_, y, _, l1, hxy, hl1⟩ := h1
    obtain _ | @⟨_, z, _, l2, hxz, hl2⟩ := h2
    rw [Q x y z hxy hxz, ih l1 l2 hl1 hl2]

[Arnav Sabharwal]

Sorry, couldn't get to this for a bit. Thank you so much @Robin Arnez!