Set Implicit Arguments.
Require Import List Omega Morphisms FinFun Init.Wf decidable.
Import ListNotations.

Arguments incl {_} _ _.
Definition seteq {X: Type} (A B: list X) := incl A B /\ incl B A.
Definition strict_incl {X: Type} (A B: list X) :=
  incl A B /\ exists x, In x B /\ ~ In x A.
Notation "a ∈ A" := (In a A) (at level 70).
Notation "A ⊆ B" := (incl A B) (at level 70).
Notation "A ⊊ B" := (strict_incl A B) (at level 70).
Notation "A === B" := (seteq A B) (at level 70).
Notation "| A |" := (length A) (at level 65).


Section BasicLemmas.

  Variable X Y: Type.

  Implicit Type f: X -> Y.
  Implicit Type p: X -> bool.
  Implicit Type A B C : list X.
  Implicit Type a b c : X. 


  Lemma incl_refl A: A ⊆ A.
  Proof. firstorder. Qed.

  Lemma incl_trans A B C: A ⊆ B -> B ⊆ C -> A ⊆ C.
  Proof. firstorder. Qed.

  Lemma strict_incl_trans A B C: A ⊊ B -> B ⊊ C -> A ⊊ C.
  Proof. firstorder. Qed.

  Lemma strict_incl_incl_trans A B C: A ⊊ B -> B ⊆ C -> A ⊊ C.
  Proof. firstorder. Qed.

  Lemma incl_strict_incl_trans A B C: A ⊆ B -> B ⊊ C -> A ⊊ C.
  Proof. firstorder. Qed.


  Lemma seteq_refl A: A === A.
  Proof. firstorder. Qed.

  Lemma seteq_trans A B C: A === B -> B === C -> A === C.
  Proof. firstorder. Qed.

  Lemma seteq_sym A B: A === B -> B === A.
  Proof. firstorder. Qed.

  
  Global Instance incl_preorder: PreOrder (@incl X). 
  Proof. firstorder. Qed.

  Global Instance strict_incl_transitive: Transitive (@strict_incl X).
  Proof. firstorder. Qed.

  Global Instance seteq_preorder: PreOrder (@seteq X).
  Proof. firstorder. Qed.

  Global Instance seteq_equivalence: Equivalence (@seteq X).
  Proof. firstorder. Qed.

  Hint Resolve incl_refl seteq_refl : listdb.





 


  (* ∈ *)
  Lemma in_ind e (P: list X -> Prop):
    (forall A, P (e :: A)) -> (forall a A, P A -> P (a :: A)) -> forall A, e ∈ A -> P A.
  Proof.
    intros BH IH; induction A; cbn;
      intuition; subst; intuition.
  Qed.

  Global Instance proper_in_incl: Proper (eq ++> incl ==> Basics.impl) (@In X).
  Proof.
    intros ?? -> ???. firstorder.   
  Qed.

  Global Instance in_seteq_proper: Proper (eq ++> seteq ++> iff) (@In X).
  Proof.
    intros ?? -> ???. firstorder.
  Qed.


  (* ⊆ *)
  Global Instance subrel_incl_seteq: subrelation seteq (@incl X).
  Proof. intros ??; firstorder. Qed.

  Global Instance incl_seteq_proper: Proper (seteq ++> seteq ++> iff) (@incl X).
  Proof. firstorder. Qed.

  
  Lemma incl_app A B C: A ++ B ⊆ C <-> A ⊆ C /\ B ⊆ C.
  Proof. induction A; firstorder. Qed.

  Lemma seteq_incl_left A B: A === B -> A ⊆ B.
  Proof. firstorder. Qed.

  Lemma seteq_incl_right A B: A === B -> B ⊆ A.
  Proof. firstorder. Qed.
  
  Lemma incl_seteq A B: A ⊆ B -> B ⊆ A -> A === B.
  Proof. firstorder. Qed.


  Lemma incl_nil A: nil ⊆ A.
  Proof. intros x []. Qed.

  Lemma incl_cons a A B: a :: A ⊆ B <-> a ∈ B /\ A ⊆ B.
  Proof. split; unfold incl; firstorder; congruence. Qed.

  Lemma incl_cons_build a A B: a ∈ B -> A ⊆ B -> a :: A ⊆ B.
  Proof. intuition. Qed.

  Lemma incl_cons_project_l a A B: a :: A ⊆ B -> a ∈ B.
  Proof. intuition. Qed.

  Lemma incl_cons_project_r a A B: a :: A ⊆ B -> A ⊆ B.
  Proof. firstorder. Qed.


  Lemma incl_cons_drop b A B : A ⊆ B -> A ⊆ b :: B.
  Proof. firstorder. Qed.
  
  Lemma incl_filter p A: filter p A ⊆ A.
  Proof. induction A as [|a A]; cbn; try destruct (p a); firstorder. Qed.


  Lemma incl_distr_left A B C: A ⊆ B -> A ⊆ B ++ C.
  Proof. firstorder. Qed.

  Lemma incl_distr_right A B C: A ⊆ C -> A ⊆ B ++ C. 
  Proof. firstorder.  Qed.

  Lemma incl_app_project_left A B C: A ++ B ⊆ C -> A ⊆ C.
  Proof. firstorder. Qed. 

  Lemma incl_app_project_right A B C: A ++ B ⊆ C -> B ⊆ C.
  Proof. firstorder. Qed.

  Lemma incl_app_build A B C: A ⊆ C -> B ⊆ C -> A ++ B ⊆ C.
  Proof. intros; eapply incl_app; intuition. Qed.


  Global Instance incl_cons_proper: Proper (eq ++> incl ++> incl) (@cons X).
  Proof. intros ??-> ???; firstorder. Qed.

  Global Instance seteq_cons_proper: Proper (eq ++> seteq ++> seteq) (@cons X).
  Proof. intros ??-> ???; firstorder. Qed.

 
  
  Hint Resolve incl_seteq seteq_incl_left seteq_incl_right incl_nil
       incl_cons incl_cons_build incl_cons_project_l incl_cons_project_r
       incl_cons_drop incl_filter
       incl_distr_left incl_distr_right incl_app_project_left
       incl_app_project_right incl_app_build : listdb.


  (* ⊊ *)
  Lemma strict_incl_incl A B: A ⊊ B -> A ⊆ B.
  Proof. firstorder. Qed.

  Lemma incl_strict_incl x A B: x ∈ A -> ~ x ∈ B -> A ⊆ B -> A ⊊ B.
  Proof. firstorder. Qed.

  Lemma strict_incl_eq A B: A ⊊ B -> ~ A === B.
  Proof. firstorder. Qed.

  Lemma strict_incl_project A B: A ⊊ B -> exists x, x ∈ B /\ ~ x ∈ A.
  Proof. firstorder. Qed.

  Global Instance strict_incl_incl_subrel:
    subrelation (@strict_incl X) (@incl X).
  Proof. firstorder. Qed.


  Section WellFoundedStrictInclusion.

    Context {D: Dis X}.
    Lemma nodup_seteq A:
      nodup D A === A.
    Proof.
      split; intros ?; eapply nodup_In; eauto.
    Qed.

    Lemma wf_strict_incl: well_founded (@strict_incl X).
    Proof.
      eapply well_founded_lt_compat with (f := fun A => length (nodup eq_dec A)). 
      intros A B [H [x [H1 H2]]].
      assert (nodup eq_dec A ⊆ nodup eq_dec B) as H3 by now rewrite !nodup_seteq.
      eapply NoDup_incl_length in H3 as H4; [| eapply NoDup_nodup].
      eapply le_lt_or_eq in H4 as []; eauto; exfalso.
      eapply NoDup_length_incl in H3. 
      rewrite !nodup_seteq in H3; intuition.
      eapply NoDup_nodup. omega.
    Qed.
    
  End WellFoundedStrictInclusion.
    
  (* app *)
  Global Instance proper_app_incl: Proper (incl ++> incl ++> incl) (@app X).
  Proof.
    intros A A' H1 B B' H2; induction A; firstorder.  
  Qed.
  
  Global Instance proper_app_seteq: Proper (seteq ++> seteq ++> seteq) (@app X).
  Proof.
    intros A A' [H1 H2] B B' [H3 H4].
    split; eapply proper_app_incl; firstorder. 
  Qed.

  Hint Rewrite app_nil_l app_nil_r : listdb.
  Hint Rewrite <- app_comm_cons : listdb.
  Hint Rewrite -> in_app_iff : listdb. 

  Lemma app_comm A B: A ++ B === B ++ A.
  Proof.
    split; intros ?; autorewrite with listdb; firstorder.
  Qed.





  (* rev *)
  Lemma rev_seteq A: rev A === A.
  Proof.
    induction A; cbn; autorewrite with listdb; intuition.
  Qed.

  Global Instance proper_incl_seteq: Proper (@seteq X ++> @seteq X ++> iff) incl.
  Proof.
    intros ??????; firstorder.
  Qed.

  Global Instance proper_rev_incl: Proper (incl ++> incl) (@rev X).
  Proof.
    intros A B H. now rewrite rev_seteq, H, rev_seteq. 
  Qed.
  
  
  Global Instance proper_rev_seteq: Proper (seteq ++> seteq) (@rev X).
  Proof.
    intros A B [H1 H2]; split; eapply proper_rev_incl; eauto.  
  Qed.

  Hint Rewrite rev_seteq rev_involutive rev_length rev_app_distr : listdb.  



  (* map *)
  Lemma map_id_list (g: X -> X) A:
    (forall x, x ∈ A -> g x = x) -> map g A = A.
  Proof.
    intros. induction A; cbn in *; eauto.
    rewrite H; intuition.
    rewrite IHA; firstorder.
  Qed.

  Lemma map_id A: map id A = A.
  Proof.
    induction A; unfold id in *; cbn; congruence.
  Qed.

  Lemma map_nil f: map f nil = nil.
  Proof.
    reflexivity.
  Qed.

  Global Instance map_incl_proper : Proper (eq ++> incl ++> incl) (@map Y X).
  Proof.
    intros ?? -> A B H.
    induction A; cbn; eauto with listdb.
    eapply incl_cons_build; firstorder. 
    eapply in_map; firstorder.
  Qed.      

  Global Instance map_seteq_proper : Proper (eq ++> seteq ++> seteq) (@map Y X).
  Proof.
    intros ?? -> A B [H1 H2]; split; apply map_incl_proper; firstorder. 
  Qed.      



  Hint Rewrite map_id map_rev map_nil map_cons map_app map_length : listdb.
  Hint Resolve in_map : listdb.





  (* length *)
  Hint Rewrite app_length map_length rev_length : listdb.



  (* filter *)
  Lemma filter_length p A: length (filter p A) <= length A.
  Proof. induction A; cbn; [ constructor | ]; destruct (p a); cbn; omega. Qed.


  Global Instance filter_incl_proper: Proper (eq ++> incl ++> incl) (@filter X).
  Proof.
    intros ?? ->  A B H2; induction A; cbn; eauto with listdb.
    destruct y eqn: H1; eauto with listdb. 
    eapply incl_cons_build; eauto with listdb.
    eapply filter_In; intuition. 
  Qed.

  Global Instance filter_seqteq_proper: Proper (eq ++> seteq ++> seteq) (@filter X).
  Proof.
    intros f g -> A B [H2 H3]; split; apply filter_incl_proper; firstorder. 
  Qed.
  

   
End BasicLemmas.

Hint Resolve incl_refl seteq_refl : listdb.
Hint Resolve incl_seteq seteq_incl_left seteq_incl_right incl_nil
     incl_cons incl_cons_build incl_cons_project_l incl_cons_project_r
     incl_cons_drop incl_filter
     incl_distr_left incl_distr_right incl_app_project_left
     incl_app_project_right incl_app_build : listdb.
Hint Rewrite -> in_app_iff : listdb.
Hint Rewrite <- app_comm_cons : listdb.
Hint Rewrite app_nil_l app_nil_r : listdb.
Hint Rewrite rev_seteq rev_involutive rev_length rev_app_distr : listdb.
Hint Rewrite map_id map_rev map_nil map_cons map_app : listdb.
Hint Resolve in_map : listdb.
Hint Rewrite app_length map_length rev_length : listdb.

Hint Extern 4 => 
  match goal with
  |[ H: ?x ∈ nil |- _ ] => destruct H
  end.



Ltac lsimpl := autorewrite with listdb. 
Tactic Notation "lsimpl" "in" hyp_list(H) := autorewrite with listdb in H. 
Tactic Notation "lsimpl" "in" "*" := autorewrite with listdb in *. 

Ltac lauto  := eauto with listdb. 
