definition vs theorem

Stream: new members

[Holly Liu]

hi! i was wondering what the difference between definition and theorem is, and when to use one over the other? i'm reading about the pragmatic differences in the documentation but i'm still not understanding it.

[Mario Carneiro]

The rule used in mathlib is: if it's a proof (something whose type has type Prop), then use theorem or lemma, otherwise use def

[Holly Liu]

thanks!

[Mario Carneiro]

as for the technical differences:

• defs are elaborated synchronously, and can add additional local definitions to the environment
• theorem is opaque by default and you have to use some heavyweight tactics to get at the definition of the theorem after the fact
• The type of a def can depend on / be inferred from the term, while theorem requires that the type typecheck without looking at the term. So in particular def foo := bar works but theorem foo := bar doesn't, it always has to be theorem foo : type := bar

[Holly Liu]

what is the definition of the theorem?

[Mario Carneiro]

it checks the type of bar and that becomes the type of foo too

[Mario Carneiro]

for example:

def foo := 1 -- foo : nat
def bar := foo -- bar : nat

[Mario Carneiro]

Actually maybe that's not your question. def and theorem are both lean built-ins

[Holly Liu]

so is the definition of the theorem something you use to check the type of bar, something like using #check? sorry nevermind i think i understand. thanks

[Mario Carneiro]

I don't know what you mean by the definition of the theorem. The theorem is defined by the theorem foo : type := bar line

[Mario Carneiro]

you can see a definition after the fact (even for autogenerated definitions) using #print foo

[Mario Carneiro]

that will show you what lean inferred for all the missing bits

[Holly Liu]

yes i was getting confused about the semantics. that clears it up a lot.