getting started questions

Stream: new members

[Yunjiang Jiang]

Is there an existing stream for beginner questions? I am puzzled by line 49 of the beginner exercise file:

infix ` is_a_max_of `:55 := is_max.

What does 55 stand for? It may be helpful to add an explanation in the tutorial.

[Notification Bot]

This topic was moved here from #general > getting started questions by Bryan Gin-ge Chen

[Bryan Gin-ge Chen]

The 55 denotes the "precedence" of the notation. It's not something you have to worry about at that point in the tutorial, but if you're interested you can read more about it in TPiL: https://leanprover.github.io/theorem_proving_in_lean/interacting_with_lean.html#notation

(As you can see, I've moved your question to the #new members stream.)

[Yunjiang Jiang]

Thanks @Bryan Gin-ge Chen! I added this as a comment in the tutorial.

[Yunjiang Jiang]

I tried compiling the tutorial exercise tutorials/src/exercises/00_first_proofs.lean but got a bunch of errors. I tried both homebrew and the curl installation. Any tip on how compile works?

yunjiang.jiang@jdadmins-MacBook-Pro dev % lean tutorials/src/exercises/00_first_proofs.lean
/Users/yunjiang.jiang/dev/tutorials/src/exercises/00_first_proofs.lean:1:0: error: file 'data/real/basic' not found in the search path
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more
/Users/yunjiang.jiang/dev/tutorials/src/exercises/00_first_proofs.lean:1:0: error: file 'tactic/suggest' not found in the search path
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more
/Users/yunjiang.jiang/dev/tutorials/src/exercises/00_first_proofs.lean:11:0: error: invalid import: data.real.basic
could not resolve import: data.real.basic
/Users/yunjiang.jiang/dev/tutorials/src/exercises/00_first_proofs.lean:11:0: error: invalid import: tactic.suggest
could not resolve import: tactic.suggest
/Users/yunjiang.jiang/dev/tutorials/src/exercises/00_first_proofs.lean:15:0: error: command expected
/Users/yunjiang.jiang/dev/tutorials/src/exercises/00_first_proofs.lean:24:7: error: unknown identifier 'upper_bounds'
/Users/yunjiang.jiang/dev/tutorials/src/exercises/00_first_proofs.lean:27:23: error: unknown identifier 'ℝ'
/Users/yunjiang.jiang/dev/tutorials/src/exercises/00_first_proofs.lean:27:35: error: unknown identifier 'ℝ'

...

[Kevin Buzzard]

Did you install the tutorial using leanproject? You need to be in the tutorial directory to make command line Lean work as Lean needs to know precisely which version of Lean and mathlib it's using and it will see it from the leanpkg.toml file in the tutorial directory.

[Yunjiang Jiang]

@Kevin Buzzard Thanks! I installed using leanproject and it did work inside tutorial directory now. The latex shortcut with vscode is also really nice.

[Yunjiang Jiang]

Also this line does not work for me code tutorials. Is the code command specific to MacOS? I am not familiar with it.

[Kevin Buzzard]

Just open VS Code in any way you like, and then select "File -> Open Folder" and select the tutorials directory.

[Yunjiang Jiang]

I have a really hard time understanding this proof in the tutorial. What does the line cases hx with x_in x_up mean exactly? Are x_in and x_up the two cases that hx gets broken into? Is the unique maximum property of \R used implicitly in linarith?

/-
Let's prove something now! A set of real numbers has at most one maximum. Here
everything left of the final : is introducing the objects and assumption. The equality
x = y right of the colon is the conclusion.
-/
lemma unique_max (A : set ℝ) (x y : ℝ) (hx : x is_a_max_of A) (hy : y is_a_max_of A) : x = y :=
begin
-- We first break our assumptions in their two constituent pieces.
-- We are free to choose the name following with
cases hx with x_in x_up,
cases hy with y_in y_up,
-- Assumption x_up means x isn't less than elements of A, let's apply this to y
specialize x_up y,
-- Assumption x_up now needs the information that y is indeed in A.
specialize x_up y_in,
-- Let's do this quicker with roles swapped
specialize y_up x x_in,
-- We explained to Lean the idea of this proof.
-- Now we know x ≤ y and y ≤ x, and Lean shouldn't need more help.
-- linarith proves equalities and inequalities that follow linearly from
-- the assumption we have.
linarith,
end

[Kyle Miller]

Are you able to step through the proof to see how the goal state changes after each tactic?

Assuming you do, then what cases does is take hx, which is a proof that x is_a_max_of A, and then split it up into its two parts and give the parts names. If I remember correctly, x is_a_max_of A is a conjunction consisting of the fact that x ∈ A and that x is at least as large as every element of A. So, x_in becomes a proof of the first fact, and x_up a proof of the second.

[Kyle Miller]

linarith looks at inequalities in the current context and tries to prove the goal automatically. I don't think it knows anything about ℝ per se.

[Kyle Miller]

Also, if this is the 00_first_proofs file, if I remember right it's more of an overview of things that are covered again in the next tutorials, so you might want to skip ahead if.

[Yunjiang Jiang]

@Kyle Miller Thanks that helps a lot. How does stepping through work with lean? Also the lemma is false for general posets right? So surely it uses the linear ordering property of A somewhere? I will take a look at the next tutorial as you suggested.

[Kyle Miller]

Are you using VS Code? There should be a goal window that you can open up, and as you move your cursor around it will update with relevant information.

[Kyle Miller]

@Yunjiang Jiang I haven't opened up this file to check, but based on the comments that you have copied, I'm pretty sure linarith is just applying an antisymmetry lemma given the fact that x ≤ y and y ≤ x have been proved. The lemma might be false in general, but this last step is true for posets. (linarith doesn't seem to apply the general poset lemma le_antisymm but rather its own linarith.eq_of_not_lt_of_not_gt for linear orders.)

If you don't have an interactive goal window working, this will be very hard to follow!

[Yunjiang Jiang]

@Kyle Miller I managed to get the goal displayed on the side panel now. Previously I opened a vscode workspace at the parent directory of the tutorial project, which had many compilation errors. It's indeed quite useful! Regarding posets, you are right linarith application is pretty straightforward. The deduction of $x \le y$ actually comes from the definition of is_max, which is given above

/-- The set of upper bounds of a set of real numbers ℝ -/
def up_bounds (A : set ℝ) := { x : ℝ | ∀ a ∈ A, a ≤ x}

/-- Predicate `is_max a A` means `a` is a maximum of `A` -/
def is_max (a : ℝ) (A : set ℝ) := a ∈ A ∧ a ∈ up_bounds A

[Heather Macbeth]

To aid your readers, enclose a Lean code block with triple ` above and below, see #backticks.

/-- The set of upper bounds of a set of real numbers ℝ -/
def up_bounds (A : set ℝ) := { x : ℝ | ∀ a ∈ A, a ≤ x}

/-- Predicate is_max a A means a is a maximum of A -/
def is_max (a : ℝ) (A : set ℝ) := a ∈ A ∧ a ∈ up_bounds A

[Yunjiang Jiang]

@Heather Macbeth DONE. Thanks.

[Yunjiang Jiang]

I am not following the definition of set:def set (α : Type u) := α → Prop in set.lean. Can someone help me dissect it?

[Kyle Miller]

@Yunjiang Jiang Prop is the type of all propositions. There are only two, true and false. A function α → Prop is a predicate on α in basically the usual logic sense -- for each term of α the function selects either true or false. Predicates are the same as sets, in that elements of a set are those terms for which the predicate evaluates to true. (Conversely, if you have a set s, then the function that for a given a evaluates to whether a ∈ s is a predicate.)

The definition says "given a type α, then set α is equal to the type of all functions α → Prop. Don't worry about the u for now.

[Kyle Miller]

The set notation { x : ℝ | ∀ a ∈ A, a ≤ x} is a special way to write a predicate that should be interpreted as a set (and it's designed to look like the usual set builder notation in math). A set ℝ in this case. This says "to decide whether an element x is in this set, evaluate to whether ∀ a ∈ A, a ≤ x." So it can be viewed as a predicate ℝ → Prop.

[Kyle Miller]

The ∈ notation is merely a way to evaluate a set's underlying predicate. The statement x ∈ up_bounds A is exactly the same as ∀ a ∈ A, a ≤ x due to the definition of up_bounds.

[Kyle Miller]

You can technically also write x ∈ up_bounds A as (up_bounds A) x since, as we've established, up_bounds A is also a function ℝ → Prop, but that's considered somewhat bad style since the way sets are encoded as predicates is an implementation detail.

[Kyle Miller]

(deleted)

[Yunjiang Jiang]

Several questions regarding this example:

example {x y : ℝ} : (∀ ε > 0, y ≤ x + ε) →  y ≤ x :=
begin
  contrapose!,
  exact assume h, ⟨(y-x)/2, by linarith, by linarith⟩,
end

Is h a special keyword in lean that always refers to the hypothesis (stuff in bracket) or an antecedent of the compound proof that follows? Also
since by is supposed to stand for begin/end pair, I tried the following, but got a bunch of compile errors.

example {x y : ℝ} : (∀ ε > 0, y ≤ x + ε) →  y ≤ x :=
begin
  contrapose!,
  exact assume h, ⟨
    (y-x)/2,
    begin
      linarith
      begin
        linarith
      end
    end
  ⟩,
end

[Mario Carneiro]

Is h a special keyword in lean that always refers to the hypothesis (stuff in bracket) or an antecedent of the compound proof that follows?

No, assume is a keyword (equivalent to \lam or fun) that should be followed by a name that is bound to the antecedent. It's basically the name of the function parameter and it can be whatever you want

[Mario Carneiro]

since by is supposed to stand for begin/end pair, I tried the following, but got a bunch of compile errors.

You got the scoping wrong in your example. exact is taking a lambda assume h, ... where the body of the lambda is a triple ⟨(y-x)/2, ..., ...⟩, where the two tuple arguments are by linarith. So the begin end equivalent would be

example {x y : ℝ} : (∀ ε > 0, y ≤ x + ε) →  y ≤ x :=
begin
  contrapose!,
  exact assume h, ⟨(y-x)/2, begin linarith end, begin linarith end⟩,
end

[Mario Carneiro]

importantly, the difference between by tac and begin tac, tac, ... , end is that by tac only takes one tactic (although you can build composite tactics using ; that count as one for this purpose) while begin ... end takes a comma separated list of tactics. Using a comma in by tac, ... will take you back out of tactic mode and that comma should mean something in the surrounding expression context (here it's part of a pairing operator)

[Yunjiang Jiang]

@Mario Carneiro thanks for the thorough explanation. I just figured the by translation part also. What's an example where the dummy variable h is actually used by an assume clause?

[Mario Carneiro]

example (x : ℕ) : 0 < x → 0 < x ∧ 0 < x :=
assume h : 0 < x,
⟨h, h⟩

[Mario Carneiro]

By the way, the proof is actually using h in that example, but it's being automatically picked up by linarith so the name itself isn't important. I can do something similar in this example by using the assumption tactic to be vague about which hypothesis is being used:

example (x : ℕ) : 0 < x → 0 < x ∧ 0 < x :=
assume h : 0 < x,
⟨by assumption, by assumption⟩

[Eric Schneider]

Screen-Shot-2021-12-05-at-10.10.43-PM.png
Anyone know what I should do here?

[Johan Commelin]

My uneducated guess would be that you should first run brew upgrade or maybe sudo brew upgrade and then try again.

[Kyle Miller]

It's saying that you don't have write permissions to /usr/local/man, and it gives you two commands to run. I've also heard a suggestion to run brew update twice and then brew doctor to check for errors.

[Eric Schneider]

I ran those two lines of code at the bottom, the ‘sudo...’ and the ‘chmod...’

[Eric Schneider]

Screen-Shot-2021-12-05-at-10.37.05-PM.png

[Eric Schneider]

I have this now

[Johan Commelin]

Uggh, I don't have a mac. What is the file that you use to configure your environment? Setting PATH etc...

[Eric Schneider]

No idea, I just do what I’m told

[Kyle Miller]

Did you do brew update? Mac OS doesn't use .profile anymore since it's switched to the zsh shell from bash

[Eric Schneider]

No, I just copied those two lines

[Johan Commelin]

Kyle Miller said:

Did you do brew update? Mac OS doesn't use .profile anymore since it's switched to the zsh shell from bash

Ooh! Did that happen recently? Should we update install scripts/instructions?

[Kyle Miller]

About two years ago, but I update things so infrequently on my own mac I figured I'd mention it just in case.

[Johan Commelin]

So why does https://leanprover-community.github.io/install/macos.html#intel-macs mention ~/.profile ?

[Kyle Miller]

@Eric Schneider Good news: that "no such file or directory" means the install script worked.

[Kyle Miller]

@Johan Commelin I didn't realize the error was from the command line you're supposed to paste in. source ~/.profile is wrong, but I'm not sure what would be correct. I'd guess either source ~/.zprofile or source ~/.zshrc (more likely the latter, or maybe a source command isn't needed after all)

[Kyle Miller]

But zsh also has some cache for the path that you're supposed to reset, I think.

[Johan Commelin]

Like I said, I don't know a thing about Macs.

[Johan Commelin]

Some Linux knowledge transfers, but I have no clue what breaks.

[Eric Schneider]

That’s weird but good to know. Thank you!

[Eric Schneider]

Now I just need to figure out how to use lean…

[Alice Wyan]

Very n00b question. Lean uses many Unicode characters as operators and symbols, more than most computer languages. Is there a "usual" way to input these easily on VSCode? Or does everyone copy/paste them from other source files whenever needed?

[Martin Dvořák]

You can write LaTeX code for them.

[Johan Commelin]

\le becomes ≤ and \nat becomes ℕ, \not becomes ¬, etc...

[Martin Dvořák]

Also, the most often used symbols have a short alias. For example \r can be used as \rightarrow.

[Johan Commelin]

aka \to

[Johan Commelin]

See #translations for the full list

[Kevin Buzzard]

Just to be clear -- n00b questions are more than welcome in #new members -- that's what it's for

[Martin Dvořák]

Johan Commelin said:

See #translations for the full list

The link doesn't work in my browser.

[Rémy Degenne]

If you hover over a symbol in VSCode you will get a tooltip explaining how to type it.

[Johan Commelin]

Weird, it's supposed to link to https://github.com/leanprover/vscode-lean/blob/master/translations.json

[Arthur Paulino]

I think this is the link: https://github.com/leanprover/vscode-lean/blob/master/src/abbreviation/abbreviations.json

[Martin Dvořák]

Definitely memorize \la for lambda. That will save you a lot of time.

[Bryan Gin-ge Chen]

Johan Commelin said:

Weird, it's supposed to link to https://github.com/leanprover/vscode-lean/blob/master/translations.json

The file was moved a while ago; I've updated the linkifier so this should hopefully work now: #translations

[Johan Commelin]

Wunderbar!

[Arthur Paulino]

Isn't it better to keep consistency with, say, #abbreviations instead? Or is it something we don't care much?

[Alice Wyan]

Ah, thank you! Hadn't seen the hover text, that's really neat :)