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