## Stream: new members

### Topic: lemma, theorem, def

#### 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?

#### Johan Commelin (Feb 05 2021 at 08:00):

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

#### Johan Commelin (Feb 05 2021 at 08:00):

So you cannot use lemma and def interchangeably

#### 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

#### 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?

#### 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.

#### Kevin Buzzard (Feb 05 2021 at 08:05):

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

#### Huỳnh Trần Khanh (Feb 05 2021 at 08:07):

that clears it up, thanks!

#### 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 value,
intro accumulated,
exact accumulated + value,
end
end


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

#### 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

#### 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

#### 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
{"ft_lang_label":"__label__en","ft_lang_prob":0.8990092,"math_prob":0.48892057,"size":2268,"snap":"2021-21-2021-25","text_gpt3_token_len":635,"char_repetition_ratio":0.15282686,"word_repetition_ratio":0.07594936,"special_character_ratio":0.2813051,"punctuation_ratio":0.13319239,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9776764,"pos_list":[0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24],"im_url_duplicate_count":[null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null,null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2021-05-10T18:36:49Z\",\"WARC-Record-ID\":\"<urn:uuid:9ab2e015-579d-4a1e-b5e7-ed0c8ad23061>\",\"Content-Length\":\"14083\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:6e4722bc-d79b-4fa8-bcd1-8160b3b9e0bb>\",\"WARC-Concurrent-To\":\"<urn:uuid:41e464a0-eeb9-45bd-89dc-671b6d38a6d3>\",\"WARC-IP-Address\":\"185.199.110.153\",\"WARC-Target-URI\":\"https://leanprover-community.github.io/archive/stream/113489-new-members/topic/lemma.2C.20theorem.2C.20def.html\",\"WARC-Payload-Digest\":\"sha1:SJY4G6HLZ5OOW7DOWM42OOW6XEOZ3KNE\",\"WARC-Block-Digest\":\"sha1:355ZD2FY3QOE2XYZ33LHG2HXBWQHRE7Q\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2021/CC-MAIN-2021-21/CC-MAIN-2021-21_segments_1620243991759.1_warc_CC-MAIN-20210510174005-20210510204005-00088.warc.gz\"}"}