fix: handle dependent fields when deriving BEq

[arthur-adjedj]

Closes #3740

If a field x : xType appears in the type of another field y : f xType, it's generally not possible to derive a faithful BEq instance because the two y fields won't necessarily have definitionally equal types. However, such a problem can be avoided whenever the BEq on xType is Lawful. This PR uses eq_of_beq whenever xType appears in another fvar's types, and unifies the dependent types as needed.

[timotree3]

One downside of this derive handler is that the code it produces using Eq.rec sometimes can't be reduced by the kernel, while a hand-written implementation might use easier to reduce type-specific operations like Fin.cast. For this to be a problem, it requires that (x == y) = true is a defeq but x = y is not, otherwise Eq.rec successfully reduces. A likely way this could happen is with quotients:

def ZMod5 : Type := Quot (· % 5 = · % 5)

abbrev ZMod5.val : ZMod5 → Nat :=
  Quot.lift (· % 5) sorry

instance : BEq ZMod5 where
  beq x y := x.val == y.val

instance : LawfulBEq ZMod5 := sorry

structure MyStruct where
  x : ZMod5
  y : Fin x.val

-- This is approximately what would be generated by `deriving BEq` after this PR
def instBEqGenerated : BEq MyStruct where
  beq x y :=
    if h : x.1 == y.1 then
      let x2' : Fin y.1.val := (eq_of_beq h) ▸ x.2
      x2' == y.2
    else
      false

def instBEqPreferred : BEq MyStruct where
  beq x y :=
    if h : x.1 == y.1 then
      let x2' : Fin y.1.val := Fin.cast (eq_of_beq h) x.2
      x2' == y.2
    else
      false

#reduce instBEqPreferred.beq ⟨Quot.mk _ 6, 0⟩ ⟨Quot.mk _ 11, 0⟩ -- true
#reduce instBEqGenerated.beq ⟨Quot.mk _ 6, 0⟩ ⟨Quot.mk _ 11, 0⟩ -- _ (Nat.rec _ _ (⋯ ▸ 0))

That said, it doesn't seem feasible in the short term to generate code using functions like Fin.cast, so I don't think this concern should block the PR. In the long term, this could be solved with a typeclass EqFunctor F where mapEq : x = y → F x → F y .

[semorrison]

LGTM. Could you mark this as ready for review if you're happy to proceed with this?

[semorrison]

@arthur-adjedj, could you take a look at the CI failure?

[arthur-adjedj]

As it turns out, some parts of the code rely on the reduction behaviour of the derived instances, and these issues only arise when compiling on stage2, which I didn't try locally until now. Most of these are easy to correct, but I would rather not make this fix a breaking change, and I don't have much time to allocate to fixing this PR right now. I'll mark this as WIP and ping you back once I get this in a better state. Sorry for the trouble.

[arthur-adjedj]

WIP

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d4d7c72365f9278a384719b176a24cf2adb8e11e --onto 93c9ae7c20b1d0ba4faa18e361dfadc45543ac12. (2024-06-29 14:45:01)
• ✅ Mathlib branch lean-pr-testing-3792 has successfully built against this PR. (2024-06-29 19:25:21) View Log
• ✅ Mathlib branch lean-pr-testing-3792 has successfully built against this PR. (2024-06-30 11:05:04) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0768ad4eb9020af0777587a25a692d181e857c14 --onto 5938dbbd14145c9b78f7645c4777f62a3fc8212c. (2024-07-25 00:56:01)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 54c22efca1cb6fdcea694b894ca9830d0b5c4b0e --onto 39e0b41fe1ab4d16f15efb0dc9bd7607a8941713. (2024-07-26 01:32:00)

[arthur-adjedj]

@semorrison
I have managed to get the same reduction behavior for derived instances as was previously present. This implied reordering the appearance of the construction of rhs, and removing the initial true value where it wasn't necessary. The only difference left between this and the previous implementation is that the chaining of && operations is now done from left to right instead of right to left (see src/Init/Data/Nat/Linear.lean, where eq₁ == eq₂ && lhs₁ == lhs₂ && rhs₁ == rhs₂ becomes eq₁ == eq₂ && (lhs₁ == lhs₂ && rhs₁ == rhs₂)). This only breaks one place of the codebase, and Batteries/Mathlib seems to compile correctly. Lastly, this update requires an update to stage0, which I believe implies some complications with regards to the merging process ?

[semorrison]

I have rebased this onto nightly-with-mathlib, re-running the update stage0 step, and then force pushed.

[semorrison]

Oops, there are stage0 changes since nightly-with-mathlib. Repeating, but rebasing onto master.

[semorrison]

Could you confirm that I correctly removed the WIP label?

[arthur-adjedj]

Ah yes, not putting this as awaiting-review was an oversight on my end.