…です。一般の形では Coq で証明できませんが、P : bool -> bool にしてあるので証明できます。 P のありうる値は 4 通りあります（厳密には外延的に等価なものを除いて 4 通りですが、この問題では気にしなくていいです）。P true = true かつ P false = false のときは a = false であればよく、それ以外のときは a = true であればよいです。 あとは場合分けをするだけですが、単純に destruct (P true) …

…ない話です．挙動は Coq 8.5pl2 で確認しました．他のバージョンでどうかは調べていません．Set Implicit Arguments してから，なんか依存型を定義します． Coq < Set Implicit Arguments. Coq < Inductive Fin : nat -> Set := | F0 n : Fin (S n) | FS n : Fin n -> Fin (S n). Coq < Coq < Fin is defined Fin_rect…

先日 Coq 8.5 がリリースされたので入れてみた話。coq 自体のコンパイルは問題なくできたけど，その後 ssreflect のコンパイルに失敗した。make すると Error: The files /usr/local/lib/coq/parsing/pcoq.cmi and /usr/local/lib/coq/lib/compat.cmi make inconsistent assumptions over interface Compatと言われる。問題の co…

…ます。今日ちょっと coq-smie-indent.el などを見てみたら，by のインデントの調整くらいはすぐにできそうな気がしたのでやってみました。 (defadvice coq-smie-rules (around ssr-by-tactical (kind token) activate) (if (and (eq kind :before) (equal token "by") (save-excursion (skip-chars-backward "\t\n\r…

Coq の証明を書くときに，ただ tactics を一列に並べて書くと，まったく読めなかったり Coq のバージョンが上がって証明が通らなくなったときにどこでこけてるのかわからなくなったりして不都合なので，証明の構造を proof script のテキスト上にも反映させましょうという話はたぶん昔からあって，昔はインデントとかでそれをやっていたのですが最近は Coq の側でそういうことをサポートするための仕組みが入りました。具体的には bullet と brace ですが，その…

http://lkozima.hatenablog.com/entry/2014/09/15/013735 の続き。ホーア論理の健全性の証明をやろうとしていたのでした。一箇所ちょっと難しいところがあるような気がしたのでそれについて書こうとしていたのですが，あれこれ調べているうちに簡単な解決策があることに気付いたうえに，それで解決してしまうとあんまり an exercise in dependent types になりませんでした。困った。でも簡単な方法があることがわかっている…

…ーア論理の拡張）を Coq で書いてみたらどうだろうかということを少し思いつつも，あんまり時間がないし単に頑張ったらできましたというだけでは誰も興味を持たないだろうということで手をつけずにいました。ところが先日ちょっと真面目に考えてみたところ，上記と同様の問題が発生するようだ（あるいはもしかしたらもっと深刻かもしれない）ということがすぐにわかりました。同様のといっても手続き型言語のホーア論理なので変数の束縛はないのですが，新しい変数を作るという操作が必要な箇所があるので，たぶ…

…とみなして を と書きます。 をで定めます。このとき losing は F の最小不動点です。なのでこの述語に対する帰納法の原理は「F の prefixed-point は losing に含まれる」つまりになります。これはもうちょっと強めることができてともできます。ここで F の定義を展開すると，上に coq で書いた帰納法の原理が出てきます。長いので帰納法の仮定のところだけ書くととなります。forall m : nat, ... の部分に対応していることがわかるでしょう。

…中では思うのですが，coq 上でやろうとするとうまくいかない。*1どううまくいかないかというと， Coq < Goal forall n, losing n -> exists m, n = 4 * m. 1 subgoal ============================ forall n : nat, losing n -> exists m : nat, n = 4 * m Unnamed_thm < induction 1. 1 subgoal x : nat…

久しぶりに Coq を触っててしばらくはまった話。とりあえず準備。 Require Import Program. Set Implicit Arguments. Inductive fin : nat -> Set := | First : forall n, fin (S n) | Next : forall n, fin n -> fin (S n).fin n はサイズ n の有限集合の型みたいなのです。手っ取り早く例を作るために cpdt から拾ってきました。で，こ…

…ています。今回のは Coq'Art にも似たような例が書いてあった気がしますが。 問題設定 Z -> Z な関数 f と，Z -> Prop な述語(「よい」整数の定義)が与えられます。 0 書けたら，sum の値は証明の中身には依存しないはずなので，それを証明しましょう。 あなぷるの JMO2011-3 (http://as305.dyndns.org/aps/problem/view/46) やってて出てきたものを少し変形した問題を考えます。関数の定義域が nat だと帰…

Coq のモジュールシステムについて，使い方がいまいちつかめてない気がしたので stdlib でどう使われてるのか見てみました。はじめに，モジュールとはどういうものかを一応言語化してみる。Coq の module はまあいわゆる module だと思っていればよいと思うのですが，そうすると module type は module の仕様を書いたものです。その型をもつ module が仕様の実装ということになります。別の module に依存した module のことを fu…

…る例を作りました。 Coq < Section dep_test. Coq < Variables A B : Set. A is assumed B is assumed Coq < Variables (g : A -> B) (P : B -> Prop) (T : Type) (Q : T -> Prop) (b : forall x, P (g x) -> T). g is assumed P is assumed T is assumed Q is assumed…

…elim の続きで，Coq'Art 15 章に載っている方針による別証明について。なぜそっちはうまくいくのか。ちなみにここに書くことが Coq'Art にきちんと解説されていたかどうかは覚えていませんが，こういうことを細かく解説したものを読んだ記憶がないので触れていなかったのかもしれません。とりあえず定義を再掲。 Definition pred_partial : forall n, n <> 0 -> nat. intro n; case n. intro h; elim …

…てみます。例として Coq'Art の chapter 10 にあるものを取り上げてみます。web から拾ってきた仏語版だと 10.2.4 節，289 ページから 290 ページにかけて書いてあります。先に必要な定義をしておきます。 Definition pred_partial : forall n, n <> 0 -> nat. intro n; case n. intro h; elim h; reflexivity. intros p ?; exact p. Defi…

Coq.Sets.Ensembles がなんだかうまく使えないなあ，と思った話。ちなみに以下で使う諸定義は http://coq.inria.fr/stdlib/Coq.Sets.Ensembles.html を必要に応じて参照してください。具体的には何かというと， Coq < Goal forall x : A, forall X : Ensemble A, In _ (Add _ X x) x. 1 subgoal ============================…

…かやってみました。 Coq < Goal forall A (xs ys zs : list A), xs ++ ys ++ zs = (xs ++ ys) ++ zs. 1 subgoal ============================ forall (A : Type) (xs ys zs : list A), xs ++ ys ++ zs = (xs ++ ys) ++ zs Unnamed_thm2 < induction xs. 2 subgoals A …

…end の結合性。 Coq < Goal forall A (xs ys zs : list A), xs ++ ys ++ zs = (xs ++ ys) ++ zs. 1 subgoal ============================ forall (A : Type) (xs ys zs : list A), xs ++ ys ++ zs = (xs ++ ys) ++ zs induction をするに決まっている。 Unnamed_thm0 < induc…

…でやってみました。 Coq < Goal forall n, n = 0 \/ 1 <= n. 1 subgoal ============================ forall n : nat, n = 0 \/ 1 <= n こんなのを証明してみましょう。帰納法に決まってるので帰納法を使います。 Unnamed_thm < induction n. 2 subgoals ============================ 0 = 0 \/ 1 <= 0 su…

…月の終わりごろから Coq で遊んでいます。あまり自明でないこともだんだんできるようになってきた気がしますが，なにかがわかるようになってくるということとなにかがわからないと気付くこととはたいていの場合同時に起こることのようです。tactic が何をやっているのかがよくわからない，ということが最近わかりはじめました。goal を変形すると言うけど，goal とかそれに対する操作は CIC の外にある概念であって，それが CIC の中で書ける proof term とどうつながっ…