Zulip Chat Archive

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,
  rw add_zero at hb,
  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?

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

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.