Require Import Pip.Model.Lib.
Import List Coq.Logic.Classical_Prop.
Import List.ListNotations Lia.

Lemma NoDupSplit (A: Type) :
∀ l l': list A ,
NoDup (l++l') → NoDup l ∧ NoDup l'.

Definition disjoint {A : Type} (l1 l2 : list A) : Prop :=
∀ x : A, In x l1 → ¬ In x l2 .

Lemma NoDupSplitInclIff (A: Type) :
∀ l l': list A ,
NoDup (l++l') ↔ (NoDup l ∧ NoDup l') ∧ disjoint l l'.
Lemma inclDisjoint (A : Type) (l l' l1 l2 : list A):
disjoint l l' → incl l1 l → incl l2 l' → disjoint l1 l2.

Lemma removeNotIn (A :Type) (eq_dec : ∀ x y : A, {x = y} + {x ≠ y}):
∀ l a, ¬ In a l → remove eq_dec a l =l.

Lemma removeIncl (A :Type) (eq_dec : ∀ x y : A, {x = y} + {x ≠ y}):
∀ l a, incl (remove eq_dec a l) l.

Lemma removeNoDup
(A :Type) (eq_dec : ∀ x y : A, {x = y} + {x ≠ y}):
∀ l a,NoDup l → NoDup (remove eq_dec a l).

Lemma removeLength (A :Type) (eq_dec : ∀ x y : A, {x = y} + {x ≠ y}):
∀ l a, NoDup l → In a l → S (length (remove eq_dec a l)) = length l.

Lemma removeCons (A :Type) (eq_dec : ∀ x y : A, {x = y} + {x ≠ y}):
∀ l a b, a ≠ b → remove eq_dec a (b ::l) = b :: (remove eq_dec a l) .

Lemma removeConsEq (A :Type) (eq_dec : ∀ x y : A, {x = y} + {x ≠ y}):
∀ l a , remove eq_dec a (a ::l) =remove eq_dec a l .

Lemma removeStillIn (A :Type) (eq_dec : ∀ x y : A, {x = y} + {x ≠ y}):
∀ a b : A, ∀ l' l: list A ,
a ≠ b → remove eq_dec a l' = l → In b l' → In b l.

Lemma removeStillInIncl (A :Type) (eq_dec : ∀ x y : A, {x = y} + {x ≠ y}):
∀ v a : A , ∀ l l1 l' : list A, v ≠ a → remove eq_dec a l' = l →
incl l1 l' → In v l1 → In v l.

Lemma addLengthIn (A : Type) (eq_dec : ∀ x y : A, {x = y} + {x ≠ y}) :
∀ l' l, ∀ x b : A,
length l' = S (length l) →
incl l l' →
x ≠ b →
In x l' →
¬ In x l →
In b l' →
NoDup l →
NoDup l' →
In b l.

Lemma flat_map_app_cons (A : Type) (f : A → list A ):
∀ l1 p l2 ,
flat_map f (l1 ++ p :: l2) =
flat_map f l1 ++
flat_map f [p] ++
flat_map f l2.

Lemma flat_map_app (A : Type) (f : A → list A ):
∀ l1 l2 ,
flat_map f (l1 ++ l2) =
flat_map f l1 ++
flat_map f l2.

Lemma disjointPermut(A : Type) :
∀ l1 l2 : list A,
disjoint l1 l2 → disjoint l2 l1.

 Lemma length_diff (A : Type):
 ∀ (l1 l2 :list A), length l1 ≠ length l2 → l1 ≠ l2.

Lemma app_cons_not (A : Type) :
∀ (l1 : list A) l2 a, l1 ++ a :: l2 ≠ l1 ++ l2.