August 2017 M T W T F S S « Jan 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31
Category Archives: Coq
Coq provides many tactics. In this post we show a number of proofs that use different tactics to prove a simple proposition of first order logic, namely which in Coq translates to forall P Q : Prop, P /\ Q … Continue reading
One of the strong points of Coq is its powerful proof automation facility embodied in the tactic language . Instead of having to write new tactics in ML, compiling them, and jumping through all sorts of hoops in the process, … Continue reading
The Maybe monad is pretty useful whenever you’re dealing with partial functions, especially in a language like Coq (or rather Gallina if you want to be exact) which requires all functions to be total.
A test case for Coq syntax highlighting in GeSHi (for the WP-Syntax plugin). Inductive nat : Set := | O : nat | S : nat -> nat. Inductive fin : nat -> Type := | FO : forall … Continue reading