Unexpected behavior of sorry

Stream: lean4

[Tomas Skrivan]

I got really badly tripped over by the fact that

def F (x : X) : X := sorry

does not behave the same as

def G : X → X := sorry

In particular, I find surprising that this proofs passes

example (a b : Nat) : F a = F b := by rfl; done  -- rfl succeeds

and this fails as expected

example (a b : Nat) : G a = G b := by rfl; done  -- rfl fails

Is this expected behavior?

[Gabriel Ebner]

It is certainly well known and there are regular threads about this here on Zulip.

[Tomas Skrivan]

I guess it boils down to if we want this work or not

example : (sorry : Nat) = (sorry : Nat) := by rfl; done

[Tomas Skrivan]

I see, it is not known to me :grinning: and I didn't stumble on such a thread yet.

[Sebastian Ullrich]

Making isDefEq nonreflexive sounds like a perfect recipe for disaster, even if it's restricted to the elaborator

[Gabriel Ebner]

We don't have to make isDefEq nonreflexive. We'd only need to make the sorry elaborator nondeterministic (i.e., returns a different expression every time).

[Tomas Skrivan]

Yes return different expression every time and also capture local variables.

For example

def F (x : X) : X := sorry

would expand to

axiom F.sorry {X} : X → X
def F (x : X) : X := F.sorry x

[Sebastian Ullrich]

There could be quite a few local variables! But it's an interesting suggestion.

[Tomas Skrivan]

It might not be so bad as the variable capture is not necessary for propositional sorry.

[Kevin Buzzard]

The moral I've always taken from this story is "don't ever sorry definitions and then start writing proofs about them, because the proofs might break later"

[Tomas Skrivan]

That is exactly what I have learned the hard way :grinning_face_with_smiling_eyes: