calc

calc は計算モードに入るためのタクティクです．推移律が成り立つような二項関係をつなげて，一つの証明項を構成します．

-- `calc` そのものは `import` なしで使える
import Mathlib.Tactic -- 大雑把に import する


variable (a b : ℝ)

example : 2 * a * b ≤ a ^ 2 + b ^ 2 := by
  -- a ^ 2 - 2 * a * b + b ^ 2 ≥ 0 を示せばよい
  suffices a ^ 2 - 2 * a * b + b ^ 2 ≥ 0 from by
    linarith

  -- 少しずつ式変形して示していく
  calc a ^ 2 - 2 * a * b + b ^ 2
    _ = (a - b) ^ 2 := by ring
    _ ≥ 0 := by positivity

calc の直後に来る項も _ で省略することができます．

example : ∀ x y ε : ℝ, 0 < ε → ε ≤ 1 → |x| < ε → |y| < ε → |x * y| < ε := by
  intro x y ε epos ele1 xlt ylt
  show |x * y| < ε

  calc
    _ = |x| * |y| := abs_mul x y
    _ < ε * ε := by gcongr
    _ ≤ 1 * ε := by gcongr
    _ = ε := by simp

カスタマイズ

自前で定義した二項関係も，Trans 型クラスのインスタンスにすれば calc で使用することができます．

/-- 絶対値が同じであることを表す二項関係 -/
def same_abs (x y : Int) : Prop := x = y ∨ x = - y

-- same_abs のための中値記法を用意する
-- このファイル内でだけ有効にするために local と付けた
local infix:50 " ≡ " => same_abs

variable {x y z : Int}

-- same_abs の推移律
def same_abs_trans (hxy : x ≡ y) (hyz : y ≡ z) : x ≡ z := by
  dsimp [same_abs]

  -- hxy と hyz について場合分けをする
  rcases hxy with hxy | hxy <;> rcases hyz with hyz | hyz

  -- omega でカタをつける
  all_goals omega

-- same_abs を「推移的な二項関係」として登録する
instance : Trans same_abs same_abs same_abs where
  trans := same_abs_trans

-- same_abs についても calc が使える!
example (hxy : x ≡ y) (h : y = z) : x ≡ z := calc
  x ≡ y := hxy
  _ = z := h