Add Coq

[carlpaten]

Coq is a programming language for dependently-typed programming. While it is popular in certain niches, there are few snippets of idiomatic Coq code across the web. Adding Coq support to Code Wars would help remediate that.

There are tons of Coq exercises available online which could serve as katas, for example in the MIT-licensed Software Foundations.

---

From #720

• Name: Coq
• Website: https://coq.inria.fr
• Language Version: Coq 8.9.0

The following are optional, but will help us add the language:

• Test Frameworks: None - as discussed in Add Agda #719 , we probably need to special-case this language such that successful compilation results in an automatic pass
• How to install: coq/coq/INSTALL. I'll try to see if there is an easier way in the meantime - I personally installed Coq on my Mac using Homebrew (which does all the hard work for you) so I'm not exactly sure how it's done on Linux
• How to compile/run: coqc solution.v to compile the user solution solution.v. AFAIK only 1 file can be compiled at a time so the entire suite (preloaded, solution, test cases) may need 3 separate calls to coqc. There is also coqchk which checks the compiled .v files, e.g. coqchk solution.vo where solution.vo was compiled from coqc solution.v
• Any comments: (e.g., what's interesting about this language) Coq is a dedicated proof assistant which is often used in the industry to prove the correctness of certain programs. Its support for theorem proving far surpasses that of Haskell/Idris so including it on Codewars should open up a huge variety of non-trivial (where "trivial" means toy proofs like A + B = B + A) theorem-proving Kata. Also, unlike Idris, Coq always enforces totality so it shouldn't be possible to subvert proofs using escape hatches like believe_me or assert_total.

👍 reaction might help. Special mentions: @ice1000 , @MarisaKirisame

---

• Install Coq 8.9.0
• Support testing
• Logo for icon
• CodeMirror mode (coq.js from ejgallego/CodeMirror)

[kazk]

If I'm not misunderstanding, Coq is very different kind of language.

Any specific examples of exercises? How can it be tested?
Links to useful resources will help.

---

http://coq.inria.fr/
The mirror of language repository on GitHub: https://github.com/coq/coq

[carlpaten]

Any specific examples of exercises?

There are quite a few here, for example:

A list is a subsequence of another list if all of the elements in the first list occur in the same order in the second list, possibly with some extra elements in between. For example,

 [1;2;3]

is a subsequence of each of the lists

 [1;2;3]
 [1;1;1;2;2;3]
 [1;2;7;3]
 [5;6;1;9;9;2;7;3;8]

but it is not a subsequence of any of the lists

 [1;2]
 [1;3]
 [5;6;2;1;7;3;8].

• Define an inductive proposition subseq on list nat that captures what it means to be a subsequence. (Hint: You'll need three cases.)
• Prove subseq_refl that subsequence is reflexive, that is, any list is a subsequence of itself.
• Prove subseq_app that for any lists l1, l2, and l3, if l1 is a subsequence of l2, then l1 is also a subsequence of l2 ++ l3.
• (Optional, harder) Prove subseq_trans that subsequence is transitive — that is, if l1 is a subsequence of l2 and l2 is a subsequence of l3, then l1 is a subsequence of l3. Hint: choose your induction carefully!

---

How can it be tested?

The Software Foundations book comes with grading scripts that cover some of the exercises. Here is one.

[kazk]

How do you test that submitted solution has valid proof for subseq_refl?
The following has subseq_refl, but shouldn't pass.
(I don't know Coq, only skimmed through some pages of the book.)

(* Define an inductive proposition `subseq` on `list nat` *)
(* Inductive subseq : list nat -> list nat -> Prop := . *)

(* Prove that subsequence is reflexive. Any list is a subsequence of itself. *)
Theorem subseq_refl :
  1 + 1 = 2. (* irrelevant fact *)
Proof.
  reflexivity.
Qed.

---

Supporting something like the following (first exercise from the book) is more straight forward, but less interesting:

(* Define `nandb` which returns `true` if either or both of its inputs are `false`. *)
Inductive bool : Type :=
  | true : bool
  | false : bool.

Definition negb (b:bool) : bool :=
  match b with
  | true => false
  | false => true
  end.

Definition nandb (b1:bool) (b2:bool) : bool :=
  match b1 with
  | true => (negb b2)
  | false => true
  end.

(* compile-time tests? *)
Definition test_nandb1 : (nandb true false) = true :=
  eq_refl.
Definition test_nandb2 : (nandb false false) = true :=
  eq_refl.
Definition test_nandb3 : (nandb false true) = true :=
  eq_refl.
Definition test_nandb4 : (nandb true true) = false :=
  eq_refl.

---

Also, we need to output test results in Codewars' format.

---

• https://packages.ubuntu.com/trusty/coq
• https://github.com/uhub/awesome-coq
• https://github.com/clarus/coq-cunit
• https://github.com/coq-io

[gallais]

The way proofmarket used to do it is use a file specifically for checking which resembles something like this:

Require Import Definitions.
Require Import Solutions.
Theorem subseq_refl_check : (* the exact statement *)
Proof.
exact subseq_refl
Qed.

If the user has changed the type of subseq_refl then the proof for subseq_refl_check won't be valid.

[kazk]

Thanks @gallais :)

(* Solution.v *)
Theorem identity : 1 * 1 = 1.
Proof.
  reflexivity.
Qed.

(* Check.v *)
Theorem identity_check : forall A, A -> A.
Proof.
  exact identity.
Qed.

Error:
The term "identity" has type "1 * 1 = 1" while it is expected to have type
 "forall A : Type, A -> A".

(* Definition.v *)
Definition identity_def := forall A, A -> A.
(*
Error:
The term "identity" has type "1 * 1 = 1" while it is expected to have type
 "identity_def".
*)

[DonaldKellett]

A potential issue I just discovered: in Coq it is possible to defer a proof using tactic admit followed by marking a proof as Admitted instead of the usual Qed:

(* Solution.v *)
Theorem solution : 1 + 1 = 2.
Proof.
  admit.
Admitted.

Even if I then use this admitted "proof" in another proof as follows:

(* TestSuite.v *)
Require Import Solution.
Theorem test_suite : 1 + 1 = 2.
Proof.
  exact solution.
Qed.

... both files can still be successfully compiled using coqc and verified using coqchk. A potential solution could be to search the user solution for keywords "admit"/"Admitted"/etc. and make the existence of these terms a failed test.

[gallais]

verified using coqchk.

Do you really get a 0 exit code? i.e. if you run coqchk file.vo && echo "Success!",
do you get Success! displayed in your terminal?

[DonaldKellett]

Do you really get a 0 exit code? i.e. if you run coqchk file.vo && echo "Success!",
do you get Success! displayed in your terminal?

Yes - copying/pasting the files as-is and executing coqc Solution.v && coqc TestSuite.v && coqchk Solution.vo && coqchk TestSuite.vo && echo "Success" on my Mac prints "Success" at the very end.

[MarisaKirisame]

@DonaldKellett Print Assumptions my_definition.
What happend is, coq make the rest of your goal a Variable (that is not defined, but declared), and 'prove' your goal with that Variable. If you want to search for variable, you also have to eliminate Parameter/Variable/Axiom as they do the same. I think Print Assumptions is the cleaner approach.

[MarisaKirisame]

opam install coq work well for me on linux.

[kazk]

@MarisaKirisame

Also, we need to check if user include additional axiom or not. (Anything could be included as axiom, to circumvent any proving) This is a Coq command but I dont know how to do it externally.
codewars/codewars.com#1234 (comment)

I think I found how to do that. coqchk --output-context shows Axioms.

Using the same example

coqc Solution.v && coqc TestSuite.v && \
  coqchk -silent --output-context TestSuite.vo

CONTEXT SUMMARY
===============

* Theory: Set is predicative
  
* Axioms:
    Solution.solution

The exit code is still zero and I don't think there's a way to make it considered error.

Also found this:

The effect of coqchk is only to return with normal exit code in case of success, and with positive exit code if an error has been found. Error messages are not deemed to help the user understand what is wrong.

https://coq.inria.fr/refman/practical-tools/coq-commands.html#compiled-libraries-checker-coqchk

---

I'll put Coq on hold for now. For theorem proving, we now have Agda (and Idris). I'm pretty happy with how Agda turned out and excited to see it opening up possibilities for new challenges. Agda was easy to work with and it seems to fit Codewars pretty well. I was hoping Coq to be similar, but I have a feeling that it'll be significantly more difficult and I'm honestly not really motivated.

[Zimmi48]

I would say that using coqchk is probably not really needed for this application. Running Print Assumptions test_suite. within TestSuite.v and checking that the output (when running `coqc) is exactly "Closed under the global context" (which means no axiom / admitted) should be sufficient. When doing exercises relying on some allowed axioms (such as excluded middle), the output will be instead the list of axioms and their types and it should be possible as well to verify that this output is exactly the one that was expected.

[DonaldKellett]

Thanks for your input @Zimmi48 , glad to see that this language request for Codewars has attracted the attention of a official Coq maintainer 🎉

With regards to Coq exercises involving customized allowed axioms, there's currently no feasible way to tell the CW runner which axioms are allowed on a kata-to-kata basis since the output testing is not done within Coq itself. Perhaps a suitable tradeoff would be to let a Coq solution pass if and only if the entire suite (preloaded, solution, tests) compiles and the output message from coqc is exactly "Closed under the global context". Obviously, this would limit the range of possible proofs that could be authored as Kata but would open many new possibilities nonetheless.

@kazk What do you think?

[kazk]

I'm fine with that. We might find a better way later too.

Can anyone provide some examples similar to the Agda one (#719 (comment))? I'd like to experiment with some variations and see how the output looks like. More examples will be better.

Also, Coq doesn't have module declaration right? So I guess we'll just have fixed file names like Solution.v, Preloaded.v, Test.v.

[Zimmi48]

I'm not exactly sure how you're planning to use it but Coq does have a module system. Example:

Module Solution.

  Theorem identity : 1 * 1 = 1.
  Proof.
    reflexivity.
  Qed.

End Solution.

Module Check.

  Theorem identity_check : forall A, A -> A.
  Proof.
    Fail exact Solution.identity.
(*
The command has indeed failed with message:
The term "Solution.identity" has type 
"1 * 1 = 1" while it is expected to have type
 "forall A : Type, A -> A".
*)
    Import Solution.
    Fail exact identity.
(*
The command has indeed failed with message:
The term "identity" has type "1 * 1 = 1"
while it is expected to have type
 "forall A : Type, A -> A".
*)

[kazk]

Some updates...

Coq module works little bit different from what I imagined from @Zimmi48's comment.

coqc Solution.v outputs Solution.vo (library?) and this can be loaded from other files using Require Solution. Solution can contain multiple modules. Require Import Solution loads Solution and brings the definitions into scope.
So deciding a filename using Module declaration is weird. I'll probably just have Solution.v, Preloaded.v, and Tests.v.

Only considering passed when the output is exactly "Closed under the global context\n" and treating anything else as failure works, but I'm concerned about the output being a huge wall of text. I'm going to play with it and see if I can do some postprocessing.

---

Software Foundations book OP posted got some updates and it's now a series (maybe it was before, but I don't remember seeing other volumes). The volume 4 is called QuickChick: Property-Based Testing in Coq.

Also, the original book's grading script contains something like

From Coq Require Export String.
Parameter MISSING: Type.

Module Check.
Ltac check_type A B :=
    match type of A with
    | context[MISSING] => idtac "Missing:" A
    | ?T => first [unify T B; idtac "Type: ok" | idtac "Type: wrong - should be (" B ")"]
    end.
End Check.

Maybe we can have our version of something like this? It might help with having a better output.

[Zimmi48]

Sorry about not being fully clear earlier. Files define modules and the filename is the name of the module. Explicit module declarations are only used to define nested modules. The Require command is specific to files while the Import command is generic to all modules. I thought you wanted to define several modules in the same file that's what I was showing.

[kazk]

@Zimmi48 Thanks for clarifying. Also, no need to apologize, I really appreciate your help.

Are the error messages in certain format? If it is, I can do some postprocessing to make it display better on Codewars. I was able to do that for Agda because it has a consistent format using a pretty printer.

So far, I've seen errors like

File "./SolutionTest.v", line 3, characters 8-20:
Error: The reference Foo.plus_n_O was not found in the current environment.

File "./Solution.v", line 3, characters 2-13:
Error: In environment
n : nat
Unable to unify "n + 0" with "n".

written to stderr. It'll be helpful if I can see other possible errors.

---

I think we can do

• PASSED, if stdout is exactly "Closed under the global context\n" and stderr is empty
• FAILED, otherwise. Output anything in stdout as part of a failure message. If anything is written to stderr, split each error message and display each separately.

[Zimmi48]

Coq error messages will just be printed like you saw, with location information and a leading "Error: ". Warnings will be printed with a leading "Warning: ". I can show you the file with the printing business but the error messages themselves are not gathered in a single place like in Agda but all over the code. We have documented many error and warning messages in https://coq.inria.fr/refman/coq-exnindex.html. However, the list is not exhaustive yet, especially regarding warnings.

[Bubbler-4]

For simple type-checking tests, the following code will work:

From Coq Require Export String.

Module test.

Ltac check_type A B :=
    first [(match type of A with
    | ?T => first [unify T B; idtac "<PASSED::>" A ": Type is correct" |
                   idtac "<FAILED::>" A ": Type is wrong - should be (" B ")"]
    end) | idtac "<FAILED::>" A ": Missing definition"]; idtac "".

Theorem one_times_one : 1 * 1 = 1.
Proof. reflexivity. Qed.

Goal True.
check_type one_times_one (1 * 1 = 1).
check_type one_times_one (1 * 2 = 2).
check_type one_times_two (1 * 2 = 2).
Abort.

End test.

Command: coqc source.v && coqchk source.vo -silent -o

Result:

<PASSED::> one_times_one : Type is correct

<FAILED::> one_times_one : Type is wrong - should be ( (1 * 2 = 2) )

<FAILED::> one_times_two : Missing definition


CONTEXT SUMMARY
===============

* Theory: Set is predicative

* Axioms: <none>

We'll need post-processing for context summary part to convert it to a CW pass/fail.

---

For errors, only the first error is displayed when a source file has multiple issues, so I guess "printing a huge wall of text" is not very likely.

From my experience, error/warning messages start with Error: / Warning: and end with a period plus whitespace. I guess we can wrap each of them into an error (+ failed test) / log (or whatever suits better) block.

[kazk]

@Bubbler-4 I like that.
I wrote a version that checks for "Closed under the global context\n" few weeks ago, but haven't made any progress since.

We can have a module with code like check_type maintained by the community to check whatever. Kata "tests" can use that to output Codewars format.

We'll need post-processing for context summary part to convert it to a CW pass/fail.

Can you post some example outputs and what should be considered a failure?

[Bubbler-4]

Can you post some example outputs and what should be considered a failure?

Any global axioms like the following

Parameter one_times_two : 1 * 2 = 2.
Theorem one_times_three : 1 * 3 = 3.
Proof. admit. Admitted.

are shown at the Axioms section like this.

CONTEXT SUMMARY
===============

* Theory: Set is predicative

* Axioms:
    scratch2.test.one_times_two
    scratch2.test.one_times_three

Ending with * Axioms: <none> (as shown in the last post) is a pass, anything else on extra lines is a failure. The other lines, starting from CONTEXT SUMMARY up to Theory: ..., are irrelevant.

[kazk]

@Bubbler-4

coqchk source.vo -silent -o takes a long time.
Looks like it's checking all the libraries.

• coqchk -o source.vo 2>&1 | wc -l (showing processed files) is 34745
• coqchk -o -silent source.vo 2>&1 | wc -l is 7

Is there some kind of caching like Agda? It doesn't seem like it because running the command again produces the same output and takes as long.

[Bubbler-4]

@kazk I couldn't find a way around it either. Then we should go back to Print Assumptions way, and do more post-processing. How about this:

-- source.v
Theorem thm1 : 1 = 1 + 0. Proof. admit. Admitted.
Print Assumptions thm1.

Parameter thm2 : 1 + 0 = 0 + 1.
Print Assumptions thm2.

Theorem thm3 : 1 = 0 + 1. Proof. rewrite <- thm2. exact thm1. Qed.
Print Assumptions thm3.

Theorem thm4 : 1 = 1. Proof. reflexivity. Qed.
Print Assumptions thm4.

-- command: coqc source.v

-- output:
Axioms:
thm1 : 1 = 1 + 0
Axioms:
thm2 : 1 + 0 = 0 + 1
Axioms:
thm2 : 1 + 0 = 0 + 1
thm1 : 1 = 1 + 0
Closed under the global context

Now the problem is how to process it. My idea:

• Convert the exact text Closed under the global context into a pass.
• Convert Axioms: followed by one or more lines of ident : whatever into a failure, but one caveat is that the whatever can be split into several lines like this (from SW Foundations book):

Axioms:
NatList.test_alternate1 : NatList.alternate
                            (NatList.cons 1
                               (NatList.cons 2 (NatList.cons 3 NatList.nil)))
                            (NatList.cons 4
                               (NatList.cons 5 (NatList.cons 6 NatList.nil))) =
                          NatList.cons 1
                            (NatList.cons 4
                               (NatList.cons 2
                                  (NatList.cons 5
                                     (NatList.cons 3
                                        (NatList.cons 6 NatList.nil)))))

This regex will probably work.

[monadius]

It is possible to use the -norec option to make coqchk faster: coqchk -o -norec source.vo. But it is still not ideal: on my machine it takes about 6 seconds.

[kazk]

I think we're almost there.

Errors and warnings written to stderr are wrapped and appended to stdout output. I don't know if we'll ever have multiple errors and warnings at the same time, but it should be supported.

I'm using this pattern to extract. Not trying to perfect this and will adjust as we find edge cases.

[Bubbler-4]

If there's an Error in the output, does the entire test suite fail?

[kazk]

Yeah, coqc also sets the exit code to non zero in that case.

[kazk]

I'm preparing for alpha release and need a super basic (probably not worth making a kata) example.

Can anyone provide a Coq version of #719 (comment)? It doesn't need to be exact. Failing version, working version, and some check.

Solution is written to Solution.v so Require Import Solution. will work (preloaded goes to Preloaded.v). I've also included check_type in Check.v. We can turn this module into a community project if anyone is interested in maintaining and expanding it.

[Bubbler-4]

Here is one (not tested though).

Initial solution:

Theorem ex : 1 * 1 = 1.
Proof. admit. Admitted.

or (this will make the compiler complain about open goal)

Theorem ex : 1 * 1 = 1.
Proof.

Complete solution:

Theorem ex : 1 * 1 = 1.
Proof. reflexivity. Qed.

Test:

Require Import Solution.
Require Import Check.

Goal True.
check_type ex (1 * 1 = 1).
Abort.
Print Assumptions ex.

[DonaldKellett]

Maybe something like this?

Initial Solution (Solution.v):

Theorem eq_trans : forall a b c : Type,
  a = b -> b = c -> a = c.
Proof.
  (* TODO: Prove it *)
Admitted.

Complete Solution (Solution.v):

Theorem eq_trans : forall a b c : Type,
  a = b -> b = c -> a = c.
Proof.
  intros a b c eq1 eq2.
  rewrite -> eq1.
  rewrite -> eq2.
  reflexivity.
Qed.

Test Cases (Check.v):

Add LoadPath "/Users/donaldl/Desktop/".

Require Import Solution.

Theorem eq_trans_test : forall a b c : Type,
  a = b -> b = c -> a = c.
Proof.
  exact eq_trans.
Qed.

Print Assumptions eq_trans_test.

Running coqc Solution.v && coqc Check.v with the initial solution gives

Axioms:
eq_trans : forall a b c : Type, a = b -> b = c -> a = c

And with the final solution:

Closed under the global context

[monadius]

An example with Preloaded.

Preloaded (Preloaded.v):

Definition preloaded_def (n : nat) := n + n.

Initial solution (Solution.v):

Require Import Preloaded.
From Coq Require Import Arith.

Lemma preloaded_lemma (n : nat) : preloaded_def n = n * 2.
Proof. Admitted.

Complete solution (Solution.v):

Require Import Preloaded.
From Coq Require Import Arith.

Lemma preloaded_lemma (n : nat) : preloaded_def n = n * 2.
Proof.
  unfold preloaded_def; rewrite -> mult_comm; simpl.
  rewrite <- plus_n_O; reflexivity.
Qed.

Tests (Test.v):

Require Preloaded.
Require Import Check Solution.

Goal True.
  check_type preloaded_lemma (forall n, Preloaded.preloaded_def n = n * 2).
Abort.

Print Assumptions preloaded_lemma.

Attempt to cheat (Solution.v):

Require Import Preloaded.

Definition preloaded_def (n : nat) := n * 2.

Lemma preloaded_lemma n : preloaded_def n = n * 2.
Proof. reflexivity. Qed.

It fails with the message <FAILED::> preloaded_lemma : Type is wrong - should be ((forall n : nat, Preloaded.preloaded_def n = n * 2) ).

[kazk]

Thanks! I'll try releasing tonight after work.

[kazk]

Found few bugs:

(this will make the compiler complain about open goal)

Theorem ex : 1 * 1 = 1.
Proof.

The output is Error: There are pending proofs: ex. and it's not wrapped because I assumed the error to always have location information. The exit code is non zero so it's still considered a failure though.

---

Attempt to cheat (Solution.v):

Require Import Preloaded.

Definition preloaded_def (n : nat) := n * 2.

Lemma preloaded_lemma n : preloaded_def n = n * 2.
Proof. reflexivity. Qed.

The output is

<FAILED::> preloaded_lemma : Type is wrong - should be (
(forall n : nat, Preloaded.preloaded_def n = n * 2) )

<PASSED::>Closed under the global context

The new line after should be ( causes

---

I forgot to mention, but I added idac ""; to check_type to get \n<PASSED::> and \n<FAILED::> so it currently looks like this:

From Coq Require Export String.

Ltac check_type A B :=
    first [(match type of A with
    | ?T => first [unify T B; idtac ""; idtac "<PASSED::>" A ": Type is correct" |
                   idtac ""; idtac "<FAILED::>" A ": Type is wrong - should be (" B ")"]
    end) | idtac ""; idtac "<FAILED::>" A ": Missing definition"]; idtac "".

---

I don't think these will be a huge issue for now. So I'm still planning to release it tonight and let you play with it to find more bugs 😁 It should be easier to fix/improve check_type on Codewars too.

[kazk]

Coq is now available on Codewars! Thanks for all the help.

Have fun and please let me know if you find any issues.

[JasonGross]

Where can I find Coq on codewars? I don't see it on the main page of https://www.codewars.com , and can't find code for it in this repo...

[kazk]

https://www.codewars.com/kata/search/coq

Currently there's 7 kata.

[monadius]

There are at least 8 Coq katas. For some reason, this kata is not displayed in the search results when Coq is selected.

[kazk]

@monadius sometimes Codewars fails to update the search index. I just did it manually and it now shows 8.

[ice1000]

And there are three more after some translations get approved

[monadius]

@kazk could you change the default test code to the following:

Require Solution.

Theorem example_test : forall a b c : Type,
  a = b -> b = c -> a = c.
Proof.
  exact Solution.example.
Qed.
Print Assumptions example_test.

The main issue with Require Import Solution is that users can redefine many things in the solution module (for example, tactics and notations can be redefined). I would like to thank @JasonGross for discovering this issue (see this discussion).

[kazk]

Updated the default test code and fixed the output of pending proofs.