(* Switch Coq into implicit argument mode *)

Global Set Implicit Arguments.

(* Load basic Coq libraries *)

Require Export Omega List Morphisms.

Module Base.

  (* Inversion tactic *)

  Ltac inv H := inversion H; subst; try clear H.

  Lemma size_recursion (X : Type) (sigma : X → nat) (p : X → Type) :
    (∀ x, (∀ y, sigma y < sigma x → p y) → p x) →
    ∀ x, p x.

  Section Iteration.
    Variable X : Type.
    Variable f : X → X.

    Fixpoint it (n : nat) (x : X) : X :=
      match n with
        | 0 ⇒ x
        | S n' ⇒ f (it n' x)
      end.

    Lemma it_ind (p : X → Prop) x n :
      p x → (∀ z, p z → p (f z)) → p (it n x).

    Definition FP (x : X) : Prop := f x = x.

    Lemma it_fp (sigma : X → nat) x :
      (∀ n, FP (it n x) ∨ sigma (it n x) > sigma (it (S n) x)) →
      FP (it (sigma x) x).
  End Iteration.

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

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

  (* Register dec as a type class *)


  Definition decision (X : Prop) (D : dec X) : dec X := D.

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

  (* Hints for auto concerning dec *)

  Hint Extern 4 ⇒
  match goal with
    | [ |- dec ?p ] ⇒ exact (decision p)
  end.

  (* Improves type class inference *)

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

  (* Register instance rules for dec *)

  Global Instance True_dec : dec True :=
    left I.

  Global Instance False_dec : dec False :=
    right (fun A ⇒ A).

  Global Instance impl_dec (X Y : Prop) :
    dec X → dec Y → dec (X → Y).

  Global Instance and_dec (X Y : Prop) :
    dec X → dec Y → dec (X ∧ Y).

  Global Instance or_dec (X Y : Prop) :
    dec X → dec Y → dec (X ∨ Y).

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

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

  Global Instance iff_dec (X Y : Prop) :
    dec X → dec Y → dec (X ↔ Y).

  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.

  Global Instance bool_eq_dec :
    eq_dec bool.

  Global Instance nat_eq_dec :
    eq_dec nat.

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

  (* Notations for lists *)

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

  Hint Unfold equi.

  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).
  Notation "A === B" := (equi A B) (at level 70).

  (* The following comments are for coqdoc *)

  Hint Rewrite <- app_assoc : list.
  Hint Rewrite rev_app_distr map_app prod_length : list.
  (* Print Rewrite HintDb list. *)

  Lemma list_cycle (X : Type) (A : list X) x :
    x::A ≠ A.

  Global Instance list_eq_dec X :
    eq_dec X → eq_dec (list X).

  Global Instance list_in_dec (X : Type) (x : X) (A : list X) :
    eq_dec X → dec (x ∊ A).

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


  Global Instance list_forall_dec X A (p : X → Prop) :
    (∀ x, dec (p x)) → dec (∀ x, x ∊ A → p x).

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

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

  Lemma list_exists_not_incl X (A B : list X) :
    eq_dec X →
    ¬ A ⊆ B → ∃ x, x ∊ A ∧ ¬ x ∊ B.

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

  Hint Resolve in_eq in_nil in_cons in_or_app.

  Section Membership.
    Variable X : Type.
    Implicit Types x y : X.
    Implicit Types A B : list X.

    Lemma in_sing x y :
      x ∊ [y] → x = y.

    Lemma in_cons_neq x y A :
      x ∊ y::A → x ≠ y → x ∊ A.

    Lemma not_in_cons x y A :
      ¬ x ∊ y :: A → x ≠ y ∧ ¬ x ∊ A.

    Definition disjoint A B :=
      ¬ ∃ x, x ∊ A ∧ x ∊ B.

    Lemma disjoint_nil B :
      disjoint nil B.

    Lemma disjoint_nil' A :
      disjoint A nil.

    Lemma disjoint_symm A B :
      disjoint A B → disjoint B A.

    Lemma disjoint_incl A B B' :
      B' ⊆ B → disjoint A B → disjoint A B'.

    Lemma disjoint_forall A B :
      disjoint A B ↔ ∀ x, x ∊ A → ¬ x ∊ B.

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

  Hint Resolve disjoint_nil disjoint_nil'.

  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_sing x A y :
      x::A ⊆ [y] → x = y ∧ A ⊆ [y].

    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.

    Lemma incl_app_left A B C :
      A ++ B ⊆ C → A ⊆ C ∧ B ⊆ C.

  End Inclusion.

  Definition inclp (X : Type) (A : list X) (p : X → Prop) : Prop :=
    ∀ x, x ∊ A → p x.

  Global Instance incl_preorder X :
    PreOrder (@incl X).

  Global Instance equi_Equivalence X :
    Equivalence (@equi X).

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

  Global Instance cons_incl_proper X x :
    Proper (@incl X ==> @incl X) (@cons X x).

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

  Global Instance in_incl_proper X x :
    Proper (@incl X ==> Basics.impl) (@In X x).

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

  Global Instance app_incl_proper X :
    Proper (@incl X ==> @incl X ==> @incl X) (@app X).

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

  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 filter (X : Type) (p : X → Prop) (p_dec : ∀ x, dec (p x)) : list X → list X :=
    fix f A := match A with
                 | nil ⇒ nil
                 | x::A' ⇒ if decision (p x) then x :: f A' else f A'
               end.


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

    Lemma in_filter_iff 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.

    Lemma filter_id A :
      (∀ x, x ∊ A → p x) → filter p A = A.

    Lemma filter_app A B :
      filter p (A ++ B) = filter p A ++ filter p B.

    Lemma filter_fst x A :
      p x → filter p (x::A) = x::filter p A.

    Lemma filter_fst' x A :
      ¬ p x → filter p (x::A) = filter p A.

  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_mono 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.

    Lemma filter_and A :
      filter p (filter q A) = filter (fun x ⇒ p x ∧ q x) A.

  End FilterLemmas_pq.

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

    Lemma filter_comm A :
      filter p (filter q A) = filter q (filter p A).
  End FilterComm.

  Section Removal.
    Variable X : Type.
    Context {eq_X_dec : eq_dec X}.

    Definition rem (A : list X) (x : X) : list X :=
      filter (fun z ⇒ z ≠ x) A.

    Lemma in_rem_iff x A y :
      x ∊ rem A y ↔ x ∊ A ∧ x ≠ y.

    Lemma rem_not_in x y A :
      x = y ∨ ¬ x ∊ A → ¬ x ∊ rem A y.

    Lemma rem_incl A x :
      rem A x ⊆ A.

    Lemma rem_mono A B x :
      A ⊆ B → rem A x ⊆ rem B x.

    Lemma rem_cons A B x :
      A ⊆ B → rem (x::A) x ⊆ B.

    Lemma rem_cons' A B x y :
      x ∊ B → rem A y ⊆ B → rem (x::A) y ⊆ B.

    Lemma rem_in x y A :
      x ∊ rem A y → x ∊ A.

    Lemma rem_neq x y A :
      x ≠ y → x ∊ A → x ∊ rem A y.

    Lemma rem_app x A B :
      x ∊ A → B ⊆ A ++ rem B x.

    Lemma rem_app' x A B C :
      rem A x ⊆ C → rem B x ⊆ C → rem (A ++ B) x ⊆ C.

    Lemma rem_equi x A :
      x::A ≡ x::rem A x.

    Lemma rem_comm A x y :
      rem (rem A x) y = rem (rem A y) x.

    Lemma rem_fst x A :
      rem (x::A) x = rem A x.

    Lemma rem_fst' x y A :
      x ≠ y → rem (x::A) y = x::rem A y.

    Lemma rem_id x A :
      ¬ x ∊ A → rem A x = A.

    Lemma rem_reorder x A :
      x ∊ A → A ≡ x :: rem A x.

    Lemma rem_inclr A B x :
      A ⊆ B → ¬ x ∊ A → A ⊆ rem B x.

  End Removal.

  Hint Resolve rem_not_in rem_incl rem_mono rem_cons rem_cons' rem_app rem_app' rem_in rem_neq rem_inclr.

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

    Fixpoint card A :=
      match A with
        | nil ⇒ 0
        | x::A ⇒ if decision (x ∊ A) then card A else 1 + card A
      end.

    Lemma card_in_rem x A :
      x ∊ A → card A = 1 + card (rem A x).

    Lemma card_not_in_rem A x :
      ¬ x ∊ A → card A = card (rem A x).

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

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

    Lemma card_cons_rem x A :
      card (x::A) = 1 + card (rem A x).

    Lemma card_0 A :
      card A = 0 → A = nil.

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

    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.

  End Cardinality.

  Global Instance card_equi_proper X (D: eq_dec X) :
    Proper (@equi X ==> eq) (@card X D).

  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_cons 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).

    Lemma dupfree_card A (eq_X_dec : eq_dec X) :
      dupfree A → card A = |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_id_equi A :
      undup A ≡ A.

    Lemma dupfree_undup A :
      dupfree (undup A).

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

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

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

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

  End Undup.

  Section PowerRep.
    Variable X : Type.
    Context {eq_X_dec : eq_dec X}.

    Fixpoint power (U : list X ) : list (list X) :=
      match U with
        | nil ⇒ [nil]
        | x :: U' ⇒ power U' ++ map (cons x) (power U')
      end.

    Lemma power_incl A U :
      A ∊ power U → A ⊆ U.

    Lemma power_nil U :
      nil ∊ power U.

    Definition rep (A U : list X) : list X :=
      filter (fun x ⇒ x ∊ A) U.

    Lemma rep_power A U :
      rep A U ∊ power U.

    Lemma rep_incl A U :
      rep A U ⊆ A.

    Lemma rep_in x A U :
      A ⊆ U → x ∊ A → x ∊ rep A U.

    Lemma rep_equi A U :
      A ⊆ U → rep A U ≡ A.

    Lemma rep_mono A B U :
      A ⊆ B → rep A U ⊆ rep B U.

    Lemma rep_eq' A B U :
      (∀ x, x ∊ U → (x ∊ A ↔ x ∊ B)) → rep A U = rep B U.

    Lemma rep_eq A B U :
      A ≡ B → rep A U = rep B U.

    Lemma rep_injective A B U :
      A ⊆ U → B ⊆ U → rep A U = rep B U → A ≡ B.

    Lemma rep_idempotent A U :
      rep (rep A U) U = rep A U.

    Lemma dupfree_power U :
      dupfree U → dupfree (power U).

    Lemma dupfree_in_power U A :
      A ∊ power U → dupfree U → dupfree A.

    Lemma rep_dupfree A U :
      dupfree U → A ∊ power U → rep A U = A.

    Lemma power_extensional A B U :
      dupfree U → A ∊ power U → B ∊ power U → A ≡ B → A = B.

  End PowerRep.

  Module FCI.
    Section FCI.
      Variable X : Type.
      Context {eq_X_dec : eq_dec X}.
      Variable step : list X → X → Prop.
      Context {step_dec : ∀ A x, dec (step A x)}.
      Variable V : list X.

      Lemma pick (A : list X) :
        { x | x ∊ V ∧ step A x ∧ ¬ x ∊ A } + { ∀ x, x ∊ V → step A x → x ∊ A }.

      Definition F (A : list X) : list X.
      Defined.

      Definition C := it F (card V) nil.

      Lemma it_incl n :
        it F n nil ⊆ V.

      Lemma incl :
        C ⊆ V.

      Lemma ind p :
        (∀ A x, inclp A p → x ∊ V → step A x → p x) → inclp C p.

      Lemma fp :
        F C = C.

      Lemma closure x :
        x ∊ V → step C x → x ∊ C.

    End FCI.

  End FCI.

  Definition dupfree_inv := dupfree_cons.
  Ltac dupapply H1 lemma H2 := pose (H2:= H1) ; apply lemma in H2.

End Base.