Coq関係で最近やったこと

期末試験での現実逃避のため最近改めてCoqに触ってみた。ここでは、その内容と自分の理解について簡単にまとめて書き残すが、不正確な内容が含まれているかもしれない。

関数の連続性、数列の収束

微積分の証明をCoqで扱ってみたいなと思ったので、関係しそうなところを調べてみた。
Coqで実数を扱うには
Require Import Coq.Reals.Reals.
をすれば大丈夫だと思われる。

実数に対して四則演算、大小関係などがNotationとして定義されているが、これらは自然数でのものとしっかり区別しなくてはならないし、Scopeに気をつけなくてはならない。その辺についてはたぶんhttp://coq.inria.fr/refman/Reference-Manual014.htmlに書いてある。
例えば

Require Import Coq.Reals.Reals.
Goal forall n:nat, INR n < INR (n+1).
(*INR:nat->Rは自然数から実数への包含写像*)

としても

Error: In environment
n : nat
The term "INR n" has type "R" while it is expected to have type "nat".

というエラーが出る。
これは"<"が自然数natにおける不等号と解釈されているせいである。実数Rにおける不等号と解釈させるにはOpen Scopeして

Require Import Coq.Reals.Reals.
Open Scope R_scope.
Goal forall n:nat, INR n < INR (n+1).

または%Rを後ろにつけて

Require Import Coq.Reals.Reals.
Goal forall n:nat, (INR n < INR (n+1))%R.

とする。
逆にOpen Scope R_scopeしているときに

Require Import Coq.Reals.Reals.
Open Scope R_scope.
Goal forall n:nat, n < n+1.

とnatの不等式を書いてもエラーになるので、%natをつけるなどして対処する。

調べた標準ライブラリ

http://coq.inria.fr/library/Coq.Reals.Raxioms.html
公理的に実数を定義している。
自然数から実数への包含写像INRなどもここで定義されている。

http://coq.inria.fr/stdlib/Coq.Reals.Rdefinitions.html
四則演算、不等号、NotationやInfixなど

http://coq.inria.fr/library/Coq.Reals.Ranalysis1.html
には関数の連続性や微分可能性に関する定義があるようで、
continuity_ptが一点での連続性、continuityが実数全体での連続性、と言う具合に_ptがつくものは点での性質を表す。

http://coq.inria.fr/library/Coq.Reals.Rseries.html
数列の収束Un_cv、単調増加性Un_growingなどが定義されている。

http://coq.inria.fr/library/Coq.Reals.Rfunctions.html
R_dist 距離 絶対値をとるだけ
infinite_sum
sum_f_R0 Nまでのf_nの和
sum_f sからnまでのfの和?
sum_nat_f_O natの数列の和
powerRZ x^n

http://coq.inria.fr/stdlib/Coq.Reals.RIneq.html
実数の不等式
Record posreal

http://coq.inria.fr/library/Coq.Reals.Rbasic_fun.html
Rabs
Rmax
Rmin

タクティック

最近知ったタクティックを簡単にまとめ

Variable
Un_cvの定義においてUnが暗黙のうちに使われているように見えるが、よく見るとSectionの最初にVariable Un : nat -> R.とかかれている。リファレンスマニュアルを読んだ感じだとどうやらSectionの中ではVariableで宣言したUnはUn_cvの定義などにおいて暗黙に使えるようになるが、外からUn_cvを利用するときは明示的に与えなくてはならないらしい。
数列{1/n}が0に収束する事を書きたければ
Goal Un_cv (fun (n:nat) => / (INR n)) 0.
のようにUn_cvにUn:nat->Rに当たるものを与える。

Record
正の実数posrealは次のように定義されている。
Record posreal : Type := mkposreal {pos :> R; cond_pos : 0 < pos}.
これを使うと
Goal forall r:posreal, r > 0.
のように書ける。
Recordの定義のcond_pos : 0 < posは仮定として用いることができる。

Goal forall r:posreal, r > 0.
intro.
apply cond_pos.
Qed.

destruct r.
とかもできるみたい。

{A}+{B}
Axiom total_order_T : forall r1 r2:R, {r1 < r2} + {r1 = r2} + {r1 > r2}.
のように、{A}+{B}が成り立つときに、AかBかで場合分けしてDefinitionを書きたいときがある。
二つの実数のうち小さい方を返すRminを参考にした。

(*Lemma Rle_dec : forall r1 r2, {r1 <= r2} + {~ r1 <= r2}.*)
Definition Rmin (x y:R) : R :=
  match Rle_dec x y with
    | left _ => x
    | right _ => y
  end.

left, rightでパターンマッチさせればいいらしい。

infix
中置記法にする。
http://coq.inria.fr/library/Coq.Reals.Rdefinitions.html
を見れば分かると思う。

NotationもInfixと似たようなことに使われているようだが、たぶんInfix以上のこと、例えば三項演算子のようなものを定義したり、左結合、右結合を指定したり、異なる演算子の間での結合の強さを指定したりできるものだと思う。

info_auto
autoの中で実際何をしているかを表示する。

auto with Hintdb
ヒントデータベースHintdbを利用してautoする。
Hintdbとしては実数関係のヒントデータベースrealなんかがある。
Print HintDb Hintdbで表示できる。

ltac
タクティックをいくつか組み合わせて新しくタクティックを定義するようなものととりあえず理解している。http://coq.inria.fr/refman/Reference-Manual011.htmlに説明されていると思うが、しっかりと読んではいない。
Require Import Coq.Reals.RealsをするとRComputeやRegなどが使えるようになる。

http://coq.inria.fr/refman/Reference-Manual011.htmlに書いてあるタクティックについて
idtac:何もしない/文字列や数字を表示
repeat: 繰り返せるだけ繰り返す
try: error levelを1引く
fail: errorを出す
など

実際に動作を見ればわかりやすいと思う。

Goal forall (P Q:Prop), P/\Q -> Q /\ P.
intros.
destruct H.
split; [apply H0 | apply H].
(*splitでできた二つのゴールの一つ目にapply H0、二つ目にapply H*)
Qed.

Goal forall (P Q:Prop), P/\Q -> Q /\ P.
idtac "message".
idtac 1.
(*メッセージを表示*)
idtac.
(*何もしない*)
repeat intro.
(*繰り返し*)
first [apply H | idtac].
first [apply H | split].
(*[]の中のtacticを前から順に適用できるか試し、どれかが適用できれば成功してそこで終了、どれもできなければ失敗*)
fail || idtac.
try(try (fail 1)).
fail 2 || idtac.
(*tryや||が一つあるごとにlevelが1ずつ引かれていく?*)
(*ただのfailはlevel 0?*)
progress idtac.
(*進歩があれば成功*)
solve [idtac | intuition].
(*証明が完了するまで進めば成功?*)

Ocamlでtacticを書く

qnighyさんの記事CoqのtacticをOCamlで書く話 - 簡潔なQを見て少しやってみようかと
環境はUbuntu 13.04
ocaml-native-compilers libcoq-ocamlをインストール

Make

-R . evar_match
evar_match.ml

evar_match.ml

open Pp
open Term
open Refiner

TACTIC EXTEND evar_match
| [ "evar_match" constr(x) ] ->
    [ match kind_of_term x with
        | Evar _ -> tclIDTAC
        | _ -> tclFAIL 0 (str "not an evar")
    ]
END

この二つのファイルを作ってから

$ coq_makefile -f Make -o Makefile
$ make

を実行。

これでevar_matchというtacticが使えるようになる。
evar_match.v

Declare ML Module "evar_match".

Goal forall (x y z : nat), x = y -> y = z -> x = z.
  intros;
  eapply trans_eq;
  match goal with
    | |- ?a = ?b => evar_match a; idtac a
    | |- ?a = ?b => evar_match b; idtac b
  end.

感想

記事が長くなって、途中から書くのが面倒になってしまった。次からは長い記事は分割して書くようにする。
リファレンスマニュアルをあまり読んでいないが、読むべきだなと思った。