Library EVMOpSem.Lem.lem_sorting

Require Import Arith.
Require Import Bool.
Require Import List.
Require Import String.
Require Import Program.Wf.

Require Import coqharness.

Open Scope nat_scope.
Open Scope string_scope.

Require Import lem_bool.
Require Export lem_bool.
Require Import lem_basic_classes.
Require Export lem_basic_classes.
Require Import lem_maybe.
Require Export lem_maybe.
Require Import lem_list.
Require Export lem_list.
Require Import lem_num.
Require Export lem_num.

Require Import Coq.Lists.List.
Require Export Coq.Lists.List.



Program Fixpoint isPermutationBy {a : Type} (eq : a -> a -> bool ) (l1 : list a) (l2 : list a) : bool := match ( l1) with
  | [] => null l2
  |( x :: xs) =>
      match ( deleteFirst (eq x) l2) with
        | None => false
        | Some ys => isPermutationBy eq xs ys
      end
    
end.


Program Fixpoint isSortedBy {a : Type} (cmp : a -> a -> bool ) (l : list a) : bool := match ( l) with
  | [] => true
  | x1 :: xs =>
    match ( xs) with
      | [] => true
      | x2 :: _ => (cmp x1 x2 && isSortedBy cmp xs)
    end
end.




Program Fixpoint insertBy {a : Type} (cmp : a -> a -> bool ) (e : a) (l : list a) : list a:= match ( l) with
  | [] => [e]
  | x :: xs => if cmp x e then x :: (insertBy cmp e xs) else (e :: (x :: xs))
end.

Definition insertSortBy {a : Type} (cmp : a -> a -> bool ) (l : list a) : list a:= List.fold_left (fun (l : list a) (e : a) => insertBy cmp e l) l [].




Definition predicate_of_ord {a : Type} (f : a -> a -> ordering ) (x : a) (y : a) : bool :=
  match ( f x y) with
    | LT => true
    | EQ => true
    | GT => false
  end.