読者です 読者をやめる 読者になる 読者になる

きくらげ観察日記

好きなことを、適当に。

Coq

Coqで型クラスで群論

Coq

群論に関する定義をするのであれば、型クラスを使うのが一番うまくいくと思います。 Class Group G := { gunit : G; gadd : G -> G -> G; ginv : G -> G; gadd_unit_l : forall g : G, gadd gunit g = g; gadd_unit_r : forall g : G, gadd g gunit = g; gad…

Coqで型クラスでモナド

Coq

Haskell大好きなので、モナドを実装できそうな言語があればとりあえず実装してしまう癖があります。 Coqでモナド使うほどのことを書くのか、と言われればアレですが。 Class Monad (M : Type -> Type) := { point {A : Type} : A -> M A; bind {A B : Type} …

Coqで型クラス

Coq

Coqにも型クラスがあるらしいです。 Class Ord a := { le : a -> a -> bool }.これでleというメソッドを持つ型クラスOrdを定義できます。インスタンス定義は以下のように行います。 Fixpoint le_nat (n m : nat) : bool := match n, m with | O, O => true |…

Coqで代数的データ型の各要素についての等式を得る

Coq

前提 C x y z = C x' y' z から x = x', y = y', z = z' を導くためのタクティックが用意されています。 injection 等式 H : C x y z = C x' y' z' についてinjection Hをすると、ゴールをx = x' -> y = y' -> z = z' -> (元のゴール)という形に書き換えてく…

Coqで等式の左右を入れ替える

Coq

タイトルの通りです。eq_reflをdestructしていい感じにやるような方法でも解けることは解けます。 Goal forall (T : Type) (x y : T), x = y -> y = x. Proof. intros T x y H. (* H : x = y *) destruct H. (* Goal: x = x *) reflexivity. Qed.しかし、等…

Coqのintrosでパターンマッチング

Coq

destructは以下のような代数的データ型 Inductive T : Type := | C1 : x11 -> x12 -> ... -> T | C2 : x21 -> x22 -> ... -> T ... | Cn : xn1 -> xn2 -> ... -> T.の値xに対して、 destruct x as [x11 x22 ... | x21 x22 ... | ... | xn1 xn2 ... ]でパター…

Coqのsplit, left, rightについてもう少し詳しく

Coq

inkar-us-i.hatenablog.com上の記事でandを証明するためにsplit, orを証明するためにleft, rightを使えばいいと書きましたが、実はこれらのタクティックはもう少し一般的に作られています。 split splitはandのみではなく、コンストラクタがC : X1 -> X2 -> …

Coqで「任意のxについて…」「あるxが存在して…」を扱う

Coq

Coqで「任意のxについて…」を表すforall xは、xを受け取って残りの命題の証明を返す関数となっています。 Definition prop_1 : forall (x : nat), x = x := fun x => eq_refl x.また、「あるxが存在して…」を表すexists xは、以下のようなデータ型として定義…

Coqで「…かつ…」、「…または…」を扱う

Coq

連言「かつ」、選言「または」を表すandとorは、Coqでは次のようなデータ構造として定義されています。 Inductive and (A B:Prop) : Prop := conj : A -> B -> A /\ B where "A /\ B" := (and A B) : type_scope. Inductive or (A B:Prop) : Prop := | or_in…

Coqで定理の証明中に補題を示す

Coq

assertタクティックを使うと、証明の途中で他の補題を証明できます。 Goal forall P Q R : Prop, P -> (P \/ Q -> R) -> R. Proof. intros P Q R H1 H2. (* H1 : P *) (* H2 : P \/ Q -> R *) (* 先にP -> Rを示す *) assert (P -> R). { (* P -> R の証明 *…

Coqで前提や定理を適用して証明する

Coq

ゴールが前提や既にある定理そのものである場合が、証明の一番簡単なパターンです。 前提がゴールそのものである場合 assumptionを使うと、前提にあるゴールと全く同じ命題をそのまま適用してくれます。 Goal forall P : Prop, P -> P. Proof. intros. (* P …

Coqで数学的帰納法を行う

Coq

数学的帰納法を行いたい場合は、基本的にelimかinductionのどちらかのタクティックを利用します。 elim こちらが最も基本的な帰納法です。elim x.とすることで、xについての帰納法を行うことができます。 例えば、以下のコードでは直接to_zero n = 0を示すの…

Coqでデータ型に対して条件分岐を行う

Coq

証明中にデータ型に対して条件分岐を行うためには、case, case_eq, destruct等を使います。 とりあえず普通に条件分岐をする caseは普通の条件分岐です。例えばb : boolに対してcase b.とすると、b = trueである場合とb = falseである場合の2つに分かれ、そ…

Coqで定理の特定の項だけを書き換える

Coq

rewriteやsimplを使って定理を書き換えようとすると、どうしても思ったとおりに書き換えがいかないことがあります。 (* 結合法則と交換法則を使って、3つの項を入れ替える *) Goal forall (T : Type) (op : T -> T -> T), (forall x y z : T, op (op x y) z …

Coqで既存の定理、定義に従って計算する。

Coq

定義に従って計算する 定義に従って計算するには、simpl, compute, unfoldが使えます。 simpl.はゴールの式をいい感じに簡単にしてくれるのに対し、compute.はとりあえず式展開します。また、unfoldは定義の左辺から右辺に書き換えます。 Fixpoint fact (n :…

Coqで前提の矛盾から定理を証明する

Coq

矛盾を導く方法は何通りかあります。 すでに前提にFalseがある場合。 まずは一番基本的な方法から。既に前提にFalseがある場合です。 Falseの定義は、以下のようになっています。 Inductive False := (* コンストラクタが1つもない *).従って、前提にP : Fal…

coq-modeとproofgeneralでcoq環境を作る

Coq

EmacsでCoqを扱う場合、proofgeneralというものを使うのが一般的らしいです。 $ sudo apt-get install coq proofgeneral Ubuntuの場合はどちらもaptのリポジトリに入っているので、上のコマンドを打つだけでインストールは完了です。 (load-file "/usr/share…