How does def differ from theorem?

Stream: lean4

[Bob Rubbens]

I was tinkering with lean 4, and I ran into the following difference. Even though I use exactly the same lambda term to construct both a theorem and a def, lean handles them differently. Is there an explanation about how this is implemented, or can someone maybe explain it? Is it the fact that proof irrelevance requires that "theorem5" is actually allowed to behave differently from "def5", even though I used the exact same term, and Prop is nowhere in sight?

def def5: Nat → Nat := fun _ => 5
theorem theorem5: Nat → Nat := def5

theorem result5 : def5 n = theorem5 m := by
  have hdef : def5 n = 5 := by
    rfl
    done
  have htheorem : theorem5 m = 5 := by
    -- rfl -- Not sure what to do here, I would expect it would just become 5 but apparently for theorems this definition is not handled transparently...?
    sorry
  simp [hdef, htheorem]
  done

#eval def5 0 -- Ok, prints 5
#eval theorem5 0 -- Error, "failed to compile definition, consider marking it as 'noncomputable' because it depends on 'theorem5', and it does not have executable code"

Thanks for any tips, sources or explanations!

[David Renshaw]

Note that you get the same error for def5 if you instead define it as

noncomputable def def5: Nat → Nat := fun _ => 5

[Bob Rubbens]

Yes, excuse my slowness, in what way is that significant? They still reduce to exactly the same term, right?

[David Renshaw]

You can think of theorem as syntactic sugar for noncomputable def (plus maybe @[irreducible] and a few other attributes, I forget exactly which)

[David Renshaw]

This works for your htheorem:

  have htheorem : theorem5 m = 5 := by
    unfold theorem5 def5
    rfl

[Ruben Van de Velde]

theorem is meant for theorems, not definitions. In particular, the value is not usable

[Eric Rodriguez]

David Renshaw said:

You can think of theorem as syntactic sugar for noncomputable def (plus maybe @[irreducible] a few other attributes, I forget exactly which)

there's also some stuff about when the expected type gets elaborated

[David Renshaw]

It would be cool if theorem had some hovertext that explained this stuff. Or maybe if jump-to-def on theorem took you to some helpful docs.

[Mario Carneiro]

PR's welcome...

[Bob Rubbens]

@David Renshaw Ah thanks, I was wondering if something like that is possible. That kind of clears it up for me.

Just out of academic interest, a follow up question: it is safe to unfold (supposedly) opaque definitions like this, as it is only possible to unfold them anyway in a theorem context? In other words, it is impossible to write a def which sneakily uses result5 to (indirectly) use theorem5 to compute a value?

Sorry for being so specific, I am just very confused about where the line is in lean between computability and noncomputability, and how lean enforces this. On the one hand in lean it seems to be handled watertight, and on the other hand the approach of using "noncomputable" and some attributes here and there feels ad-hoc to me (and hence must be leading to problems somewhere, is my intuition).

[Mario Carneiro]

What lean calls "computable" is really "try to compile it to executable code and error otherwise". When you put noncomputable (or theorem) on a definition you are instructing the compiler not to generate code for it, so if you ever try to call this function later from compiled code (i.e. another computable def or directly in #eval) then it will cause an error because there is no function to call

[Mario Carneiro]

it's not really a static analysis, it's directing the actual output of the process

[Bob Rubbens]

Huh, okay. But I can see the term that is constructed using #print. So I guess the code generated and the term (which in my case happens to be computable) are different things deep inside lean, then, right?

[Mario Carneiro]

that's right

[Bob Rubbens]

I see, okay. It feels like such a smart system though so I can't help myself wondering what it is doing behind the scenes

[Mario Carneiro]

the term is what is used by the kernel and elaborator

[Bob Rubbens]

(And also then how it guarantees soundness of it all. But I guess in code generation this is not so strict)

[Mario Carneiro]

the generated code is sort of separate / parallel to the rest of it

[Mario Carneiro]

I believe you can also #print generated code, it has some magic names derived from the original

def foo : Nat := 5
#print foo._cstage1 -- unsafe def foo._cstage1 : Nat := 5
#print foo._cstage2 -- unsafe def foo._cstage2 : _obj := 5

theorem foo' : Nat := 5
#print foo'._cstage1 -- unknown constant 'foo'._cstage1'
#print foo'._cstage2 -- unknown constant 'foo'._cstage2'

[Eric Wieser]

Why is theorem foo : Nat := 1 legal in the first place?

[Kevin Buzzard]

It's not legal in mathlib in the sense that a linter will complain.

[Eric Wieser]

Right, but this regularly trips up new users who aren't working in mathlib or running the linter

[Eric Wieser]

And it's not clear that the current behavior is wanted by anyone

[Bob Rubbens]

Would you prefer getting an error or warning when the type in a theorem statement is of a universe that doesn't make sense in the usual case you use Lean? Not trying to be annoying, just trying to make concrete (and curious about) what the non-intuitive part is you are talking about here.

[Mario Carneiro]

I think it would be reasonable and relatively easy to upgrade the defTheorem linter to a core linter so that it triggers immediately without #lint

[Mario Carneiro]

there are use cases for defs of prop type but I don't know any for theorems containing data. @[irreducible] def or opaque is the alternative I would suggest for those cases

[Eric Wieser]

What's the use case for def for proofs? I believe one could exist, but I can't think of one myself

[Eric Wieser]

In lean 3, one answer was that the def allowed an incomplete type so that you could work out the statement by writing the proof, but that doesn't work any more in lean 4

[Markus Schmaus]

In lean 4 it's possible to omit the type entirely with def and therefore have a def lemma state whatever the proof ends up proving. I've written a transform tactic based on conv which uses this feature:

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Using.20Tactics.20to.20Generate.20.60.3D.60.20Theorems/near/404933569

[Kyle Miller]

I had added an error for using theorem with data in Lean 3:

theorem a : nat := 1
-- error: theorems do not get VM compiled, use 'def' or add 'noncomputable' modifier to 'a'

I don't remember if there were any use cases for noncomputable theorem though. (#704 and #712)