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

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 …

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

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

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