Full Disclosure
mailing list archives
proving _anything_ in the Coq proof assistant (in addition to code execution). ``coqchk'' passes too
From: Georgi Guninski <guninski () guninski com>
Date: Tue, 3 May 2011 13:34:16 +0300
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
rwxrxrx 1 joro joro 10301 20110503 12:53 bLOB
rwrr 1 joro joro 125 20110503 12:53 fib5.v
joro () j:/tmp/test1$ coqc fib5.v
Trivially true. coqchk may pass
joro () j:/tmp/test1$ ls l
total 24
rwxrxrx 1 joro joro 10301 20110503 12:53 bLOB
rwrr 1 joro joro 51 20110503 12:55 fib5.glob
rwrr 1 joro joro 125 20110503 12:53 fib5.v
rw 1 joro joro 812 20110503 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
[1] http://coq.inria.fr/
_______________________________________________
FullDisclosure  We believe in it.
Charter: http://lists.grok.org.uk/fulldisclosurecharter.html
Hosted and sponsored by Secunia  http://secunia.com/
By Date
By Thread
Current thread:
 proving _anything_ in the Coq proof assistant (in addition to code execution). ``coqchk'' passes too Georgi Guninski (May 03)
