11/27 に、Coq Partyに参加してきました。 資料などはこちら。 エンジニア・ミーツ・Coq すぐ分かる形式手法 形式手法とは？ 品質の高いソフトウェアを作るための科学的な仕様記述・検証手法 仕様化の正しさは終盤のシステムテストまで分からない 結合テスト…

10/9に名古屋Hackathon - ラムダ村に参加しました。 自分は Coq 組で参加。Coq to Scala をやってた。 Coq 組の朝は遅い。にわとりなのに。 環境構築に時間かかってた。make 長い・・・ 最初は Scheme や Haskell のを修正していく感じだったけど、読むだけ…

Require Import List. Theorem sum_10_eq_55 : fold_left (fun y x => y + x) (seq 1 10) 0 = 55. Proof. reflexivity. Qed.ぅゎ、reflexivity っぉぃ。

Coq で練習してたファイルたちを github で管理。 rf0444's coq

Coqりさん 証明のかけら の続き (再挑戦)。 Require Import Arith. Fixpoint fib1 n:nat := match n with | 0 => 0 | 1 => 1 | S (S m as p) => fib1 p + fib1 m end. Fixpoint fib2 n a b:nat := match n with | 0 => a | S n => fib2 n b (a + b) end. Lem…

K I = F と、S K K = I を証明してみる。 Definition I {A:Type} x:A := x. Definition K {A B:Type} (x:A) (y:B) := x. Definition F {A B:Type} (x:A) (y:B) := y. Definition S {A B C:Type} (x:A->B->C) (y:A->B) (z:A) := x z (y z). Theorem ki_f : fo…

自分の Coq メモを晒してみる。 ■ ; について T1 ; T2 T1 適用後、T1 によって出来た全てのサブゴールに対して T2 を適用 T1 ; [T2 | T3] T1 適用後、T1 によって出来たサブゴール a, b に対して、a に T2、b に T3 を適用 (不要なら T2, T3 を省略可(何もし…

8/29 に、Coq庵 に行ってきました。 資料等はこちら。 行き道で祭りやってた。 一部道が通れなかったりして、少し迷うなど。 初めてのCoq 仕様記述言語 Prolog ACL2, HOL/Light 完全自動証明 自動で証明してくれるが、表現力がやや低い Isabelle/HOL, Coq, A…

楚人に盾と矛とを鬻（ひさ）ぐ者有り。之（これ）を誉めて（ほめて）曰く「吾が盾の堅きこと、能く（よく）陥す（とほす）もの莫し（なし）」と。また、その矛をほめていはく、「わが矛の利なること、物において陥（とほ）さざることなきなり。」と。あるひ…

Coq りさん Coq りさん、フィボナッチ数列の末尾再帰にしたやつって、本当に元のと同じなんですか？ Fixpoint fib1 (n : nat) : nat := match n with | 0 => 0 | 1 => 1 | S n => fib1 n + fib1 (pred n) end. Fixpoint fib2 (a b n : nat) : nat := match n…

∃a∀b[P(a, b)] → ∀b∃a[P(a, b)] Lemma exists_forall : forall (A:Type)(P: A -> A -> Prop), (exists a:A, forall b:A, P a b) -> (forall b:A, exists a:A, P a b). Proof. intros A P H1 a. elim H1. intros x H2. exists x. apply H2. Qed.

4/25に、Proof Cafe (栄)に参加してきました。 Coq 初体験。 最初は、id:yoshihiro503 さんから資料に沿って Coq の解説が。 Vernacular が分かれば Coq が分かる？ Coq のファイルの拡張子は .v Checkで 型を調べる。 ガリナ(Gallina)：ラムダ式 nat : 型を…