前回の記事では普通の証明としてEuclideanDomainには零因子がないことを示しました。こんな感じでした。
$a, b$を零因子、すなわち$a\ne 0, b\ne 0, a * b=0$とします。$a * b = 0$及び$r\; 0\; a$から$r\; (a*b)\; a$。これはmul_left_not_lt a bに矛盾します。これで無事に任意のEuclideanDomainには零因子がないこと、すなわち整域であることが証明できました。
まあいいんですけど、この証明を見て細かいことを言えば$r\; 0\; a$は自明でしょうか。そういうことをきちんと詰めるための道具が形式的証明のツールであり、Lean4があるわけです。目の前にLean4があり、形式化されたユークリッド整域の定義があるわけですから、その範囲で零因子が存在しないことを形式的に証明しましょう。
まずは$a\ne 0$から$r\; 0\; a$を示します。
theorem zero_bottom {R : Type u} [self : EuclideanDomain R](a : R) (ha: a≠0): EuclideanDomain.r 0 a := by
have h1 : a % a =0 := by simp
have h2 : EuclideanDomain.r (a%a) a := by
exact EuclideanDomain.mod_lt a ha
rw [h1] at h2
exact h2
a%a=0は自明ですからsimpタクティクで示すことができました。またEuclideanDomain.mod_ltという定理があり、任意のa, b≠0についてr(a%b) bがわかっています。ここにb=aとするとr(a%a) aがわかります。これがh2です。この式のa%aを0で書き換える(rwタクティク)とr 0 aとなり証明が終了しています。
つぎに零因子がないことを証明します。a≠0, b≠0ならばa * b ≠ 0と定式化できます。
theorem nonzero_divisors {R : Type u} [self : EuclideanDomain R](a b: R) (ha: a≠0) (hb: b≠0) : a * b ≠ 0 := by
by_contra h1
have rab_lt_a: EuclideanDomain.r (a*b) a := by
rw [h1]
exact zero_bottom a ha
have not_rab_lt_a: ¬ EuclideanDomain.r (a*b) a := by
exact EuclideanDomain.mul_left_not_lt a hb
contradiction
証明は背理法を使うのでby_contraタクティクを使用します。結論を否定したh1: a * b = 0が仮定に入ります。h1と直前に証明したzero_bottom定理を使うとr(a*b) aはほぼ自明に示せます。
さらにEuclideanDomainではmul_left_not_ltという制約があります。それは¬ r (a*b) aです。これでA=r(a*b) aについてAと¬Aが示せたので矛盾です。contradictionタクティクで矛盾を指摘して証明が終了します。
rがwell founded relationだからといってr 0 aが自明になるわけではありません。Lean4で形式証明をすることでr 0 aも零因子がないこともしっかりと自信を持つことができます。
もうひとつ、形式的証明を作れれば自分の理解は正しいことをLean4が保証してくれます。これは非常に嬉しいです。
