Help with proof syntax

Stream: new members

[Mike]

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]

You could cheat with

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

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

[Alex J. Best]

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]

@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]

@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]

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]

Sure: https://github.com/avigad/mathematics_in_lean_source/issues/138