Global Set Implicit Arguments. 
Global Unset Strict Implicit.

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

(** printing el #∊# *)
(** printing <<= #⊆# *)

(** * Membership

We use the following facts from the standard library List.
- [in_eq :  x el x::A]
- [in_nil :  ~ x el nil]
- [in_cons :  x el A -> x el y::A]
- [in_or_app :  x el A \/ x el B -> x el A++B]
- [in_app_iff :  x el A++B <-> x el A \/ x el B]
- [in_map_iff :  y el map f A <-> exists x, f x = y /\ x el A]
*)

Hint Resolve in_eq in_nil in_cons in_or_app.

Lemma in_sing X (x y : X) :
  x el [y] -> x = y.

Proof. simpl. intros [[]|[]]. reflexivity. Qed.

Lemma in_cons_neq X (x y : X) A :
  x el y::A -> x <> y -> x el A.

Proof. simpl. intros [[]|D] E ; congruence. Qed.

Definition disjoint (X : Type) (A B : list X) :=
  ~ exists x, x el A /\ x el B.

Lemma disjoint_forall X (A B : list X) :
  disjoint A B <-> forall x, x el A -> ~ x el B.

Proof.
  split.
  - intros D x E F. apply D. exists x. auto.
  - intros D [x [E F]]. exact (D x E F).
Qed.
  
Lemma disjoint_cons X (x : X) A B :
  disjoint (x::A) B <-> ~ x el B /\ disjoint A B.

Proof.
  split.
  - intros D. split.
    + intros E. apply D. eauto.
    + intros [y [E F]]. apply D. eauto.
  - intros [D E] [y [[F|F] G]]. 
    + congruence.
    + apply E. eauto.
Qed.

(** * Inclusion

We use the following facts from the standard library List.
- [A <<= B = forall y, x el A -> x el B]
- [incl_refl :  A <<= A]
- [incl_tl :  A <<= B -> A <<= x::B]
- [incl_cons : x el B -> A <<= B -> x::A <<= B]
- [incl_appl : A <<= B -> A <<= B++C]
- [incl_appr : A <<= C -> A <<= B++C]
- [incl_app : A <<= C -> B <<= C -> A++B <<= C]
*)

Hint Resolve incl_refl incl_tl incl_cons incl_appl incl_appr incl_app.

Lemma incl_nil X (A : list X) :
  nil <<= A.

Proof. intros x []. Qed.

Hint Resolve incl_nil.

Lemma incl_map X Y A B (f : X -> Y) :
  A <<= B -> map f A <<= map f B.

Proof.
  intros D y E. apply in_map_iff in E as [x [E E']].
  subst y. apply in_map_iff. eauto.
Qed.

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

  Lemma incl_nil_eq A :
    A <<= nil -> A=nil.

  Proof.
    intros D. destruct A as [|x A].
    - reflexivity.
    - exfalso. apply (D x). auto.
  Qed.

  Lemma incl_shift x A B :
    A <<= B -> x::A <<= x::B.

  Proof. intros D y E. destruct E ; subst ; auto. Qed.

  Lemma incl_lcons x A B :
    x::A <<= B <-> x el B /\ A <<= B.

  Proof. 
    split. 
    - intros D. split ; hnf ; auto.
    - intros [D E] z [F|F] ; subst ; auto.
  Qed.

  Lemma incl_rcons x A B :
    A <<= x::B -> ~ x el A -> A <<= B.

  Proof. intros C D y E. destruct (C y E) as [F|F] ; congruence. Qed.

  Lemma incl_lrcons x A B :
    x::A <<= x::B -> ~ x el A -> A <<= B.

  Proof.
    intros C D y E.
    assert (F: y el x::B) by auto.
    destruct F as [F|F] ; congruence.
  Qed.

End Inclusion.

(** * Equivalence *)

Definition equi X (A B : list X) : Prop :=
  A <<= B /\ B <<= A.

Notation "A === B" := (equi A B) (at level 70).
(** printing === #≡# *)

Hint Unfold equi.

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

  Lemma equi_push x A :
    x el A -> A === x::A.

  Proof. auto. Qed.

  Lemma equi_dup x A :
    x::A === x::x::A.

  Proof. auto. Qed.

  Lemma equi_swap x y A:
    x::y::A === y::x::A.

  Proof. split ; intros z ; simpl ; tauto. Qed.

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

  Proof. 
    split ; intros y.
    - intros [D|D].
      + subst ; auto.
      + apply in_app_iff in D as [D|D] ; auto.
    - intros D. apply in_app_iff in D as [D|D].
      + auto.
      + destruct D ; subst ; auto.
  Qed.

  Lemma equi_rotate x A :
    x::A === A++[x].
  
  Proof. 
    split ; intros y ; simpl.
    - intros [D|D] ; subst ; auto.
    - intros D. apply in_app_iff in D as [D|D].
      + auto.
      + apply in_sing in D. auto.
  Qed.
End Equi.

(** * Automatic Decision Inference *)

Definition dec (X : Prop) : Type := {X} + {~ X}.
Definition decision (X : Prop) (D : dec X) : dec X := D.
Arguments decision X {D}.
Existing Class dec.

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

Definition eq_list_dec (X : Type) :  
  (forall x y : X, dec (x=y)) -> forall A B : list X, dec (A = B).
  intros D. apply list_eq_dec. exact D. 
Defined.

Existing Instance eq_nat_Dec.
Existing Instance eq_list_dec.

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

Instance in_Dec (X : Type) (x : X) (A : list X) :  eq_dec X -> dec (x el A).
  intros D. apply in_dec. exact D.
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).
Proof. unfold dec ; tauto. Qed.
Instance and_dec (X Y : Prop) :  dec X -> dec Y -> dec (X /\ Y).
Proof. unfold dec ; tauto. Qed.
Instance or_dec (X Y : Prop) :  dec X -> dec Y -> dec (X \/ Y).
Proof. unfold dec ; tauto. Qed.

(* 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).
Proof. intros D. exact (decision (X -> False)). Qed.

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.

Proof. unfold dec ; tauto. Qed.

Lemma dec_DM_and X Y :  
  dec X -> dec Y -> ~ (X /\ Y) -> ~ X \/ ~ Y.

Proof. unfold dec ; tauto. Qed.

Lemma dec_DM_impl X Y :  
  dec X -> dec Y -> ~ (X -> Y) -> X /\ ~ Y.

Proof. unfold dec ; tauto. Qed.

Lemma dec_prop_iff (X Y : Prop) : 
  (X <-> Y) -> dec X -> dec Y.

Proof.
  intros A [B|B]. 
  - left. tauto.
  - right. tauto.
Qed.

(** * List Quantification *)

Lemma sigma_forall_list X A (p : X -> Prop) (p_dec : forall x, dec (p x)) :
  {x | x el A /\ ~ p x} + {forall x, x el A -> p x}.
  
Proof.
  induction A as [|x A] ; simpl.
  - right. tauto.
  - destruct IHA as [[y [D E]]|D].
    + left. eauto. 
    + destruct (p_dec x) as [E|E].
      * right. intros y [[]|F] ; auto.
      * left. eauto.
Qed.

Arguments sigma_forall_list {X} A p {p_dec}.

Instance forall_list_dec X A (p : X -> Prop) (p_dec : forall x, dec (p x)) :
  dec (forall x, x el A -> p x).

Proof.
  destruct (sigma_forall_list A p) as [[x [D E]]|D] 
  ; unfold dec ; auto.
Qed.

Instance exists_list_dec X A (p : X -> Prop) (p_dec : forall x, dec (p x)) :
  dec (exists x, x el A /\ p x).

Proof.
  destruct (sigma_forall_list A (fun x => ~ p x)) as [[x [D E]]|D].
  - left. apply dec_DN in E ; eauto.
  - right. intros [x [E F]]. exact (D x E F).
Qed.

Lemma dec_DM_forall X A  (p : X -> Prop) : 
  (forall x, dec (p x)) ->
  ~ (forall x, x el A -> p x) -> exists x, x el A /\ ~ p x.

Proof. 
  intros D E. destruct (sigma_forall_list A p) as [F|F].
  + destruct F as [x F]. eauto.
  + contradiction (E F).
Qed.

Lemma dec_cc X (p : X -> Prop) A : 
  eq_dec X -> (forall x, dec (p x)) -> 
  (exists x, x el A /\ p x) -> {x | x el A /\ p x}.

Proof.
  intros D E. 
  destruct (sigma_forall_list A (fun x => ~ p x)) as [[x [F G]]|F].
  - intros _. exists x. apply dec_DN in G ; auto.
  - intros G. exfalso. destruct G as [x [G H]]. exact (F x G H).
Qed.

(** * Filter *)

Section Filter.
  Variable X : Type.
  Variable p : X -> Prop.
  Variable p_dec : forall 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.

Arguments filter {X} p {_} _.

Section FilterLemmas.
  Variable X : Type.
  Variable p : X -> Prop.
  Context {p_dec : forall x, dec (p x)}.

  Lemma in_filter x A :
    x el filter p A <-> x el A /\ p x.
    
  Proof. 
    induction A as [|y A] ; simpl.
    - tauto.
    - decide (p y) as [B|B] ; simpl ; split.
      + intros [C|C] ; subst ; tauto.
      + tauto.
      + tauto.
      + intros [[[]|C] D] ; tauto.
  Qed.

  Lemma filter_incl A :
    filter p A <<= A.
  
  Proof.
    intros x D. apply in_filter in D. apply D.
  Qed.

  Lemma filter_mono A B :
    A <<= B -> filter p A <<= filter p B.

  Proof.
    intros D x E. apply in_filter in E as [E E'].
    apply in_filter. auto.
  Qed.

End FilterLemmas.

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

  Lemma filter_pq_incl A :
    (forall x, x el A -> p x -> q x) -> filter p A <<= filter q A.

  Proof. 
    intros D x E. apply in_filter in E as [E E'].
    apply in_filter. auto.
  Qed.

  Lemma filter_pq_eq A :
    (forall x, x el A -> (p x <-> q x)) -> filter p A = filter q A.

  Proof. 
    intros C ; induction A as [|x A] ; simpl.
    - reflexivity.
    - decide (p x) as [D|D] ; decide (q x) as [E|E].
      + f_equal. auto.
      + exfalso. apply E, (C x) ; auto.
      + exfalso. apply D, (C x) ; auto.
      + auto.
  Qed.

End FilterLemmas_pq.

Lemma separation X A p (D : forall x : X, dec (p x)) :
  {B | forall x, x el B <-> x el A /\ p x}.

Proof. exists (filter p A). intros x. apply in_filter. Qed.

(** * Setoid Rewriting *)

Instance equi_Equivalence X : Equivalence (@equi X).

Proof. constructor ; hnf ; firstorder. Qed.

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

Proof. hnf. intros x y []. hnf. firstorder. Qed.

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

Proof. 
  hnf. intros A B D. hnf. intros A' B' E.
  destruct D, E ; auto.
Qed.

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

Proof. hnf. intros x y []. hnf. firstorder. Qed.

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

Proof. hnf. intros x y D. hnf. firstorder. Qed.

Instance incl_preorder X : PreOrder (@incl X).

Proof. constructor ; hnf ; unfold incl ; auto. Qed.

(** * Duplicate-free lists *)

Inductive dupfree (X : Type) : list X -> Prop :=
| dupfreeN : dupfree nil
| dupfreeC x A : ~ x el 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 el A /\ dupfree A.

  Proof. intros D. inversion D ; subst ; auto. Qed.

  Lemma dupfree_app A B :
    disjoint A B -> dupfree A -> dupfree B -> dupfree (A++B).

  Proof.
    intros D E F. induction E as [|x A E' E] ; simpl.
    - exact F.
    -  apply disjoint_cons in D as [D D'].
       constructor ; [|exact (IHE D')].
       intros G. apply in_app_iff in G ; tauto.
  Qed.

  Lemma dupfree_map Y A (f : X -> Y) :
    (forall x y, x el A -> y el A -> f x = f y -> x=y) -> 
    dupfree A -> dupfree (map f A).

  Proof.
    intros D E. induction E as [|x A E' E] ; simpl.
    - constructor.
    - constructor ; [|now auto].
      intros F. apply in_map_iff in F as [y [F F']].
      rewrite (D y x) in F' ; auto.
  Qed.

  Lemma dupfree_filter p (p_dec : forall x, dec (p x)) A :
    dupfree A -> dupfree (filter p A).

  Proof.
    intros D. induction D as [|x A C D] ; simpl.
    - left.
    - decide (p x) as [E|E] ; [|exact IHD].
      right ; [|exact IHD].
      intros F. apply C. apply filter_incl in F. exact F.
   Qed.

  Lemma dupfree_dec A :
    eq_dec X -> dec (dupfree A).

  Proof.
    intros D. induction A as [|x A].
    - left. left.
    - decide (x el A) as [E|E].
      + right. intros F. remember (x::A) as B. destruct F ; congruence.
      + destruct (IHA) as [F|F].
        * left. right ; assumption.
        * right. intros G. apply F.
          remember (x::A) as B. destruct G ; congruence.
  Qed.

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 el A') then undup A' else  x :: undup A'
    end.

  Lemma undup_equi A :
    undup A === A.

  Proof.
    induction A as [|x A] ; simpl.
    - reflexivity.
    - decide (x el A) as [E|E].
      + setoid_rewrite IHA. apply equi_push, E.
      + setoid_rewrite IHA. reflexivity.
  Qed.

  Lemma undup_dupfree A :
    dupfree (undup A).

  Proof.
    induction A as [|x A] ; simpl.
    - left.
    - decide (x el A) as [E|E]. 
      + exact IHA.
      + right.
        * setoid_rewrite undup_equi. exact E.
        * exact IHA.
  Qed.

  Lemma undup_homo A B :
    A <<= B <-> undup A <<= undup B.

  Proof.
    setoid_rewrite (undup_equi A). setoid_rewrite (undup_equi B).
    reflexivity.
  Qed.

  Lemma undup_iso A B :
    A === B <-> undup A === undup B.

  Proof.
    setoid_rewrite (undup_equi A). setoid_rewrite (undup_equi B).
    reflexivity.
  Qed.

  Lemma undup_eq A :
    dupfree A -> undup A = A.

  Proof.
    intros E. induction E as [|x A E F] ; simpl.
    - reflexivity.
    - decide (x el A) as [G|G].
      + contradiction (E G).
      + f_equal. exact IHF.
  Qed.

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

  Proof. apply undup_eq. apply undup_dupfree. Qed.

End Undup.

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

  Lemma dupfree_reorder A x :
    dupfree A -> x el A -> 
    exists A', A === x::A' /\ |A'| < |A| /\ dupfree (x::A').

  Proof.
    intros E. revert x. induction E as [|y A H] ; intros x F.
    - contradiction F.
    - destruct F as [F|F].
      + subst y. exists A. auto using dupfree. 
      + specialize (IHE x F). destruct IHE as [A' [G [K1 K2]]].
        exists (y::A'). split ; [|split].
        * setoid_rewrite G. apply equi_swap.
        * simpl. omega.
        * { apply dupfree_inv in K2 as [K2 K3]. right. 
            - intros [M|M] ; subst ; auto.
            - right ; [|exact K3].
              intros M ; apply H. apply G. auto. }
   Qed.

  Lemma dupfree_le A B :
    dupfree A -> dupfree B -> A <<= B -> |A| <= |B|.

  Proof. 
    intros E ; revert B.
    induction A as [|x A] ; simpl ; intros B F G.
    - omega.
    - apply incl_lcons in G as [G H]. 
      destruct (dupfree_reorder F G) as [B' [K [L M]]].
      apply dupfree_inv in E as [E1 E2].
      apply dupfree_inv in M as [M1 M2].
      cut (A <<= B').
      { intros N. specialize (IHA E2 B' M2 N). omega. }
      apply incl_rcons with (x:=x) ; [|exact E1].
      setoid_rewrite H. apply K.
  Qed.

  Lemma dupfree_eq A B :
    dupfree A -> dupfree B -> A === B -> |A|=|B|.

  Proof. 
    intros D E [F G]. 
    apply (dupfree_le D E) in F. 
    apply (dupfree_le E D) in G. 
    omega.
  Qed.

  Lemma dupfree_lt A B x :
    dupfree A -> dupfree B -> A <<= B -> 
    x el B -> ~ x el A  -> |A| < |B|.

  Proof.
    intros E F G H K.
    destruct (dupfree_reorder F H) as [B' [L [M N]]].
    rewrite (dupfree_eq F N L). 
    cut (|A|<=|B'|). { simpl ; omega. }
    apply dupfree_le.
    - exact E.
    - apply (dupfree_inv N).
    - apply incl_rcons with (x:=x).
      + setoid_rewrite G. apply  L.
      + exact K.
  Qed.

  Lemma dupfree_ex A B :
    eq_dec X -> dupfree A -> dupfree B -> |A| < |B| -> exists x, x el B /\ ~ x el A.

  Proof.
    intros D E F H.
    destruct (sigma_forall_list B (fun x => x el A)) as [[x K]|K].
    - exists x ; exact K.
    - exfalso. apply dupfree_le in K ; auto ; omega.
  Qed.


  Lemma dupfree_equi A B :
    eq_dec X -> dupfree A -> dupfree B -> A <<= B -> |A|=|B| -> A === B.

  Proof.
    intros C D E F G. split. exact F.
    destruct (sigma_forall_list B (fun x => x el A)) as [[x [H K]]|H].
    - exfalso. assert (L:=dupfree_lt D E F H K). omega.
    - exact H.
  Qed.

End DupfreeLength.

(** * Cardinality *)

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.

  Proof.
    intros E. apply dupfree_le.
    - apply undup_dupfree. 
    - apply undup_dupfree.
    - apply undup_homo, E.
  Qed.

  Lemma card_eq A B :
    A === B -> card A = card B.

  Proof.
    intros [E F]. apply card_le in E. apply card_le in F. omega.
  Qed.

  Lemma card_equi A B :
    A <<= B -> card A = card B -> A === B.

  Proof.
    intros D E. apply <- undup_iso. 
    apply dupfree_equi.
    - exact eq_X_dec.
    - apply undup_dupfree.
    - apply undup_dupfree.
    - apply undup_homo, D.
    - exact E.
  Qed.   

  Lemma card_lt A B x :
    A <<= B -> x el B -> ~ x el A -> card A < card B.

  Proof.
    intros D E F.
    apply (dupfree_lt (A:= undup A) (B:= undup B) (x:=x)).
    - apply undup_dupfree.
    - apply undup_dupfree.
    - apply undup_homo, D.
    - apply undup_equi, E.
    - setoid_rewrite undup_equi. exact F.
  Qed.

  Lemma card_or A B :
    A <<= B -> A === B \/ card A < card B.

  Proof.
    intros D. assert (F:= card_le D).
    apply le_lt_eq_dec in F as [F|F].
    - auto.
    - left. exact (card_equi D F).
  Qed.

  Lemma card_ex A B :
    card A < card B -> exists x, x el B /\ ~ x el A.

  Proof.
    intros E.
    destruct (dupfree_ex (A:=undup A) (B:=undup B)) as [x F].
    - exact eq_X_dec.
    - apply undup_dupfree.
    - apply undup_dupfree.
    - exact E.
    - exists x. setoid_rewrite undup_equi in F. exact F.
  Qed.

End Cardinality.