Code review request

Stream: new members

[Martin Dvořák]

Hi! I am new to Lean.

Would somebody experienced be willing to perform a code review for (any subset of) my three recent attempts at proving theorems in Lean, please? They are all very well-known theorems and they are all very easy to prove; therefore, I could easily google for solutions by other people and read them. However, I would like to get a feedback directly on the code that I wrote.

Limits of sequences (very basic properties):
http://pub.ist.ac.at/~mdvorak/Lean/Sequences_limits.lean

Complete induction (proved using the standard induction):
http://pub.ist.ac.at/~mdvorak/Lean/Complete_induction.lean

Cantor's theorem (or rather a theorem whose corollary is the Cantor's theorem):
http://pub.ist.ac.at/~mdvorak/Lean/Cantor_explained.lean

[Patrick Massot]

Hint: if you create a proper Lean project and push it to GitHub then people will be able to type leanproject get martin_gihtub_login:martin_project and immediately play with it

[Martin Dvořák]

Oh. Is there any step-by-step guide on how to create a proper Lean project? So far, I have always played with single files.

[Eric Wieser]

(for me, your webserver is serving up those files with no encoding; meaning they end up garbled when I try to read them in-browser)

[Martin Dvořák]

I am sorry. I will try to fix it. I have never dealt with encoding before. Clearly, I need Unicode for Lean files.

[Patrick Massot]

The unicode issue will become irrelevant once you'll follow https://leanprover-community.github.io/install/project.html#creating-a-lean-project

[Martin Dvořák]

Thank you!

[Martin Dvořák]

Can you please check it here?

https://github.com/madvorak/Lean-first-steps

[Eric Wieser]

A quick comment: you should not be using λ (t : T), ¬g t t, and should instead use λ (t : T), t ∉ g t. Calling sets as functions results in weird statements that read as nonsense and don't match any lemmas.

[Martin Dvořák]

Thank you!

In fact, I was playing with the difference between ℕ → Prop and set ℕ in the file Complete_induction.lean. I realized that with sets I can use both ∈ and function syntax, whereäs with props I can use only the function syntax. This distinction showed me that the word set is probably more than a syntactic sugar; however, I didn't elaborate more.

[Martin Dvořák]

Do you think I should also replace P : ℕ → Prop by P : set ℕ in the induction (where P is the first parameter — the property I claim natural numbers to have) ?