lemma, theorem, def

Stream: new members

[Huỳnh Trần Khanh]

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

[Johan Commelin]

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

[Johan Commelin]

So you cannot use lemma and def interchangeably

[Huỳnh Trần Khanh]

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]

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]

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

[Kevin Buzzard]

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

[Huỳnh Trần Khanh]

that clears it up, thanks!

[Huỳnh Trần Khanh]

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]

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]

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]

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