Earn extra honor and gain new allies!
Honor is earned for each new codewarrior who joins.
Learn more
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!"
Theoretical Computer Science
Mathematics
Algorithms
Numbers

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 {}
Loading more items...