-
Notifications
You must be signed in to change notification settings - Fork 220
Language Coq
Beta
8.9.0
None - the solution passes the Kata as long as it successfully compiles and all Print Assumptions commands in the Submit tests output Closed under the global context. Note that you are not allowed to assume any axioms, even commonly used ones such as "excluded middle" or "functional extensionality". This is a compromise that the Codewars community has agreed on in order to facilitate fully automated testing of Kata solutions.
Kata Example - A + B = B + A? Prove it!
NOTE: This is a hypothetical Coq version of the Kata linked above. Please do NOT submit a Coq translation to that Kata due to the sheer difference in difficulty of solving the same task between Haskell and Coq.
The following example demonstrates how a Coq Kata is typically set up on Codewars as well as guidelines on how to develop your solution locally.
The preloaded section contains key definitions and notations used in the Kata that the solver is not supposed to edit. It may be left empty if all the definitions and/or notations required are already present in the Coq standard library or one of the supported packages (see the "Packages" section for a list of supported packages). In our case of "A + B = B + A? Prove it!", since addition is already defined in the standard library, there is no need to fill anything in in the Preloaded section.
Kata authors should ensure that the code for the Preloaded section is displayed in full within the Kata Description. Solvers can then copy the Preloaded code from the Kata description into a file named Preloaded.v on their local machine.
Kata authors should always include Require Import Preloaded as the first line of the Initial Solution, followed by any theorems that the solver is expected to complete with the proofs replaced by admit and Admitted in place of Qed:
Require Import Preloaded.
Theorem addition_is_commutative : forall n m : nat, n + m = m + n.
Proof.
admit.
Admitted.Solvers may wish to copy the Initial Solution into a file named Solution.v on their local machine in order to develop their solution locally.
The Sample and Submit Tests for a typical Coq Kata should be identical unless doing so spoils the solution to the Kata (e.g. in Playing with opacity which leverages random testing in the Submit tests). The first two lines of the testing file should always be, in the exact order displayed below:
Require Solution.
Require Import Preloaded.Any other test setup may expose vulnerabilities such as allowing the solver to cheat by redefining the definitions/notations initially defined in the Preloaded section. If you see a Coq Kata which does not follow this setup then it is a Kata issue and you may safely raise an Issue in the Kata discourse (by leaving a comment and labelling your comment with the "Issue" tag).
Below the first two lines shown above, additional Requires/Require Imports may be added as required, followed by one "testing theorem" per theorem that the solver is expected to complete. The statement of the "testing theorem" must be identical to that that the solver is expected to complete, and its proof body should be exactly exact Solution.<INSERT_THEOREM_NAME_HERE>., ending in Qed. Each such "testing theorem" should then be accompanied by a Print Assumptions command printing out its assumptions:
(* Tests.v for "A + B = B + A? Prove it!" - The full test suite *)
Require Solution.
Require Import Preloaded.
(* "Testing theorem" *)
Theorem addition_is_commutative_test : forall n m : nat, n + m = m + n.
Proof. exact Solution.addition_is_commutative. Qed.
(* ... followed by [Print Assumptions] *)
Print Assumptions addition_is_commutative_test.To test your solution locally, solvers may wish to copy the testing code into a file Tests.v on their local machine and compile it along with Preloaded.v and Solution.v. A correct solution should only see one or more lines of Closed under the global context printed to the console.
12 seconds
None