⇒
into ⇒
(WTH!8.9.0
is currently the latest.ocaml
& opam
first.coqide
also requires system package gtsourceview
v2.xpacman -Sy gtksourceview2
opam install coq coqide -y
.v
extension yourself–CoqIDE does not do this for you like other editors.Ctrl-End
: plays the script to the endCtrl-Home
: resets the script to its beginningCtrl-Down
: advances the script by a single lineCtrl-Up
: reverse the script by a single lineCtrl-Right
: advances or reverses the script to the cursor's linecompany-coq
and Proof General.For the cheaters Formalizing 100 theorems in Coq
Vernacular
, which manages definitionsTactics
is used to write proofs Gallina
is used to express what you want to proveVernacular Command Reference. Notes on specific commands created as I learn about them below.
Inductive
: is similar to type
in OCaml, but types in Coq are much more expressive than in other languages.Inductive type_name : Set := | Variant1 : element1, | Variant2 : element1.
Definition
: can be used to bind a term to a name.Definition <func_name> (<arg_name> : <arg_type)... : <ret_type> := <func_body>
Definition <func_name> (arg_1_name arg_2_name arg_3_name : <arg_type>) : <ret_type> := <func_body>
Fixpoint
: can be used to define recursive functions. Use it in place of Definition
. Theorem
:Theorem
: Lemma
, Remark
, Corollary
, Proposition
, Example
Theorem <test_name>: [<quantifier>,] <boolean expression>.
forall n:nat
:Theorem n_plus_0 : forall n:nat, 0 + n = n.
Check
: displays the type of an expression.Notation
: Defines a custom operator.Notation "x + y" := (plus x y) (at level 50, left associativity) : nat_scope.
Proof
Begins a proof.Qed
ends a proof.Proof
and Qed
are part of the tactics sub-language.match expr | <pattern1> => <match_item> | <pattern2> => <match_item> end.
match n, m with | O , _ => O | S _ , O => n | S n', S m' => minus n' m' end.
n
is a nat
, then the expression S n
is the same as n + 1
.nat
modeled as a linked list with no item–the value is encoded in the number of links in the list. (This is a *very* weird way to model numbers.)nat
which takes a single argument having type nat
.::
list cons
operatorGoal
: unfold
:Context
: Quantifier
:++
operator seen on this page?Theorem
? i.e. Lemma
, Remark
, Corollary
, Proposition
, Example
?Definition instrDenote (i : instr) (s : stack) : option stack := match i with | iConst n => Some (n :: s) | iBinop b => match s with | arg1 :: arg2 :: s' => Some ((binopDenote b) arg1 arg2 :: s') | _ => None end end.