isDefEq on structures

Stream: lean4 dev

[Reid Barton]

mathlib's algebraic hierarchy design involves a lot of "defeq diamonds" which I have parodied in the following form.

structure Gr (α : Type) where
  add : α → α → α
  add_comm : ∀ (a b : α), add a b = add b a

def gr1 : Gr Nat where
  add x y := x + y
  add_comm x y := Nat.add_comm x y

def gr2 : Gr Nat where
  add x y := (x + y) + 0
  add_comm x y :=
    show (x + y) + 0 = (y + x) + 0
    from Nat.add_comm x y

set_option trace.Meta.isDefEq true in
#check (rfl : gr1 = gr2)

To check that gr1 and gr2 are defeq Lean checks that the add fields are defeq three times. The last two are to check that the types of the add_comm fields are defeq. But of course they have to be once the add fields are, because that's how structures work.
Couldn't Lean do better here?
(The trace output below is actually printed twice, but I think that's due to some detail of the way I set up the defeq test.)

trace output

[Meta.isDefEq] ✅ gr1 = gr2 =?= ?m.740 = ?m.740
  [Meta.isDefEq] ✅ Gr Nat =?= ?m.739
    [Meta.isDefEq] Gr Nat [nonassignable] =?= ?m.739 [assignable]
    [Meta.isDefEq] ✅ Sort ?u.738 =?= Type
  [Meta.isDefEq] ✅ gr1 =?= ?m.740
    [Meta.isDefEq] gr1 [nonassignable] =?= ?m.740 [assignable]
    [Meta.isDefEq] ✅ Gr Nat =?= Gr Nat
  [Meta.isDefEq] ✅ gr2 =?= gr1
    [Meta.isDefEq] ✅ gr2 =?= gr1
      [Meta.isDefEq] ✅ gr2 =?= { add := fun x y => x + y, add_comm := gr1.proof_1 }
        [Meta.isDefEq] ✅ Gr Nat =?= Gr Nat
        [Meta.isDefEq] ✅ gr2.add =?= fun x y => x + y
          [Meta.isDefEq] ✅ fun x y => x + y =?= fun a => Gr.add gr2 a
            [Meta.isDefEq] ✅ Nat =?= Nat
            [Meta.isDefEq] ✅ fun y => x + y =?= Gr.add gr2 x
              [Meta.isDefEq] ✅ fun y => x + y =?= fun a => Gr.add gr2 x a
                [Meta.isDefEq] ✅ Nat =?= Nat
                [Meta.isDefEq] ✅ x + y =?= Gr.add gr2 x y
                  [Meta.isDefEq] ✅ x + y =?= gr2.1 x y
                    [Meta.isDefEq] ✅ x + y =?= x + y + 0
                      [Meta.isDefEq] ✅ instHAdd.1 x y =?= instHAdd.1 (x + y) 0
                        [Meta.isDefEq] ✅ Add.add x y =?= Add.add (x + y) 0
                          [Meta.isDefEq] ✅ instAddNat.1 x y =?= instAddNat.1 (x + y) 0
                            [Meta.isDefEq] ✅ Nat.add x y =?= Nat.add (x + y) 0
                              [Meta.isDefEq] ❌ x =?= x + y
                                [Meta.isDefEq] ❌ x =?= instHAdd.1 x y
                                  [Meta.isDefEq] ❌ x =?= Add.add x y
                                    [Meta.isDefEq] ❌ x =?= instAddNat.1 x y
                                      [Meta.isDefEq] ❌ x =?= Nat.add x y
                                        [Meta.isDefEq.onFailure] ❌ x =?= Nat.add x y
                              [Meta.isDefEq] ✅ Nat.add x y =?= x + y
                                [Meta.isDefEq] ✅ Nat.add x y =?= Nat.add x y
        [Meta.isDefEq] ✅ gr2.add_comm =?= gr1.proof_1
          [Meta.isDefEq] ✅ ∀ (a b : Nat), Gr.add gr2 a b = Gr.add gr2 b a =?= ∀ (x y : Nat), x + y = y + x
            [Meta.isDefEq] ✅ Nat =?= Nat
            [Meta.isDefEq] ✅ Nat =?= Nat
            [Meta.isDefEq] ✅ Gr.add gr2 a b = Gr.add gr2 b a =?= a + b = b + a
              [Meta.isDefEq] ✅ Gr.add gr2 a b =?= a + b
                [Meta.isDefEq] ✅ gr2.1 a b =?= a + b
                  [Meta.isDefEq] ✅ a + b + 0 =?= a + b
                    [Meta.isDefEq] ✅ instHAdd.1 (a + b) 0 =?= instHAdd.1 a b
                      [Meta.isDefEq] ✅ Add.add (a + b) 0 =?= Add.add a b
                        [Meta.isDefEq] ✅ instAddNat.1 (a + b) 0 =?= instAddNat.1 a b
                          [Meta.isDefEq] ✅ Nat.add (a + b) 0 =?= Nat.add a b
                            [Meta.isDefEq] ❌ a + b =?= a
                              [Meta.isDefEq] ❌ instHAdd.1 a b =?= a
                                [Meta.isDefEq] ❌ Add.add a b =?= a
                                  [Meta.isDefEq] ❌ instAddNat.1 a b =?= a
                                    [Meta.isDefEq] ❌ Nat.add a b =?= a
                                      [Meta.isDefEq.onFailure] ❌ Nat.add a b =?= a
                            [Meta.isDefEq] ✅ a + b =?= Nat.add a b
                              [Meta.isDefEq] ✅ Nat.add a b =?= Nat.add a b
              [Meta.isDefEq] ✅ Gr.add gr2 b a =?= b + a
                [Meta.isDefEq] ✅ gr2.1 b a =?= b + a
                  [Meta.isDefEq] ✅ b + a + 0 =?= b + a
                    [Meta.isDefEq] ✅ instHAdd.1 (b + a) 0 =?= instHAdd.1 b a
                      [Meta.isDefEq] ✅ Add.add (b + a) 0 =?= Add.add b a
                        [Meta.isDefEq] ✅ instAddNat.1 (b + a) 0 =?= instAddNat.1 b a
                          [Meta.isDefEq] ✅ Nat.add (b + a) 0 =?= Nat.add b a
                            [Meta.isDefEq] ❌ b + a =?= b
                              [Meta.isDefEq] ❌ instHAdd.1 b a =?= b
                                [Meta.isDefEq] ❌ Add.add b a =?= b
                                  [Meta.isDefEq] ❌ instAddNat.1 b a =?= b
                                    [Meta.isDefEq] ❌ Nat.add b a =?= b
                                      [Meta.isDefEq.onFailure] ❌ Nat.add b a =?= b
                            [Meta.isDefEq] ✅ b + a =?= Nat.add b a
                              [Meta.isDefEq] ✅ Nat.add b a =?= Nat.add b a
              [Meta.isDefEq] ✅ Nat =?= Nat
[Meta.isDefEq] ✅ Gr Nat =?= Gr Nat
[Meta.isDefEq] ✅ Gr Nat =?= Gr Nat
[Meta.isDefEq] ✅ Gr Nat =?= Gr Nat
[Meta.isDefEq] ✅ Gr Nat =?= ?m.737
  [Meta.isDefEq] Gr Nat [nonassignable] =?= ?m.737 [assignable]
  [Meta.isDefEq] ✅ Sort ?u.736 =?= Type
[Meta.isDefEq] ✅ Gr Nat =?= Gr Nat

[Reid Barton]

This is extremely bad when combined with the way Lean checks defeq of projections (which lean4#2003 is about) if gr1 and gr2 are actually defined in terms of some other structures say comm_gr1 and comm_gr2 because checking equality of each field of the gr* triggers checking equality of the entirety of the comm_gr* structures, leading to huge blowups if this pattern is nested.
But even in a simple case like the one above we could save a lot of work by not testing things repeatedly.

[Reid Barton]

A related question which came up is whether, when we test isDefEq of two expressions, we are supposed to be allowed to assume that their types are already known to be defeq. This is the way type theories are usually presented on paper so I was assuming it was allowed to assume this, but Lean seems not to use this knowledge (for testing defeq of propositions specifically) so maybe it is not intended to be a precondition.

[Reid Barton]

As the example shows it's not just one extra check per "axiom" (like add_comm), but one per occurrence of a field in the axiom. So comm is 2, assoc is 4, distrib is 5, etc. Already for a Ring, it adds up fast.

[Reid Barton]

On the bright side, we can say that there is finally some practical purpose to figuring out whether the right unit axiom of a group follows from the left unit axiom

[Kevin Buzzard]

You might find that hard to remove that axiom even if you can prove it from the others, because group extends monoid and it's not true for monoids.