Equality of records with members whose types are dependent (Lean 4)

Question

(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 and b, if 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 lu), because their equality cannot be even stated (trying so produces a "type mismatch" error, since they are of different types).

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" here)

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, and heq.to_eq seems to not exist anymore. What happended to heq?

Answer 1

It is pretty simple. I'll give you a few options so you can learn more about Lean.

A brute force way to do it is to use calc. I know I taught you last time about ▸ but in your proof of PreInterval.eq since it is purely equational reasoning, you can just use calc for a straightforward and easy to read proof.

theorem Interval.eq_calc_proof
  (a b: Interval)
  (lEq: a.lower = b.lower)
  (uEq: a.upper = b.upper)
: a = b := calc
    a = ⟨ a.lower, a.upper, a.lu ⟩ := rfl
    _ = ⟨ b.lower, b.upper, b.lu ⟩ := by simp [lEq, uEq]
    _ = b := rfl

Notice the important thing is to solve ⟨ a.lower, a.upper, a.lu ⟩ = ⟨ b.lower, b.upper, b.lu ⟩ and the simp tactic is smart enough to solve this.

A very useful thing to understand about structures is that ultimately every property about structures and inductives come from their eliminator/recursor, in this case Interval.rec. While I don't encourage you to use it directly, knowing it exists helps. One way rec is used implicitely is in tactics and tools which let you work with inductives, like match, induction, and cases. (A structure is basically an inductive with one constructor mk.) By applying the cases tactic, we are reducing a structure to talking about the stuff inside the structure.

theorem Interval.eq_cases_proof
  (a b: Interval)
  (lEq: a.lower = b.lower)
  (uEq: a.upper = b.upper)
: a = b := by
  cases a
  cases b
  simp [lEq, uEq]

It may also help to see what is internally going on by using the more explicit version of the cases tactic:

theorem Interval.eq_cases_proof2
  (a b: Interval)
  (lEq: a.lower = b.lower)
  (uEq: a.upper = b.upper)
: a = b := by
  cases a with 
  | mk al au aul =>
    cases b with
    | mk bl bu bul =>
      simp [lEq, uEq]

Also along with the eliminator/recursor Interval.rec, Lean automatically generates a few helper theorems for each structure, including the following one. (In Lean 3 it is a bit easier to find these theorems. You can just type #print Interval. and Lean's autocomplete will fill in all possible completions after the projection dot .. Lean 4 doesn't have this yet.) See this answer for explanation about these automatic theorems and more about rec.

#check Interval.mk.injEq
-- Interval.mk.injEq :
-- ∀ (lower upper : Nat) (lu : lower ≤ upper)
--   (lower_1 upper_1 : Nat) (lu_1 : lower_1 ≤ upper_1),
-- ({ lower := lower, upper := upper, lu := lu } = 
--  { lower := lower_1, upper := upper_1, lu := lu_1 }) =
-- (lower = lower_1 ∧ upper = upper_1)

This theorem may be good enough for your purposes, but if not, you can easily use it to prove your lemma rewriting your goal with it:

theorem Interval.eq_injEq_proof
  (a b: Interval)
  (lEq: a.lower = b.lower)
  (uEq: a.upper = b.upper)
: a = b := by
  rw [Interval.mk.injEq]
  exact ⟨lEq, uEq⟩

(Note, all these proofs use the propext axiom which is used freely in Lean, even at the lowest levels. I believe this theorem requires it because you require that the proof of a.lu is equal to the proof of b.lu without giving that as an assumption. [Edit: I checked in Lean 3, which isn't so aggressive with propext and I can construct a proof with no extra axioms, besides proof irrelevance, which is built into the definitional equality rules of Lean's Prop.])

Answer 2

This is a very slick solution that I use all the time:

structure Interval where
  lower: Nat
  upper: Nat
  lu: lower ≤ upper

protected theorem Interval.eq : ∀ {a b : Interval}, a.lower = b.lower → a.upper = b.upper → a = b
| ⟨_,_,_⟩, ⟨_,_,_⟩, rfl, rfl => rfl

Maybe it's a bit too slick since it relies on the fact that structures have only one constructor and so does equality.

In tactic mode, the equivalent is this:

protected theorem Interval.eq' {a b : Interval} (hl : a.lower = b.lower) (hu : a.upper = b.upper) : a = b := by
  cases a
  cases b
  cases hl
  cases hu
  rfl

This version is a bit longer but it allows you to follow the reasoning step by step.

Answer 3

I think the simplest way of reproducing your error is this snippet, using × as the simplest "dependent record type":

def SigmaEq {α : Type u} (β : α → Type v)
  (a b : (x : α) × (β x)) :=
  (a.1 = b.1) ∧ (a.2 = b.2)

Lean4 thinks that a.2 and b.2 does not have the same type:

type mismatch
  b.snd
has type
  β b.fst : Type v
but is expected to have type
  β a.fst : Type v

And this quite understandable, because they indeed have different types. However, since we already have a proof p : a.1 = b.1, we can cast using this type:

theorem Eq.coe {α : Sort u} {P : α → Type v} {a b : α} (h₁ : Eq a b) (h₂ : P a) : P b :=
  Eq.ndrec h₂ h₁

def SigmaEq {α : Type u} (β : α → Type v)
  (a b : (x : α) × (β x)) :=
  (p : a.1 = b.1) ×' (p.coe a.2 = b.2)

(I've tried to use ndrec and subst directly, but subst seems to be only about propositions, and ndrec gives me strange error).

To construct something of type SigmaEq, we first construct the proof p : a.1 = a.2, then destruct p so that the type of a.2 becomes P b.1 instead of the original P a.1.

P.S. using heterogeneous equality is an overkill on the theory side and user experience side. The usual equality helps type inference: if you have a = b and you know the type of a, Lean can figure out the type of b. If it's heterogeneous, both sides should have their types known in advance. This may lead to extra type annotations and inconveniences. I also personally hate heterogeneous equality because it assumes axiom K in its elimination, but that's another story.