Casting vs HEq

Stream: lean4

[Joey Eremondi]

I'm for advice choosing between having equalities between terms using cast, vs. having heterogeneous equalities.

I'm in a situation where I have (a : A), (b : B), and a proof pf : (A = B). I want to write the type a = b, but I can't because they don't have the same type.

If I write (cast pf a) = b, then the problem is I have a cast in my goals, and I can't figure out how to get rid of it, even though I have the proof that the types are equal. In Agda I'd just pattern match on the equality but that doesn't seem like the lean way to do things. And applying the equality eliminator by hand seems overkill because I'd have to figure out the motive myself.

If I write HEq a b, things generally work. But this seems "lossy" since it's forgetting that I already have the proof that the types are the same. I'm worried that simp won't be as able to reason about HEq , and HEq seems like a "dead end" in the sense that once you have an HEq proof there don't seem to be ways to get it back to a normal equality.

Are there tactics for getting rid of casts in proofs? Or is HEq the way to go to avoid having casts in goal types?

[Kevin Buzzard]

simp might well get rid of casts for you.

The advice we usually give is to avoid casts if you can -- type equality is hard to work with in Lean's type theory.

[Eric Wieser]

I think Kevin's response possibly sends the wrong message; we try to avoid Heq for the same reason as we avoid casts!

[Jannis Limperg]

Anything you can do in Agda should also work in Lean. In particular, Lean's pattern matching should be as powerful as Agda's (without --without-K). cases eq, where eq : A = B, might also do the trick.

If you know eq : A = B and heq : HEq a b, then you should be able to match on eq and apply docs#eq_of_heq (or just match on heq).

I generally prefer casts (aka "path over" from HoTT) to HEq, but your mileage may vary.

[Eric Wieser]

In my experience casts are equally bad: usually what I actually have is x : A i and y : A j, and both HEq a b and cast h a b throw away the information that i = j`

[Eric Rodriguez]

have you ported your indexed equality test to lean4?

[Eric Wieser]

No, but I think @Scott Morrison or @Joël Riou independently PR'd a category-theory-specific version which has been merged

[Eric Wieser]

(well remembered!)

[Joe Hendrix]

In verification, I try to eliminate both cast and HEq early on. I think both are a sign one is working with the wrong types.

For example, if I have to cast because I am trying to prove two vectors Vector m A and Vector n A then I would switch to trying to prove their underlying arrays or lists are equal and avoid both cast and HEq.

[Alex Keizer]

You can also often avoid dealing with casts by explicitly choosing an isomorphism between the equal types and using that to go between the types. For example, instead of casting with a proof that Fin i = Fin j, we can call Fin.cast : i = j -> Fin i -> Fin j

[Kyle Miller]

@Joey Eremondi Could you make a not-necessarily-minimal #mwe that's got enough details to demonstrate your situation? There's a lot of general advice about cast/heq, but concrete advice can vary a lot case-by-case.

[Alex Keizer]

Joey Eremondi said:

If I write HEq a b, things generally work. But this seems "lossy" since it's forgetting that I already have the proof that the types are the same.

This is not necessarily true, btw. HEq a b implies that the types of a and b are equal, this is called type_eq_of_heq

[Joey Eremondi]

@Kyle Miller What I'm working on is here, it's abstract but a fairly small file: https://github.com/JoeyEremondi/lean-cwf/blob/main/LeanCwf/CwF.lean

Basically CwFs are a way to model the semantics of programming languages in Category Theory. The laws are very dependent, because types depend on contexts and terms depend on types.

e.g. tmSubComp has to be a heterogenous equation, because to be well typed, it depends on the equality of tySubComp.

Likewise, in ext_nat, we can't even give the argument to ext without casting by tySubComp.

And then for example I'm trying to prove ext_unique, but when I do rw, it just generates a new variable that shadows the old one, but the old one still appears in the goal type.

[Trebor Huang]

You might want to consult Agda formalizations of displayed categories for many tricks that tame the dependency. Two more ways to deal with it is to (1) take Sigma types, or in category theory jargon, let Tm be a functor from the category of elements of Ty, or (2) take Sigma types another way, so Tm G is the collection of all terms in context G regardless of type, and have a typeof operator assigning the types.

[Kyle Miller]

One design pattern that might be useful here is writing a custom cast function that rewrites just a specific part of a term. In this case, write a function Tm.cast that rewrites just the T argument of Tm T. This lets you write simp lemmas and such that have access to the proof of equality that wouldn't be accessible from a HEq term or a general cast term. This design pattern is used in docs#SimpleGraph.Walk.copy, docs#Quiver.Hom.cast, and docs#Quiver.Path.cast for rewriting indices. You can write algebraic rules like docs#Quiver.Hom.cast_cast and docs#Quiver.Hom.cast_rfl_rfl

[Junyan Xu]

Alex Keizer said:

Joey Eremondi said:

If I write HEq a b, things generally work. But this seems "lossy" since it's forgetting that I already have the proof that the types are the same.

This is not necessarily true, btw. HEq a b implies that the types of a and b are equal, this is called type_eq_of_heq

The usual problem is that you have a type family F, a : F i and b : F j, and you know i = j. Then HEq a b only implies F i = F j but forgets that i = j. (encountered this in algebraic geometry (sheaves)).

[Kyle Miller]

(This in particular is what the design pattern I mentioned is meant to help with -- remembering this i = j equality.)