Library EVMOpSem.Lem.lem_list

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_maybe.
Require Export lem_maybe.
Require Import lem_basic_classes.
Require Export lem_basic_classes.
Require Import lem_function.
Require Export lem_function.
Require Import lem_tuple.
Require Export lem_tuple.
Require Import lem_num.
Require Export lem_num.

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



Definition null {a : Type} (l : list a) : bool := match ( l) with [] => true | _ => false end.




Instance x145_Eq{a: Type} `{Eq a}: Eq (list a):= {
   isEqual := (list_equal_by (fun x y => x = y));
   isInequal l1 l2 := negb ((list_equal_by (fun x y => x = y) l1 l2))
}.



Program Fixpoint lexicographicCompareBy {a : Type} (cmp : a -> a -> ordering ) (l1 : list a) (l2 : list a) : ordering := match ( (l1,l2)) with
  | ([], []) => EQ
  | ([], _::_) => LT
  | (_::_, []) => GT
  | (x::xs, y::ys) =>
      match ( cmp x y) with
        | LT => LT
        | GT => GT
        | EQ => lexicographicCompareBy cmp xs ys
      end
    
end.


Program Fixpoint lexicographicLessBy {a : Type} (less : a -> a -> bool ) (less_eq : a -> a -> bool ) (l1 : list a) (l2 : list a) : bool := match ( (l1,l2)) with
  | ([], []) => false
  | ([], _::_) => true
  | (_::_, []) => false
  | (x::xs, y::ys) => ((less x y) || ((less_eq x y) && (lexicographicLessBy less less_eq xs ys)))
end.


Program Fixpoint lexicographicLessEqBy {a : Type} (less : a -> a -> bool ) (less_eq : a -> a -> bool ) (l1 : list a) (l2 : list a) : bool := match ( (l1,l2)) with
  | ([], []) => true
  | ([], _::_) => true
  | (_::_, []) => false
  | (x::xs, y::ys) => (less x y || (less_eq x y && lexicographicLessEqBy less less_eq xs ys))
end.

Instance x144_Ord{a: Type} `{Ord a}: Ord (list a):= {
   compare := (lexicographicCompareBy compare);
   isLess := (lexicographicLessBy isLess isLessEqual);
   isLessEqual := (lexicographicLessEqBy isLess isLessEqual);
   isGreater x y := (lexicographicLessBy isLess isLessEqual y x);
   isGreaterEqual x y := (lexicographicLessEqBy isLess isLessEqual y x)
}.



Program Fixpoint reverseAppend {a : Type} (l1 : list a) (l2 : list a) : list a:= match ( l1) with
                                | [] => l2
                                | x :: xs => reverseAppend xs (x :: l2)
                               end.


Program Fixpoint map_tr {a b : Type} (rev_acc : list b) (f : a -> b) (l : list a) : list b:= match ( l) with
  | [] => List.rev rev_acc
  | x :: xs => map_tr ((f x) :: rev_acc) f xs
end.

Program Fixpoint count_map {a b : Type} (f : a -> b) (l : list a) (ctr : nat ) : list b:=
  match ( l) with
  | [] => []
  | hd :: tl => f hd ::
    (if nat_ltb ctr( 5000%nat) then count_map f tl ( Coq.Init.Peano.plus ctr( 1%nat))
    else map_tr [] f tl)
  end.




Definition concat {a : Type} : list (list a) -> list a:= List.fold_right (@ List.app _) [].




Program Fixpoint dest_init_aux {a : Type} (rev_init : list a) (last_elem_seen : a) (to_process : list a) : (list a*a) % type:=
  match ( to_process) with
    | [] => (List.rev rev_init, last_elem_seen)
    | x::xs => dest_init_aux (last_elem_seen::rev_init) x xs
  end.

Definition dest_init {a : Type} (l : list a) : option ((list a*a) % type) := match ( l) with
  | [] => None
  | x::xs => Some (dest_init_aux [] x xs)
end.

Program Fixpoint index {a : Type} (l : list a) (n : nat ) : option a := match ( l) with
  | [] => None
  | x :: xs => if beq_nat n( 0%nat) then Some x else index xs (Coq.Init.Peano.minus n( 1%nat))
end.

Program Fixpoint findIndices_aux {a : Type} (i:nat ) (P : a -> bool ) (l : list a) : list (nat ):=
  match ( l) with
    | [] => []
    | x :: xs => if P x then i :: findIndices_aux ( Coq.Init.Peano.plus i( 1%nat)) P xs else findIndices_aux ( Coq.Init.Peano.plus i( 1%nat)) P xs
 end.
Definition findIndices {a : Type} (P : a -> bool ) (l : list a) : list (nat ):= findIndices_aux( 0%nat) P l.

Definition findIndex {a : Type} (P : a -> bool ) (l : list a) : option (nat ) := match ( findIndices P l) with
  | [] => None
  | x :: _ => Some x
end.



Program Fixpoint genlist {a : Type} (f : nat -> a) (n : nat ) : list a:=
  match ( (n : nat )) with
    | 0%nat => []
    | S (n') => (@ List.app _)(genlist f n') [(f n')]
  end.

Program Fixpoint replicate {a : Type} (n : nat ) (x : a) : list a:=
  match ( n) with
    | 0%nat => []
    | S (n') => x :: replicate n' x
  end.

Program Fixpoint splitAtAcc {a : Type} (revAcc : list a) (n : nat ) (l : list a) : (list a*list a) % type:=
  match ( l) with
    | [] => (List.rev revAcc, [])
    | x::xs => if nat_lteb n( 0%nat) then (List.rev revAcc, l) else splitAtAcc (x::revAcc) (Coq.Init.Peano.minus n( 1%nat)) xs
  end.

Definition splitAt {a : Type} (n : nat ) (l : list a) : (list a*list a) % type:=
   splitAtAcc [] n l.

Definition take {a : Type} (n : nat ) (l : list a) : list a:= (@ fst _ _) (splitAt n l).

Definition drop {a : Type} (n : nat ) (l : list a) : list a:= (@ snd _ _) (splitAt n l).

Program Fixpoint splitWhile_tr {a : Type} (p : a -> bool ) (xs : list a) (acc : list a) : (list a*list a) % type:= match ( xs) with
  | [] =>
    (List.rev acc, [])
  | x::xs =>
    if p x then
      splitWhile_tr p xs (x::acc)
    else
      (List.rev acc, (x::xs))
end.

Definition splitWhile {a : Type} (p : a -> bool ) (xs : list a) : (list a*list a) % type:= splitWhile_tr p xs [].

Definition takeWhile {a : Type} (p : a -> bool ) (l : list a) : list a:= (@ fst _ _) (splitWhile p l).

Definition dropWhile {a : Type} (p : a -> bool ) (l : list a) : list a:= (@ snd _ _) (splitWhile p l).

Program Fixpoint isPrefixOf {a : Type} `{Eq a} (l1 : list a) (l2 : list a) : bool := match ( (l1, l2)) with
  | ([], _) => true
  | (_::_, []) => false
  | (x::xs, y::ys) => (x = y) && isPrefixOf xs ys
end.

Program Fixpoint update {a : Type} (l : list a) (n : nat ) (e : a) : list a:=
  match ( l) with
    | [] => []
    | x :: xs => if beq_nat n( 0%nat) then e :: xs else x :: (update xs ( Coq.Init.Peano.minus n( 1%nat)) e)
end.


Definition elemBy {a : Type} (eq : a -> a -> bool ) (e : a) (l : list a) : bool := List.existsb (eq e) l.
Definition elem {a : Type} `{Eq a} : a -> list a -> bool := elemBy (fun x y => x = y).
Program Fixpoint find {a : Type} (P : a -> bool ) (l : list a) : option a := match ( l) with
  | [] => None
  | x :: xs => if P x then Some x else find P xs
end.


Definition lookupBy {a b : Type} (eq : a -> a -> bool ) (k : a) (m : list ((a*b) % type)) : option b := option_map (fun (x : (a*b) % type) => (@ snd _ _) x) (find (
  fun (p : (a*b) % type) => match ( (p) ) with ( (k', _)) => eq k k' end) m).


Definition partition {a : Type} (P : a -> bool ) (l : list a) : (list a*list a) % type:= (List.filter P l, List.filter (fun (x : a) => negb (P x)) l).

Definition reversePartition {a : Type} (P : a -> bool ) (l : list a) : (list a*list a) % type:= partition P (List.rev l).

Program Fixpoint deleteFirst {a : Type} (P : a -> bool ) (l : list a) : option (list a) := match ( l) with
                            | [] => None
                            | x :: xs => if (P x) then Some xs else option_map (fun (xs' : list a) => x :: xs') (deleteFirst P xs)
                          end.


Definition deleteBy {a : Type} (eq : a -> a -> bool ) (x : a) (l : list a) : list a:= fromMaybe l (deleteFirst (eq x) l).
Program Fixpoint zip {a b : Type} (l1 : list a) (l2 : list b) : list ((a*b) % type):= match ( (l1, l2)) with
  | (x :: xs, y :: ys) => (x, y) :: zip xs ys
  | _ => []
end.

Program Fixpoint unzip {a b : Type} (l : list ((a*b) % type)) : (list a*list b) % type:= match ( l) with
  | [] => ([], [])
  | (x, y) :: xys =>
  match ( unzip xys) with (xs, ys) => ((x :: xs), (y :: ys)) end
end.

Instance x143_SetType{a: Type} `{SetType a}: SetType (list a):= {
  setElemCompare := lexicographicCompareBy setElemCompare
}.


Program Fixpoint allDistinct {a : Type} `{Eq a} (l : list a) : bool :=
  match ( l) with
    | [] => true
    |( x::l') => negb (elem x l') && allDistinct l'
  end.

Program Fixpoint mapMaybe {a b : Type} (f : a -> option b ) (xs : list a) : list b:=
  match ( xs) with
  | [] => []
  | x::xs =>
      match ( f x) with
      | None => mapMaybe f xs
      | Some y => y :: (mapMaybe f xs)
      end
  end.

Program Fixpoint mapiAux {a b : Type} (f : nat -> b -> a) (n : nat ) (l : list b) : list a:= match ( l) with
  | [] => []
  | x :: xs => (f n x) :: mapiAux f ( Coq.Init.Peano.plus n( 1%nat)) xs
end.
Definition mapi {a b : Type} (f : nat -> a -> b) (l : list a) : list b:= mapiAux f( 0%nat) l.

Definition deletes {a : Type} `{Eq a} (xs : list a) (ys : list a) : list a:=
  List.fold_left (flip (deleteBy (fun x y => x = y))) ys xs.

Program Fixpoint catMaybes {a : Type} (xs : list (option a )) : list a:=
  match ( xs) with
    | [] =>
        []
    |( None :: xs') =>
        catMaybes xs'
    |( Some x :: xs') =>
        x :: catMaybes xs'
  end.