proving anything in the Coq proof assistant (in addition to code execution). “coqchk” passes too
if some poor soul needs help with a coq [1] homework, this may help.
if some poor AV vendor need a proof his solution is bullet proof this may help too…
joro@j:/tmp/test1$ tar xvf ../proof.tar fib5.v bLOB joro@j:/tmp/test1$ ls -l total 16 -rwxr-xr-x 1 joro joro 10301 2011-05-03 12:53 bLOB -rw-r--r-- 1 joro joro 125 2011-05-03 12:53 fib5.v joro@j:/tmp/test1$ coqc fib5.v Trivially true. coqchk may pass joro@j:/tmp/test1$ ls -l total 24 -rwxr-xr-x 1 joro joro 10301 2011-05-03 12:53 bLOB -rw-r--r-- 1 joro joro 51 2011-05-03 12:55 fib5.glob -rw-r--r-- 1 joro joro 125 2011-05-03 12:53 fib5.v -rw------- 1 joro joro 812 2011-05-03 12:55 fib5.vo joro@j:/tmp/test1$ coqchk fib5 Welcome to Chicken 8.2pl1 (February 2010) [intern /tmp/test1/fib5.vo ... done] ...snip... Checking library: fib5 *** vo structure validated *** checking cst: <>.fib5.thm1 checking cst: <>.fib5.really Modules were successfully checked joro@j:/tmp/test1$ tail fib5.v Theorem really: True = False. Proof. intuition. Qed. joro@j:/tmp/test1$ coqchk -v The Coq Proof Checker, version 8.2pl1 (February 2010) compiled on Feb 27 2010 16:09:50
to compile the plugin: ocamlopt -o bLOB -shared a.ml
a.ml is at: http://j.ludost.net/blog/misc/a.ml tar with the proof is at: http://j.ludost.net/blog/misc/proof.tar