0
$\begingroup$

I installed zenon (opam package, github) and tried to use it to generate a Coq proof.

I couldn't find any documentation for the Zenon's main syntax, so I looked at its test suite.

I grabbed this test out of its test suite.

$sig P ("nat") "Prop"
$sig Q ("nat") "Prop"

$hyp "h1" (A. ((x "nat") (P x)))
$hyp "h2" (A. ((x "nat") (Q x)))
$goal (-. (\/ (A. ((x "nat") (-. (Q x)))) (A. ((x "nat") (-. (P x))))))

zenon -ocoq test01.znn produces the following output.

(* PROOF-FOUND *)                                            
(* BEGIN-PROOF *)
Theorem zenon_thm : (~((forall x : nat, (~(Q x)))\/(forall x : nat, (~(P x))))).
Proof.
apply NNPP. intro zenon_G.
apply zenon_G. zenon_intro zenon_H3.
apply (zenon_or_s _ _ zenon_H3); [ zenon_intro zenon_H5 | zenon_intro zenon_H4 ].
generalize (h2 O). zenon_intro zenon_H6.
generalize (zenon_H5 O). zenon_intro zenon_H7.
exact (zenon_H7 zenon_H6).
generalize (h1 O). zenon_intro zenon_H8.
generalize (zenon_H4 O). zenon_intro zenon_H9.
exact (zenon_H9 zenon_H8).
Qed.
(* END-PROOF *)

I wrote the above to test01.v and tried to compile that into a .vo file.

coqc test01.v
File "./test01.v", line 3, characters 43-44:
Error: The reference Q was not found in the current environment.

I'm not sure how to fix this. P and Q are both defined in the znn file.

Here are the versions of Coq and Zenon involved:

zenon -v
zenon version 0.8.5 [a270] 2020-10-23
coqc -v
The Coq Proof Assistant, version 8.16.1
compiled with OCaml 4.11.1
$\endgroup$

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.