uninformative goal with `▸`

Stream: lean4

[neil]

So I'm pretty deep in "dependent typing hell" at this point, and trying to prove a bunch of nontrivial theorems about my code. Unfortunately, I've now got a proof to this state:

Goals (1)
n : Nat
s : sProduct n
b : s.bytesTypeProd
⊢ b = ⋯ ▸ ⋯ ▸ b

I have... no idea what to do here. What little documentation there is on \t is not particularly helpful, including its section in TPIL, and I don't know how to get lean to expand whatever is in those ellipses (very likely, the two casts can be made to cancel out, since doing a more complicated operation like that is how I got to this state in the first place).

[Aaron Liu]

This looks pretty easy

[Aaron Liu]

Switch to HEq and use the HEq cast lemmas

[Aaron Liu]

To expand the ellipses you can set_option pp.proofs true

[neil]

gotcha, I was just reading over a discussion you were in previously regarding the utility of HEq, so, there you go

[Aaron Liu]

@loogle HEq, Eq.rec, |- Iff ..

[loogle]

:search: eqRec_heq_iff, heq_eqRec_iff, and 6 more

[neil]

oh yup, pprint reveals that these are some annoying casts I had to work in because I am using a bunch of Vectors but decided to build my core heterogeneous list type on top of lists instead of Vector as well

[neil]

aaaaalright I'm going to read about HEq and figure this out tomorrow, then

[Ruben Van de Velde]

Generally you want to avoid the triangle. If you wrap it into something like Vector.cast, I understand you can more easily write lemmas to have simp help you out. (But I don't have direct experience)

[neil]

yeah that's what I just realized, I mostly use Vector.cast and a couple of my own.cast methods, which I have proven some useful rewrite theorems about. I should be able to replace these couple uses of the triangle with those cast lemmas, and so just avoid this problem entirely

[neil]

(I had a couple \t uses left in because I figured that I would change the types of the relevant expressions in parts of these implementations, but since I'm proving theorems now, I might as well get rid of those uses now as well)

[neil]

yup, that did it!

[neil]

ok I forgot that I didn't actually prove the .cast theorems I needed, and revisiting them, I run into some real weird stuff (MWE):

abbrev MHList.{u, v} {α : Type u} (motive : α → Type v) : List α → Type v
  | [] => PUnit
  | a :: as => match as with
    | [] => motive a
    | _ :: _ => (motive a) × (MHList motive as)

/--
Cast an MHList, from `MHList motive as` to `MHList newMotive bs`, provided that
the element types remain constant; that is, `as.map motive = bs.map newMotive`.
-/
def MHList.cast (ms : MHList (motive : α → Type u) (as : List α))
                      (newMotive : β → Type u) (bs : List β)
                      (eq : as.map motive = bs.map newMotive)
  : MHList newMotive bs :=
  match as, bs, ms with
  | [], [], _ => .unit
  | a :: as', b :: bs', ms =>
    -- NOTE: we need to give lean some help so that this match expression can
    -- rule out unreachable cases in which as' and bs' have differing lengths.
    -- We do this by refining eq to relate to as' and bs' directly, then
    -- discriminating on it in addition to as' and bs'.
    let eq' : as'.map motive = bs'.map newMotive := by
      simp at eq ; simp[eq]
    match has : as', hbs : bs', ms, eq' with
    | [], [], m, _ =>
        let castBisA : motive a = newMotive b := by simp at eq ; assumption
        let fullCast : MHList motive [a] = MHList newMotive [b] := by
          unfold MHList ; simp[*]
        fullCast ▸ m
    | _ :: _, _ :: _, (m, ms), _ =>
        let casts : motive a = newMotive b ∧ as'.map motive = bs'.map newMotive := by
          rw[←has] at eq ; rw[←hbs] at eq ; simp at eq ; assumption

        let eqHead : motive a = newMotive b := by simp[casts]
        let m' := eqHead ▸ m

        let eqTail : as'.map motive = bs'.map newMotive := by simp[casts]
        let ms' := hbs ▸ MHList.cast ms newMotive bs' (has ▸ eqTail)

        (m', ms')

theorem mhlist_cast_rfl.{u, v}
  {α : Type u} {motive : α → Type v} {as : List α} {ms : MHList motive as}:
  MHList.cast ms motive as rfl = ms :=
  match as, ms with
  | [], _ => by rfl
  | a :: as', ms =>
    match h : as', ms with
    | [], m => by rfl
    | head :: tail, (m, ms') => by
      -- failed to generate equational theorem for 'MHList.cast'
      -- unfold MHList.cast
      --
      -- proof state:
      -- ⊢ MHList.cast (m, ms') motive (a :: head :: tail) rfl = (m, ms')
      -- no way to eval/simp this to (MHList.cast ms' motive (head :: tail) rfl = ms'), so the termination checker fails...
      apply mhlist_cast_rfl

[neil]

"failed to generate equational theorem" is unfortunately pretty opaque. I wrote MHList.cast when I was first learning how to do dependently-typed programming in lean a month ago, so it's likely that I could rewrite it in a more reasonable way, but since the types are so generic, I think frequent usage of the triangle is unavoidable.

[neil]

and I only have this problem with MHList.cast; I have no problems stating and proving theorems which rely on simplifying other functions, like MHList.map (basically fmap)

[neil]

also, I tried changing the match structure of the mhlist_cast_rfl proof to "match" the match structure of the MHList.cast definition, but that didn't really help (as expected)

[neil]

the proofs for Vector.cast seem to all just rely on rcases ... ; simp, which doesn't seem like it would work for me here as an approach

[Aaron Liu]

Try delta MHList.cast

[Aaron Liu]

Then you can use simp

[Aaron Liu]

Or maybe fun_induction MHList.cast

[neil]

so, in the interesting branch, doing delta MHList.cast seems sort of promising but then simp produces a horrific term (and not the one I would have expected)

[neil]

ayy lmao

-- by fun_induction MHList.cast
Failed to realize constant MHList.cast.induct_unfolding:
  Cannot derive functional induction principle (please report this issue)
    failed to generate equational theorem for 'MHList.cast'

[neil]

so is this some sort of problem with the compiler, where it's not generating enough stuff for MHList.cast?

[Kyle Miller]

One way to go about this is to make the cast definition just be a wrapper around ▸, then prove some equation lemmas for it. The equation lemmas are pretty tricky... I was only able to write some meaningful ones when both of the lists have been destructured.

import Mathlib

abbrev MHList.{u, v} {α : Type u} (motive : α → Type v) : List α → Type v
  | [] => PUnit
  | [a] => motive a
  | a :: as => motive a × MHList motive as

theorem MHList.cast_aux
    {motive : α → Type u} {as : List α}
    (newMotive : β → Type u) (bs : List β)
    (eq : as.map motive = bs.map newMotive) :
    MHList motive as = MHList newMotive bs := by
  fun_induction MHList motive as generalizing bs with
  | case1 => simp at eq; subst_vars; rfl
  | case2 => cases bs <;> simp_all
  | case3 _ as' _ ih =>
    cases as'
    · simp_all
    match bs with
    | [] => simp at eq
    | [_] => simp at eq
    | _ :: _ :: _ =>
      simp at eq
      congr
      · simp [eq]
      · apply ih
        simp [eq]

/--
Cast an MHList, from `MHList motive as` to `MHList newMotive bs`, provided that
the element types remain constant; that is, `as.map motive = bs.map newMotive`.
-/
def MHList.cast
    {motive : α → Type u} {as : List α}
    (ms : MHList motive as)
    (newMotive : β → Type u) (bs : List β)
    (eq : as.map motive = bs.map newMotive) :
    MHList newMotive bs :=
  MHList.cast_aux newMotive bs eq ▸ ms

@[simp]
theorem mhlist_cast_rfl.{u, v}
    {α : Type u} {motive : α → Type v} {as : List α} {ms : MHList motive as} :
    MHList.cast ms motive as rfl = ms := by
  rfl

@[simp]
theorem MHList.cast_nil
    {motive : α → Type u}
    (ms : MHList motive [])
    (newMotive : β → Type u) :
    MHList.cast ms newMotive [] rfl = .unit :=
  rfl

@[simp]
theorem MHList.cast_singleton
    {motive : α → Type u}
    (a : α) (m : motive a)
    (newMotive : β → Type u) (b : β)
    (eq : List.map motive [a] = List.map newMotive [b]) :
    MHList.cast (motive := motive) (as := [a]) m newMotive [b] eq =
      haveI : motive a = MHList newMotive [b] := by simpa using eq
      this ▸ m := by
  rfl

@[simp]
theorem MHList.cast_cons_cons
    {motive : α → Type u}
    (a a' : α) (as'' : List α) (m : motive a) (ms' : MHList motive (a' :: as''))
    (newMotive : β → Type u) (b b' : β) (bs'' : List β)
    (eq : List.map motive (a :: a' :: as'') = List.map newMotive (b :: b' :: bs'')) :
    MHList.cast (motive := motive) (as := a :: a' :: as'') (m, ms') newMotive (b :: b' :: bs'') eq =
      haveI h1 : motive a = newMotive b := by simp at eq; simp [eq]
      haveI h2 : List.map motive (a' :: as'') = List.map newMotive (b' :: bs'') := by simp at eq; simp [eq]
      (h1 ▸ m, ms'.cast newMotive (b' :: bs'') h2) := by
  dsimp [cast]
  generalize_proofs pf1 pf2 pf3
  apply eq_of_heq
  apply rec_heq_of_heq (C := fun (x : Type u) => x)
  congr
  · apply HEq.symm
    apply rec_heq_of_heq (C := fun (x : Type u) => x)
    rfl
  · apply HEq.symm
    apply rec_heq_of_heq (C := fun (x : Type u) => x)
    rfl

[neil]

Thanks @Kyle Miller

I think I’m just going to leave this as admitted for now, and hope that some further compiler development makes it possible to work with my existing defn of cast. In any case, I appreciate your example since it demonstrates some usage of HEq stuff, which I know I need to get familiar with eventually

Edit: wait jk i thought your implementation was much more complex than it actually is. So, thanks even more than before! I should be able to just copy this wholesale and actually understand it

[Max Nowak 🐉]

At least sometimes you can collapse ⋯ ▸ ⋯ ▸ b into (⋯ ▸ ⋯) ▸ b, which can be less painful to deal with.