Why wrap h ▸ v ?

Stream: new members

[mars0i]

In another thread, @Kyle Miller helpfully suggested using this definition

def Vect.cast {m n : Nat} (h : m = n) (v : Vect α m) : Vect α n :=
  h ▸ v

to solve a problem I encountered. This allows replacing part of the type ofv using the equality in h. This seems like a is generally useful idea (which I've already used in another part of the same code).

What I'm wondering is why it was necessary to define a custom function as a wrapper for h ▸ v. When I try to use ▸ alone I get errors, but I don't understand them. (I can give details about the errors, but I thought the answer to why a wrapper is needed might not depend on the errors.)

Full context:

inductive Vect (α : Type u) : Nat → Type u where
   | nil : Vect α 0
   | cons : α → Vect α n → Vect α (n + 1)
deriving Repr

def Vect.cast {m n : Nat} (h : m = n) (v : Vect α m) : Vect α n :=
  h ▸ v

def Vect.revHelper (xs : Vect a n) (acc : Vect a m) : Vect a (m + n) :=
  match xs with
  | .nil => acc
  | .cons y ys =>
    (revHelper ys (.cons y acc)).cast (by rw [Nat.succ_add]; rfl)

[Kyle Miller]

The custom function is just to sort of delimit the rewrite. Once Vect.cast is defined, the ▸ is safely processed, and then Vect.cast has the helpful property that if the expected type is known and v is known, then the type of h is known — that is, it helps with elaboration.

It's also good because you can write lemmas about Vect.cast, like that Vect.cast rfl v = v, which is almost impossible to do for ▸, since ▸ is a "magic" operator that computes a rewrite using all the available details.

[Kyle Miller]

In general, I think it's a good design pattern to define cast functions for rewriting indices for types, like the Nat index here.

[Kyle Miller]

Simp lemmas to go with the cast function:

@[simp] theorem Vect.cast_rfl (v : Vect α m) : v.cast rfl = v := rfl
@[simp] theorem Vect.cast_cast (h : m = m') (h' : m' = m'') (v : Vect α m) :
  (v.cast h).cast h' = v.cast (h.trans h') := by subst_vars; rfl

[Kyle Miller]

This is also a useful lemma, for pushing all the casts to one side of an equality:

theorem Vect.eq_cast (h : n = m) (v : Vect α m) (w : Vect α n) :
  v = w.cast h ↔ v.cast h.symm = w := by subst_vars; rfl

[Kyle Miller]

This is another useful lemma: how the cast function interacts with cons:

@[simp] theorem Vect.cons_cast (h : m = n) (v : Vect α m) :
    Vect.cons x (v.cast h) = (Vect.cons x v).cast (by rw [h]) := by
  subst_vars; rfl

I think generally you want to push casts "outward"

[Kyle Miller]

The short of it is that the algebraic rules for Vector.cast are very useful if you want to prove anything.

[mars0i]

Thanks @Kyle Miller. That's quite interesting. Some of it is slightly over my head at this point, but I'll keep it in mind as I learn more.

(It turned out that there was another line where I needed to rewrite a term, and Vect.cast made it easy to figure out how to do it following your illustration. The whole thing seemed so easy, that I was surprised that it was necessary to write a special cast function. But I accept that it's a design pattern and I can easily write other cast functions as needed. I don't have a full grasp of the benefits you described, but I appreciate that they are there.

When I encountered similar problems in Idris and Agda, sometimes I felt that it was the sort of thing that I'd worked through in textbooks, and that I should know how to do, but figuring out how to apply the idea in a new situation and writing custom proof functions seemed like a pain. No doubt it's not a pain in Idris and Agda if you're used to doing it a lot, but doing this kind of thing in Lean seems easier, at least in this kind of situation. Part of it was that it was easy to find a simple theorem I neededte for the cast.)

[Violeta Hernández]

Tangential, but it's generally better to use cast for definitions rather than ▸, since it has nicer simp lemmas.

[Violeta Hernández]

(though if you're already proving said simp lemmas for your API, this might be moot)