Proofs with HEq goals

Stream: mathlib4

[Julia Scheaffer]

Recently, I have learned how to use cast, and that is going great, but occasionally I get goals that use HEq which I don't know how to solve. Usually I can change these to use cast and solve them, but not always. Here is a recent example i have attempted to minimize.

import Mathlib

inductive Stack.{u} : List (Type u) -> Type (u + 1) where
  | nil : Stack []
  | cons {α β}: α -> Stack β -> Stack (α :: β)

infixr:67 "; " => Stack.cons

variable {A : Type u} {α β : List (Type u)} {a : Stack α} {b : Stack β}

def Stack.cast (a : Stack α) (h : α = β) : Stack β := h ▸ a

theorem Stack.eq_cast_iff_heq (h : α = β) : a = b.cast h.symm <-> a ≍ b := by
  rw [Stack.cast, Eq.rec_eq_cast, _root_.eq_cast_iff_heq]

theorem Stack.cons_cancel {x : A} {h : α = β} :
    x; a = (x; b).cast (by rw [h]) -> a = b.cast h.symm := by
  rw [eq_cast_iff_heq (by rw [h]), eq_cast_iff_heq h]
  -- I dont know how to use function injectivity over heq
  grind only [cons.inj]
  -- But thankfully grind does!

In this case I needed to use the injectivity of cons to reach my goal, but I don't know how to do this across an HEq instead of a normal equality. Thankfully grind does know how, but I would like to rewrite this without using grind. What sort of tactics is grind using in this situation?

I have also come across other situations where I can't solve a goal, but grind does in some non-obvious (to me) way.

[Aaron Liu]

theorem Stack.cons_cancel {x : A} {h : α = β} :
    x; a = (x; b).cast (by rw [h]) -> a = b.cast h.symm := by
  rw [eq_cast_iff_heq (by rw [h]), eq_cast_iff_heq h]
  subst h
  rw [heq_iff_eq, heq_iff_eq]
  intro h
  exact (cons.inj h).2

[Julia Scheaffer]

I didn't know about the subst tactic. Thank you!

[Kyle Miller]

Most cast lemmas can start with subst_vars, and then you can treat the cast as being an id.

theorem Stack.eq_cast_iff_heq (h : α = β) : a = b.cast h.symm <-> a ≍ b := by
  subst_vars
  rw [heq_iff_eq]
  rfl

theorem Stack.cons_cancel {x : A} {h : α = β} :
    x; a = (x; b).cast (by rw [h]) -> a = b.cast h.symm := by
  subst_vars
  intro h
  exact (cons.inj h).2

[Kyle Miller]

For your lemmas, it's good to make sure the hypotheses are used as pure variables, for example avoiding use of h.symm and instead phrase it as

theorem Stack.eq_cast_iff_heq (h : β = α) : a = b.cast h <-> a ≍ b := by
  subst_vars
  rw [heq_iff_eq]
  rfl

That way when you rewrite with the lemma, Lean can solve for h by unification, and you don't need to supply it as an argument to the lemma.

[Julia Scheaffer]

Kyle Miller said:

For your lemmas, it's good to make sure the hypotheses are used as pure variables, for example avoiding use of h.symm and instead phrase it as ...

Thank you for the recommendation! This has shortened a couple of my proofs by a few lines :smile: