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

if ($IsWindows) {
  Write-Host "Windows"
} elseif ($IsMacOS) {
  Write-Host "macOS"
} elseif ($IsLinux) {
  Write-Host "Linux"
} else {
  Write-Host "(unknown)"
}
Theorem Proving

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 ;-)

Require Import Preloaded.

Theorem lcs_correct : forall {A} (eq_dec : forall x y : A,
  {x = y} + {x <> y}) xs ys zs,
    lcs eq_dec xs ys = zs ->
    IsLCS zs xs ys.
Proof.
  admit.
Admitted.
Advanced Language Features
Fundamentals
Theorem Proving

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 *)
From Coq Require Import Lists.List omega.Omega.
Import ListNotations.

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

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.

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.

Fail Compute (interleave [1;2;3] [4;5;6]).

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

Compute (interleave [1;2;3] [4;5;6]).

Example test_interleave1:
  interleave [1;2;3] [4;5;6] = [1;4;2;5;3;6].
Proof. reflexivity. Qed.
Example test_interleave2:
  interleave [1] [4;5;6] = [1;4;5;6].
Proof. reflexivity. Qed.
Example test_interleave3:
  interleave [1;2;3] [4] = [1;4;2;3].
Proof. reflexivity. Qed.
Example test_interleave4:
  interleave [] [20;30] = [20;30].
Proof. reflexivity. Qed.
Code
Diff
  • From TLC Require Import LibTactics.
     
    Inductive R : nat -> nat -> Prop :=
      | R_0_1 : R 0 1.
    
    Example not_R_S_n_m : forall n m, ~ R (S n) m.
    Proof.
      (* Duplicate current subgoal to demonstrate two ways to prove
         the same statement *)
      dup.
    
      (* Was ... *)
      intros n m H; inversion H.
    
      (* Is now ... *)
      introv H; inverts H.
    
    Qed.
  • 11
    From TLC Require Import LibTactics.
    
    2
    2+
     
    
    33
    Inductive R : nat -> nat -> Prop :=
    
    44
      | R_0_1 : R 0 1.
    
    55
    66
    Example not_R_S_n_m : forall n m, ~ R (S n) m.
    
    77
    Proof.
    

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

From TLC Require Import LibTactics.

Inductive R : nat -> nat -> Prop :=
  | R_0_1 : R 0 1.

Example not_R_S_n_m : forall n m, ~ R (S n) m.
Proof.
  (* Duplicate current subgoal to demonstrate two ways to prove
     the same statement *)
  dup.

  (* Was ... *)
  intros n m H; inversion H.

  (* Is now ... *)
  introv H; inverts H.

Qed.

Just confirming that Idris does not enforce totality by default.

module PartialFunction

%access export

-- Partial function (implicit)
add : Int -> Int -> Int
add 3 5 = 8

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.

module TotalitySubversion

%access export
%default total

partial
add' : Int -> Int -> Int
add' 3 5 = 8

add : Int -> Int -> Int
add = assert_total add'

Expected result - compilation error.

module Example

%access export
%default partial

add : Int -> Int -> Int
add 3 5 = 8

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

module StateTest (factorialWithState) where

import Prelude

import Control.Monad.State (State, evalState, get, put)
import Data.Tuple (Tuple(..))

factorialWithState :: Int -> Int
factorialWithState n = evalState executionLoop (Tuple n 1)
  where
    executionLoop :: State (Tuple Int Int) Int
    executionLoop = do
      Tuple counter result <- get
      if counter == 0
        then pure result
        else do
          put (Tuple (counter - 1) (result * counter))
          executionLoop

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

Code
Diff
  • module BigIntExample where
    
    -- purescript-bigints now available on Codewars
    -- but fails with runtime JavaScript error due to
    -- missing JavaScript module
    
    import Prelude
    
    import Data.BigInt (BigInt, fromString)
    import Data.Maybe (fromJust)
    import Partial.Unsafe (unsafePartial)
    
    biiiig :: BigInt
    biiiig = unsafePartial fromJust $ fromString "917389127398375893457348957389457128937189237189237894357389457438957348957348957348947128937128937128937"
  • 11
    module BigIntExample where
    
    22
    3+
    -- purescript-bigints now available on Codewars
    
    4+
    -- but fails with runtime JavaScript error due to
    
    5+
    -- missing JavaScript module
    
    6+
    33
    import Prelude
    
    44
    55
    import Data.BigInt (BigInt, fromString)
    
    66
    import Data.Maybe (fromJust)
    
    77
    import Partial.Unsafe (unsafePartial)
    
    88
    99
    biiiig :: BigInt
    
    1010
    biiiig = unsafePartial fromJust $ fromString "917389127398375893457348957389457128937189237189237894357389457438957348957348957348947128937128937128937"
    

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

module LeibnizExample where

import Data.Leibniz

reflexivity :: forall a. a ~ a
reflexivity = id

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

module RatioExample where

import Prelude

import Data.Ratio

myRatio :: Ratio Int
myRatio = 3 % 10 -- 3 to 10, or 0.3

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

module BigIntExample where

import Prelude

import Data.BigInt (BigInt, fromString)
import Data.Maybe (fromJust)
import Partial.Unsafe (unsafePartial)

biiiig :: BigInt
biiiig = unsafePartial fromJust $ fromString "917389127398375893457348957389457128937189237189237894357389457438957348957348957348947128937128937128937"

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

module WelcomePureScript (welcomeMsg) where

welcomeMsg :: String
welcomeMsg = "Welcome, PureScript!"
Loading more items...