Equality of structures with pi-type fields

Stream: general

[Nicholas Phair]

Good morning. I’m trying to prove an equality between two values of a structure arising from the ofArray definition. The difficulty is that one of the structure fields is a Pi-type (Fin n → _), so after simplification I end up needing to relate functions whose domains are definitionally different but provably equal.

Here is a minimal example that captures the idea.

structure PArg (k : Nat) where
  name : String

structure PSig (k : Nat) where
  n    : Nat
  args : Fin n → PArg k

@[inline] def ofArray {k : Nat} (xs : Array (PArg k)) : PSig k :=
  { n := xs.size, args := fun i => xs[i] }

theorem ofArray_ofFn {k : Nat} {ps : PSig k} :
  ofArray (Array.ofFn ps.args) = ps := by
  cases ps with
  | mk n args =>
    simp [ofArray, Array.getElem_ofFn]

    have y : (fun i : Fin n => (Array.ofFn args)[i]) = args := by
      funext i
      simp [Array.getElem_ofFn]

    -- have h  : (Array.ofFn args).size = n := by exact Array.size_ofFn
    -- have h' : n = (Array.ofFn args).size := by simp
    -- exact heq_of_eq y
    sorry

After simp the remaining goal is:

k n : Nat
args : Fin n → PArg k
y : (fun i => (Array.ofFn args)[i]) = args
⊢ (fun i => args ⟨↑i, ⋯⟩) ≍ args

The type of i in the y hypothesis differs from the type of i in the goal. Though, i can show they are equal (with h or h'). My attempts to rewrite fail. Does anyone have suggestions about how to finish this off?

Thank you, Nick

[Ilmārs Cīrulis]

Don't know if you are okay with using Mathlib in this problem, but rw! tactic works.

import Mathlib.Tactic.DepRewrite

structure PArg (k : Nat) where
  name : String

structure PSig (k : Nat) where
  n    : Nat
  args : Fin n → PArg k

@[inline] def ofArray {k : Nat} (xs : Array (PArg k)) : PSig k :=
  { n := xs.size, args := fun i => xs[i] }

theorem ofArray_ofFn {k : Nat} {ps : PSig k} :
  ofArray (Array.ofFn ps.args) = ps := by
  cases ps with
  | mk n args =>
    simp [ofArray, Array.getElem_ofFn]

    have y : (fun i : Fin n => (Array.ofFn args)[i]) = args := by
      funext i
      simp [Array.getElem_ofFn]

    rw! (castMode := .all) [Array.size_ofFn]
    simp

[Nicholas Phair]

Thank you @Ilmārs Cīrulis . I ultimately would like to avoid mathlib here, but getting unstuck is more of a priority at the moment and your solution does that. Thanks for the prompt reply.

[Vlad Tsyrklevich]

If you import Mathlib, exact? closes the goal (with your h in scope.) Then you find that it is just using a single 2-line lemma you can pull out if you want to avoid Mathlib (but developing with Mathlib and then pulling it out at the end may honestly be easier, Mathlib has many useful helpers)

structure PArg (k : Nat) where
  name : String

structure PSig (k : Nat) where
  n    : Nat
  args : Fin n → PArg k

@[inline] def ofArray {k : Nat} (xs : Array (PArg k)) : PSig k :=
  { n := xs.size, args := fun i => xs[i] }

theorem Fin.heq_fun_iff {α : Type} {k l : Nat} (h : k = l) {f : Fin k → α} {g : Fin l → α} :
    f ≍ g ↔ ∀ i : Fin k, f i = g ⟨(i : Nat), h ▸ i.2⟩ := by
  subst h
  simp [funext_iff]

theorem ofArray_ofFn {k : Nat} {ps : PSig k} :
  ofArray (Array.ofFn ps.args) = ps := by
  cases ps with
  | mk n args =>
    simp [ofArray, Array.getElem_ofFn]
    exact (Fin.heq_fun_iff Array.size_ofFn).mpr (congrFun rfl)

[Aaron Liu]

mathlib-free:

structure PArg (k : Nat) where
  name : String

structure PSig (k : Nat) where
  n    : Nat
  args : Fin n → PArg k

@[inline] def ofArray {k : Nat} (xs : Array (PArg k)) : PSig k :=
  { n := xs.size, args := fun i => xs[i] }

theorem ofArray_ofFn {k : Nat} {ps : PSig k} :
  ofArray (Array.ofFn ps.args) = ps := by
  cases ps with
  | mk n args =>
    -- simp? [ofArray, Array.getElem_ofFn]
    simp only [ofArray, Fin.getElem_fin, Array.getElem_ofFn, PSig.mk.injEq, Array.size_ofFn,
      true_and]
    exact Eq.rec (motive := fun (x : Nat) (h : n = x) =>
        (fun i : Fin x => args ⟨i.1, h.symm ▸ i.2⟩) ≍ args)
      HEq.rfl Array.size_ofFn.symm

[Nicholas Phair]

Thank you both, and for the strategy for pulling out the lemmas I care about.

[Jakub Nowak]

mathlib is kinda more experimental so it has many new useful tactics that aren't in core, but there's no mathlib changelog so the only way to learn about these new tactics I found is to be active here on zulip. Eventually useful things should be merged into core. E.g. the dependant rewrite strategy used by rw! should probably be eventually merged into rw (and a few other tactics that do rewrites internally, like match or cases).