Equalities between dependent structures

Stream: lean4

[mniip]

Hello! Suppose I'm working with a structure where some fields' types depend on others, e.g.:

def nfold (α : Type u) : ℕ → Type u
  | Nat.zero => PUnit
  | Nat.succ n => α × nfold α n
structure L (α : Type u) : Type u where
  len : ℕ
  elems : nfold α len

def nfold.nil : nfold α 0 := ()
def L.nil : L α := { len := 0, elems := nfold.nil }

def nfold.append : {n : Nat} → (xs : nfold α n) → (ys : nfold α m) → nfold α (m + n)
  | Nat.zero, (), ys => ys
  | Nat.succ _, (x, xs), ys => (x, nfold.append xs ys)
def L.append (xs ys : L α) : L α :=
  { len := ys.len + xs.len
  , elems := nfold.append xs.elems ys.elems }

In general, how does one prove propositional equality theorems about such structures? For example, I can prove:

theorem L.nil_append {xs : L α} : L.append L.nil xs = xs := rfl

because this equality holds definitionally, by the happenstance of all the relevant functions being defined recursively on the right argument. However the converse is trickier:

theorem L.append_nil {xs : L α} : L.append xs L.nil = xs := sorry

Ultimately I want to proceed by induction on the length, but the dependent types are getting in the way.
In a HoTT setting I would set up an extensionality lemma for the dependent pair involving a transport, and also formulate the append/nil lemma for nfold in terms of a transport as well, and those two pieces make up the puzzle:

def L.ext (p : l1 = l2) (q : p ▸ e1 = e2) : L.mk l1 e1 = L.mk l2 e2 := by
  cases p; cases q; rfl
theorem nfold.append_nil {xs : nfold α n} : Nat.zero_add n ▸ nfold.append xs nfold.nil = xs := by
  induction n with
    | zero => rfl
    | succ n ih =>
      simp [nfold] at xs
      cases xs with | mk x xs =>
      simp [nfold.append]
      -- α: Type
      -- n: ℕ
      -- ih: ∀ {xs : nfold α n}, (_ : 0 + n = n) ▸ append xs nil = xs
      -- x: α
      -- xs: nfold α n
      -- ⊢ (_ : 0 + Nat.succ n = Nat.succ n) ▸ (x, append xs nil) = (x, xs)
      sorry
theorem L.append_nil {xs : L α} : L.append xs L.nil = xs := by
  apply L.ext
  apply nfold.append_nil

However to prove the inductive step I would need to use a bunch of facts about how transporting (▸) interacts with other types, based on the "motive" being used in the transport (e.g. Coq-HoTT calls these transport_prod, transport_const, etc). I wasn't able to find such a collection of facts in mathlib4 though. I could certainly implement them by hand but that seems counterproductive.

When using simp on an equality of L's, it seems to suggest that I HEq is the way forward:

theorem L.append_nil {xs : L α} : L.append xs L.nil = xs := by
  cases xs with | mk len elems =>
  simp [L.append, L.nil]
  -- α: Type
  -- len: ℕ
  -- elems: nfold α len
  -- ⊢ HEq (nfold.append elems nfold.nil) elems
  sorry

With HEq I can do pretty much the same thing:

def L.ext (p : l1 = l2) (q : HEq e1 e2) : L.mk l1 e1 = L.mk l2 e2 := by
  cases p; cases q; rfl
theorem nfold.append_nil {xs : nfold α n} : HEq (nfold.append xs nfold.nil) xs := by
  induction n with
    | zero => rfl
    | succ n ih =>
      simp [nfold] at xs
      cases xs with | mk x xs =>
      simp [nfold.append]
      -- α: Type
      -- n: ℕ
      -- ih: ∀ {xs : nfold α n}, HEq (append xs nil) xs
      -- x: α
      -- xs: nfold α n
      -- ⊢ HEq (x, append xs nil) (x, xs)
      sorry
theorem L.append_nil {xs : L α} : L.append xs L.nil = xs := by
  apply L.ext
  . apply Nat.zero_add
  . apply nfold.append_nil

But once again the inductive step relies on a theorem about HEq that I cannot find in mathlib4.

What is the "normal" way to manipulate such dependent equalities?

[James Gallicchio]

I think the only way is to do manual generalizations at just the right moment to avoid any HEqs popping up :)

This is very difficult, and painful, to do in general. I think that's just the reality of working with proof irrelevance; it's nice until it's not.

The way we usually deal with this is to avoid as many dependent types as possible, and to build specialized "cast" functions for those datatypes which must appear in dependently typed situations (see eg Fin.cast).

[James Gallicchio]

(I'm sure the proof wizards can finish your proof, but I tried to find the right generalization for a while and couldn't come up with one that worked :big_smile:)

[mniip]

avoid as many dependent types as possible

Yeah I wish I could do that. My main type looks something like:

structure Bazaar.Indexed (α : Type u) (β : Type v) (τ : Type w) : Type (max u v w) where
  length : ℕ
  elements : Vector α length
  continuation : Vector β length → τ

build specialized "cast" functions for those datatypes which must appear in dependently typed situations (see e.g. Fin.cast)

But Fin.cast is no different from a ▸ in that you have to prove lemmas about how it commutes with other data.

[Yaël Dillies]

No it is different because ▸ can rewrite other things than just the indices you would like to rewrite.

[Kyle Miller]

@mniip Here's how I might set this up. It's annoying having to flesh out the API for cast, but then you can avoid HEq

code

import Mathlib.Tactic.Common

set_option autoImplicit true

inductive nfold (α : Type u) : ℕ → Type u
  | nil : nfold α 0
  | cons (x : α) (xs : nfold α n) : nfold α (n + 1)

def nfold.cast (elems : nfold α n) (h : n = n') : nfold α n' :=
  h ▸ elems

@[simp]
theorem nfold.cast_cast (elems : nfold α n) (h : n = n') (h' : n' = n'') :
    (elems.cast h).cast h' = elems.cast (h.trans h') := by subst_vars; rfl

@[simp]
theorem nfold.cast_rfl (elems : nfold α n) : elems.cast rfl = elems := rfl

def nfold.append : {n : Nat} → (xs : nfold α n) → (ys : nfold α m) → nfold α (m + n)
  | Nat.zero, .nil, ys => ys
  | Nat.succ _, .cons x xs, ys => nfold.cons x (xs.append ys)

@[simp]
theorem nfold.cons_cast (x : α) (elems : nfold α n) (h : n = n') :
    nfold.cons x (elems.cast h) = (nfold.cons x elems).cast (by cases h; rfl) := by
  cases h; rfl

@[simp]
theorem nfold.append_cast_left (xs : nfold α n) (ys : nfold α m) (h : n = n') :
    (xs.cast h).append ys = (xs.append ys).cast (by cases h; rfl) := by
  cases h; rfl

@[simp]
theorem nfold.append_cast_right (xs : nfold α n) (ys : nfold α m) (h : m = m') :
    xs.append (ys.cast h) = (xs.append ys).cast (by cases h; rfl) := by
  cases h; rfl

@[simp]
theorem nfold.cons_append (x : α) (xs : nfold α n) (ys : nfold α m) :
    (nfold.cons x xs).append ys = nfold.cons x (xs.append ys) := rfl

structure L (α : Type u) : Type u where
  len : ℕ
  elems : nfold α len

def L.nil : L α := L.mk 0 nfold.nil

theorem L.ext {α : Type u} {len len' : ℕ} {elems : nfold α len} {elems' : nfold α len'}
    (hlen : len = len') (helems : elems.cast hlen = elems') :
    L.mk len elems = L.mk len' elems' := by
  subst_vars; rfl

def L.append (xs ys : L α) : L α where
  len := ys.len + xs.len
  elems := nfold.append xs.elems ys.elems

theorem L.nil_append {xs : L α} : L.append L.nil xs = xs := rfl

theorem L.append_nil {xs : L α} : L.append xs L.nil = xs := by
  obtain ⟨len, elems⟩ := xs
  rw [append]
  refine L.ext ?_ ?_
  · simp [nil]
  induction len with
  | zero => cases elems; rfl
  | succ len ih =>
    obtain ⟨x, elems'⟩ := elems
    rw [nfold.cons_append, ← nfold.cons_cast, ih]

I've never tried handling this using lemmas on the structure of the motive of Eq.rec, which sounds like what transport lemmas might be similar to. Having a cast function is nice because it puts a constraint on what the motive can be, and it seems like it makes it easier to write simp lemmas.

[Notification Bot]

y-samuel has marked this topic as resolved.

[Notification Bot]

y-samuel has marked this topic as unresolved.