## Stream: new members

### Topic: Help with proof syntax

#### Mike (Oct 19 2023 at 14:04):

Trying to work out my own proof from an exercise in Mathematics in Lean

import Mathlib.Analysis.SpecialFunctions.Log.Basic
import MIL.Common

variable (a b c d e : ℝ)
open Real

example : |a * b| ≤ (a ^ 2 + b ^ 2) / 2 := by
have h₁ : 0 ≤ a^2 - 2 * a * b + b^2
calc
a^2 - 2*a*b + b^2 = (a-b)^2 := by ring
_ ≥ 0 := by apply pow_two_nonneg
have h₂ : a*b ≤ (a^2 + b^2)/2
calc
a*b ≤ (a^2 + b^2)/2 := by linarith
have h₃ : -a*b ≤ (a^2 + b^2)/2
calc


The book recommends using abs_le'.mpr, so I wanted to apply that with h₂ and h₃.

Could someone show me how to finish the proof without using constructor (is it even possible)? The book's solution uses it:

theorem fact1 : a * b * 2 ≤ a ^ 2 + b ^ 2 := by
have h : 0 ≤ a ^ 2 - 2 * a * b + b ^ 2
calc
a ^ 2 - 2 * a * b + b ^ 2 = (a - b) ^ 2 := by ring
_ ≥ 0 := by apply pow_two_nonneg
linarith

theorem fact2 : -(a * b) * 2 ≤ a ^ 2 + b ^ 2 := by
have h : 0 ≤ a ^ 2 + 2 * a * b + b ^ 2
calc
a ^ 2 + 2 * a * b + b ^ 2 = (a + b) ^ 2 := by ring
_ ≥ 0 := by apply pow_two_nonneg
linarith

example : |a * b| ≤ (a ^ 2 + b ^ 2) / 2 := by
have h : (0 : ℝ) < 2 := by norm_num
apply abs_le'.mpr
constructor
· rw [le_div_iff h]
apply fact1
rw [le_div_iff h]
apply fact2


Edit: This works. It's mostly based on the book's solution

example : |a * b| ≤ (a ^ 2 + b ^ 2) / 2 := by
have h₁ : 0 ≤ a^2 -2*a*b + b^2
calc
a^2 -2*a*b + b^2 = (a-b)^2 := by ring
_ ≥ 0 := by apply pow_two_nonneg
have h₂ : 0 ≤ a^2 + 2*a*b + b^2
calc
a^2 + 2*a*b + b^2 = (a+b)^2 := by ring
_ ≥ 0 := by apply pow_two_nonneg
have g₁ : a*b ≤ (a ^ 2 + b ^ 2)/2 := by
rw [le_div_iff]
linarith
norm_num
have g₂ : -(a * b) ≤ (a^2 + b^2)/2 := by
rw [le_div_iff]
linarith
norm_num
apply abs_le'.mpr
constructor
apply g₁
apply g₂


It seems like constructor is necessary because abs_le'.mpr has an ∧ that has to be satisfied, and I can't figure out how to use case here (maybe because it's not possible).

#### Ruben Van de Velde (Oct 19 2023 at 15:47):

You could cheat with

  apply abs_le'.mpr ⟨?_, ?_⟩


but I'm not sure what makes you want to avoid constructor

#### Alex J. Best (Oct 19 2023 at 15:54):

You can use show_term constructor to see what a tactic did, in this case constructor is equivalent to refine { left := ?left, right := ?right }, so you could use that instead

#### Mike (Oct 19 2023 at 16:33):

@Ruben Van de Velde @Alex J. Best The pdf Mathematics in Lean didn't introduce constructor, so I have no idea what it's doing. I was just hoping that there was a way to solve it that just used apply, linarith, and have (even if it's a clunky proof).

Right now I'm stuck on an even simpler problem.

example : |a * b| ≤ (a ^ 2 + b ^ 2) / 2 := by
have h₁ : 0 ≤ 1/2*a^2 -a*b + 1/2*b^2
calc
1/2*a^2 -a*b + 1/2*b^2 = ((a-b)^2)/2 := by ring
_ ≥ 0 := by
rw [le_div_iff norm_num]
have h₂ : a*b ≤ (a ^ 2 + b ^ 2) / 2
calc
a*b ≤ (a ^ 2 + b ^ 2) / 2 := by linarith [h₁]
have h₃ : 0 ≤ 1/2*a^2 + a*b + 1/2*b^2
calc -- This is underlined in red, and there's an error message: expected '|'  Lean 4
1/2*a^2 + a*b + 1/2*b^2 = (a+b)^2/2 := by ring
_ ≥ 0 := by
rw [le_div_iff norm_num]
have h₄ : -a*b ≤ (a ^ 2 + b ^ 2) / 2
calc
a*b ≤ (a ^ 2 + b ^ 2) / 2 := by linarith [h₃]
apply
abs_le'.mpr h₂ h₄


It looks like the proof of h₃ doesn't work, but Lean Infoview doesn't show any error messages.

#### Kyle Miller (Oct 19 2023 at 20:26):

@Mike It looks like constructor is introduced in the next chapter: https://leanprover-community.github.io/mathematics_in_lean/C03_Logic.html#index-18

#### Patrick Massot (Oct 19 2023 at 22:41):

If the solution uses a tactic that was not explained at this stage then it's a clear bug. Could you open a GitHub issue about it?

#### Kyle Miller (Oct 20 2023 at 04:09):

Last updated: Dec 20 2023 at 11:08 UTC