Twitterで「各桁の和が3の倍数な整数は3の倍数、定理証明の練習に良さそう」
というのがあったので、チャレンジしてみる。
sumDigitは各桁の和を求める関数だが、
ここで一つズルをする。
直接、各桁の和を求めるのではなく、再帰した時の関係性を書くのだ。
| n | sumDigit n | sumDigit (n-3)を引く |
|---|---|---|
| 9 | 9 | 3 |
| 10 | 1 | -6 |
| 19 | 10 | 3 |
| 20 | 2 | -6 |
| 99 | 18 | 3 |
| 100 | 1 | -6-9 |
普段は3だが、繰り上がりのところで-6になる。
そして100で-9追加、1000で-9-9追加になる。
これは、繰り上がりがある所では、
sumDigit (S (S (S n))) = -3a + sumDigit n
と置けそうだ。
こうすることによって、3の倍数か調べる時に、aを落とせる訳だ。
（190223追記）
Leanで関数内のif文は、
by_casestacticと、
rw if_posで突破できた。
.
.
Idris版もやってみる。
……まぁ すぐに詰んでやろう
Idrisのif文はwith (式) proof pで突破できるし、
簡約もバッチリだ。
.
.
