Hello RISC-V World!

where fastify

It's pitch black here and I seem to be surrounded by cold, metallic walls. And the world is wobbly ... wait, am I stuck in a container? And where is this ship headed? Help!

Just checking whether PowerShell submissions on Codewars are executed in a Linux (most likely), Windows (less likely) or macOS (probably not) environment.

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 :(