coqグループ

ProofCafe

■ ProofCafe has moved ProofCafe勉強会のWikiは移動しました。こちらをご覧ください。 ProofCafe - Front Page 以下は昔のProofCafeに関する情報です。 ProofCafe(栄)とは CPDTを読...

SSReflectCheatSheet

SSReflect CheatSheet 移転中 => http://kikwiki.wikkii.com/wiki/SSReflect_CheatSheet ここから下は古い ■ Import Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq. Require Import paths choice fintype tuple...

Coqチラシの裏

CoqCheatSheetを補完するとも思えない。 前提が H : A /\ B refine (and_ind _ H). , refine (match H with conj H0 H1 => _ end). H : A \/ B refine (or_ind _ _ H). , refine (match H with or_introl H0 => _ | o...

clear

不要な前提を消去するタクティック。不要な前提が多すぎてごちゃごちゃしすぎる場合に見た目をすっきりさせることができる。ただし不要じゃない前提を消してしまった場合は証明...

はじめの一歩

■ coqの起動 [#he48700c] 対話環境を使う -> Terminalでcoqtopコマンドを実行 emacsで使う -> ProofGeneral 特別な開発環境を使う -> coqide ■ 操作方法 [#p168315c] 概要:...

リンク集

ツール Coq本体 Proof General 日本語 Coq CheatSheet Coq クィックリファレンス ホワット・ア・ワンダフル・ワールド 1 2 3 4 5 6 7 8 9 10 11 12 はじめ...

CoqCheatSheet

目次 [Coq][CheatSheet]Coq CheatSheet 前提が ゴールが ■ [Coq][CheatSheet]Coq CheatSheet Coq Tipsを補完する形で。 前提が A /\ Bdestruct?, decompose[and], elim A \/ Bdestruct?, decompose[or],elim ~Pel...

right

Coq < Goal B -> A \/ B. 1 subgoal ============================ B -> A \/ B Unnamed_thm4 < intro. 1 subgoal H : B ============================ A \/ B Unnamed_thm4 < right. 1 subgoal H : B ===============...

left

Coq < Goal A -> A \/ B. 1 subgoal ============================ A -> A \/ B Unnamed_thm4 < intro. 1 subgoal H : A ============================ A \/ B Unnamed_thm4 < left. 1 subgoal H : A ================...

rewrite

Coq < Goal forall x, x = 1 -> 2 = 1 + x. 1 subgoal ============================ forall x : nat, x = 1 -> 2 = 1 + x Unnamed_thm3 < intros. 1 subgoal x : nat H : x = 1 ============================ 2 = 1 + x Unnamed_thm...