changing a proof can break a later proof

Stream: lean4

[Jovan Gerbscheid]

When working on #21330, which changes some aesop proofs to be rfl proofs, I discovered that replacing a proof in one declaration can break a proof in a later declaration. This seems very worrying to me, because it means that a proof can be, in some sense, "wrong" even if lean says it is correct. And making a change to a proof in one file can break a later file.

Here is the minimal working example:

abbrev Comma : Type := PLift (4 = 4)

variable [Inhabited Comma]

structure CommaMorphism (c : Comma) where
  s : String
  w : default = c

def mk (s : String) : CommaMorphism ⟨rfl⟩ where
  s := s
  w := rfl -- replace this with `id rfl` for the example to work

/-
(kernel) declaration type mismatch, '_example' has type
  ∀ [inst : Inhabited Comma] (X : Comma) (f : CommaMorphism X), f = f
but it is expected to have type
  ∀ [inst : Inhabited Comma] (X : Comma) (f : CommaMorphism X), f = mk f.s
-/
example (X : Comma) (f : CommaMorphism X) :
  f = mk f.s := by rfl

By using #print mk, we can see how the different proofs of w affect the definition of mk. If the proof is given as rfl, then #print mk shows that the proof is replaced by mk.proof_2 : default = default, but when the proof is given as id rfl, then it shows mk.proof_2 : default = { down := rfl }. Although these versions are definitionally equal (as proven by rfl), the second option is better because it matches the expected type of the proof.

Interestingly, this minimal example can also be fixed by replacing default = c with c = default

The original example involved the Discrete category, in which a morphism from X to Y is defined as a PLift of X = Y, and the relevant constants are CategoryTheory.Comma.fromProd and CategoryTheory.Comma.equivProd.

[Aaron Liu]

I've encountered this issue before while working on @Kevin Buzzard 's Formalizing Mathematics about half a year ago.

[Kyle Miller]

Interesting. This is an example of the elaborator defeq accepting something the kernel defeq doesn't.

I wouldn't attribute the error to the way AbstractNestedProofs works. There's no reason to expect the following variation to fail:

abbrev Comma : Type := PLift (4 = 4)

variable [Inhabited Comma]

structure CommaMorphism (c : Comma) where
  s : String
  w : default = c

theorem proof_2 : default = (default : Comma) := rfl

def mk (s : String) : CommaMorphism ⟨rfl⟩ where
  s := s
  w := proof_2

/-
(kernel) declaration type mismatch, '_example' has type
  ∀ [inst : Inhabited Comma] (X : Comma) (f : CommaMorphism X), f = f
but it is expected to have type
  ∀ [inst : Inhabited Comma] (X : Comma) (f : CommaMorphism X), f = mk f.s
-/
example (X : Comma) (f : CommaMorphism X) :
  f = mk f.s := rfl

[Junyan Xu]

This is an example of the elaborator defeq accepting something the kernel defeq doesn't.

Maybe connected to #mathlib4 > Slow rfl (timeout) with `Algebra.adjoin` @ 💬 which is also about structure eta.