Style feedback

Stream: new members

[Martin C. Martin]

Section 2.5 in "Mathematics in Lean" has us prove:

(h : a ≤ b) (h' : 0 ≤ c) : a * c ≤ b * c

Here's my proof, but it feels a little verbose and awkward. Is there a simpler / more readable / more canonical proof?

variables {R : Type*} [ordered_ring R]
variables a b c : R

example (h : a ≤ b) (h' : 0 ≤ c) : a * c ≤ b * c :=
begin
  nth_rewrite 0 ← add_zero (a * c),
  have h1 : b * c = a * c + (b - a) * c,
  by noncomm_ring,
  rw h1,
  apply add_le_add_left,
  apply mul_nonneg,
  { simp, exact h },
  exact h'
end

[Kevin Buzzard]

What are the types of a,b,c?

[Martin C. Martin]

(Edit: Actually, an ordered_ring.) Sorry, updated. They're in a metric_space.

[Martin C. Martin]

I just noticed that Mathematics in Lean comes with solutions! Here's their solution to the problem:

theorem aux1 : a ≤ b → 0 ≤ b - a :=
begin
  intro h,
  rw [←sub_self a, sub_eq_add_neg, sub_eq_add_neg, add_comm, add_comm b],
  apply add_le_add_left h
end

theorem aux2 : 0 ≤ b - a → a ≤ b :=
begin
  intro h,
  rw [←add_zero a, ←sub_add_cancel b a, add_comm (b - a)],
  apply add_le_add_left h
end

example (h : a ≤ b) (h' : 0 ≤ c) : a * c ≤ b * c :=
begin
  have h1 : 0 ≤ (b - a) * c,
  { exact mul_nonneg (aux1 _ _ h) h' },
  rw sub_mul at h1,
  exact aux2 _ _ h1
end

[Jireh Loreaux]

Not a metric_space (at least not by itself), there's no dist here. It's an ordered_ring R with a b c : R

[Jireh Loreaux]

Note that the solutions named the first two examples (and changed to theorem) so that they could be used in the proof of the third one.

[Martin C. Martin]

Ugh! Sorry, I got it mixed up with the next question. :) Yes, this is an ordered_ring, I updated my example.

[Jireh Loreaux]

Here are a few ways I would consider doing it (of course, the last one is cheating in some sense). Note that sub_nonneg is an ↔ combining aux1 and aux2. the positivity tactic is pretty cool in case you haven't learned about it yet.

import tactic.positivity

variables {R : Type*} [ordered_ring R]
variables a b c : R

example (h : a ≤ b) (h' : 0 ≤ c) : a * c ≤ b * c :=
begin
  rw ←sub_nonneg at h ⊢,
  rw ←sub_mul,
  exact mul_nonneg h h',
end

example (h : a ≤ b) (h' : 0 ≤ c) : a * c ≤ b * c :=
begin
  rw ←sub_nonneg at h ⊢,
  rw ←sub_mul,
  positivity,
end

example (h : a ≤ b) (h' : 0 ≤ c) : a * c ≤ b * c :=
mul_le_mul_of_nonneg_right h h'

[Martin C. Martin]

Thanks, those are much better! And I hadn't heard of the positivity tactic, thanks for the tip.

[Martin C. Martin]

When working forward (i.e. adding new things to the context from what we already know, as opposed to working backward from the goal), is there a way to add a hypothesis without stating it's type? For example, in

variables {X : Type*} [metric_space X]
variables x y z : X

example (x y : X) : 0 ≤ dist x y :=
begin
  have h1 : dist x x ≤ (dist x y) + (dist y x),
  { exact dist_triangle x y x},
  sorry
end

that's kind of a lot of typing to just say h1 is dist_triangle x y x.

[Kyle Miller]

You probably can do have h1 := dist_triangle x y x here

[Ruben Van de Velde]

variables {X : Type*} [metric_space X]
variables x y z : X

example (x y : X) : 0 ≤ dist x y :=
begin
  have h1 := dist_triangle x y x,
  sorry
end

[Martin C. Martin]

Dude! So the ": type" is optional, I thought I tried leaving that out and it didn't work, but it's working now. :) It seems also have h1 := is the same as have h1, from?

[Martin C. Martin]

.

[Jireh Loreaux]

It's optional if Lean can infer the type from the term you provided. Sometimes this doesn't work if the term you provided has metavariables.

[Jireh Loreaux]

Although on second thought, I think it still "works" it's just that h1 is pretty useless because it has metavariables in its type.

[Kevin Buzzard]

Although it's not great style, h1 is not useless if it has metavariables in its type -- you can sometimes just continue and they'll be unified later on (and the random non-Prop goals will magically disappear).

[Jireh Loreaux]

This is sometimes true, but in practice I frequently find that unification fails in those situations.

[Jireh Loreaux]

Maybe this is because the metavariables I have include some TC goals that depend on how they unify? I'm not sure, I don't have an example at hand.