A simpler way to do numerical calculations

Stream: new members

[Yongxi Lin (Aaron)]

import Mathlib

open Real

example : 1 / (16 : ℝ) * (2 - (8 * (2 ^ (1 / (12 : ℝ)) - 1) + 2 ^ (12 / (5 : ℝ)) * (2 ^ (2 / (15 : ℝ)) - 1) +
    4 * (2 ^ (1 / (6 : ℝ)) - 1) + 2 ^ (12 / (6 : ℝ)) * (2 ^ (4 / (21 : ℝ)) - 1) + 2 ^ (3 / (2 : ℝ)) * (2 ^ (5 / (24 : ℝ)) - 1) +
    2 ^ (4 / (3 : ℝ)) * (2 ^ (2 / (9 : ℝ)) - 1) + 2 ^ (6 / (5 : ℝ)) * (2 ^ (7 / (30 : ℝ)) - 1) +
    2 ^ (12 / (11 : ℝ)) * (2 ^ (8 / (33 : ℝ)) - 1))) < 0 := by
  have := add_one_lt_exp (by positivity : log 2 * (1 / 12) ≠ 0)
  have := add_one_lt_exp (by positivity: log 2 * (12 / 5) ≠ 0)
  have := add_one_lt_exp (by positivity : log 2 * (2 / 15) ≠ 0)
  have := add_one_lt_exp (by positivity : log 2 * (1 / 6) ≠ 0)
  have := add_one_lt_exp (by positivity : log 2 * (12 / 7) ≠ 0)
  have := add_one_lt_exp (by positivity : log 2 * (4 / 21) ≠ 0)
  have := add_one_lt_exp (by positivity : log 2 * (3 / 2) ≠ 0)
  have := add_one_lt_exp (by positivity : log 2 * (5 / 24) ≠ 0)
  have := add_one_lt_exp (by positivity : log 2 * (4 / 3) ≠ 0)
  have := add_one_lt_exp (by positivity : log 2 * (2 / 9) ≠ 0)
  have := add_one_lt_exp (by positivity : log 2 * (6 / 5) ≠ 0)
  have := add_one_lt_exp (by positivity : log 2 * (7 / 30) ≠ 0)
  have := add_one_lt_exp (by positivity : log 2 * (12 / 11) ≠ 0)
  have := add_one_lt_exp (by positivity : log 2 * (8 / 33) ≠ 0)
  norm_num [exp_mul, exp_log] at *
  have := log_two_gt_d9
  nlinarith

Is there a way to make the code more concise? I am asking because I have 10 other similar goals like this that I need to finish.

[Jakub Nowak]

Maybe tactics from this project would help you? #general > LeanCert - Verified Computation & Interval Arithmetic
I haven't used it, but from what I understand it should deal with this kind of goals with only constants.

[Bbbbbbbbba]

Hmm, so I found out that even if I proved hf : ∀ x, x ≠ 0 → 0 < f x, positivity seems unable to use it unless I give it every case it needs to use explicitly. Is there a way around this?

[Jakub Nowak]

Maybe you could try hf {x} (h : x ≠ 0 := by positivity) : 0 < f x?

[Bbbbbbbbba]

Hmm, when I write have hf {x} (h : x ≠ 0 := by positivity) : 0 < f x := by, the default value for h does not seem to work

[Bbbbbbbbba]

As a lemma the default for h works, but I still need to manually specify x for positivity to use it

[Jakub Nowak]

@Yongxi Lin (Aaron) I wouldn't say it's simpler, but it automates your proof, so it might help with other goals?

import Mathlib

open Real

example : 1 / (16 : ℝ) * (2 - (8 * (2 ^ (1 / (12 : ℝ)) - 1) + 2 ^ (12 / (5 : ℝ)) * (2 ^ (2 / (15 : ℝ)) - 1) +
    4 * (2 ^ (1 / (6 : ℝ)) - 1) + 2 ^ (12 / (6 : ℝ)) * (2 ^ (4 / (21 : ℝ)) - 1) + 2 ^ (3 / (2 : ℝ)) * (2 ^ (5 / (24 : ℝ)) - 1) +
    2 ^ (4 / (3 : ℝ)) * (2 ^ (2 / (9 : ℝ)) - 1) + 2 ^ (6 / (5 : ℝ)) * (2 ^ (7 / (30 : ℝ)) - 1) +
    2 ^ (12 / (11 : ℝ)) * (2 ^ (8 / (33 : ℝ)) - 1))) < 0 := by
  have h₁ {x} (h : x ≠ 0 := by positivity) : log 2 * x + 1 < 2 ^ x := by
    have := add_one_lt_exp (by positivity : log 2 * x ≠ 0)
    norm_num [exp_mul, exp_log] at this
    exact this
  have h₂ {x : ℝ} (h : 0 ≤ x := by positivity) : (0 : ℝ) ≤ 2 ^ x - 1 := by
    norm_num
    exact Real.one_le_rpow (by norm_num) h
  repeat grw [←h₁]
  · have := log_two_gt_d9
    nlinarith
  all_goals exact h₂

[Bbbbbbbbba]

Yongxi Lin (Aaron) said:

import Mathlib

open Real

example : 1 / (16 : ℝ) * (2 - (8 * (2 ^ (1 / (12 : ℝ)) - 1) + 2 ^ (12 / (5 : ℝ)) * (2 ^ (2 / (15 : ℝ)) - 1) +
    4 * (2 ^ (1 / (6 : ℝ)) - 1) + 2 ^ (12 / (6 : ℝ)) * (2 ^ (4 / (21 : ℝ)) - 1) + 2 ^ (3 / (2 : ℝ)) * (2 ^ (5 / (24 : ℝ)) - 1) +
    2 ^ (4 / (3 : ℝ)) * (2 ^ (2 / (9 : ℝ)) - 1) + 2 ^ (6 / (5 : ℝ)) * (2 ^ (7 / (30 : ℝ)) - 1) +
    2 ^ (12 / (11 : ℝ)) * (2 ^ (8 / (33 : ℝ)) - 1))) < 0 := by
  have := add_one_lt_exp (by positivity : log 2 * (1 / 12) ≠ 0)
  have := add_one_lt_exp (by positivity: log 2 * (12 / 5) ≠ 0)
  have := add_one_lt_exp (by positivity : log 2 * (2 / 15) ≠ 0)
  have := add_one_lt_exp (by positivity : log 2 * (1 / 6) ≠ 0)
  have := add_one_lt_exp (by positivity : log 2 * (12 / 7) ≠ 0)
  have := add_one_lt_exp (by positivity : log 2 * (4 / 21) ≠ 0)
  have := add_one_lt_exp (by positivity : log 2 * (3 / 2) ≠ 0)
  have := add_one_lt_exp (by positivity : log 2 * (5 / 24) ≠ 0)
  have := add_one_lt_exp (by positivity : log 2 * (4 / 3) ≠ 0)
  have := add_one_lt_exp (by positivity : log 2 * (2 / 9) ≠ 0)
  have := add_one_lt_exp (by positivity : log 2 * (6 / 5) ≠ 0)
  have := add_one_lt_exp (by positivity : log 2 * (7 / 30) ≠ 0)
  have := add_one_lt_exp (by positivity : log 2 * (12 / 11) ≠ 0)
  have := add_one_lt_exp (by positivity : log 2 * (8 / 33) ≠ 0)
  norm_num [exp_mul, exp_log] at *
  have := log_two_gt_d9
  nlinarith

Is there a way to make the code more concise? I am asking because I have 10 other similar goals like this that I need to finish.

For that matter, why do you have a 12 / 6 in your statement but 12 / 7 in your proof? :laughing:

[Jakub Nowak]

You can in fact remove have := add_one_lt_exp (by positivity : log 2 * (12 / 7) ≠ 0) and it still works. I've added have := add_one_lt_exp (by positivity : log 2 * (12 / 6) ≠ 0) and checked that only have := add_one_lt_exp (by positivity : log 2 * (12 / 6) ≠ 0) can be removed, not any other. Quite puzzling. Maybe the only bound needed for the proof is something that nlinarith can work out on its own, like 2 ^ (12 / (6 : ℝ)) > 0.

[Bbbbbbbbba]

Well, obviously norm_num simplifies 2 ^ (12 / 6) :laughing:

[Yongxi Lin (Aaron)]

Jakub Nowak said:

Yongxi Lin (Aaron) I wouldn't say it's simpler, but it automates your proof, so it might help with other goals?

import Mathlib

open Real

example : 1 / (16 : ℝ) * (2 - (8 * (2 ^ (1 / (12 : ℝ)) - 1) + 2 ^ (12 / (5 : ℝ)) * (2 ^ (2 / (15 : ℝ)) - 1) +
    4 * (2 ^ (1 / (6 : ℝ)) - 1) + 2 ^ (12 / (6 : ℝ)) * (2 ^ (4 / (21 : ℝ)) - 1) + 2 ^ (3 / (2 : ℝ)) * (2 ^ (5 / (24 : ℝ)) - 1) +
    2 ^ (4 / (3 : ℝ)) * (2 ^ (2 / (9 : ℝ)) - 1) + 2 ^ (6 / (5 : ℝ)) * (2 ^ (7 / (30 : ℝ)) - 1) +
    2 ^ (12 / (11 : ℝ)) * (2 ^ (8 / (33 : ℝ)) - 1))) < 0 := by
  have h₁ {x} (h : x ≠ 0 := by positivity) : log 2 * x + 1 < 2 ^ x := by
    have := add_one_lt_exp (by positivity : log 2 * x ≠ 0)
    norm_num [exp_mul, exp_log] at this
    exact this
  have h₂ {x : ℝ} (h : 0 ≤ x := by positivity) : (0 : ℝ) ≤ 2 ^ x - 1 := by
    norm_num
    exact Real.one_le_rpow (by norm_num) h
  repeat grw [←h₁]
  · have := log_two_gt_d9
    nlinarith
  all_goals exact h₂

Thanks for your code. This indeed seems much better. I guess doing numerical stuff is still kind of hard in lean.

[Chris Henson]

Some grind golfing:

import Mathlib

open Real

example : 1 / (16 : ℝ) * (2 - (8 * (2 ^ (1 / (12 : ℝ)) - 1) + 2 ^ (12 / (5 : ℝ)) * (2 ^ (2 / (15 : ℝ)) - 1) +
    4 * (2 ^ (1 / (6 : ℝ)) - 1) + 2 ^ (12 / (6 : ℝ)) * (2 ^ (4 / (21 : ℝ)) - 1) + 2 ^ (3 / (2 : ℝ)) * (2 ^ (5 / (24 : ℝ)) - 1) +
    2 ^ (4 / (3 : ℝ)) * (2 ^ (2 / (9 : ℝ)) - 1) + 2 ^ (6 / (5 : ℝ)) * (2 ^ (7 / (30 : ℝ)) - 1) +
    2 ^ (12 / (11 : ℝ)) * (2 ^ (8 / (33 : ℝ)) - 1))) < 0 := by
  have h₁ {x} (h : x ≠ 0 := by grind) : log 2 * x + 1 < 2 ^ x := by
    grind [exp_mul, exp_log, add_one_lt_exp (by positivity : log 2 * x ≠ 0)]
  have h₂ {x : ℝ} (h : 0 ≤ x := by grind) : (0 : ℝ) ≤ 2 ^ x - 1 := by grind [Real.one_le_rpow]
  repeat grw [←h₁]
  · have := log_two_gt_d9
    nlinarith
  all_goals exact h₂