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
/-- `same_abs` の反射性 -/
@[refl] theorem same_abs_refl (x : Int) : x ≡ x := by
simp [same_abs]
variable {x y z : Int}
-- メタ変数の番号を表示しないようにする
set_option pp.mvars false
-- `calc` を使おうとすると
-- `Trans` 型クラスのインスタンスではないというエラーになってしまう
/--
error: invalid 'calc' step, failed to synthesize `Trans` instance
Trans same_abs same_abs ?_
Additional diagnostic information may be available using the `set_option diagnostics true` command.
-/
#guard_msgs in
example (hxy : x ≡ y) (h : y = z) : x ≡ z := calc
x ≡ y := hxy
_ ≡ z := by rw [h]
/-- 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 := by rw [h]
証明が1行で終わらないとき
calc
を使用しているとき、証明を見やすく保つためには各行の証明は1行で完結させた方が良いのですが、そうもいかない場合があります。そのような場合、その行の証明項をメタ変数で置き換えると、証明を後回しにすることができます。
example (x y z : Nat) (hxy : x = y) (h : y = z) : x = z := by
calc
x = y := ?lem -- この行の証明を後回しにすることができる
_ = z := by rw [h]
-- 後回しにした証明を埋める
case lem =>
rw [hxy]