前の記事でcalcモードがわかっていないと書きました。calcは便利そうなのでとりあえず簡単なユースケースを勉強しました。理解できたと思うのでメモを残しておきます。
Quantifiers and Equality - Theorem Proving in Lean 4にある説明を中心にして理解しました。最も典型的なユースケースは等式A=Bを証明する場合です。式Aから始めてタクティクを使って変形し、式Bを導ければ等式証明が成功します。等式変形なので使うタクティクはrwで、仮定や既知の定理を使って式変形します。
現在勉強中の第3章「論理」の中ので分かり易い例があったので紹介します。偶関数と奇関数を定義して、奇関数と奇関数の積は偶関数になることを証明します。
偶関数、奇関数を定義する。FnEven fは「fは偶関数」という命題になる。
def FnEven (f : ℝ → ℝ) : Prop :=
∀ x, f x = f (-x)def FnOdd (f : ℝ → ℝ) : Prop :=
∀ x, f x = -f (-x)
奇関数と奇関数の積は偶関数であることをcalcを使って証明する。ofは「fは奇関数」という命題、ogは「gは奇関数」という命題で、それらを仮定して「fun x↦ f x * g x という関数（fとgの積）は偶関数」を証明する。
example (of : FnOdd f) (og : FnOdd g) : FnEven fun x ↦ f x * g x := by
intro x
dsimp -- ここまでで証明補助ウィンドウを見るとゴールはf x * g x = f (-x) * g (-x) になっている。これをcalcモードで証明する。
calc
f x * g x = -f (-x) * g (x):= by rw [of] -- fが奇関数であることを使う。
_ = -f (-x) * -g (-x) := by rw [og] -- gが奇関数であることを使う。
_ = f (-x) * g (-x) := by rw [neg_mul_neg] -- fとgの前のマイナスが打ち消しあう。ここは既知の定理neg_mul_negを使う。-- ここで補助ウィンドウでは全ての証明が終わったことが表示される。
Quantifiers and Equality - Theorem Proving in Lean 4によるとcalcモードは等式変形だけではなく、一般的な関係の証明にも使えるそうです。不等号の式の証明も例として記載されています。
