平方根を扱うタクティクをマクロとして作る例

-- sqrt_eq_cases for y = √ x
theorem eq_sqrt_cases (x y : ℝ) : y = Real.sqrt x ↔ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0 := by
  have r : y = Real.sqrt x ↔ Real.sqrt x = y := by exact eq_comm
  rw [r]
  exact Real.sqrt_eq_cases

macro "norm_sqrt_eq" : tactic => `(tactic| rw [Real.sqrt_eq_cases] <;> ring_nf <;> repeat norm_num )
macro "norm_eq_sqrt" : tactic => `(tactic| rw [eq_sqrt_cases] <;> ring_nf <;> repeat norm_num )

-- Normalize square roots of rational literals
macro "norm_sqrt" : tactic => `(tactic| first | norm_sqrt_eq | norm_eq_sqrt)

example : Real.sqrt 25 = 5 := by norm_sqrt
example : Real.sqrt 4 = 2 := by norm_sqrt
example : Real.sqrt 18 = 3*Real.sqrt 2 := by norm_sqrt
example : 2 = Real.sqrt 4:= by norm_sqrt
example : Real.sqrt (1/4) = 1/2 := by norm_sqrt
example : Real.sqrt (1/2) = Real.sqrt 2 / 2 := by norm_sqrt

lean-ja / lean-by-example

平方根を扱うタクティクをマクロとして作る例 #377