(Previously, I asked
about converting a term
a: A to a term of type
B provided that
A = B.
Apologies if this turns out to be (about) the same issue, but I am convinced
it's a different one.)
Let's say we have a structure like this (the latter example is included for completeness, but I am mainly interested in the propositional case if it makes any difference).
-- Example with a proposition structure Interval where lower: Nat upper: Nat lu: lower ≤ upper -- Example with a function structure Signature := symbol : Type arity : symbol → Type
Problem: I would like to prove that for any two intervals
a.lower = b.lower and
a.upper = b.upper, then
a = b.
(For instance to later define a pointwise partial order
on intervals, and prove that it's antisymmetric.)
As long as the structure contains no members whose types are dependent, this is a simple matter:
structure PreInterval where lower: Nat upper: Nat def PreInterval.eq (a b: PreInterval) (lEq: a.lower = b.lower) (uEq: a.upper = b.upper) : a = b := -- (Can this be done in fewer steps/without the middleman?) let aMid: a = ⟨b.lower, b.upper⟩ := lEq ▸ uEq ▸ rfl; let midB: ⟨b.lower, b.upper⟩ = b := rfl; Eq.trans aMid midB
However, this approach fails for members of dependent types (like
because their equality cannot be even stated (trying so
produces a "type mismatch" error, since they are of different
Applying the trick from the previous question does not seem to be of help, because it seems to me I don't need to convert one value into a value of the other type, I need to show that they are equal, despite that they have different types. (Or not?)
Is this possible? Or should I be doing something else?
Subquestion, if anybody knows the history:
I've looked around, and it seems to me that in Lean 2, there was
the concept of heterogenous equality, exactly for this purpose.
It allowed generalizing
congr for dependent types, and could even
be turned into a proof of regular equality! (Ctrl+F "heq.to_eq"
However, the only mention of heterogenous equality in Lean 4 that
I found was in the tutorial chapter 7,
which says it will be introduced in the next chapter, but it is not.
The source of Lean 4's Prelude warns against using it,
heq.to_eq seems to not exist anymore. What happended to