Coqを勉強してます。
コンパイラを作るには型理論を理解しているとよくて、型理論を理解するには数学的な証明とかが出来ると良くて、数学的な証明をコンピュータ上で出来ると楽に正確に勉強出来ると思うので、Coqを勉強してます。
なんとなく、勉強してる訳ではなくて必要に迫られて勉強してるのですけど、数学アレルギーを治すのに良さそうな気がしています。
http://www.iij-ii.co.jp/lab/techdoc/coqt/
ここをみながら勉強中です。2の最後までやってみました。意味が良くわかってないんですけど。1は2回やってみました。あれだな、リッジレーサーを毎回、最初からやる事でどんなスピードでも対応出来る力を付けるみたいなそんな鍛え方をしてますよ。
覚えるまで何回もやれば最初は太極拳のように遅くても徐々にスピードは増して行くのだ。最初は繰り返し大切と。しかも、慣れれば自動証明ですっ飛ばせるらしいので、こんな所はもう分かってるぜ。autoだぜ。で、きっとよくなるんでしょう。
最初は調子良く進んでたのですが、コマンドが沢山出て来て覚えきれないです。普通のプログラミング言語じゃないので、いわゆる普通のプログラミング言語の常識が通用しない。覚える事が多すぎる。訳が分からなくなって来たので、表を書いてみました。書いてみたんですけど、読み進めたら書いてあったと言う。うーむ。表が欲しいと思ってから表があるとありがたいんだけど、いきなり表があるときっと辛いんだな。むー。ないと欲しくなるし、あればあったで苦しいって言う。
表はあくまで、自分が集めたアイテムリストとしてみるといいのかもしれない。俺専用のコマンドリストを持っておけば、やったところまでは、表をみればすぐ思い出せる。
とにかく、使い慣れることだな。10分で全問解けるくらいになれてしまえばこっちの物なはずだ。
コマンド
| 英語 | 読み | 意味 |
| Definition | デフィニション | 関数の定義 関数定義or証明編集モード用 |
| Example | エグザンプル | 例の定義 関数定義or証明編集モード用 |
| Theorem | セオラム | 定理 証明編集モード用 |
| Lemma | レマ | 補題(他の命題を証明するための小定理) 証明編集モード用 |
| Remark | リマーク | 注意 証明編集モード用 |
| Fact | ファクト | 事実 証明編集モード用 |
| Corollary | コロラリ | 系(ある定理から直ちに導かれる定理) 証明編集モード用 |
| Proposition | プロポジション | 命題 証明編集モード用 |
| Goal | ゴール | 名無しの命題 証明編集モード用 |
| Inductive | インダクティブ | 型の定義 |
| Check | チェック | 要素から型を探す。 |
| Search | サーチ | 型から要素を探す。 |
| Eval | イーバル | 簡約 |
| Proof | プルーフ | 証明を開始する |
型
| 英語 | 読み | 意味 |
| Type | タイプ | 型 |
| Prop | プロップ | 命題 |
| Set | セット | 集合 |
| nat | ナット | 自然数 |
用語
| 英語 | 読み | 意味 |
| CoqIDE | コックアイディーイー | Coq用の統合開発環境 |
| Proof General | プルーフジェネラル | emacs用の開発環境 |
| coqtop | コックトップ | コマンドラインからのREPL |
| tactic | タクティク | proof-editing modeで使えるコマンド。証明を進める関数を探す為の関数かな？ |
| Proof | プルーフ | 証明 |
| Sort | ソート | 型の型 Type,Prop,Set |
| forall | フォアオール | 任意の,∀ |
| -> | ⇒ | ならば |
| proof-editing mode | プルーフエディッティングモード | 証明編集モード |
| subgoal | サブゴール | 証明における現在の結論 |
タクティク(tactic)
| 英語 | 読み | 意味 |
| intros | イントロス | 現在のサブゴールに対して、サブゴールが "forall A, B" なら仮定に A を入れてサブゴールを B に、サブゴールが "A -> B" なら仮定に "H : A" を入れてサブゴールを B に変える |
| apply | アプライ | apply HでサブゴールにHを適用する |
| Qed | キューイーディー | Quit Editing modeの略 |
| intro | イントロ | サブゴールが "forall P : 〜" の形なら P を仮定に移し、サブゴールが "A -> B" のときは A を仮定に移する |
| unfold | アンフォルド | unfold の後に書いた名前の関数を展開する |
| right | ライト | サブゴール(型)が二つ型構成子を持っているとき、二つ目の型構成子を適用する |
| left | レフト | サブゴール(型)が二つ型構成子を持っているとき、一つ目の型構成子を適用する |
| case | ケース | 場合分け |
| destruct | デストラクト | destruct H はまず case と同じはたらきをし、その後仮定にある H を消してから intro する |
| split | スプリット | サブゴール(型)が1つの型構成子をもっているとき型構成子を適用する |
| auto | オート | 自動的に証明する |
| tauto | ティーオート | autoより強力な自動証明 |
| induction x | - | x について帰納法で証明を進める |
| simpl | - | サブゴールを簡約する |
| reflexivity | - | サブゴールが等式の形で、両辺の値が等しいとき |
| f_equal | - | apply (f_equal x) のようなもの、x は省略できる |
| rewrite x | - | x の型が "forall 〜, a = b" のとき、サブゴールの a を b で書き換える |
| rewrite <- x | - | x の型が "forall 〜, a = b" のとき、サブゴールの b を a で書き換える |
以下、今日やってみたソースです。
Definition plus (n : nat)(m : nat) : nat := n + m. Definition plus1 (n m : nat) : nat := n + m. Definition plus2 n m := n + m. Definition add a b := a + b. Definition plus' : nat -> nat -> nat := fun n m => n + m. Definition id (A:Type)(a:A) := a. Definition id' : forall(A:Type), A -> A := fun A x => x. Definition prop0: forall(A: Prop), A -> A := fun A x => x. Definition p0 : forall(A: Prop), A -> A := fun A x => x. (* 命題1. 任意の命題 A B C に対して、 「B ならば C」ならば「A ならば B」ならば 「A ならば C」。*) Definition p2: forall(A B C: Prop), (B->C)->(A->B)->A->C := fun A B C b a x => (b (a x)). (*Definition prop3: forall(A : Type)(l1 l2 l3: list A), app l1 l3 = app l2 l3 -> l1 = l2. *) (* 問0. 任意の命題 A B に対して、 A ならば 「A ならば B」ならば Bが成り立つ。*) Definition prop4: forall(A B:Prop), A->(A->B)->B := fun A B a f => f a. (*問1. 任意の命題 A B C に対して、 「A ならば B ならば C」ならば「B ならば A ならば C」が成り立つ。 *) Definition prop5: forall(A B C:Prop), (A->B->C)->B->A->C := fun A B C f b a => f a b. (* Definition prop6: forall (P Q : Prop), (forall P : Prop, ((P -> Q) -> Q)) -> ((P -> Q) -> P) -> P := *) Goal forall (A : Prop), A -> A. Proof. intros. apply H. Qed. Theorem prop7 : forall (A : Prop), A -> A. Proof. intros. apply H. Qed. Lemma prop8 : forall (A : Prop), A -> A. Proof. intros. apply H. Qed. Example prop9 : forall (A : Prop), A -> A. Proof. intros. apply H. Qed. Example prop10 : forall (A : Prop), A -> A := fun A x => x. Goal forall (A : Prop), A -> A. Proof. intros. apply H. Qed. Goal forall (P Q : Prop), (forall P : Prop, (P -> Q) -> Q) -> ((P -> Q) -> P) -> P. Proof. intros. apply H0. intro. apply (H (P->Q)). apply (H P). Qed. Goal forall (P Q R : Prop), (P -> Q) -> (Q -> R) -> P -> R. Proof. intros. apply H0. apply H. apply H1. Qed. Inductive list (A : Type) : Type := | nil : list A | cons : A -> list A -> list A. (* Inductive False : Prop :=. Definition not (A : Prop) := A -> False. *) Goal forall P : Prop, P -> ~~P. Proof. intros. intro. apply H0. apply H. Qed. Goal forall P : Prop, P-> ~~P. unfold not. intros. apply H0. apply H. Qed. Goal forall (P Q : Prop), P \/ Q -> Q \/ P. Proof. intros. case H. apply or_intror. apply or_introl. Qed. Goal forall (P Q : Prop), P \/ Q -> Q \/ P. intros. destruct H. right. apply H. left. apply H. Qed. Goal forall (P Q : Prop), P /\ Q -> Q /\ P. Proof. intros. destruct H. apply conj. apply H0. apply H. Qed. Goal forall (P Q : Prop), P /\ Q -> Q /\ P. Proof. intros. destruct H. split. apply H0. apply H. Qed. Goal forall (P : Prop), P -> ~~P. info_auto. Qed. Goal forall (P : Prop), ~(P /\ ~P). Proof. intros. intro. apply H. destruct H. apply H. Qed. Goal forall (P Q : Prop), ~P \/ ~Q -> ~(P /\ Q). Proof. intros. intro. destruct H. apply H. apply H0. apply H. apply H0. Qed. Goal forall (P : Prop), (forall (P : Prop), ~~P -> P) -> P \/ ~P. Proof. intro. intro. apply H. intro. apply H0. left. apply H. intro. apply H0. right. apply H1. Qed. (* Fixpoint app (A : Type)(l l' : list A) : list A := match l with | nil => l' | cons x xs => cons A x (app A xs l') end. *) Open Scope list_scope. Fixpoint app2 (A : Type)(l l' : list A) : list A := match l with | nil => l' | cons x xs => cons A x (app2 A xs l') end. Close Scope list_scope.
