Category Archives: Coq

Several ways to prove a simple proposition

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

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

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

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

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