Freestyle Sparring

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

Create functions thas can sort an array using insertion sort algorithm. Function should return a COPY of sorted array, so the original array wouldn't be mutated

Note: you shouldn't use loops (for/while). Try to complete task in a functional way.

Write a script which can find indexes & sum of biggest possible sequence subarray items.

Example:

findBiggestSubArray([1, 2, -3, 2])
should return array like [a, b, c]
Where:
a: maximal sum of sequence
b: start index if sequence
c: last index of sequence

More examples:
findBiggestSubArray([1, 1, 1, 1, 1, 1, -5]) ==> return [6, 0, 5]
findBiggestSubArray([-9,1,3,1,1,-6,0,-9]) ==> [6, 1, 4]
findBiggestSubArray([-9,4,-1,5]) ==> [8, 1, 3]
findBiggestSubArray([-9, 4, 1, 1, -9, 5]) ==> [6, 1, 3]
findBiggestSubArray([-9]) ==> [-9, 0, 0]
findBiggestSubArray([-9,8,-2.5,2,1]) ==> [8.5, 1, 4]

This is about several ways to represent finite types (in Agda).

(Stub)

there is an error, fix it
(test kumite only)

Given a positive number N, you have to return if N is odd.

Example:
-> N = 3, return "True"
-> N = 42, return "False"

Good Luck !

Check if a given Int number have a perfect square.

A list needs to be sorted with its first field in ascending order, if a match is found then the second field should be sorted in descending order.

I found that if the second field is an integer this can be easily done by negating the integer key value.
For example:
key = lambda x: (x.name, - x.age))

The negation does not work on string.
Hence I did the following code to achieve the expected result. I would like to know other ways of sorting a list in different orders.

sort