CIS 500: Course Homepage
Tuesday/Thursday: 1:45 - 3:15, ANNS 111 Instructor Benjamin Pierce bcpierce AT cis.upenn.edu Office: Levine 562 Office hours: Mondays 2:00 - 4:00 ET Teaching Assistants Lef Ioannidis elefthei AT seas.upenn.edu Office hours: Monday and Wednesday from noon to 2PM in Levine 5th floor bump space (near elevators) Text The main texts for the course are the online books Logical Foundations and Programmin
Coq Tips
以下、Parameters A B C P Q R : Prop. を仮定。 目次 前件 (仮定) が……の場合 仮定が False の場合・仮定に矛盾がある場合 仮定が否定の場合 (~A の形) 仮定が含意の場合 (A -> B の形) 仮定が連言の場合 (A /\ B の形) 仮定が選言の場合 (A \/ B の形) 仮定が全称量化子 (forall) の場合 仮定が存在量化子 (exists) の場合 後件 (ゴール) が……の場合 ゴールが True の場合 ゴールが False・否定の場合 ゴールが含意の場合 (A -> B の形) ゴールが連言の場合 (A /\ B の形) ゴールが選言の場合 (A \/ B の形) ゴールが全称量化子 (forall) の場合 ゴールが存在量化子 (exists) の場合 ゴールが恒真命題 (トートロジー)
Coq/tactics - PukiWiki
tactic とは † Coqでの証明はtacticと呼ばれるコマンドを並べて次々に実行ことによって行われる。 このtacticの語彙が多いほど証明の記述は楽になる。 しかし、語彙を増やすようなドキュメントはオンラインに見つからないので、書きやすいところから書いてみる。 ↑ exact term † 「exact」は最もプリミティブなtacticで、現在のゴールの証明を直接記述する。 直接記述する形式は Print コマンドを使えば知ることができる。 Variables A B C:Prop. Lemma ex1: (A->B->C)->(A->B)->A->C. auto. Qed. このように簡単な定理を証明したとして、証明の内容を Print コマンドを使って表示すると Print ex1. ex1 = fun (H : A -> B -> C) (H0 : A -> B) (H1
ホワット・ア・ワンダフル・ワールド The Coq Proof Assistant A Tutorial (5) 自然演繹法 II
前回は自然演繹法についてちょっと書いただけで終ってしまったのですが，今回はちゃんと Coq を使います (笑) とりあえず，Coq のコマンドと，自然演繹法の推論規則の対応を押さえておきましょう． → 導入 intro H. → 除去 generalize (H1 H2); intro H3. ∧ 導入 split ∧ 除去 elim H; intros H1 H2. ∨ 導入の左側 left. ∨ 導入の右側 right. ∨ 除去 elim H; [intro H1 | intro H2]. ¬ 導入 intro H. ¬ 除去 absurd A; try assumption. とか contradiction. らしい．まだよくわかりません． 後ろ向き推論 apply とりあえず，対応表にそって，テキトーに証明を行ってみましょう． 例題は，チュートリアルの通りに，A ∧ B → B
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
