tutorials 0010

Stream: new members

[Jiekai]

-- 0010
example (a b : ℝ) (hb : 0 ≤ b) : a ≤ a + b :=
begin
  have key : 0 + a ≤ b + a,
  {
    exact add_le_add_right hb a,
  },
  ring, -- cursor here
end

1 goal
a b : ℝ,
hb : 0 ≤ b,
key : 0 + a ≤ b + a
⊢ a ≤ a + b

Why does ring fail here?

[Damiano Testa]

I think that ring is intended to work with equalities rather than inequalities. Some rare times, the two sides of an inequality reduce to an inequality that is true by definition (or close) and then ring might close it accidentally. For instance, this works:

lemma triv {a : ℕ} : a + 0 ≤ a :=
by ring

but I suspect that ringreduces it to a ≤ a and then it is trivial! (Although, note that ring is a little uncomfortable about this.)

[Jiekai]

Thanks. I read a few more lines in the file and learned the trick.

  have key1 : 0 + a = a,
  { ring, },
  rw key1 at key,
  have key2 : b + a = a + b,
  { ring, },
  rw key2 at key,

[Huỳnh Trần Khanh]

(deleted)

[Kevin Buzzard]

The job of norm_num is to deal with numerals like 37, not goals involving variables