まだ小学生の頃に習ったことで印象に残っているのは３の倍数の確認方法でした。各桁を足した数が３の倍数ならば元の数も３の倍数、というアレです。
倍数とか約数とかがLean4で扱えるようになり、この３の倍数の確認方法の証明を書き下してみようと思いました。自分で定理を形式化して証明を与えることを一通りやるには良いのではないかと思ったのです。
任意桁数の３の倍数で証明しようとすると、その数の10進数展開がk桁あるとして各桁を$a_n$とすると$\sum_{n=0}^{k-1} a_n\,10^n$と表すことができるところから始める必要があります。まだ$\sum$記号を勉強していないこともあり、えいやで３桁と限定することにしました。また各桁は0〜9の自然数とするのが自然なのですが計算を簡単に済ます都合で各桁は任意の整数としています。もちろんその中から常に0〜9を選べば良いだけなので定理の主張に問題が生じることはありません。
証明したいことは次の１行目で形式化出来ています。2行目でほぼ自明な補題を１つ示しています。この補題を最後の行で使いたいからです。3行目以降はcalcを使いながら100*c+10*b+をa+b+c とそれ以外に分けています。そして「それ以外」が補題から3の倍数であることから残ったa+b+cが3の倍数であることを示しています。
example {a b c:ℤ} : 3∣(100*c+10*b+a) ↔ 3∣(c+b+a) :=
have div3cb: 3∣3*(33*c+3*b) := by exact Int.dvd_mul_right 3 (33 * c + 3 * b)
calc
3∣(100*c+10*b+a)↔3∣(3*(33*c+3*b)+(c+b+a)) := by ring_nf
_ ↔ 3∣(c+b+a) := by apply divisable_add div3cb
theorem divisable_add {a b k:ℤ } (h: k∣a) : k∣(a+b)↔k∣b := by ...
この定理を示せれば３の倍数確認法の証明は上記のようにほぼ自明になります。一方divisable_addの証明はちょっと長いです。同値変形でできなくて、矢印の両方の向きを別々に証明したためです。形式証明はこんな感じです。
theorem divisable_add {a b k:ℤ } (h: k∣a) : k∣(a+b)↔k∣b := by
rcases h with ⟨m,hh⟩ -- hh:a=k*m
constructor -- k∣(a+b)→k∣b向きの証明
· intro h1 -- h1: k∣(a+b)
rcases h1 with ⟨ n, h2⟩ -- h2: a+b=k*n
rw [hh] at h2 -- h2:k*m+b=k*n
have : b= k*n-k*m := by exact eq_sub_of_add_eq' h2
have : b = k*(n-m) := by rw [Int.mul_sub];assumption
rw [this] -- ⊢ k∣k*(n-m)
exact Int.dvd_mul_right k (n - m) -- no goal-- k∣b→k∣(a+b)向きの証明
intro h1 -- h1: k∣b
rcases h1 with ⟨ n,h2⟩ -- h2: b=k*n
rw [hh,h2] -- ⊢ k∣(k*m+k*n)
have : k*m+k*n=k*(m+n) := by exact (Int.mul_add k m n).symm
rw [this] -- ⊢ k∣k*(m+n)
exact Int.dvd_mul_right k (m + n) -- no goal
出てくるタクティクは見慣れたrcases, constructor, intro, rw, have, exactだけですし、rwやexactのところでは?を付けて検索すれば書き換えルールや適用すべき定理を見つけてくれるので、証明自体はほぼ機械的に出来ました。
ところでなぜ自然数ではなく整数を使って形式化したのでしょうか。
example {a b c:ℕ} : 3∣(100*c+10*b+a) ↔ 3∣(c+b+a) := by ...
でも同じように証明できそうですが、、、とりあえずすごく複雑な証明になりました。理由は自然数が環ではないのでringとかring_nfタクティクが使えないのです。そこで細かい式変形を全部明示的に行う必要があり大変なことになります。多分何か便利な方法があると思うのですが、、、見つけられませんでした。
自然数で形式化した証明はこんな感じです。もちろんdivisable_addも自然数版が必要です。ただそちらの証明は整数版とほとんど同じで行けますので掲載は省略します。
example {a b c:ℕ} : 3∣(100*c+10*b+a) ↔ 3∣(c+b+a) := by
have divb3: 3∣ 3*(3*b) := by exact Nat.dvd_mul_right 3 (3 * b)
have divc3: 3∣ 3*(33*c) := by exact Nat.dvd_mul_right 3 (33 * c)
have : 3∣(100*c+10*b+a)↔3∣ (c+b+a) := calc
3∣(100*c+10*b+a)↔3∣(100*c+(10*b+a)) := by rw [Nat.add_assoc]
_ ↔ 3∣( (99*c+c)+(10*b+a) ) := by rw [Nat.succ_mul]
_ ↔ 3 ∣(99*c+c+(10*b+a)) := by rw [Nat.add_add_add_comm]
_ ↔ 3∣(99*c+(c+(10*b+a))) := by rw [Nat.add_assoc]
_ ↔ 3∣(3*(33*c)+(c+(10*b+a))) := by rw [@Mathlib.Tactic.RingNF.mul_assoc_rev]
_ ↔ 3∣(c+(10*b+a)) := by exact divisable_add divc3
_ ↔ 3∣(c+( (9*b+b)+a) ) := by rw [Nat.succ_mul]
_ ↔ 3∣(c+(9*b+b+a)) := by rw [Nat.add_left_comm]
_ ↔ 3∣( (9*b+b+a) +c):= by rw [Nat.add_comm]
_ ↔ 3∣(9*b+(b+a)+c):= by rw [@Mathlib.Tactic.RingNF.add_assoc_rev]
_ ↔ 3∣(3*(3*b)+(b+a)+c) := by rw [@Mathlib.Tactic.RingNF.mul_assoc_rev]
_ ↔ 3∣(3*(3*b)+( (b+a) +c)) := by rw [Nat.add_assoc]
_ ↔ 3∣( (b+a) +c) := by exact divisable_add divb3
_ ↔ 3∣(c+(b+a)) := by rw [Nat.add_comm]
_ ↔ 3∣(c+b+a) := by rw [@Mathlib.Tactic.RingNF.add_assoc_rev]
assumption
自然数の範囲でもある程度自動的に証明を進めてくれる、ringやring_nf相当のタクティクってあるのでしょうか。
