if a < b then a^3 < b^3

Stream: new members

[Lars Ericson]

This is a tricky one:

import tactic
import tactic.slim_check
import algebra.ordered_ring
universe u

theorem ex_1_3_1_f (α: Type u) [linear_ordered_ring α]
   (a b : α) (h: a < b): a^3 < b^3 :=
begin
  have h1 := pow_two_nonneg a,
  have h2 := pow_two_nonneg b,
  rw (pow_succ a 2),
  rw (pow_succ b 2),
  sorry,
end

I just found some proofs over here, so I don't actually have a question. I don't see anything that fits for this in mathlib directly. I think I can adapt this proof which looks good:

If a > b then (a - b) > 0, and so (a - b)^3 > 0.

Thus (a - b)^3 = (a^3 - 3*a^2*b + 3a*b^2 - b^3) > 0, and so

(a^3 - b^3) > (3*a^2*b - 3a*b^2) = 3ab*(a - b).

Now we know that (a - b) > 0. So if either (i) both a and b are positive, or

(ii) both a and b are negative, then 3ab*(b - a) > 0, and so

(a^3 - b^3) > 0  ----->  a^3 > b^3.

If a > 0 and b < 0 then a^3 > 0 and b^3 < 0 so a^3 > b^3.

(We can't have a < 0 and b > 0 since a > b.)

So in all cases we have that a > b implies that a^3 > b^3.

[Alex J. Best]

A linear ordered ring isn't commutative and it looks like your proof uses commutativity of multiplication to say that (a - b)^3 = (a^3 - 3*a^2*b + 3a*b^2 - b^3)

[Alex J. Best]

That proof looks quite a lot of algebraic manipulations to me though, I'd be inclined to just use facts like
0 < b \to a < b \to a * b < b *b which should be in the library, and split into cases based on whether a and b are positive or negative and build the proof that way.

[Kevin Buzzard]

If your ring is commutative then you can use that a^2+ab+b^2>=0 by completing the square

[Lars Ericson]

The setting is "ordered domain" which I've taken up to now to be integral_domain with linear_ordered_ring. It's described more here.

I just figured out how to prove a polynomial so I think I can grind through this now:

import tactic
import tactic.slim_check
import algebra.ordered_ring
universe u

lemma expand_mult (α: Type u) [integral_domain α] [linear_ordered_ring α]
   (a b : α) (h: 0 < a):
   (b-a)^3 = b^3-3*a*b^2+3*a^2*b-a^3 :=
begin
  rw pow_succ (b-a) 2,
  rw pow_succ (b-a) 1,
  simp,
  rw sub_eq_add_neg,
  repeat { rw left_distrib, rw right_distrib, },
  ring,
end

It would be nice if Lean were hybridized a bit with some kind of self-validating pre-theorem-proving-style computer algebra so I could do stuff like this:

>>> import sympy as sp
>>> a,b=sp.symbols('a,b')
>>> sp.expand((b-a)**3)
-a**3 + 3*a**2*b - 3*a*b**2 + b**3

[Yakov Pechersky]

That does not compile for me, because you have two conflicting ring on α

[Yakov Pechersky]

For me, this works instead: [integral_domain α] [linear_order α]. Perhaps I'm on an old mathlib

[Yakov Pechersky]

import tactic

lemma expand_mult (α : Type*) [integral_domain α] [linear_order α]
   (a b : α) :
   (b-a)^3 = b^3-3*a*b^2+3*a^2*b-a^3 :=
by ring_exp

[Yakov Pechersky]

No need for the positivity constraint

[Lars Ericson]

Great, thanks! ring_exp is nice. I will update my mathlib now to make sure I am in sync with latest.

[Lars Ericson]

OK so after doing leanproject upgrade-mathlib, your version works fine. My version breaks in a weird way on the ring command. It is both happy and sad. It says "goals accomplished" but also complains about ring horners:

type mismatch at application
  norm_num.subst_into_mul b (b * b) (tactic.ring.horner 1 b 1 0) (tactic.ring.horner 1 b 2 0)
    (tactic.ring.horner 1 b 3 0)
    (tactic.ring.horner_atom b)
term
  tactic.ring.horner_atom b
has type
  b = tactic.ring.horner 1 b 1 0
but is expected to have type
  b = tactic.ring.horner 1 b 1 0

on input

import tactic
import tactic.slim_check
import algebra.ordered_ring
universe u

lemma expand_mult (α: Type u) [integral_domain α] [linear_ordered_ring α]
   (a b : α) (h: 0 < a):
   (b-a)^3 = b^3-3*a*b^2+3*a^2*b-a^3 :=
begin
  rw pow_succ (b-a) 2,
  rw pow_succ (b-a) 1,
  simp,
  rw sub_eq_add_neg,
  repeat { rw left_distrib, rw right_distrib, },
  ring,
end

[Lars Ericson]

Screenshot-from-2021-01-24-21-08-38.png

[Yakov Pechersky]

You'd have to do a lot of inspection of intermediate terms, but what you'd find is that by saying [integral_domain α] [linear_ordered_ring α], you're invoking two separate, non-identical [ring α]. That means that ring is trying to bring both sides of the equation to the same terms, but is running into the problem that it doesn't know which of the two (now completely independent) inferred definitions of (+) it should be using. That's my understanding of that error.

[Bryan Gin-ge Chen]

ring should probably throw an error there instead of clearing the goal. cc: @Mario Carneiro

[Mario Carneiro]

Oh I see, yeah ring isn't very defensive against weird multiplications on the type. simp I think has the same problem

[Mario Carneiro]

I'm not sure it's worth the expense

[Lars Ericson]

This is a bit sad because if I switch from linear_ordered_ring to linear_order I lose sub_pos and probably other stuff in my theorem ex_1_3_1_f :

import tactic
import tactic.slim_check
import algebra.ordered_ring
universe u
/-
lemma expand_mult (α: Type u) [integral_domain α] [linear_ordered_ring α]
   (a b : α) (h: 0 < a):
   (b-a)^3 = b^3-3*a*b^2+3*a^2*b-a^3 :=
begin
  rw pow_succ (b-a) 2,
  rw pow_succ (b-a) 1,
  simp,
  rw sub_eq_add_neg,
  repeat { rw left_distrib, rw right_distrib, },
  ring,
end -/

lemma expand_mult (α : Type*) [integral_domain α] [linear_order α]
   (a b : α) :
   (b-a)^3 = b^3-3*a*b^2+3*a^2*b-a^3 :=
by ring_exp

theorem ex_1_3_1_f (α: Type u) [integral_domain α] [linear_order α]
   (a b : α) (h: a < b): a^3 < b^3 :=
begin
  by_cases ha : a > 0,
  by_cases hb : b > 0,
  have h1 := sub_pos.2 h,
  have h2 := pow_pos h1 3,
  have h3 := expand_mult,
  sorry,
  sorry,
  sorry,
end

I haven't actually needed integral_domain up to now, just ordered_ring or linear_ordered_ring for these:

import tactic
import tactic.slim_check
import algebra.ordered_ring
universe u

theorem ex_1_3_1_a (α: Type u) [ordered_ring α]
   (a b c : α) (h: a < b): a + c < b + c :=
  add_lt_add_right h c

theorem ex_1_3_1_b (α: Type u) [ordered_ring α]
   (a x y : α): a-x < a-y ↔ x > y := sub_lt_sub_iff_left a

lemma lt0_lt_flip (α: Type*) [linear_ordered_ring α] -- Ruben Van de Velde
   (a x : α) (hx: a * x < 0) (ha: a < 0) : 0 < x :=
  pos_of_mul_neg_right hx ha.le

theorem ex_1_3_1_c (α: Type u) [linear_ordered_ring α]
   (a x y : α) (h: a < 0): a*x > a* y ↔ x < y :=
begin
  split,
  {
    intro h0,
    have h1 := sub_lt_zero.mpr h0,
    apply sub_lt_zero.1,
    rw ← mul_sub at h1,
    have h2 := lt0_lt_flip α a (y-x) h1 h,
    rw (neg_sub x y).symm at h2,
    exact neg_pos.1 h2,
  },
  {
    intro h0,
    apply sub_lt_zero.1,
    rw ← mul_sub,
    have h1 := sub_pos.2 h0,
    exact mul_neg_of_neg_of_pos h h1,
  }
end

theorem ex_1_3_1_d (α: Type u) [linear_ordered_ring α]
   (a b c : α) (ha: 0 < c) (hacbc: a*c < b*c): a < b :=
  (mul_lt_mul_right ha).mp hacbc

theorem ex_1_3_1_e (α: Type u) [linear_ordered_ring α]
   (x : α) (h: x + x + x + x = 0) : x = 0 :=
begin
  rw (add_assoc (x+x) x x) at h,
  exact bit0_eq_zero.mp (bit0_eq_zero.mp h),
end

I'm not sure at this point exactly what combination of Lean structures equals Birkhoff and Mac Lane's notion of ordered domain.

It's more confusing because it seems from above I have to make sure my inheritance hierarchy is a tree, not a lattice, i.e. no two classes with a common superclass.

[Bryan Gin-ge Chen]

Mario Carneiro said:

I'm not sure it's worth the expense

Fair enough. Might be worth documenting these cases somewhere.

[Mario Carneiro]

@Lars Ericson The theorem should hold for a linear_ordered_ring without the integral domain part

[Mario Carneiro]

actually linear_ordered_comm_ring

[Mario Carneiro]

which is implied by the conjunction of linear_ordered_ring and integral_domain

[Lars Ericson]

Thanks Mario, all of the exercises are happy with linear_ordered_comm_ring.

[Lars Ericson]

Done, finally. I found this to be incredibly hard. I expect a one-line version from Mario soon:

import tactic
import algebra.ordered_ring
universe u

lemma together  (α: Type u) [linear_ordered_comm_ring α] (a b: α) (h: a-b = 0)  : a = b :=
  sub_eq_zero.mp h

lemma factor_expr (α: Type u) [linear_ordered_comm_ring α] (a b : α) :
  a * (b ^ 2 * -3) + (a ^ 2 * (b * 3)) = 3*a*b*(a - b) :=
begin
  apply (together α (a * (b ^ 2 * -3) + (a ^ 2 * (b * 3))) (3*a*b*(a - b))),
  ring,
end

lemma move_cubes_left (α: Type u) [linear_ordered_comm_ring α]
   (a b : α) (h: 0 < a * (b ^ 2 * -3) + (a ^ 2 * (b * 3) + (-a ^ 3 + b ^ 3))) :
   a^3- b^3 < a * (b ^ 2 * -3) + (a ^ 2 * (b * 3)) :=
begin
  linarith,
end

lemma negneg (α: Type u) [linear_ordered_comm_ring α] (a b : α): a - b = - (b - a):=
begin
  linarith,
end

lemma this_is_negative (α: Type u) [linear_ordered_comm_ring α] (a b : α)
      (h1: 0 < b - a)
      (hha: a > 0)
      (hhb: b > 0) : 3 * a * b * (a - b) < 0 :=
begin
  rw negneg α a b,
  have h3 := zero_lt_three,
  have h4 := mul_pos h3 hha,
  have h5 := mul_pos h4 hhb,
  simp,
  have h6 := neg_lt_zero.mpr h1,
  have h7 := neg_sub b  a,
  rw h7 at h6,
  exact linarith.mul_neg h6 h5,
  exact nontrivial_of_lt 0 (b - a) h1,
end

lemma this_is_positive (α: Type u) [linear_ordered_comm_ring α] (a b : α)
      (h1: 0 < b - a) (hb: b > 0) (alt0: a < 0) : 0 < 3 * a * b * (a - b) :=
begin
  have h3 := zero_lt_three,
  have h4 := mul_neg_of_pos_of_neg h3 alt0,
  have h5 := mul_neg_of_neg_of_pos h4 hb,
  have h6 := neg_lt_zero.mpr h1,
  have h7 := mul_pos_of_neg_of_neg h5 h6,
  have h8 := neg_sub b a,
  rw h8 at h7,
  exact h7,
  exact nontrivial_of_lt 0 (b - a) h1,
end

lemma simp_pow (α: Type u) [linear_ordered_comm_ring α]: (0:α)^3 = 0 :=
  tactic.ring_exp.pow_p_pf_zero rfl rfl

lemma is_lt_0 (α: Type u) [linear_ordered_comm_ring α] (b : α)
      (hb: ¬b > 0) (hb0: ¬b = 0): b < 0 :=
  (ne.le_iff_lt hb0).mp (not_lt.mp hb)

lemma odd_pos_neg_neg (α: Type u) [linear_ordered_comm_ring α] (a : α)
        (h: a < 0) : a^3 < 0 :=
  pow_bit1_neg_iff.mpr h

lemma this_be_negative (α: Type u) [linear_ordered_comm_ring α] (a b : α)
      (h1: a < b)
      (halt0: a < 0)
      (hblt0: b < 0) :
      3 * a * b * (a - b) < 0 :=
begin
  have h3 := zero_lt_three,
  have h4 := sub_lt_zero.mpr h1,
  have h5 := mul_pos_of_neg_of_neg  halt0 hblt0,
  have h6 := mul_pos h3 h5,
  have h7 := sub_lt_zero.mpr h1,
  have h8 := linarith.mul_neg h7 h6,
  finish,
  exact nontrivial_of_lt a b h1,
end

theorem ex_1_3_1_f (α: Type u) [linear_ordered_comm_ring α]
   (a b : α) (h: a < b): a^3 < b^3 :=
begin
  have h1 := sub_pos.2 h,
  have h2 := pow_pos h1 3,
  repeat { rw pow_succ' at h2, },
  simp at h2,
  rw sub_eq_neg_add at h2,
  repeat { rw right_distrib at h2, rw left_distrib at h2, },
  ring_exp at h2,
  have h3 := move_cubes_left α a b h2,
  rw factor_expr α a b at h3,
  by_cases ha : a > 0,
  {
    by_cases hb : b > 0,
    {
      have h4 := this_is_negative α a b h1 ha hb,
      have h5 := lt_trans h3 h4,
      exact sub_lt_zero.1 h5,
    },
    {
      exfalso,
      exact hb (lt_trans ha h),
    },
  },
  by_cases ha0: a = 0,
  {
    rw ha0 at *,
    simp at *,
    assumption,
  },
  {
    have halt0 := is_lt_0 α a ha ha0,
    have h3alt0 := odd_pos_neg_neg α a halt0,
    by_cases hb : b > 0,
    {
      have h3bgt0 := pow_pos hb 3,
      exact lt_trans h3alt0 h3bgt0,
    },
    by_cases hb0 : b = 0,
    {
      rw hb0,
      rw simp_pow,
      assumption,
    },
    {
      have hblt0 := is_lt_0 α b hb hb0,
      have hf := this_be_negative α a b h halt0 hblt0,
      have hf1 := lt_trans h3 hf,
      finish,
    }
  }
end

[Lars Ericson]

On the other hand, this one took 30 seconds:

import tactic
import algebra.ordered_ring
universe u

theorem ex_1_3_1_g (α: Type u) [linear_ordered_comm_ring α]
   (a b c : α) (hc: 0 ≤ c) (ha: b ≤ a): b * c ≤ a * c :=
  mul_mono_nonneg hc ha

[Lars Ericson]

This one also pretty easy except I have no idea what just happened at the end:

import tactic
import algebra.ordered_ring
universe u

theorem ex_1_3_2 (α: Type u) [linear_ordered_comm_ring α] (x:α): ¬ ∃ x:α, x^2 + 1 = 0 :=
begin
  intro h,
  cases h with x hx,
  rw (pow_two x) at hx,
  nlinarith,
end

[Lars Ericson]

This one is also free out of the box:

theorem ex_1_3_4 (α: Type u) [linear_ordered_comm_ring α] (a b:α):
  abs (abs a - abs b) ≤ abs(a-b) :=
  abs_abs_sub_abs_le_abs_sub a b

[Mario Carneiro]

theorem ex_1_3_1_f (α: Type u) [linear_ordered_comm_ring α]
   (a b : α) (h: a < b): a^3 < b^3 :=
strict_mono_pow_bit1 1 h

one line version delivered

[Lars Ericson]

Thanks @Mario Carneiro that's great! What's a bit0 and a bit1? I've seen these around but I don't know what to make of this:

def bit0 {α : Type u} [s  : has_add α] (a  : α)                 : α := a + a
def bit1 {α : Type u} [s₁ : has_one α] [s₂ : has_add α] (a : α) : α := (bit0 a) + 1

[Mario Carneiro]

it is what it says. bit0 n is the function 2*n and bit1 n is 2*n+1

[Kyle Miller]

and 37 is the number bit1 (bit0 (bit1 (bit0 (bit0 has_one.one))))

[Lars Ericson]

Thanks. I get it now. It's a way of spelling out natural numbers in base 2. There are 18 docs#bit0 theorems and 19 docs#bit1 theorems in mathlib. I didn't find any commentary. The application above was powerful. It would be nice to have an article on https://leanprover-community.github.io/ exploring the power of bit and how those 37 theorems relate.