casting over type equality

Stream: lean4

[Nick Mertes]

In Prelude.lean above the definition of cast it says "Cast across a type equality. If h : α = β is an equality of types, and a : α, then a : β will usually not typecheck directly ..."

What could go wrong if we instead tried to implement a type theory where a : β does typecheck?

[Alexander Bentkamp]

In terms of logical consistency, that wouldn't be a problem, but it makes type checking undecidable. How is the type checker supposed to know that α = β? The proof of such an equality proof could be arbitrarily complicated. Nonetheless, as far as I know, the proof assistant PVS implements a logic that allows a : β to type check, at the cost of occasionally relying on the user to assist with type checking.

[Nick Mertes]

I wonder, in the spirit of PVS, if a tool can be built on top of Lean (without destroying Lean's logic) to allow the user "help" the type checker to do something like this:

def i_wish (n : Nat) (x : Fin n) : Fin (0 + n) := x

I could cast in the above situation, but as is also explained in Prelude.lean "It is best to avoid this function (cast) if you can, because it is more complicated to reason about terms containing casts"

[Kim Morrison]

That note is only trying to tell you to use Fin.cast in favour of _root_.cast.

[Kim Morrison]

So the right hand side should probably just be x.cast (by omega).