Weird behavior of sorried definitions

Stream: general

[Adrian Marti]

While playing around with AI I ran into something that surprised me. I had a definition, where a constant was sorried, and the AI managed to prove all sorts of things about it. I extracted a minimal example:

def t (k : Nat) : Nat := sorry

theorem t_zero : t 0 = 5 := sorry

theorem t_one : t 1 = 5 := by
  unfold t -- can omit this
  exact t_zero

-- Also works like this
theorem t_two : t 2 = 5 := t_zero

Is this intended behavior? I would expect that we wouldn't be able to prove anything about the values of t for nonzero numbers.

[Floris van Doorn]

If you replace your definition by this, then everything after t_zero will fail:

def t : Nat → Nat := sorry

[Floris van Doorn]

Each sorry is unique, so e.g. this fails:

example : (sorry : Nat) = (sorry : Nat) := rfl

But if you write

def t (k : Nat) : Nat := sorry

then Lean (currently) interprets this as the constant function with some unknown value.

(cc @Kyle Miller)

[Adrian Marti]

The fact that each sorry is unique makes a lot of sense to me, intuitively. I always thought of sorry as adding an opaque constant to the theory that we can't prove anything about, so your example
example : (sorry : Nat) = (sorry : Nat) := rfl
failing makes a lot of sense to me. It didn't cross my mind that it could be the constant function with some unknown value, thanks a lot for explaining this! I kind of expected to be a term in context k : Nat |- sorry : Nat, but it's good to know that it isn't so!

[Max Nowak 🐉]

Also maybe tagging your stuff as irreducible could help.

[Jakub Nowak]

Hm, I sometimes use sorry in definitions when I want to fill it in in a way that makes my proof work. Is there some easy way to introduce dependant meta-variable? I guess that works:

def t (k : Nat) : Nat :=
  if k > 2 then
    (sorry : Nat → Nat) k
  else
    (sorry : Nat → Nat) k

Maybe it doesn't matter, I've never had a problem with this behaviour of sorry.