■

ここ「ひとり勉強会」は、会と言いつつひとりで勉強した記録を残してます。
Coq の解説記事を書くために勉強しています。

• (1): forall A B: Prop, (A->B) -> A -> B.
  • CoqIDEのつかいかた。forall と -> の証明。
• (2): forall A B: Prop, ~(A ∨ B) -> (~A ∧ ~B).
  • and と or と not の証明。Inductive な命題。
• (3): forall n: nat, exists m, (n=2*m ∨ n=2*m+1).
  • 自然数やリスト。再帰的 Inductive なデータ。= と 帰納法 と exists の証明。omega, ring, field による自動証明。標準ライブラリの使い方。
• (4): 解説テキストリンク集
• (番外編): VSTTE 2012 Software Verification Competition

つづく...