前の記事でcalcモードがわかっていないと書きました。calcは便利そうなのでとりあえず簡単なユースケースを勉強しました。理解できたと思うのでメモを残しておきます。 Quantifiers and Equality - Theorem Proving in Lean 4にある説明を中心にして理解しました。最も典型的なユースケースは等式A=Bを証明する場合です。式Aから始めてタクティクを使って変形し、式Bを導ければ等式証明が成功します。等式変形なので使うタクティクはrwで、仮定や既知の定理を使って式変形します。 現在勉強中の第3章「論理」の中ので分かり易い例があったので紹介します。偶関数と奇関数…
