calc モードの使い分け

1. 複雑な等式の証明（可読性の向上）

何段階もの変形が必要なとき、rw（書き換え）だけで済ませると、Infoview（右側のパネル）を見ない限り、途中で式がどうなっているのか人間には分かりません。

rw だけの場合: 「呪文」のように見え、他人が後から修正するのが大変です。
calc の場合: 数学の答案用紙のように、一行ごとに式が変わっていく様子がソースコードに明示されます。

2. 「等号」以外の関係を混ぜるとき（最大の強み）

rw は基本的に「イコール（）」の書き換えしかできませんが、calc は 不等号（, ） などを混ぜた連鎖を扱うことができます。

-- calc なら「等号」と「不等号」を自然に繋げられる
calc
  a = b := h1
  _ ≤ c := h2
  _ < d := h3
-- 結論として a < d が導かれる

3. 「推移律」を直感的に表現するとき

とからを導くような推移律の連鎖を、論理記号を使わずに構造的に表現できます。特に「左辺から始まって右辺で終わる」という数学的な直感に沿った記述が可能です。

🛠️ Mathlib スタイルでの使い分け基準

Mathlib の開発や査読（レビュー）では、以下のような基準で calc の使用が判断されます。

項目	`by rw [h1, h2]` を使う	`calc` を使う
目的	素早く、短く証明を終わらせる	議論のステップを明快に示す
ステップ数	1〜2 ステップ程度	3 ステップ以上の長い変形
関係性	等号（）のみ	等号と不等号（）の混在
用途	自明な補助定理、短い定義の展開	主要な定理の証明、計算がメインの証明

🚀 実践例：`(a + b) * c = c * a + c * b`

交換則と分配則を組み合わせて証明する場合を比較してみましょう。

タクティクのみ（効率重視）:

example (a b c : ℤ) : (a + b) * c = c * a + c * b := by
  rw [add_mul, mul_comm a c, mul_comm b c]

calc を使用（説明重視・Mathlib らしい美しさ）:

example (a b c : ℤ) : (a + b) * c = c * a + c * b :=
  calc
    (a + b) * c = a * c + b * c := by rw [add_mul]
    _           = c * a + b * c := by rw [mul_comm a c]
    _           = c * a + c * b := by rw [mul_comm b c]

1. 関係性の混合（Transitivity の活用）

calc の最大の魅力は、= 以外の記号を混ぜられることです。Mathlib では、Eq（等号）、LE.le（）、LT.lt（）の推移律が登録されているため、これらを自由に組み合わせられます。

example (a b c d : ℤ) (h1 : a = b) (h2 : b < c) (h3 : c ≤ d) : a < d :=
  calc
    a = b := h1
    _ < c := h2
    _ ≤ d := h3

注意: 最終的な結論の記号（この場合は <）は、連鎖の中で最も「強い」記号が自動的に選ばれます。

2. 根拠としての `by` 構文

各行の := の右側には、「その一行を証明する項」を置く必要がありますが、複雑な場合は by を使ってタクティク・モードに切り替えるのが Mathlib の常石です。

by rw [h]: 特定の仮定で書き換える。
by simp: 簡約化して等号を導く。
by linarith: 線形算術（不等式など）を一撃で解く。

calc
  (a + b) * (a + b) = a * (a + b) + b * (a + b) := by rw [add_mul]
  _                 = a * a + a * b + b * (a + b) := by rw [mul_add]
  _                 = ...

3. `_` (アンダースコア) による左辺の省略

calc では 2 行目以降、_ を使うことで「直前の行の右辺」を指すことができます。これにより、冗長な記述を避け、変形のフォーカスがどこにあるかを明確にします。

4. 項モードでの「ドット記法」と組み合わせ

根拠の部分を by を使わずに、純粋な項（Term）で書くとさらに Mathlib らしくなります。

h.symm: y = x を x = y に変換。
congr_arg f h: x = y から f x = f y を導く。

calc
  f x = f y := congr_arg f h
    _ = f z := ...

5. `conv` タクティクとの併用（部分的な書き換え）

calc の各ステップで、「式全体ではなく、右辺の中のこの部分だけを書き換えたい」という状況がよくあります。その際、conv (conversion) を by の中で使うと非常に強力です。

calc
  a + (b + c) = a + (c + b) := by
    conv =>
      rhs         -- 右辺（Right Hand Side）にフォーカス
      arg 2       -- 2番目の引数（b + c）に移動
      rw [add_comm] -- そこだけで交換則を適用

これで、式全体に rw がかかって意図しない場所まで変わってしまうのを防げます。

6. 根拠としての `linarith` (線形算術)

不等式の連鎖において、単純な rw では解けない「当たり前」の変形（例：など）には、linarith を根拠として置くのが Mathlib スタイルです。

calc
  x ≤ y     := h1
  _ < y + 1 := by linarith -- 数学的に自明な不等式を埋める
  _ ≤ z     := h2

7. 等号の「合同性」を利用する（`congr` 系）

calc の中で、わざわざ rw を使わずに「両辺に同じ操作をする」ことでステップを埋めるテクニックです。

congr_arg:
congr_fun:

calc
  f (a + b) = f (b + a) := congr_arg f (add_comm a b)

by rw と書くよりも計算資源を消費せず、項モードとして非常に高速でクリーンな証明になります。

8. インデントとフォーマットの作法（Mathlib Style Guide）

Mathlib の査読を通るためには、見た目の美しさも重要です。

演算子の位置: = や ≤ は、基本的には _ の直後に置きます。
位置合わせ: 全ての = の位置が縦に揃うようにスペースを調整します。

-- 悪い例（読みづらい）
calc a = b := h1
_ = c := h2

-- 良い例（Mathlib スタイル）
calc
  a = b := h1
  _ = c := h2
  _ = d := by
    rw [h3]
    simp

9. 項モードとしての `calc`

実は calc はタクティクではなく「項（Term）」です。そのため、by の中に入れなくても、直接関数の戻り値として使えます。

-- 関数の本体として直接 calc を置く
example (a b c : ℤ) (h1 : a = b) (h2 : b = c) : a = c :=
  calc
    a = b := h1
    _ = c := h2

1. 書き換えのターゲット指定（Precise Rewriting）

最後の行の rw [add_comm] ですが、もし式の中に他にも + があった場合、意図しない場所が入れ替わってしまうことがあります。Mathlib では、確実に特定の場所を入れ替えるために rw [add_comm n k] のように引数を与えることが推奨される場合があります。

2. 項（Term）による記述への挑戦

calc の各ステップは、実は by rw を使わずに「定理の名前＋引数」という純粋な項だけでも書けます。これができるようになると、証明のコンパイル速度が上がり、見た目もより数学的な美しさが増します。

example : (n + m) + k = m + (n + k) :=
  calc
    (n + m) + k = n + (m + k) := add_assoc n m k
    _           = (m + k) + n := add_comm (n + m) k -- (n+m) と k を入れ替え
    _           = m + (k + n) := add_assoc m k n
    _           = m + (n + k) := congr_arg (m + ·) (add_comm k n)

※ congr_arg (m + ·) は「m + という枠の中で、中身（k + n）だけを入れ替える」という高度なテクニックです。

🚀 次のステップ：不等式の連鎖

calc モードが最も威力を発揮するのは、等号だけでなく 不等号 が混ざる時です。Mathlib にある linarith（線形不等式の自動証明タクティク）と組み合わせて、これを解いてみませんか？

問題： a ≤ b かつ c < d ならば、a + c < b + d である。

variable (a b c d : ℕ)

example (h1 : a ≤ b) (h2 : c < d) : a + c < b + d :=
  calc
    a + c ≤ b + c := by rel [h1] -- Mathlibのタクティク：不等式の両辺に同じ操作をする
    _     < b + d := by linarith

新しい道具：

rel [h1]: h1 : a ≤ b を使って、式全体の関係性を保ったまま一部を置き換える便利なタクティクです。
linarith: 「ならば」といった数論的な推論を自動で行います。

Mathlibにおいて、不等式の証明を calc で書く際は、単なる rw よりも rel や gcongr、あるいは linarith といったタクティクが根拠（justification）としてよく使われます。

🛠️ 不等式の `calc` チャレンジ

import Mathlib.Tactic

variable (a b c d : ℕ)

example (h1 : a ≤ b) (h2 : c < d) : a + c < b + d :=
  calc
    a + c ≤ b + c := by gcongr -- a ≤ b なので、両辺に c を足しても不等号は維持される
    _     < b + d := by gcongr

🌟 知っておくと得する「不等式 calc」のルール

推移律の自動判定: calc は、行ごとに < や ≤ が混ざっていても、最終的な結論が ≤ になるのか < になるのかを、数学的な推論規則に基づいて自動で判定してくれます。

≤ と ≤ の連鎖 ≤
≤ と < の連鎖 <

gcongr の魔法: Mathlib スタイルでは、rw は不等号（≤）に対しては使えないことが多い（等号 = でないと書き換えられない）ため、代わりに gcongr を使うのが一般的です。