calc モード

calc は，等式や不等式の連鎖を数学の計算のように書くための構文です． 各行の右側に，そのステップの根拠を書きます． 各ステップは，前の行の右辺と次の行の左辺をつなぐ証明になっている必要があります．

example (a b c : Nat) : (a + b) + c = b + (a + c) :=
  calc
    (a + b) + c = (b + a) + c := by
      rw [Nat.add_comm a b]
    _ = b + (a + c) := by
      rw [Nat.add_assoc]

calc は等式だけでなく，推移律を持つ関係にも使えます． 次の例では ≤ の推移律を calc が使っています．

example (a b c : Nat) (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c :=
  calc
    a ≤ b := h₁
    _ ≤ c := h₂

tactic モードの中で calc を使うこともできます．

example (a b c : Nat) : (a + b) + c = b + (a + c) := by
  exact
    calc
      (a + b) + c = (b + a) + c := by
        rw [Nat.add_comm a b]
      _ = b + (a + c) := by
        rw [Nat.add_assoc]

演習

calc モードで加法の結合律・可換律を使って証明してください．

example (a b c : Nat) : a + b + c = b + a + c := by
  calc
    a + b + c = b + a + c := by
      -- `ac_rfl` または `rw [Nat.add_comm a b]` などを試す．
      sorry