Category Archives: Coq

Several ways to prove a simple proposition

Posted on 2011/02/17 by Thomas Strathmann

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 →

Posted in Coq | Tagged | Leave a comment

Beginning Ltac

Posted on 2011/02/10 by Thomas Strathmann

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 →

Posted in Coq | Tagged | Leave a comment

The Maybe monad in Coq

Posted on 2011/01/25 by Thomas Strathmann

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.

Posted in Coq, Haskell | Tagged | 8 Comments

Coq Syntax Highlighting Test

Posted on 2011/01/24 by Thomas Strathmann

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 →

Posted in Coq, Tools | Tagged , , | Leave a comment

Partiality is an effect

Posted on 2011/01/24 by Thomas Strathmann

In languages like Coq where all computations must terminate and only total functions are allowed it would still be nice to be able to express non-terminating computations. While searching for solutions other people had come up with I stumbled across … Continue reading →

Posted in Coq | Tagged , , | Leave a comment