Here's an interesting verification challenge - verify the following efficient implementation of a solution to the longest common subsequence problem (adapted from @JohanWiltink's Haskell solution to Longest Common Subsequence (Performance version)):

(* Adapted from @JohanWiltink's solution to Longest Common
   Subsequence (Performance Version) *)
Fixpoint elem_index {A : Type}
  (eq_dec : forall x y : A, {x = y} + {x <> y})
  (n : A) (l : list A) : option nat :=
  match l with
  | [] => None
  | x :: xs =>
      if eq_dec n x
        then Some O
        else
          match elem_index eq_dec n xs with
          | Some idx => Some (S idx)
          | None => None
          end
  end.

Fixpoint lcs_aux {A : Type} (gas : nat)
  (eq_dec : forall x y : A, {x = y} + {x <> y})
  (l l' : list A) : list A :=
  match gas with
  | O => []
  | S gas' =>
      match l with
      | [] => []
      | x :: xs =>
          match l' with
          | [] => []
          | y :: ys =>
              if eq_dec x y
                then x :: lcs_aux gas' eq_dec xs ys
                else
                  let
                    lcs0 := match elem_index eq_dec x ys with
                    | Some i => x :: lcs_aux gas' eq_dec
                        xs (skipn (S i) ys)
                    | None => []
                    end in
                  let
                    lcs1 := match elem_index eq_dec y xs with
                    | Some j => y :: lcs_aux gas' eq_dec
                        (skipn (S j) xs) ys
                    | None => []
                    end in
                  let lcs2 := lcs_aux gas' eq_dec xs ys in
                  let lcs0_length := length lcs0 in
                  let lcs1_length := length lcs1 in
                  let lcs2_length := length lcs2 in
                    if le_dec lcs0_length lcs1_length
                      then if le_dec lcs1_length lcs2_length
                        then lcs2
                        else lcs1
                      else if le_dec lcs0_length lcs2_length
                        then lcs2
                        else lcs0
          end
      end
  end.

Definition lcs {A : Type}
  (eq_dec : forall x y : A, {x = y} + {x <> y})
  (l l' : list A) : list A :=
  lcs_aux (length l + length l') eq_dec l l'.

Why a Kumite? Why not a Kata?

Long story short, I haven't been able to figure out how to prove it correct (hence "Open Challenge" in the title of this Kumite) or disprove it (if it turns out to be buggy and fails on some weird obscure edge case that was somehow untested in the original Kata). So if you can prove it correct or find a bug in the implementation before I do and decide not to keep your findings secret, you have two options:

• Spar on this Kumite by forking it and providing a complete (ideally axiom-free, though common axioms such as excluded middle are also acceptable) proof of the (in)correctness of the above implementation, OR
• Convert your complete solution into a Kata so other Codewarriors can try proving it correct/incorrect for themselves. You can take all the credit for coming up with this Kata.

Good luck ;-)

In Coq, every recursive definition has to provably terminate on all possible inputs; otherwise, the logical consistency of Coq would be undermined. However, it is possible to define well-founded recursive functions which fail to pass Coq's built-in termination checker since it only does a very simple check to ensure that the Fixpoint being defined is structurally recursive:

Fail Fixpoint interleave {A} (l1 l2 : list A) : list A :=
  match l1 with
  | [] => l2
  | x :: xs => x :: interleave l2 xs
  end.
(* => The command has indeed failed with message:
      Cannot guess decreasing argument of fix. *)

One way to define non-structurally-recursive functions which provably terminate in Coq is to use the Function feature. To use the Function feature, one has to first Require Import Recdef before defining the Function and specifying a measure that decreases on every recursive call, followed by a proof that the measure indeed decreases as required ending with Defined instead of the usual Qed. However, in our particular case, even Function fails us since it requires the measure to refer to exactly one argument in the function:

Require Import Recdef.

Fail Function interleave {A} (l1 l2 : list A) {measure length (l1 ++ l2)} : list A :=
  match l1 with
  | [] => l2
  | x :: xs => x :: interleave l2 xs
  end.
(* => The command has indeed failed with message:
      Recursive argument must be specified *)

In this case, we need to use Program Fixpoint instead which is very similar to Function except that the decreasing measure can refer to more than one argument. To use Program Fixpoint, one has to first import Coq.Program.Wf:

From Coq Require Import Program.Wf.

Program Fixpoint interleave {A} (l1 l2 : list A) {measure (length (l1 ++ l2))} : list A :=
  match l1 with
  | [] => l2
  | x :: xs => x :: interleave l2 xs
  end.

However, if we try to use the Program Fixpoint at this stage, Coq will complain that it is not found in the current environment:

Fail Compute (interleave [1;2;3] [4;5;6]).
(* => The command has indeed failed with message:
      The reference interleave was not found
      in the current environment. *)

This is because we haven't proven to Coq that it terminates yet. To do that, we have to focus each proof obligation generated by Program Fixpoint (1 in this particular example) using Next Obligation followed its proof. It is OK to end the proofs with Qed when using Program Fixpoint:

Next Obligation.
  simpl.
  repeat rewrite app_length.
  omega.
Qed.

Now we can compute with it:

Compute (interleave [1;2;3] [4;5;6]).
(* => = [1; 4; 2; 5; 3; 6]
      : list nat *)

Just a quick test on whether the TLC package is available on Codewars.

Just confirming that Idris does not enforce totality by default.

It seems possible to subvert the totality checker by using assert_total on a partial function to convince Idris that it is total. This would place Idris theorem-proving Kata in jeopardy.

Expected result - compilation error.

Just testing whether the State monad in PureScript is available on Codewars.

As of 09/02/2019, Data.Ratio from purescript-rationals is available on Codewars.

purescript-bigints has been added to Codewars but now it seems there is a runtime JavaScript error due to missing modules on the JavaScript end :(

A simple test on whether Data.Leibniz is available as a PureScript module on Codewars.

Just a test to see whether Data.Ratio for PureScript is available on Codewars. See test output for results.

Just testing whether arbitrary-precision integers in PureScript are supported on Codewars. See the tests for the results.

PureScript is a strongly, statically typed functional programming language that compiles to and is easily interoperable with JavaScript. Its syntax and semantics are heavily influenced by Haskell so Haskell enthusiasts should find it easy to pick up PureScript.

Please don't forget to help PureScript leave Beta on Codewars and support the Codewars PureScript community by completing, authoring and translating more PureScript Kata. - @donaldsebleung

It is not uncommon to see a middle schooler incorrectly simplify the expression (a + b)^2 to a^2 + b^2 in his/her algebra assignments. While the two expressions may be equivalent for particular values of a and b (e.g. (0 + 0)^2 = 0^2 = 0 + 0^2 = 0^2 + 0^2), it is not true in general. So, how can we convince said middle-schooler that (a + b)^2 is not equal to a^2 + b^2 in general? This is equivalent to saying:

-- N.B. The domain of a, b is the natural numbers for
-- sake of simplicity
exists a b. (a + b)^2 /= a^2 + b^2

The general method for proving statements involving existential quantifiers is to provide a specific value or set of values such that the statement to be proven holds true - such value(s) are called witnesses. So, for example, we could provide the witnesses a = 1 and b = 1 in our case which reduces the statement to:

(1 + 1)^2 /= 1^2 + 1^2

And, of course, evaluating both sides of our equation gives 4 /= 2 which trivially holds.

Unfortunately, there is no direct way to encode existential quantifiers (and inequality) as a Haskell type. So what we could do is transform our original statement using known logical equivalences. The first thing to notice is that a /= b is defined as not (a = b) for any a, b:

exists a b. not ((a + b)^2 = a^2 + b^2)

Then, de Morgan's law for quantifiers tells us that exists a. not b is logically equivalent to not (forall a. b) for any b (which may or may not be related to a). Finally, to prove that not (forall a. b), it suffices to prove that asserting forall a. b leads to a contradiction (Void in Haskell). So our final type (minus a bit of required Haskell boilerplate code) is:

(forall a b. (a + b)^2 = a^2 + b^2) -> Void

See the code provided for the exact type signature of our proof and additional clarifications/explanations.