# Zulip Chat Archive

## 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 head,
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: Dec 20 2023 at 11:08 UTC