Zulip Chat Archive

Stream: new members

Topic: lemma, theorem, def


view this post on Zulip Huỳnh Trần Khanh (Feb 05 2021 at 07:57):

it seems that the three keywords are equivalent. why does Lean have those aliases?

view this post on Zulip Johan Commelin (Feb 05 2021 at 08:00):

lemma and theorem are equivalent. They are proof irrelevant. def is for data.

view this post on Zulip Johan Commelin (Feb 05 2021 at 08:00):

So you cannot use lemma and def interchangeably

view this post on Zulip Huỳnh Trần Khanh (Feb 05 2021 at 08:01):

can you please post a code snippet where i can't replace lemma/theorem with def, that'd be much appreciated

view this post on Zulip Huỳnh Trần Khanh (Feb 05 2021 at 08:02):

or I can always replace lemma/theorem with def but there are some cases where I can't replace def with lemma/theorem?

view this post on Zulip Johan Commelin (Feb 05 2021 at 08:04):

Sure, you can use def when you would use lemma. I don't think it will break much.

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 08:05):

But if you replace def with lemma then your proofs about the definition will break

view this post on Zulip Huỳnh Trần Khanh (Feb 05 2021 at 08:07):

that clears it up, thanks!

view this post on Zulip Huỳnh Trần Khanh (Feb 05 2021 at 08:11):

one more question, why does this definition work?

def accumulate : list    := begin
  intro input,
  exact list.reverse_rec_on input
  begin
    exact 0,
  end
  begin
    intro head,
    intro value,
    intro accumulated,
    exact accumulated + value,
  end
end

wow i can define a function using syntax that looks like a proof

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 08:15):

If you use a tactic like rw when defining data then you might find that the term generated by Lean is nasty, meaning that you will have difficulty proving theorems about your definition. Here you should be fine though -- you can #print accumulate after the definition and check that it looks reasonable

view this post on Zulip Kevin Buzzard (Feb 05 2021 at 08:17):

Tactics like rw generate proof terms with eq.rec in, often buried under other junk, so it's unwise to use them in definitions

view this post on Zulip Johan Commelin (Feb 05 2021 at 09:05):

@Huỳnh Trần Khanh tactics like intro and exact are very "transparent" tactics (my terminology). They just put terms together using the basic building blocks of lambda calculus. So those tactics are safe to use in definitions. But as Kevin explains, other tactics create really ugly terms which you don't want in your definitions.


Last updated: May 10 2021 at 18:22 UTC