Stream: new members

Topic: Question about calc

Gareth Ma (Jan 16 2023 at 07:01):

Hi! I am new to lean, only played the natural number game a bit and right now trying the tutorial. I am kind of confused on how to use the calc. I can't really pinpoint what I don't understand, just... I don't understand :joy:
Can someone show how the following code can be rewritten using calc?

example (a b : ℝ) (hb : 0 ≤ b) : a ≤ a + b :=
begin
have hb : a + 0 ≤ a + b, from add_le_add_left hb a,
exact hb,
end


Gareth Ma (Jan 16 2023 at 07:06):

I tried this, but doesn't seem to work, and I am not sure why :tear:

  calc
a + 0 ≤ a + b : by { rw add_le_add_left hb a }
a ≤ a + b : by { rw add_zero },


Martin Dvořák (Jan 16 2023 at 07:29):

Solution with calc would be along these lines:

calc
a = a + 0 : reason
... ≤ a + b : reason


Martin Dvořák (Jan 16 2023 at 07:33):

PS: The dots are not a placeholder. You literally write ... there.

Gareth Ma (Jan 16 2023 at 07:40):

Oh wait, the ... is part of the syntax?

Yes.

Gareth Ma (Jan 16 2023 at 07:41):

Oh god, thanks, I will try more :)

Martin Dvořák (Jan 16 2023 at 07:42):

Lean 3 is not newline-sensitive. You must separate the reason for a = a + 0 from ≤ a + b on the next line.

Patrick Massot (Jan 16 2023 at 07:52):

@Gareth Ma when using the tutorial, it is absolutely crucial to carefully read the examples. In this case looking at them is enough, but in most cases reading the examples means moving the cursor slowly from line to line and watch the tactic state update, trying to make sure you understand why the tactic state changes like it does.

Patrick Massot (Jan 16 2023 at 07:53):

It is also important not to completely forget what the real world looks like. The calc command in particular is meant to look like the real world. On paper what you wrote would be just as meaningless as it is in Lean.

Gareth Ma (Jan 16 2023 at 07:54):

Ahh true, thank you both! The tutorial so far feels different from what I learned from the natural number game

Martin Dvořák (Jan 16 2023 at 07:56):

NNG has some modifications of how tactic-style proofs work.

Patrick Massot (Jan 16 2023 at 07:57):

NNG was never meant to be a general introduction to Lean. It was meant as a standalone game.

Gareth Ma (Jan 16 2023 at 08:00):

That makes more sense :big_smile:

Martin Dvořák (Jan 16 2023 at 08:02):

Patrick Massot said:

NNG was never meant to be a general introduction to Lean. It was meant as a standalone game.

However, it is an excellent way to draw to people to Lean!

Gareth Ma (Jan 16 2023 at 08:03):

It's definitely a nice introduction to how to "think in Lean"

Martin Dvořák (Jan 16 2023 at 08:08):

I'd even say that it is a nice introduction to how to "think mathematically".

Martin Dvořák (Jan 16 2023 at 08:09):

I hope that some famous gaming Youtubers will soon make "Let's play NNG" videos.

Last updated: Dec 20 2023 at 11:08 UTC