Global Set Implicit Arguments.
Global
Require Export Omega List Morphisms.

Export ListNotations.
Notation "| A |" := (length A) (at level 65).
Notation "x 'el' A" := (In x A) (at level 70).
Notation "A <<= B" := (incl A B) (at level 70).

Hint Resolve in_eq in_nil in_cons in_or_app.

Lemma in_sing X (x y : X) :
  x ∊ [y] → x = y.

Lemma in_cons_neq X (x y : X) A :
  x ∊ y::A → x ≠ y → x ∊ A.

Definition disjoint (X : Type) (A B : list X) :=
  ¬ ∃ x, x ∊ A ∧ x ∊ B.

Lemma disjoint_forall X (A B : list X) :
  disjoint A B ↔ ∀ x, x ∊ A → ¬ x ∊ B.

Lemma disjoint_cons X (x : X) A B :
  disjoint (x::A) B ↔ ¬ x ∊ B ∧ disjoint A B.

Hint Resolve incl_refl incl_tl incl_cons incl_appl incl_appr incl_app.

Lemma incl_nil X (A : list X) :
  nil ⊆ A.

Hint Resolve incl_nil.

Lemma incl_map X Y A B (f : X → Y) :
  A ⊆ B → map f A ⊆ map f B.

Section Inclusion.
  Variable X : Type.
  Implicit Types A B : list X.

  Lemma incl_nil_eq A :
    A ⊆ nil → A=nil.

  Lemma incl_shift x A B :
    A ⊆ B → x::A ⊆ x::B.

  Lemma incl_lcons x A B :
    x::A ⊆ B ↔ x ∊ B ∧ A ⊆ B.

  Lemma incl_rcons x A B :
    A ⊆ x::B → ¬ x ∊ A → A ⊆ B.

  Lemma incl_lrcons x A B :
    x::A ⊆ x::B → ¬ x ∊ A → A ⊆ B.

End Inclusion.

Definition equi X (A B : list X) : Prop :=
  A ⊆ B ∧ B ⊆ A.

Notation "A === B" := (equi A B) (at level 70).

Hint Unfold equi.

Section Equi.
  Variable X : Type.
  Implicit Types A B : list X.

  Lemma equi_push x A :
    x ∊ A → A ≡ x::A.

  Lemma equi_dup x A :
    x::A ≡ x::x::A.

  Lemma equi_swap x y A:
    x::y::A ≡ y::x::A.

  Lemma equi_shift x A B :
    x::A++B ≡ A++x::B.

  Lemma equi_rotate x A :
    x::A ≡ A++[x].
End Equi.

Definition dec (X : Prop) : Type := {X} + {¬ X}.
Definition decision (X : Prop) (D : dec X) : dec X := D.

Definition eq_nat_Dec (x y : nat) : dec (x = y) :=
  eq_nat_dec x y.

Definition eq_list_dec (X : Type) :
  (∀ x y : X, dec (x=y)) → ∀ A B : list X, dec (A = B).
Defined.


Notation "'eq_dec' X" := (∀ x y : X, dec (x=y)) (at level 70).

Instance in_Dec (X : Type) (x : X) (A : list X) : eq_dec X → dec (x ∊ A).
Defined.

Instance le_Dec (x y : nat) : dec (x ≤ y) :=
  le_dec x y.

Instance True_dec : dec True :=
  left I.
Instance False_dec : dec False :=
  right (fun A ⇒ A).
Instance impl_dec (X Y : Prop) : dec X → dec Y → dec (X → Y).
Instance and_dec (X Y : Prop) : dec X → dec Y → dec (X ∧ Y).
Instance or_dec (X Y : Prop) : dec X → dec Y → dec (X ∨ Y).

(* Standard modules make "not" and "iff" opaque for type class inference, can be seen with Print HintDb typeclass_instances. *)

Instance not_dec (X : Prop) : dec X → dec (¬ X).

Hint Unfold dec.

Tactic Notation "decide" constr(p) :=
  destruct (decision p).
Tactic Notation "decide" constr(p) "as" simple_intropattern(i) :=
  destruct (decision p) as i.

Tactic Notation "decide" "claim" :=
  match goal with
    | |- dec (?p) ⇒ exact (decision p)
  end.

Hint Extern 4 ⇒
match goal with
  | [ |- dec ((fun _ ⇒ _) _) ] ⇒ simpl
end : typeclass_instances.

Lemma dec_DN X :
  dec X → ~~ X → X.

Lemma dec_DM_and X Y :
  dec X → dec Y → ¬ (X ∧ Y) → ¬ X ∨ ¬ Y.

Lemma dec_DM_impl X Y :
  dec X → dec Y → ¬ (X → Y) → X ∧ ¬ Y.

Lemma dec_prop_iff (X Y : Prop) :
  (X ↔ Y) → dec X → dec Y.

Lemma sigma_forall_list X A (p : X → Prop) (p_dec : ∀ x, dec (p x)) :
  {x | x ∊ A ∧ ¬ p x} + {∀ x, x ∊ A → p x}.


Instance forall_list_dec X A (p : X → Prop) (p_dec : ∀ x, dec (p x)) :
  dec (∀ x, x ∊ A → p x).


Instance exists_list_dec X A (p : X → Prop) (p_dec : ∀ x, dec (p x)) :
  dec (∃ x, x ∊ A ∧ p x).


Lemma dec_DM_forall X A (p : X → Prop) :
  (∀ x, dec (p x)) →
  ¬ (∀ x, x ∊ A → p x) → ∃ x, x ∊ A ∧ ¬ p x.

Lemma dec_cc X (p : X → Prop) A :
  eq_dec X → (∀ x, dec (p x)) →
  (∃ x, x ∊ A ∧ p x) → {x | x ∊ A ∧ p x}.

Section Filter.
  Variable X : Type.
  Variable p : X → Prop.
  Variable p_dec : ∀ x, dec (p x).
  Fixpoint filter (A : list X) : list X :=
    match A with
      | nil ⇒ nil
      | x::A' ⇒ if decision (p x) then x :: filter A' else filter A'
    end.
End Filter.


Section FilterLemmas.
  Variable X : Type.
  Variable p : X → Prop.
  Context {p_dec : ∀ x, dec (p x)}.

  Lemma in_filter x A :
    x ∊ filter p A ↔ x ∊ A ∧ p x.

  Lemma filter_incl A :
    filter p A ⊆ A.

  Lemma filter_mono A B :
    A ⊆ B → filter p A ⊆ filter p B.

End FilterLemmas.

Section FilterLemmas_pq.
  Variable X : Type.
  Variable p q : X → Prop.
  Context {p_dec : ∀ x, dec (p x)}.
  Context {q_dec : ∀ x, dec (q x)}.

  Lemma filter_pq_incl A :
    (∀ x, x ∊ A → p x → q x) → filter p A ⊆ filter q A.

  Lemma filter_pq_eq A :
    (∀ x, x ∊ A → (p x ↔ q x)) → filter p A = filter q A.

End FilterLemmas_pq.

Lemma separation X A p (D : ∀ x : X, dec (p x)) :
  {B | ∀ x, x ∊ B ↔ x ∊ A ∧ p x}.

Instance equi_Equivalence X : Equivalence (@equi X).


Instance cons_equi_proper X :
  Proper (eq ==> @equi X ==> @equi X) (@cons X).


Instance app_equi_proper X :
  Proper (@equi X ==> @equi X ==> @equi X) (@app X).


Instance in_equi_proper X :
  Proper (eq ==> @equi X ==> iff) (@In X).


Instance incl_equi_proper X :
  Proper (@equi X ==> @equi X ==> iff) (@incl X).


Instance incl_preorder X : PreOrder (@incl X).

Inductive dupfree (X : Type) : list X → Prop :=
| dupfreeN : dupfree nil
| dupfreeC x A : ¬ x ∊ A → dupfree A → dupfree (x::A).

Section Dupfree.
  Variable X : Type.
  Implicit Types A B : list X.

  Lemma dupfree_inv x A :
    dupfree (x::A) → ¬x ∊ A ∧ dupfree A.

  Lemma dupfree_app A B :
    disjoint A B → dupfree A → dupfree B → dupfree (A++B).

  Lemma dupfree_map Y A (f : X → Y) :
    (∀ x y, x ∊ A → y ∊ A → f x = f y → x=y) →
    dupfree A → dupfree (map f A).

  Lemma dupfree_filter p (p_dec : ∀ x, dec (p x)) A :
    dupfree A → dupfree (filter p A).

  Lemma dupfree_dec A :
    eq_dec X → dec (dupfree A).

End Dupfree.

Section Undup.
  Variable X : Type.
  Context {eq_X_dec : eq_dec X}.
  Implicit Types A B : list X.

  Fixpoint undup (A : list X) : list X :=
    match A with
      | nil ⇒ nil
      | x::A' ⇒ if decision (x ∊ A') then undup A' else x :: undup A'
    end.

  Lemma undup_equi A :
    undup A ≡ A.

  Lemma undup_dupfree A :
    dupfree (undup A).

  Lemma undup_homo A B :
    A ⊆ B ↔ undup A ⊆ undup B.

  Lemma undup_iso A B :
    A ≡ B ↔ undup A ≡ undup B.

  Lemma undup_eq A :
    dupfree A → undup A = A.

  Lemma undup_idempotent A :
    undup (undup A) = undup A.

End Undup.

Section DupfreeLength.
  Variable X : Type.
  Implicit Types A B : list X.

  Lemma dupfree_reorder A x :
    dupfree A → x ∊ A →
    ∃ A', A ≡ x::A' ∧ |A'| < |A| ∧ dupfree (x::A').
  Lemma dupfree_le A B :
    dupfree A → dupfree B → A ⊆ B → |A| ≤ |B|.

  Lemma dupfree_eq A B :
    dupfree A → dupfree B → A ≡ B → |A|=|B|.

  Lemma dupfree_lt A B x :
    dupfree A → dupfree B → A ⊆ B →
    x ∊ B → ¬ x ∊ A → |A| < |B|.

  Lemma dupfree_ex A B :
    eq_dec X → dupfree A → dupfree B → |A| < |B| → ∃ x, x ∊ B ∧ ¬ x ∊ A.

  Lemma dupfree_equi A B :
    eq_dec X → dupfree A → dupfree B → A ⊆ B → |A|=|B| → A ≡ B.

End DupfreeLength.

Section Cardinality.
  Variable X : Type.
  Context {eq_X_dec : eq_dec X}.
  Implicit Types A B : list X.

  Definition card (A : list X) : nat := |undup A|.

  Lemma card_le A B :
    A ⊆ B → card A ≤ card B.

  Lemma card_eq A B :
    A ≡ B → card A = card B.

  Lemma card_equi A B :
    A ⊆ B → card A = card B → A ≡ B.

  Lemma card_lt A B x :
    A ⊆ B → x ∊ B → ¬ x ∊ A → card A < card B.

  Lemma card_or A B :
    A ⊆ B → A ≡ B ∨ card A < card B.

  Lemma card_ex A B :
    card A < card B → ∃ x, x ∊ B ∧ ¬ x ∊ A.

End Cardinality.