2007-06-15から1日間の記事一覧
証明モードのときは今までのCoqコマンドに加えて、タクティックというものを使うことができる。 タクティックは必ず小文字で始まり、ドットで終わる。 s intro. A : Prop ======================================= forall B C:Prop, (A->B->C) -> (A->B) -> …
Coqは証明支援系 (Proof Assistant) と呼ばれるシステムで、定理などの証明を構築することができる。 今回はTheoremというCoqコマンドを使ってみる。 このコマンドを使って定理を記述し、宣言することができる。 文法 [Theorem 定理の名前 : 定理の内容.] 最…
ターミナルでcoqtopと入力すると対話型証明支援系Coqが立ち上がる。 さあ、今日からCoqを使ってみよう! /yoshihiro$ coqtop Welcome to Coq 8.0pl3 (Jan 2006) Coq CoqではCoqコマンドというものを使って操作をおこなう。 まず最初にCoqを終了するCoqコマン…