le_rfl proves sorry le sorry

Stream: general

[Johan Commelin]

Is this expected:

def foo (n : ℕ) : ℤ := sorry

lemma bar : foo 0 ≤ foo 1 := le_rfl -- no errors, nothing

[Yakov Pechersky]

import data.int.basic

def foo (n : ℕ) : ℤ :=
nat.rec_on n sorry (λ _, sorry)

lemma bar : foo 0 ≤ foo 1 := le_rfl -- that properly errors

[Yakov Pechersky]

This is probably the same issue as I saw for arbitrary in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/ring.20not.20respecting.20arbitrary

[Johan Commelin]

Thanks! I'll keep that in mind, and maybe use it for some sorried defs in LTE.

[Kevin Buzzard]

Yes I think Patrick discovered this years ago. This is why it's dangerous to build an API on sorried data!

[Mario Carneiro]

The correct way to do this is def foo : ℕ -> ℤ := sorry

[Mario Carneiro]

or def foo (n : ℕ) : ℤ := (sorry : ℕ -> ℤ) n

[Mario Carneiro]

or def foo (n : ℕ) : ℤ := by revert_all; sorry

[Johan Commelin]

Mario, thanks, that last one is useful!