Zulip Chat Archive

Stream: new members

Topic: Lean's way of simple term transformations


André Beyer (Jan 21 2021 at 17:00):

Hi!
I'm often struggling with transforming terms from one to another. Here's an example:

h : 0  (n - 1) ^ 2
 2  n + 1 / n

This is easy on paper:

0(n1)2    0n22n+1    2nn2+1    2n+1n0 \le (n - 1)^2 \iff 0 \le n^2 - 2n + 1 \iff 2n \le n^2 + 1 \iff 2 \le n + \frac{1}{n}

I don't know how to best archive this using Lean - what are the best practices in such cases? Any suggestions? Thanks in advance!

Bryan Gin-ge Chen (Jan 21 2021 at 17:04):

I suppose n is a natural number coerced to a rational number? Note that you'll need an additional hypothesis of n \ne 0 since 1/0 is defined to be 0 in mathlib.

Lars Ericson (Jan 21 2021 at 17:08):

Something like this plus what Bryan just said:

import tactic

theorem ineq_on_n (n: ) : 0  (n-1)^2  2*n  n^2+1 :=
begin
  split,
  {
    intro h,
    refine eq.le _,
    sorry,
  },
  {
    intro h,
    exact zero_le ((n - 1) ^ 2),
  }
end

Johan Commelin (Jan 21 2021 at 17:44):

@André Beyer Please state problems in the form of

import whatever.you.need

example (n : nat?rat?real?) : etc :=
sorry

See also #mwe <- this is a link

Mario Carneiro (Jan 21 2021 at 17:53):

Here's a proof along those general lines:

import data.real.basic

example (n : ) (h : n > 0) : 2  n + 1 / n :=
begin
  refine le_of_mul_le_mul_left _ h,
  simp [mul_add, ne_of_gt h],
  rw  sub_nonneg,
  convert pow_two_nonneg (n - 1),
  ring,
end

Mario Carneiro (Jan 21 2021 at 17:54):

the hard part is dealing with the division, as others said

Mario Carneiro (Jan 21 2021 at 17:54):

for the most part you can just clear denominators, make it a polynomial equation, and let ring take care of the rest

Bryan Gin-ge Chen (Jan 21 2021 at 17:56):

I was just writing up a very similar proof which uses field_simp instead of the explicit lemma le_of_mul_le_mul_left:

import tactic
import tactic.field_simp

example {n : } (h : 0 < n) : 2  n + 1 / n :=
begin
  have H : n*n + 1 - 2*n = (n - 1) * (n - 1) := by ring,
  field_simp [ne_of_gt h],
  rw [le_div_iff h,  sub_nonneg, H],
  exact mul_self_nonneg _,
end

Mario Carneiro (Jan 21 2021 at 17:58):

Ah, so that's how you are supposed to use field_simp here. You can also put the ring at the end like this:

example (n : ) (h : n > 0) : 2  n + 1 / n :=
begin
  field_simp [ne_of_gt h],
  rw [le_div_iff h,  sub_nonneg],
  convert pow_two_nonneg (n - 1),
  ring,
end

André Beyer (Jan 21 2021 at 19:59):

Looks good, thank you!


Last updated: Dec 20 2023 at 11:08 UTC