Failed Tests

### Getting platform info

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)"
}``````
Failed Tests

### Open Challenge: Verifying an efficient functional implementation for the longest common subsequence problem

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.

### Non-structural well-founded recursion using Program Fixpoint

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:
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  [4;5;6] = [1;4;5;6].
Proof. reflexivity. Qed.
Example test_interleave3:
interleave [1;2;3]  = [1;4;2;3].
Proof. reflexivity. Qed.
Example test_interleave4:
interleave [] [20;30] = [20;30].
Proof. reflexivity. Qed.``````

### [Coq] TLC package on Codewars?

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.
```
Failed Tests

### [Coq] TLC package on Codewars?

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.``````

### Idris: Partial functions by default?

Just confirming that Idris does not enforce totality by default.

``````module PartialFunction

%access export

-- Partial function (implicit)
add : Int -> Int -> Int

### Idris: Subverting the totality checker

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 : Int -> Int -> Int
Failed Tests

### Idris: Total functions should not be able to make use of partial functions

Expected result - compilation error.

``````module Example

%access export
%default partial

add : Int -> Int -> Int

### PureScript State Monad on Codewars?

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``````

### PureScript Data.Ratio on Codewars?

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

Failed Tests

### Data.BigInt in PureScript?

`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"``````
•  1 1 ```module BigIntExample where ``` 2 2 3 + ```-- purescript-bigints now available on Codewars ``` 4 + ```-- but fails with runtime JavaScript error due to ``` 5 + ```-- missing JavaScript module ``` 6 + 3 3 ```import Prelude ``` 4 4 5 5 ```import Data.BigInt (BigInt, fromString) ``` 6 6 ```import Data.Maybe (fromJust) ``` 7 7 ```import Partial.Unsafe (unsafePartial) ``` 8 8 9 9 ```biiiig :: BigInt ``` 10 10 ```biiiig = unsafePartial fromJust \$ fromString "917389127398375893457348957389457128937189237189237894357389457438957348957348957348947128937128937128937" ```
Failed Tests

### PureScript Data.Leibniz on Codewars?

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``````
Failed Tests

### PureScript Data.Ratio on Codewars?

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``````
Failed Tests

### Data.BigInt in PureScript?

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"``````

### Welcome PureScript

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!"``````