## Stream: new members

### Topic: Style feedback

#### Martin C. Martin (Feb 02 2023 at 18:42):

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 mul_nonneg,
{ simp, exact h },
exact h'
end


#### Kevin Buzzard (Feb 02 2023 at 20:09):

What are the types of a,b,c?

#### Martin C. Martin (Feb 02 2023 at 20:36):

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

#### Martin C. Martin (Feb 02 2023 at 20:44):

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,
end

theorem aux2 : 0 ≤ b - a → a ≤ b :=
begin
intro h,
rw [←add_zero a, ←sub_add_cancel b a, add_comm (b - a)],
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 (Feb 02 2023 at 20:49):

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 (Feb 02 2023 at 20:51):

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 (Feb 02 2023 at 20:51):

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

#### Jireh Loreaux (Feb 02 2023 at 21:02):

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 (Feb 03 2023 at 18:19):

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

#### Martin C. Martin (Feb 03 2023 at 18:32):

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 (Feb 03 2023 at 18:34):

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

#### Ruben Van de Velde (Feb 03 2023 at 18:37):

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 (Feb 03 2023 at 18:43):

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?

.

#### Jireh Loreaux (Feb 03 2023 at 19:30):

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 (Feb 03 2023 at 19:31):

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 (Feb 03 2023 at 19:35):

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 (Feb 03 2023 at 19:56):

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

#### Jireh Loreaux (Feb 03 2023 at 19:57):

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.

Last updated: Dec 20 2023 at 11:08 UTC