Zulip Chat Archive

Stream: new members

Topic: Why wrap h ▸ v ?


mars0i (Oct 08 2024 at 19:42):

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 (Oct 08 2024 at 19:44):

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 (Oct 08 2024 at 19:46):

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 (Oct 08 2024 at 19:48):

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 (Oct 08 2024 at 19:50):

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 (Oct 08 2024 at 19:53):

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 (Oct 08 2024 at 19:54):

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

mars0i (Oct 09 2024 at 03:26):

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 (Oct 10 2024 at 07:55):

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

Violeta Hernández (Oct 10 2024 at 07:56):

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


Last updated: May 02 2025 at 03:31 UTC