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.
Require Solution.
Require Import Preloaded.
From CW Require Import Loader.
CWGroup "Solution.lcs_correct".
CWTest "should have the correct type".
CWAssert Solution.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).
CWTest "should be closed under the global context".
CWAssert Solution.lcs_correct Assumes.
CWEndGroup.
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.
Require Solution.
From CW Require Import Loader.
From Coq Require Import Lists.List.
Import ListNotations.
CWAssert Solution.test_interleave1 : (Solution.interleave [1;2;3] [4;5;6] = [1;4;2;5;3;6]).
CWAssert Solution.test_interleave1 Assumes.
CWAssert Solution.test_interleave2 : (Solution.interleave [1] [4;5;6] = [1;4;5;6]).
CWAssert Solution.test_interleave2 Assumes.
CWAssert Solution.test_interleave3 : (Solution.interleave [1;2;3] [4] = [1;4;2;3]).
CWAssert Solution.test_interleave3 Assumes.
CWAssert Solution.test_interleave4 : (Solution.interleave [] [20;30] = [20;30]).
CWAssert Solution.test_interleave4 Assumes.
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.
1 1 From TLC Require Import LibTactics.
2 − 2 + 3 3 Inductive R : nat -> nat -> Prop :=
4 4 | R_0_1 : R 0 1.
5 5 6 6 Example not_R_S_n_m : forall n m, ~ R (S n) m.
7 7 Proof.
… Expand 8 8 (* Duplicate current subgoal to demonstrate two ways to prove
9 9 the same statement *)
10 10 dup.
11 11 12 12 (* Was ... *)
13 13 intros n m H; inversion H.
14 14 15 15 (* Is now ... *)
16 16 introv H; inverts H.
17 17 18 18 Qed.
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.
Require Solution.
Theorem not_R_S_n_m_test : forall n m, ~ Solution.R (S n) m.
Proof.
exact Solution.not_R_S_n_m.
Qed.
Print Assumptions not_R_S_n_m_test.
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
module PartialFunctionSpec
import Specdris.Spec
import PartialFunction
%access export
specSuite : IO ()
specSuite = spec $ do
describe "add" $ do
it "adds two integers" $ do
(3 `add` 5) `shouldBe` 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'
module TotalitySubversionSpec
import Specdris.Spec
import TotalitySubversion
%access export
%default total
specSuite : IO ()
specSuite = spec $ do
describe "add" $ do
it "adds two natural numbers" $ do
(3 `add` 5) `shouldBe` 8
Expected result - compilation error.
module Example
%access export
%default partial
add : Int -> Int -> Int
add 3 5 = 8
module ExampleSpec
import Specdris.Spec
import Example
%access export
%default total
specSuite : IO ()
specSuite = spec $ do
describe "add" $ do
it "adds two natural numbers" $ do
(3 `add` 5) `shouldBe` 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
module StateTestSpec where
import Prelude
import Test.Spec (Spec, describe, it)
import Test.Spec.Assertions (shouldEqual)
import StateTest (factorialWithState)
spec :: Spec Unit
spec =
describe "StateTest.factorialWithState" do
describe "Fixed tests" do
it "should work for some fixed tests" do
factorialWithState 0 `shouldEqual` 1
factorialWithState 1 `shouldEqual` 1
factorialWithState 2 `shouldEqual` 2
factorialWithState 3 `shouldEqual` 6
factorialWithState 4 `shouldEqual` 24
factorialWithState 5 `shouldEqual` 120
factorialWithState 6 `shouldEqual` 720
factorialWithState 7 `shouldEqual` 5040
factorialWithState 8 `shouldEqual` 40320
factorialWithState 9 `shouldEqual` 362880
factorialWithState 10 `shouldEqual` 3628800
As of 09/02/2019, Data.Ratio
from purescript-rationals
is available on Codewars.
module ExampleSpec where import Prelude import Test.Spec (Spec, describe, it) import Test.Spec.Assertions (shouldEqual) import RatioExample (myRatio) import Data.Ratio spec :: Spec Unit spec = describe "Is Data.Ratio in PureScript available on Codewars?" do describe "Let us see ... " do it "This should compile with passed tests if it is indeed supported." do myRatio `shouldEqual` myRatio
1 1 module ExampleSpec where
2 2 3 3 import Prelude
4 4 5 5 import Test.Spec (Spec, describe, it)
6 6 import Test.Spec.Assertions (shouldEqual)
7 7 8 8 import RatioExample (myRatio)
9 + import Data.Ratio
9 9 10 10 spec :: Spec Unit
11 11 spec =
12 12 describe "Is Data.Ratio in PureScript available on Codewars?" do
13 13 describe "Let us see ... " do
14 14 it "This should compile with passed tests if it is indeed supported." do
15 − true `shouldEqual` true
16 + myRatio `shouldEqual` myRatio
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 :(
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"
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
module DummySpec where
import Prelude
import Test.Spec (Spec, describe, it)
import Test.Spec.Assertions (shouldEqual)
import LeibnizExample
spec :: Spec Unit
spec =
describe "Data.Leibniz" do
describe "Availability on Codewars" do
it "This should compile if it is indeed available on Codewars" do
true `shouldEqual` true
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
module ExampleSpec where
import Prelude
import Test.Spec (Spec, describe, it)
import Test.Spec.Assertions (shouldEqual)
import RatioExample (myRatio)
spec :: Spec Unit
spec =
describe "Is Data.Ratio in PureScript available on Codewars?" do
describe "Let us see ... " do
it "This should compile with passed tests if it is indeed supported." do
true `shouldEqual` true
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"
module ExampleSpec where
import Prelude
import Test.Spec (Spec, describe, it)
import Test.Spec.Assertions (shouldEqual)
import BigIntExample (biiiig)
spec :: Spec Unit
spec =
describe "Is Data.BigInt available on Codewars?" do
describe "Let's see" do
it "This should compile with passed tests if it is indeed supported." do
true `shouldEqual` true
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!"
module ExampleSpec where
import Prelude
import Test.Spec (Spec, describe, it)
import Test.Spec.Assertions (shouldEqual)
import WelcomePureScript (welcomeMsg)
spec :: Spec Unit
spec =
describe welcomeMsg do
it "PureScript is a strongly and statically typed functional programming language that compiles to and is easily interoperable with JavaScript." do
welcomeMsg `shouldEqual` welcomeMsg
it "Its syntax and semantics are heavily influenced by Haskell so Haskell programmers should find it easy to pick up PureScript." do
welcomeMsg `shouldEqual` welcomeMsg
it "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" do
welcomeMsg `shouldEqual` welcomeMsg
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.
{-# LANGUAGE
KindSignatures,
GADTs,
TypeOperators,
TypeFamilies,
UndecidableInstances,
RankNTypes,
EmptyCase #-}
module TheMiddleSchoolersMistake where
-- Void - the type representing contradictions in Haskell
import Data.Void
-- Peano's axioms for the natural numbers
data Z
data S n
data Natural :: * -> * where
NumZ :: Natural Z
NumS :: Natural n -> Natural (S n)
-- Axiom of reflexivity of equality: The very notion
-- of equality itself mandates that everything be
-- considered equal to itself
data (:=:) :: * -> * -> * where
Refl :: a -> a :=: a
-- Peano addition, multiplication and exponentation
type family (:+:) (n :: *) (m :: *) :: *
type instance Z :+: n = n
type instance S n :+: m = S (n :+: m)
type family (:*:) (n :: *) (m :: *) :: *
type instance Z :*: n = Z
type instance S n :*: m = m :+: (n :*: m)
type family (:^:) (n :: *) (m :: *) :: *
type instance n :^: Z = S Z
type instance n :^: S m = n :*: (n :^: m)
-- Useful type synonyms for readability
type N1 = S Z -- The natural number 1
type N2 = S N1 -- The natural number 2
type N4 = N2 :+: N2 -- The natural number 4
-- Our proof that (a + b)^2 /= a^2 + b^2 in general
proof ::
(forall n m.
Natural n ->
Natural m ->
((n :+: m) :^: N2) :=: ((n :^: N2) :+: (m :^: N2))) -> Void
proof mistake = let
-- 1 is a natural number
one :: Natural N1
one = NumS NumZ
-- To disprove (a + b)^2 = a^2 + b^2, we provide witnesses
-- a = 1, b = 1 to our counterexample. A witness is a
-- value demonstrating the correctness of a logical statement
-- involving existential quantifiers
-- N.B. The witnesses could be anything else as long as it
-- proves our point. For example, we could've chosen a = 2,
-- b = 3 instead and show that (2 + 3)^2 = 5^2 = 25 /= 13 =
-- 2^2 + 3^2
erroneous :: N4 :=: N2
erroneous = mistake one one in
-- Now we consider all possible cases where 4 = 2 and
-- describe how to construct a proof of Void in each case
-- However, there are no constructors that would allow us
-- to construct a value of such a type! The only possible
-- constructor we could consider is Refl, but Refl always
-- constructs values of a :=: a, never a :=: b where a and
-- b are distinct types. Therefore, we have already
-- considered all (0) possible cases of 4 = 2 and we are
-- done here.
case erroneous of {}
module DummySpec where
import Test.Hspec
import TheMiddleSchoolersMistake
spec :: Spec
spec = do
describe "Proof" $ do
it "should type-check" $ do
"Proof" `shouldNotBe` "Good luck!"