また ill-typed term が出てくる例

証明がうまくいかなくて工夫が必要な事例を集めようとしています。今回のは Coq'Art にも似たような例が書いてあった気がしますが。 問題設定 Z -> Z な関数 f と,Z -> Prop な述語(「よい」整数の定義)が与えられます。 0 書けたら,sum の値は証明の中身…

Coq.Arith.MinMax 見てみた

Coq のモジュールシステムについて,使い方がいまいちつかめてない気がしたので stdlib でどう使われてるのか見てみました。はじめに,モジュールとはどういうものかを一応言語化してみる。Coq の module はまあいわゆる module だと思っていればよいと思う…

pattern で ill-typed term が出てくる例

依存型を使っていると destruct が ill-typed term を作って失敗することがあるんですが,その原因が何なのかがよくわからないので似たような現象を起こす小さな例を探しています。pattern でおそらく同様の原因によるものと思われるエラーが出る例を作りま…

maximal induction principle の話

前回のうまくいかない elim の続きで,Coq'Art 15 章に載っている方針による別証明について。なぜそっちはうまくいくのか。ちなみにここに書くことが Coq'Art にきちんと解説されていたかどうかは覚えていませんが,こういうことを細かく解説したものを読ん…

Ltac と proof term 5

tactic が proof term を生成していく様子を何度か観察しましたが,何のためにそんなことをしていたかというと,ときどき tactic が失敗してよくわからないエラーを出すことがあるのでその理由を知りたかったのです。今回はそこに近づこうとしてみます。例と…

auto の話

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

Ltac と proof term 4

append の結合性の別証明。f_equal を使ったらどうなるかやってみました。 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 …

Ltac と proof term 3

今度は等式の証明でやってみました。append の結合性。 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…

Ltac と proof term 2

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

Ltac と proof term

一月の終わりごろから Coq で遊んでいます。あまり自明でないこともだんだんできるようになってきた気がしますが,なにかがわかるようになってくるということとなにかがわからないと気付くこととはたいていの場合同時に起こることのようです。tactic が何を…