isDefEq not transitive?

Stream: mathlib4

[Thomas Murrills]

Here's something strange: defeq is apparently not transitive at reducible transparency. Is this a known caveat, or is something odd about the following example?

import Lean
import Mathlib.Data.List.Basic

open Lean Elab Expr Meta Tactic
/-- Check that the types of two fvars in the context are defeq at reducible transparency. -/
syntax (name := checkDefEq) "check_defEq " ident ident : tactic

elab_rules : tactic
| `(tactic| check_defEq $x $y) => withMainContext do
  let x ← getFVarId x
  let y ← getFVarId y
  unless (← withNewMCtxDepth <| withReducible <| isDefEq (← x.getDecl).type (← y.getDecl).type) do
    throwError "{(← x.getDecl).type} and {(← y.getDecl).type} are not defeq"

-- Transitivity doesn't hold:
example (h₁ : 1 - 1 = x) (h₂ : 0 = x) : True := by
  have h₃ := h₁
  simp at h₁
  check_defEq h₁ h₂ -- works
  check_defEq h₂ h₃ -- works
  check_defEq h₁ h₃ -- 0 = x and 1 - 1 = x are not defeq
  trivial

You'll notice that this imports Mathlib.Data.List.Basic. If I weaken it to Mathlib.Data.Init.Core, the problem goes away. I'm still trying to locate the offending import. Whatever it is, it's something to do with instances—there's no issue at .instances transparency.

[Eric Wieser]

My guess is lean4#2074

[Eric Wieser]

But in general defeq-as-judged-by-the-kernel isn't transitive

[Thomas Murrills]

That's odd. Shouldn't it be?

[Eric Wieser]

My memory is that this is the thing that Coq people complain about; Lean makes a set of choices that makes perfect defeq checking intractible (or something). It turns out we hardly ever care.

[Jireh Loreaux]

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/subject.20reduction for an in-depth discussion

[Thomas Murrills]

ah, that thread will be very informative, thanks!

[Mario Carneiro]

I don't think this example has anything to do with that though, this is a really basic transitivity failure

[Johan Commelin]

I think @Chris Hughes posted another basic example a while ago.
Over here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Nontransitivity.20of.20DefEq

[Gabriel Ebner]

mathlib-free version:

import Lean

class Zero (α : Type u) where
  zero : α

instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
  ofNat := ‹Zero α›.1

instance : Zero Nat where
  zero := 0

open Lean Elab Expr Meta Tactic in
/-- Check that the types of two fvars in the context are defeq at reducible transparency. -/
elab (name := checkDefEq) "check_defEq " x:term:max y:term:max : tactic => withMainContext do
  let x ← getFVarId x
  let y ← getFVarId y
  unless (← withNewMCtxDepth <| withReducible <| isDefEq (← x.getDecl).type (← y.getDecl).type) do
    throwError "{(← x.getDecl).type} and {(← y.getDecl).type} are not defeq"

-- Transitivity doesn't hold:
example (h₁ : 1 - 1 = x) (h₂ : 0 = x) : True := by
  have h₃ : @OfNat.ofNat Nat (nat_lit 0) Zero.toOfNat0 = x := h₁
  check_defEq h₁ h₂ -- works
  check_defEq h₂ h₃ -- works
  check_defEq h₁ h₃ -- 0 = x and 1 - 1 = x are not defeq
  trivial

[Gabriel Ebner]

I'm 99% sure this is a bug. lean4#2109

[Gabriel Ebner]

@Thomas Murrills Is this issue blocking anything?

[Thomas Murrills]

Luckily it’s not blocking anything at all! It just happened to come up while making a test for fail_if_no_progress.

[Gabriel Ebner]

As a very very very hacky workaround, we could redefine Zero.toOfNat0 as follows:

instance Zero.toOfNat0 [Zero α] : OfNat α (nat_lit 0) :=
  ‹Zero α›.casesOn (⟨·⟩)