Lean初心者なんですけど多項式難しすぎない？

書いた数学の証明に自信がなかったので、Leanで確認したかったんです。初心者なんですけどなんとか証明を書きあげました。一か月で1万行ぐらい書いた気がします。何度も書き直したので最終的に2000行ぐらいに収まりました。

さわってみた感想

UXは非常によいです。Coqでは上に戻ったり下に進んだりすごいめんどくさかったところが、Leanではマウスカーソルで適当に移動して、好きな場所を簡単に編集できます。編集しかけのコード片が残っていても、なにやらいいような感じで処理してくれます。

言語に関しては、byをどこにでも書けるのがいいですね。これにより証明を含んだ型の値も簡単に構築できます。あと、if h : e then e else eの形のdif式も便利です。フィールドアクセス風の式は最高です。

気になった点は、型クラスのインスタンスを解決できないエラーが初心者には難しいところですね。最初の数日は相当苦労しました。あとλが変数名に使えません。

多項式の扱い方

今回は多項式が乱舞する証明となったので、多項式の話をします。Leanには多項式のモジュールが2つあって、ひとつ目はMathlib.Algebra.Polynomialで一変数多項式を扱うことができます。もうひとつはMathlib.Algebra.MvPolynomialで、多変数多項式を扱うことができます。今回わたしが使いたかった多項式は

Y^2+a_1XY+a_3Y=X^3+a_2X^2+a_4X+a_6

という二変数多項式のため、迷わずMvPolynomialを選んだのですが、これは失敗でした。Mathlib.Algebra.Polynomial.Bivariateにある二変数多項式の方が楽だと思います。最終的にこちらを使いました。これは、実際は二変数というより、$K[X][Y]$、すなわち一変数多項式を係数とする一変数多項式なのですが、二変数多項式と同じものです。今回のように変数の数が固定で数も少ない場合は、このように一変数多項式を積み重ねて使うとよいと思います。MvPolynomialは何変数でも受け入れるような汎用性が必要なときに使いましょう。

問題の多項式は、$a_1$から$a_6$まで5つのパラメーターがあるので、それをまとめた構造体を作りましょう。

structure Weierstrass K where
  a₁ : K
  a₂ : K
  a₃ : K
  a₄ : K
  a₆ : K

最初にやることは、多項式を返すメソッドを生やすことです。

namespace Weierstrass
variable {K : Type*} [Field K]

noncomputable def polynomial (W : Weierstrass K) : K[X][Y] :=
    C (X^3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆) - Y^2 - C (C W.a₁ * X + C W.a₃) * Y

K[X]やK[X][Y]の値はPolynomial.CやPolynomial.X、Polynomial.Yを使って作ります。係数の値はC aと書かないといけません。KからK[X]への自動変換があるとよさそうに見えますが、幻想です。実際にありません。例えば$abX$という多項式は

C (a * b) * X

と書いたり、

C a * C b * X

とも書くことができますが、自動変換なんてあった日には

a * b * X

なんてどこで変換が行われて、かっこがどこに付いてるのか地獄になるのは目に見えています。ただし、自然数からK[X]への自動変換はあるので、

C 2 * X = 2 * X

という式がでてきたりします。これはringでは証明できません。2をどちらかに統一する必要があります。これがよく出てくるのが

(X + C a)^2

みたいな式をringで展開したときで、自然数の2が変換されてでてきたりして混乱します。

え、そんなの式を見れば分かる？ほんとに？

(C (C u) * C (C u) * C X + C (C r)) * ((C (C u) * C (C u) * C X + C (C r)) * (C (C u) * C (C u) * C X + C (C r))) +
            C (C W.a₂) * ((C (C u) * C (C u) * C X + C (C r)) * (C (C u) * C (C u) * C X + C (C r))) +
          C (C W.a₄) * (C (C u) * C (C u) * C X + C (C r)) +
        C (C W.a₆) -
      (C (C u) * (C (C u) * C (C u)) * Y + C (C u) * C (C u) * C (C s) * C X + C (C t)) *
        (C (C u) * (C (C u) * C (C u)) * Y + C (C u) * C (C u) * C (C s) * C X + C (C t)) -
    (C (C W.a₁) * (C (C u) * C (C u) * C X + C (C r)) + C (C W.a₃)) *
      (C (C u) * (C (C u) * C (C u)) * Y + C (C u) * C (C u) * C (C s) * C X + C (C t)) =
  C (C u) ^ 6 * (C X * (C X * C X)) +
            (C (C W.a₂) - C (C s) * C (C W.a₁) + C (C 3) * C (C r) - C (C s) * C (C s)) * C (C u) ^ 4 * (C X * C X) +
          (C (C W.a₄) - C (C s) * C (C W.a₃) + C (C 2) * C (C r) * C (C W.a₂) -
                    (C (C t) + C (C r) * C (C s)) * C (C W.a₁) +
                  C (C 3) * (C (C r) * C (C r)) -
                C (C 2) * C (C s) * C (C t)) *
              (C (C u) * C (C u)) *
            C X +
        (C (C W.a₆) + C (C r) * C (C W.a₄) + C (C r) * C (C r) * C (C W.a₂) + C (C r) * (C (C r) * C (C r)) -
              C (C t) * C (C W.a₃) -
            C (C t) * C (C t) -
          C (C r) * C (C t) * C (C W.a₁)) -
      C (C u) ^ 6 * (Y * Y) -
    ((C (C W.a₁) + C (C 2) * C (C s)) * C (C u) ^ 5 * C X +
        (C (C W.a₃) + C (C r) * C (C W.a₁) + C (C 2) * C (C t)) * (C (C u) * (C (C u) * C (C u)))) *
      Y

これだと、ringが通りません。

simp [C_ofNat]をするといい感じになるので、下のようになりringで通るようになります。

(C (C u) * C (C u) * C X + C (C r)) * ((C (C u) * C (C u) * C X + C (C r)) * (C (C u) * C (C u) * C X + C (C r))) +
            C (C W.a₂) * ((C (C u) * C (C u) * C X + C (C r)) * (C (C u) * C (C u) * C X + C (C r))) +
          C (C W.a₄) * (C (C u) * C (C u) * C X + C (C r)) +
        C (C W.a₆) -
      (C (C u) * (C (C u) * C (C u)) * Y + C (C u) * C (C u) * C (C s) * C X + C (C t)) *
        (C (C u) * (C (C u) * C (C u)) * Y + C (C u) * C (C u) * C (C s) * C X + C (C t)) -
    (C (C W.a₁) * (C (C u) * C (C u) * C X + C (C r)) + C (C W.a₃)) *
      (C (C u) * (C (C u) * C (C u)) * Y + C (C u) * C (C u) * C (C s) * C X + C (C t)) =
  C (C u) ^ 6 * (C X * (C X * C X)) +
            (C (C W.a₂) - C (C s) * C (C W.a₁) + 3 * C (C r) - C (C s) * C (C s)) * C (C u) ^ 4 * (C X * C X) +
          (C (C W.a₄) - C (C s) * C (C W.a₃) + 2 * C (C r) * C (C W.a₂) - (C (C t) + C (C r) * C (C s)) * C (C W.a₁) +
                  3 * (C (C r) * C (C r)) -
                2 * C (C s) * C (C t)) *
              (C (C u) * C (C u)) *
            C X +
        (C (C W.a₆) + C (C r) * C (C W.a₄) + C (C r) * C (C r) * C (C W.a₂) + C (C r) * (C (C r) * C (C r)) -
              C (C t) * C (C W.a₃) -
            C (C t) * C (C t) -
          C (C r) * C (C t) * C (C W.a₁)) -
      C (C u) ^ 6 * (Y * Y) -
    ((C (C W.a₁) + 2 * C (C s)) * C (C u) ^ 5 * C X +
        (C (C W.a₃) + C (C r) * C (C W.a₁) + 2 * C (C t)) * (C (C u) * (C (C u) * C (C u)))) *
      Y

他に間違いやすいものとして

C u^6
C (u^6)

もringは何も助けてくれないので気を付けましょう。

扱いが難しいのは逆数の係数です。

C u⁻¹

が出てくる式には要注意です。上にでてきたような複雑な式にところどころC u⁻¹が入ってて、C uと相殺することで等号が成り立つといった証明は地獄です。なぜかというと

C u⁻¹

を変換して

(C u)⁻¹

にすることができないからです。これができればfieldを使えばだいぶましになるでしょうが、多項式は乗法について逆元をとる演算を持っていません。よってこれを相殺するには、例えば

C u⁻¹ * X * C u

みたいな式の場合、mul_commやmul_assocを頑張って

(C u⁻¹ * C u) * X

この形まで持ってきて、←C_mulで

C (u⁻¹ * u) * X

にしてから、field_simpで消す必要があります。もちろん、これが上のような複雑な式に入っていた場合、とてもじゃないですが証明不能になります。

多項式=多項式のパターンはこれくらいにして次に行きましょう

eval一族

eval系の関数は多項式と代入したい値を受け取って、変数に値を代入した結果を返してくれます。一番汎用的なものはeval₂です。こいつは代入だけでなく、係数に対しても与えた関数を適用して変形してくれます。ですが、この2つの指定を同時に使うことはそうないと思うので、特化したバージョンが用意されています。

evalはK[X]に対して、Kの値しか代入させてくれません。結果もK固定です。我々のWeierstrass型の多項式も、Kの値を代入して結果が0になる図形を考察するものですから、evalを使います。K[X][Y]の場合は2つKを受け取るevalEvalになります。

noncomputable def eval (W : Weierstrass K) (p : Affine K) : K :=
    W.polynomial.evalEval p.x p.y

noncomputable def mem (W : Weierstrass K) (p : Affine K) : Prop :=
    W.eval p = 0

instance instMemberShip : Membership (Affine K) (Weierstrass K) where
    mem := mem

こんな感じで、Weierstrassが集合っぽく見えるようp ∈ Wと書けるようにしてみました。Affine KはKのペアです。

やりたいのはこの曲線と直線の交点を扱うことです。Lineという型も用意しました。

structure Line (K : Type u) where
  a : K
  b : K

これは、$Y = aX + b$という直線を表す型です。こちらの多項式は単純で

namespace Line

noncomputable def polynomial (L : Line K) : K[X][Y] :=
    C (C L.a * X) - Y + CC L.b

noncomputable def eval (L : Line K) (p : Affine K) : K :=
    L.polynomial.evalEval p.x p.y

noncomputable def mem (L : Line K) (p : Affine K) : Prop :=
    L.eval p = 0

instance instMemberShip : Membership (Affine K) (Line K) where
    mem := mem

となり、こちらもp ∈ Lと書けるようにしています。

2つの交点を表す型も作りましょう。

-- W ∩ L
structure Intersection (K : Type*) where
  W : Weierstrass K
  L : Line K

簡単ですね。こちらのmemは上と違って

namespace Intersection

noncomputable def mem (I : Intersection K) (p : Affine K) :=
    p ∈ I.W ∧ p ∈ I.L

instance instMemberShip : Membership (Affine K) (Intersection K) where
    mem := mem

としています。すなわち、曲線と直線のどちらにも属している点が交点です。これは多項式でも書けます。

\begin{cases}
Y^2+a_1XY+a_3Y=X^3+a_2X^2+a_4X+a_6\\
Y=aX+b
\end{cases}

この連立方程式の解が交点ですから、下の式を上の式に代入して

(aX+b)^2+a_1X(aX+b)+a_3(aX+b)=X^3+a_2^2+a_4X+a_6

を満たす$X$が交点の$x$座標になります。このような多項式の代入もeval一族です。

noncomputable def polynomial (I : Intersection K) : K[X] :=
    I.W.polynomial.eval (C I.L.a * X + C I.L.b)

今回はK[X][Y]のYに代入して、結果がK[X]なので、evalでできます。

さて、p ∈ IとI.polynomial.eval p.x = 0は同値かというと、これだけだと$y$座標が拘束できてないので同値ではありませんが、$y$についての条件も適当に追加すれば同値になります。このへんは次の節でやりましょう。

evalファミリーには、mapやcompといった特殊なものもありますが、詳しくはマニュアルを見てください。

最後に、これらの関数はだいたいみんな環準同型になっていて、evalRingHomのような変種が用意されています。これの便利なところを紹介しておきましょう。

多項式を受け取って何か値を返す関数はevalのように様々なものがありますが、これらの関数どうしが等しいことを示したいことも多いはずです。このとき思いつくのが、Xの行先とC aの行先が一致していたら、どんな多項式を渡しても行先が等しくなるのではないかという考えです。RingHomバージョンを使っていると、この論法を使用することができます。関数=関数の形のゴールに変形しておき、extを使えばできます。最初の変形にはRingHom.congr_funを使うのがよいでしょう。合成関数は← RingHom.comp_applyで作れます。

似たようなものにAlgHomがあり、RingHomより強いのですが、RingHomで十分な場合はRingHomを使った方がいいでしょう。AlgHomには係数を指定する必要があり、

K[X] →ₐ[K] S

のような型になります。真ん中に指定したKが係数になり、K代数の準同型であることを示しています。これは色々使ってると

K[X] →ₐ[K[X]] S

みたいなのがでてきたりして、係数を合わせないと合成できないという事態が発生します。RingHomならこのような調整は不要です。

根

次にやりたいことは、Intersectionの点が2つ見つかったときに、もうひとつの点が必ずあることです。I.polynomialは3次式なので、これは必ず見つかります。まず、根と点の関係を正確に書くために、根のMultisetを点のMultisetに変換しましょう。

$x$座標だけから$y$座標を計算して直線上の点に変換する関数は簡単に書けます。

namespace Line

noncomputable def point_at_x (L : Line K) (x : K) : Affine K :=
    ⟨x, L.a * x + L.b⟩

多項式の根全体はPolynomial.rootsで取得することができます。これはMultisetなので、根の多重度も考慮した集合になっています。これには$x$座標しか入っていないので、上の関数を使って、点のMultisetにしましょう。

namespace Intersection

noncomputable def points (I : Intersection K) : Multiset (Affine K) :=
    I.polynomial.roots.map I.L.point_at_x

これで、最初に定義した$\in$と多項式の根から作った$\in$が同値であることを示すことができます。

lemma mem_iff_points_mem {I : Intersection K} {p : Affine K} :
    p ∈ I ↔ p ∈ I.points

右辺の$\in$はMultisetの$\in$であるため、多重度を考慮した議論ができます。ここでは2点が含まれていたら、もう1点含まれているという議論をやりたいため、この形式を使う必要があり、以下の定理になります。

lemma two_points_exists_third [DecidableEq K] {I : Intersection K} {p₁ p₂ : Affine K}
    (h2 : {p₁, p₂} ≤ I.points) :
    ∃p₃, I.points = {p₁, p₂, p₃} := by

Multisetには集合間の包含関係を表す述語に$\subset$と$\le$の2つがあります。ここでは多重度も含めて比較してくれる後者を使う必要があります。これにより、p₁とp₂が等しいときにも正しい言明になっています。$S \subset T$は$p\in S$ならば$p\in T$という定義です。$\subset$ではどういう反例ができるのか考えてみるのもいいでしょう。

この証明はMultisetの要素数cardを比較することで行います。3次方程式なので、要素数は3以下であり、$\{p_1, p_2\}$の要素数は2なので(多重度も含めた要素数であることに注意)、まず、証明すべきことはI.points.cardが2ではないことです。

lemma card_points_ne_two {I : Intersection K} :
    I.points.card ≠ 2 := by

これを証明するには、2であるとして矛盾を示すわけですが、Polynomial.exists_prod_multiset_X_sub_C_mulという便利な定理が準備されています。

theorem Polynomial.exists_prod_multiset_X_sub_C_mul{R : Type u} [CommRing R] [IsDomain R] (p : Polynomial R) :
∃ (q : Polynomial R),
  (Multiset.map (fun (a : R) => X - C a) p.roots).prod * q = p ∧ p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0

これは多項式$p$にたいして

p = q*\prod (X-a)^i

となる$q$が存在するという定理で、この総積はp.rootsの要素すべてにわたる積で、$i$はその要素の多重度になります。さらに、この$q$は根をもたず、次数は$p$の次数からp.roots.cardを引いたものにできるという定理です。この定理を使うと$q$は次数1のはずなのに、根を持たないということになり矛盾します。

根の数が3以下であることは、Polynomial.card_roots'で簡単に示せます。次数に関しては次節でやりましょう。

lemma card_points_le_three {I : Intersection K} :
    I.points.card ≤ 3 := by
  rw [card_points_card_roots, ← I.polynomial_natDegree_three]
  apply card_roots'

これにより先に書いた第3の点が存在することは簡単に証明できます。

根が3つあれば、完全に因数分解することができます。

lemma three_points_factor {I : Intersection K} {p₁ p₂ p₃ : Affine K}
    (h3 : I.points = {p₁, p₂, p₃}) :
    I.polynomial = (X - C p₁.x) * (X - C p₂.x) * (X - C p₃.x)

逆に完全に因数分解できれば、ちょうど3点持つことも言えます。

lemma factor_three_points {I : Intersection K} {p₁ p₂ p₃ : Affine K}
    (hp₁ : p₁ ∈ I.L) (hp₂ : p₂ ∈ I.L) (hp₃ : p₃ ∈ I.L)
    (hf : I.polynomial = (X - C p₁.x) * (X - C p₂.x) * (X - C p₃.x)) :
    I.points = {p₁, p₂, p₃} := by

因数分解できると、解と係数の関係を使って3つ目の点の座標を求める公式が得られます。

lemma three_points_sum {I : Intersection K} {p₁ p₂ p₃ : Affine K}
    (h3 : I.points = {p₁, p₂, p₃}) :
    p₁.x + p₂.x + p₃.x = I.L.a^2 + I.W.a₁ * I.L.a - I.W.a₂

noncomputable def third_point (I : Intersection K) (p₁ p₂ : Affine K) :=
    I.L.point_at_x (I.L.a^2 + I.W.a₁ * I.L.a - I.W.a₂ - p₁.x - p₂.x)

lemma third_point_points [DecidableEq K] {I : Intersection K} {p₁ p₂ : Affine K}
    (h2 : {p₁, p₂} ≤ I.points) :
    I.points = {p₁, p₂, I.third_point p₁ p₂} := by

次数と係数

前節で次数はでてきましたが、説明をしませんでした。次数にはdegreeとnatDegreeの2種類が用意されています。通常、数学では多項式の次数は自然数か$-\infty$を取ることになっています。多項式$0$の次数が$-\infty$であり、そのほかの多項式の次数は自然数です。これに対応したものがdegreeで、$\mathbb{N}\cup\{\bot\}$の値を返します。一方でnatDegreeは多項式$0$にたいして$0$を割り当てるため、自然数しか返しません。状況に応じて適切に使い分ける必要があります。

我々の多項式が3次式であることを示しましょう。degreeとnatDegreeの両方あったほうが便利なので、degreeから計算して、natDegreeを次に計算します。

lemma polynomial_degree_three {I : Intersection K} :
    I.polynomial.degree = 3 := by
  simp [polynomial_eq]
  compute_degree <;> try trivial
  simp

lemma polynomial_natDegree_three {I : Intersection K} :
    I.polynomial.natDegree = 3 := by
  exact natDegree_eq_of_degree_eq_some I.polynomial_degree_three

多項式の次数に関する証明に役立つtacticがcompute_degreeです。

以下の形のゴールに使えます。

• natDegree f = d
• degree f = d
• natDegree f ≤ d (or <)
• degree f ≤ d (or <)
• coeff f d = r, if d is the degree of f

ただ、このtacticはかなり重いので、なるべくきれいな形の多項式にしてから使わないといけない気がします。あと、係数を計算するcoeffは最上位の係数のときにしか使えないので注意してください。

多項式の根を扱っていると、多項式が0でないことを要請されることが多くあります。この証明はnatDegreeが$\bot$でないことを使うのが簡単です。

lemma polynomial_ne_zero {I : Intersection K} :
    I.polynomial ≠ 0 := by
  rw [← degree_ne_bot, polynomial_degree_three]
  simp

重根と微分

多項式の重根というのは微分と関係しているのでした。多項式$p$の根が重根となるのは、$p$の根であり$p$の微分の根でもあることと同値です。これを使って、I.polynomialが重根を持つことと、直線が接線になっていることが同値であることを証明していきます。

重根と微分に関する定理は、少し見つけにくいですがMathlib.Algebra.Polynomial.FieldDivisionにあります。

例えば上の重根と微分の根の関係は以下の定理になります。

theorem Polynomial.one_lt_rootMultiplicity_iff_isRoot{R : Type u} [CommRing R] {p : Polynomial R} {t : R} (h : p ≠ 0) :
1 < rootMultiplicity t p ↔ p.IsRoot t ∧ (derivative p).IsRoot t

我々の多項式も微分しておきましょう。

noncomputable def derivative (I : Intersection K) : K[X] :=
    I.polynomial.derivative

lemma derivative_eq (I : Intersection K) :
    I.derivative = C 3 * X^2 + C (2 * I.W.a₂) * X + C I.W.a₄
      - C (2 * I.L.a) * (C I.L.a * X + C I.L.b) -C (2 * I.W.a₁ * I.L.a) * X
      - C (I.W.a₁ * I.L.b) - C (I.W.a₃ * I.L.a)

これと重根の関係は上記の定理で簡単に示せます。接線との関係を調べましょう。Weierstrassの方の多項式は2変数で、

F(X,Y) = X^3+a_2X^2+a_4X+a_6-Y^2-a_1XY-a_3Y

の形でした。これを$X$と$Y$でそれぞれ偏微分して、それらの比を使えば接線の傾きがわかります。2変数多項式にはK[X][Y]の型を使っていたので、$X$での偏微分は$Y$の多項式の係数を微分するだけです。$Y$での偏微分は単に1変数の微分derivativeでできます。

namespace Weierstrass

noncomputable def dxf (W : Weierstrass K) : K[X][Y] :=
    W.polynomial.sum fun e f => C f.derivative * Y^e

noncomputable def dyf (W : Weierstrass K) : K[X][Y] :=
    W.polynomial.derivative

$F(X,Y)$の$(X,Y)$に直線の方程式$(X,aX+b)$を代入した結果(すなわちI.polynomial)の微分は合成関数の微分により、各偏微分の線形結合の形で書けます。

namespace Intersection

noncomputable def dxf (I : Intersection K) : K[X] :=
    I.W.dxf.eval (C I.L.a * X + C I.L.b)

noncomputable def dyf (I : Intersection K) : K[X] :=
    I.W.dyf.eval (C I.L.a * X + C I.L.b)

lemma derivative_eq_dxf_dyf (I : Intersection K) :
    I.derivative = I.dxf + C I.L.a * I.dyf := by
  simp [derivative_eq, dxf, dyf, Weierstrass.dxf_eq, Weierstrass.dyf_eq, C_ofNat]
  ring

こういうのは合成関数の微分を頑張ってライブラリーから探さずに、展開して等しいでやっちゃうのが早いです。

tangent_atの定義は同値なものがいくつか得られたわけですが、これにしておきましょう。

noncomputable def tangent_at (I : Intersection K) (p : Affine K) :=
    p ∈ I ∧ I.eval_derivative p.x = 0

lemma tangent_at_iff {I : Intersection K} {p : Affine K} (Hnneq : p ≠ I.W.neg p) :
    I.tangent_at p ↔ p ∈ I ∧ I.L.a = -I.W.eval_dxf p / I.W.eval_dyf p := by

これで、直線の傾きと接線と重根がひとつに繋がりました。

lemma tangent_at_two_points [DecidableEq K] {I : Intersection K} {p : Affine K} :
    I.tangent_at p ↔ {p, p} ≤ I.points := by

接線以外の直線として、2点を繋ぐ直線も考えます。そして、2点が等しければ接線を使い、異なれば弦を使う関数lineを作りました。

noncomputable def chord (p₁ p₂ : Affine K) : Line K :=
  ⟨(p₂.y - p₁.y) / (p₂.x - p₁.x), (p₁.y * p₂.x - p₂.y * p₁.x) / (p₂.x - p₁.x)⟩

noncomputable def tangent (p : Affine K) (W : Weierstrass K) : Line K :=
  ⟨-W.eval_dxf p / W.eval_dyf p, p.y + W.eval_dxf p / W.eval_dyf p * p.x⟩

noncomputable def line [DecidableEq K] (W : Weierstrass K) (p₁ p₂ : Affine K) : Line K :=
    if p₁ = p₂ then tangent p₁ W else chord p₁ p₂

このlineは$W$と必ず2点で交わることがわかります。すなわち、3点で交わります。

lemma line_two_pints [DecidableEq K] {W : Weierstrass K} {p₁ p₂ : Affine K}
    (hp₁ : p₁ ∈ W) (hp₂ : p₂ ∈ W) (hnneg : p₁ ≠ W.neg p₂) :
    {p₁, p₂} ≤ ((Line.line W p₁ p₂).intersection W).points := by

最後にここまでの集大成として、関数starを定めます。これは上記の3つ目の点です。

namespace Weierstrass

noncomputable def star (W : Weierstrass K) (p₁ p₂ : Affine K) : Affine K :=
    ((Line.line W p₁ p₂).intersection W).third_point p₁ p₂

lemma star_iff {W : Weierstrass K} {p₁ p₂ p₃ : Affine K}
    (hp₁ : p₁ ∈ W) (hp₂ : p₂ ∈ W) (hnneg : p₁ ≠ W.neg p₂) :
    p₃ = W.star p₁ p₂ ↔ ∃(L : Line K), (L.intersection W).points = {p₁, p₂, p₃} := by

最後の定理から、starが可換であることは簡単にわかります。

lemma star_comm {W : Weierstrass K} {p₁ p₂ : Affine K}
    (hp₁ : p₁ ∈ W) (hp₂ : p₂ ∈ W) (hnneg : p₁ ≠ W.neg p₂) :
    W.star p₁ p₂ = W.star p₂ p₁ := by
  generalize hp₃ : W.star p₂ p₁ = p₃
  symm at hp₃ ⊢
  rw [star_iff hp₂ hp₁ (W.nneg_symm hnneg)] at hp₃
  rw [star_iff hp₁ hp₂ hnneg]
  obtain ⟨L, hl⟩ := hp₃
  use L
  rw [hl]
  simp [Multiset.cons_swap p₁ p₂]

さて、私の目標の定理までまだ半分しか進んでいませんが、この記事は多項式の話なのでここまでにしておきましょう。証明の残りを見たい方は https://github.com/kik/EcGroupLaw をどうぞ。最終目標は

theorem lemma_EC_assoc {W : Weierstrass K} {P Q R : EC W} (hns : ¬W.singular) :
    (P + Q) + R = P + (Q + R)

となっております。

最後にここまでの証明で一番役に立ったtacticを紹介します。

linear_combination

linear_combinationは神tacticです。