
Recent Posts
Archives
Categories
January 2020 M T W T F S S « Nov 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 Meta
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
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
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.
Coq Syntax Highlighting Test
A test case for Coq syntax highlighting in GeSHi (for the WPSyntax plugin). Inductive nat : Set :=  O : nat  S : nat > nat. Inductive fin : nat > Type :=  FO : forall … Continue reading
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 nonterminating computations. While searching for solutions other people had come up with I stumbled across … Continue reading