同値性を示すためにそれぞれの矢印を示した。論理パズルみたいな問題だが、¬を扱ういい練習問題だと思う。 Lemma p10_left : (forall A, ~~A -> A) -> (forall A B, (~B -> ~A) -> (A -> B)). Proof. intros. apply H. intro. elim (H0 H2). apply H1. Qed. …

まずAかBかで場合を分けて、Aのときは¬AかCかで場合分けすればできる。Aと¬Aが同時に成り立つとなんでも証明できてしまうということを利用しよう。排中律は別に必要なく証明できる。 Proposition p09 : forall A B C, (A \/ B) /\ (~A \/ C) -> B \/ C. Proo…

以前Merge Sort を実装して証明した。 http://d.hatena.ne.jp/yoshihiro503/20090923ソースコード全体は以下。 http://bitbucket.org/yoshihiro503/mergesort/

http://d.hatena.ne.jp/yoshihiro503/20090708 で証明した。

リストのappendの結合則は非常に便利だが、証明は簡単だ。こういった性質はテストでは網羅的にチェックできないため、証明という検証方法がプログラムの品質を高める上で非常に有効だと思う。 Require Import List. Proposition p06 : forall {A} (l1 l2 l3:…

中間値の定理もCoqの標準ライブラリに存在する。Rsqrt_def.vの中にIVTという名前で見つけることができる。 Lemma IVT : forall (f:R -> R) (x y:R), continuity f -> x < y -> f x < 0 -> 0 < f y -> { z:R | x <= z <= y /\ f z = 0 }. ただ、中間値が f x …

Bolzano Weierstrass の定理はCoqではもう既に証明されていて、しかもそれは標準ライブラリに備わっている！ Rtopology.vというライブラリのソースを見ればこの定理を見つけることができる。 Theorem Bolzano_Weierstrass : forall (un:nat -> R) (X:R -> Pr…

Coqでの実数は9つの項と17の公理で定義されている。項の型と意味はだいたい次の様な感じ。 Parameter R : Set. (* 実数全体 *) Parameter R0 : R. (* 実数の0 *) Parameter R1 : R. (* 実数の1 *) Parameter Rplus : R -> R -> R. (* 実数上での足し算 *) Pa…

この問題はCoqの自然数ライブラリを使った。まずを計算するsum関数を定義した。 Require Import Arith. Fixpoint sum n := match n with | O => O | S n => S n + sum n end. 自然数では割り算が難しいので、全体に2を掛けた次の形をまず証明する。 Lemma p0…

自然数の様々な性質は既にCoqの標準ライブラリに豊富に揃っているが、これらの性質は非常にベーシックなので、一から定義して証明してみた。以下はCoqのArithライブラリも特別なタクティックも使わずに実装した。まず、自然数全体の型 nat を定義する。 Indu…

Proof Party に行けないけど、参加してるつもりで問題に挑戦してみた。今日は名古屋で一人証明パーティ。パズルと応用問題は解いていない。東京は遠いので、Proof Partyの次回がもしあれば 名古屋か関西で開催していただければありがたいです。> ranhaさん