Daily Archives: 2011/02/17

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