Require Import Coq.Bool.Bool.
Require Import Coq.Arith.Arith.
Require Import Coq.Arith.EqNat.
Require Import Coq.omega.Omega.
Require Import Coq.Lists.List.
Require Import Coq.omega.Omega.
Require Import Coq.Sets.Multiset.
Require Import Coq.Lists.ListSet.
Require Import Coq.Strings.String.
Require Import Coq.Classes.RelationClasses.
Open Scope string_scope.

Import ListNotations.


Set Implicit Arguments.
Scheme Equality for list.

Fixpoint trueForAll {A:Type} (f:A->Prop) (l:list A) : Prop :=
  match l with
  | [] => True
  | h::ts => (f h) /\ (trueForAll f ts)
  end.

Fixpoint btrueForAll {A:Type} (f:A->bool) (l:list A) : bool :=
  match l with
  | [] => true
  | h::ts => andb (f h) (btrueForAll f ts)
  end.

Fixpoint trueForOne {A:Type} (f:A->Prop) (l:list A) : Prop :=
  match l with
  | [] => True
  | h::ts => (f h) \/ (trueForAll f ts)
  end.

Fixpoint btrueForOne {A:Type} (f:A->bool) (l:list A) : bool :=
  match l with
  | [] => true
  | h::ts => orb (f h) (btrueForOne f ts)
  end.

Fixpoint appendAny {A:Type} l1 l2 : list A :=
  match l1 with
  | [] => l2
  | h :: t => h :: (appendAny t l2)
  end.

Fixpoint consEnd {A:Type} fs f : (list A) :=
  match fs with
  | [] => [f]
  | h :: t => h :: (consEnd t f)
  end.

Fixpoint lastElement {A:Type} (a:A) (als:list A) : A :=
  match als with
  | [] => a
  | h :: t => lastElement h t
  end.

Fixpoint secondLastElement {A:Type} (a:A) (als:list A) : A :=
  match als with
  | [] => a
  | h::[] => a
  | h1 :: h2 :: t => lastElement h1 (h2::t)
  end.

Fixpoint listWithoutLastElement {A:Type} (als:list A) : list A :=
  match als with
  | [] => []
  | h::[] => []
  | h :: t => h:: listWithoutLastElement t
  end.

Definition isLastElement {A:Type} (a:A) (als:list A) : Prop := (eq a (lastElement a als)).

Lemma listEq : forall {A:Type} (h1:A) h2 ts2 ts1, h1=h2 -> ts2=ts1 -> h1::ts2=h2::ts1.

Lemma listEqHead : forall {A:Type} (h:A) ts2 ts1, ts2=ts1 -> h::ts2=h::ts1.

Lemma listEqTail : forall {A:Type} (h1:A) h2 ts, h1=h2 -> h1::ts=h2::ts.

Fixpoint removeElement {A:Type} (eqA:forall a b : A, {a = b} + {a <> b}) (e:A) (l:list A) : list A :=
  match l with
    | [] => []
    | h::ts => if (eqA h e) then ts else (h::(removeElement eqA e ts))
  end.

Inductive prefixList {A:Type} : (list A) -> (list A) -> Prop :=
  | Empty_PreFix : forall l, prefixList [] l
  | Head_PreFix : forall l1 l2 a, prefixList l1 l2 -> prefixList (a::l1) (a::l2)
  | Next_PreFix : forall l1 l2 a, prefixList l1 l2 -> prefixList l1 (a::l2).

Fixpoint NotIn {A:Type} (a : A) (ls : list A) : Prop :=
  match ls with
    | [] => True
    | h::ts => a <> h /\ NotIn a ts
  end.

Fixpoint noCommonElements {A:Type} (f1:list A) (f2:list A): Prop :=
 match f1 with
  | [] => True
  | f11::f1s => NotIn f11 f2 /\ noCommonElements f1s f2
end.

Fixpoint termsDoNotAppear {A:Type} (f1: list A) (f2:list (list A)): Prop :=
 match f2 with
  | [] => True
  | f21::f2s => noCommonElements f1 f21 /\ termsDoNotAppear f1 f2s
end.

Fixpoint someCommonElements {A:Type} (f1:list A) (f2:list A): Prop :=
 match f1 with
  | [] => False
  | f11::f1s => In f11 f2 \/ someCommonElements f1s f2
end.

Fixpoint mapFunction {A:Type} {B:Type} (f:A -> B) (als:list A) : (list B) :=
  match als with
    | [] => []
    | h::ts => (f h)::(mapFunction f ts)
  end.

Fixpoint mapListFunction {A:Type} {B:Type} (f:A -> (list B)) (als:list A) : (list B) :=
  match als with
    | [] => []
    | h::ts => appendAny (f h) (mapListFunction f ts)
  end.

Inductive orderedSubList {A:Type} : (list A) -> (list A) -> Prop :=
 | Empty_O_SubList : forall l, orderedSubList [] l
 | Same_O_SubList : forall l1 l2 h1 h2, orderedSubList l1 l2 -> orderedSubList (h1::l1) (h2::l2)
 | Next_O_SubList : forall (l1:list A) l2 h, orderedSubList l1 l2 -> orderedSubList l1 (h::l2).

Lemma idIsOrderedSublist : forall {A:Type} (rl:list A), orderedSubList rl rl.