| title | tags | author | slide |
|---|---|---|---|
Coq で環のイデアルを作ってみる |
Coq |
mathink |
false |
- Coq で環のイデアルを定義して、具体例を一個作ってみた。
- 「Coq で環」 の続き。
- ソースコードもその続き。
-
$Z_n$ でちょっと遊んだよ
環
部分群であるということは、加法の演算と、逆元の演算、その両者について閉じているということになります。
今回は、部分群を経由せずにこれらの条件を直接書き下してイデアルの型 Ideal を定義します。
また、左とか右とか言わず、いきなり両側です。
イデアルを「どう記述するか」という部分は大事なところなので、表現に注目してください。
Module Ideal.
Open Scope ring_scope.
Class spec (R: Ring)(P: R -> Prop) :=
proof {
contain_subst: Proper ((==) ==> flip impl) P;
add_close:
forall x y,
P x -> P y -> P (x + y);
inv_close:
forall x,
P x -> P (x^-1);
z_close:
P 0;
mul_close:
forall x y,
P x -> P y -> P (x * y);
left_mul:
forall a x,
P x -> P (a * x);
right_mul:
forall a x,
P x -> P (x * a)
}.
Structure type (R: Ring) :=
make {
contain: R -> Prop;
prf: spec contain
}.
Module Ex.
Existing Instance prf.
Existing Instance contain_subst.
Notation isIdeal := spec.
Notation Ideal := type.
Coercion prf: Ideal >-> isIdeal.
Arguments isIdeal (R P): clear implicits.
End Ex.
End Ideal.
Export Ideal.Ex.
部分集合をどう記述するのか、というところが重要なポイントです。
今回の定義では P で以って、 P x が真になることと解釈することにしました。
そのため、例えば「加法について閉じている」という言明は
forall x y, P x -> P y -> P (x + y)
になります。他の演算についても同様です。
また、P は setoid 上の述語なので、R の項についての代入が可能でなければなりません。
それを意味するのが contain_subst です。
述語は、 contain という名前で type 型のフィールドとして与えられています。
環 R に対して、 Ideal R 型の要素 I は Ideal.contain I という R 上の述語を生成し、その述語を用いることで、R の元 x がイデアル I に含まれるか否かを示す命題を Ideal.contain I x と記述することが出来ます。
Arguments コマンドに clear: implicits というサフィックスを付けると、函数に元々設定されていた引数の暗黙性がリセットされます。
このようにしたのは isIdeal R P という記述にすることで、 P が R の carrier Type 上の述語でも問題なく記述できるようにするためです。
R が Canonical Structure として定義されていれば問題は起きないのですが、そうでない場合、たとえば P を Z 上の述語にしてしまうと、 Z_ring のイデアルだと認識できないのです(今回は、前回に Z_ring を Canonical Structure として定義しているので大丈夫ですが、毎回そうできるとも限りません)。
なお、この段落の言っている意味がわからない場合、スルーしてもらっても構いません。
その場合、 Arguments の行はおまじないみたいなものだと思っておいてください。
## 構成してみる。
前回 で環の例として整数の環 Z_ring: Ring を構成しました。
ですので、イデアルの具体例として
を構成してみたいと思います。
Instance Zn_is_ideal (n: Z): isIdeal Z_ring `(exists x, m = x * n).
これが、まず示すべき命題です。
整数
を満たす fun m => の省略を行なっています。
今回はせっかくですので、証明とそれぞれのサブゴールも記しておきます。
Proof.
split.
- Show.
(* 1 focused subgoals (unfocused: 6) *)
(* , subgoal 1 (ID 704) *)
(* n : Z *)
(* ============================ *)
(* Proper ((==) ==> flip impl) (fun m : Z_ring => exists x : Z, m = x * n) *)
(* (dependent evars:) *)
intros x y Heq P; simpl.
now rewrite Heq; auto.
- Show.
(* 1 focused subgoals (unfocused: 5) *)
(* , subgoal 1 (ID 705) *)
(* n : Z *)
(* ============================ *)
(* forall x y : Z_ring, *)
(* (exists x0 : Z, x = x0 * n) -> *)
(* (exists x0 : Z, y = x0 * n) -> exists x0 : Z, (x + y)%rng = x0 * n *)
(* (dependent evars:) *)
intros x y [p Hp] [q Hq]; subst.
exists (p + q).
now rewrite <- Z.mul_add_distr_r.
- Show.
(* 1 focused subgoals (unfocused: 4) *)
(* , subgoal 1 (ID 706) *)
(* n : Z *)
(* ============================ *)
(* forall x : Z_ring, *)
(* (exists x0 : Z, x = x0 * n) -> exists x0 : Z, (x ^-1)%rng = x0 * n *)
(* (dependent evars:) *)
intros x [p Hp]; subst; simpl.
exists (-p).
now rewrite Zopp_mult_distr_l.
- Show.
(* 1 focused subgoals (unfocused: 3) *)
(* , subgoal 1 (ID 707) *)
(* n : Z *)
(* ============================ *)
(* exists x : Z, 0%rng = x * n *)
(* (dependent evars:) *)
now (exists 0).
- Show.
(* 1 focused subgoals (unfocused: 2) *)
(* , subgoal 1 (ID 708) *)
(* n : Z *)
(* ============================ *)
(* forall x y : Z_ring, *)
(* (exists x0 : Z, x = x0 * n) -> *)
(* (exists x0 : Z, y = x0 * n) -> exists x0 : Z, (x * y)%rng = x0 * n *)
(* (dependent evars:) *)
intros x y [p Hp] [q Hq]; subst.
exists ((p * q) * n).
rewrite <- Z.mul_shuffle1.
now rewrite !Z.mul_assoc.
- Show.
(* 1 focused subgoals (unfocused: 1) *)
(* , subgoal 1 (ID 709) *)
(* n : Z *)
(* ============================ *)
(* forall a x : Z_ring, *)
(* (exists x0 : Z, x = x0 * n) -> exists x0 : Z, (a * x)%rng = x0 * n *)
(* (dependent evars:) *)
intros a x [p Hp]; subst.
exists (a * p).
rewrite Z.mul_assoc.
rewrite Z.mul_shuffle0.
now rewrite Z.mul_comm.
- Show.
(* 1 focused subgoals (unfocused: 0) *)
(* , subgoal 1 (ID 710) *)
(* n : Z *)
(* ============================ *)
(* forall a x : Z_ring, *)
(* (exists x0 : Z, x = x0 * n) -> exists x0 : Z, (x * a)%rng = x0 * n *)
(* (dependent evars:) *)
intros a x [p Hp]; subst.
exists (p * a).
now rewrite Z.mul_shuffle0.
Qed.
証明が終われば、あとはそれを使ってイデアルを定義するだけです。
Definition Zn_ideal (n: Z) := Ideal.make (Zn_is_ideal n).
今回も、このイデアルを使って少し遊んでみましょう。
定義した Zn_ideal で遊んでみます。といっても、元が所属しているか否かの証明くらいしかやることはないのですが。
まずは普通に特定の元が含まれることを確認してみましょう。
Goal Ideal.contain (Zn_ideal 2) 10.
Proof.
simpl.
(* ============================ *)
(* exists x : Z, 10 = x * 2 *)
now exists 5.
Qed.
はい、証明まで一通り見せました。簡単ですね。
より一般に Zn_ideal 2 がちゃんと
与える数の積の順序が逆ですが、あまり気にしないでください(可換ですからね)。
Goal forall n,
Ideal.contain (Zn_ideal 2) (n * 2).
Proof.
simpl; intros.
now exists n.
Qed.
さて、これで終わりでしょうか？
いいえ、違いますね。何故なら、これまでの命題は任意の元が
ですので、もう一つ示すべきことがあります。
です。実際にやってみましょう。 Coq で書くと次のようになります。
Goal forall n,
~ Ideal.contain (Zn_ideal 2) (n * 2 + 1).
証明は、 ZArith ライブラリに用意されている補題などを使えばそれほど難しくありません。
SearchAbout を駆使すればすぐに証明できると思います。
Proof.
intros n H; simpl in H.
assert (H': exists x, n * 2 + 1 = 2 * x).
{
destruct H as [m Hm]; exists m.
now rewrite (Z.mul_comm 2 m).
}
rewrite <- Zeven_ex_iff in H'.
revert H'.
apply Zodd_not_Zeven.
rewrite Zodd_ex_iff.
now exists n; rewrite Z.mul_comm.
Qed.
全文載せてますけれど。
今回は環のイデアルを Coq で定義して、その具体例を構成し、さらにそれが正しく機能しているかを(ほんの少し)確かめてみました。
前回のコードと合わせれば、お好きな環とイデアルについて色々と実験が出来ると思います。 是非、試してみてはいかがでしょうか。
今回利用したスクリプト全体は https://gist.github.com/mathink/429bc2aef396fac12ed2 にあります。前回のコード と併せてご利用ください。
私？気が向いたらやります。