Lvc.Constr.CSet

Require Export Setoid Coq.Classes.Morphisms.
Require Export Sets SetInterface SetConstructs SetProperties.
Require Import EqDec Computable Util.
Require Export CSetNotation CSetTac CSetBasic CSetCases CSetGet CSetComputable CSetDisjoint.

Set Implicit Arguments.

Lemma Proper_eq_fun X H0 (f:X→X)
: @Proper (X → X)
           (@respectful X X
                        (@_eq X (@SOT_as_OT X (@eq X) H0))
                        (@_eq X (@SOT_as_OT X (@eq X) H0))) f.

Hint Resolve Proper_eq_fun.

Hint Resolve incl_empty minus_incl incl_right incl_left : auto.

Definition pe X `{OrderedType X} := prod_eq (@Equal X _ _) (@Equal X _ _).

Instance pe_morphism X `{OrderedType X}
 : Proper (Equal ==> Equal ==> (@pe X _)) pair.

Instance pe_refl X `{OrderedType X} : Symmetric (@pe _ _).

Instance pe_sym X `{OrderedType X} : Symmetric (@pe _ _).

Instance pe_trans X `{OrderedType X} : Transitive (@pe _ _).

Ltac pe_rewrite :=
  repeat
    (match goal with
       | [ H : pe ?an _, H´ : context [?an] |- _ ] ⇒ rewrite H in H´; simpl in H´
       | [ H : pe ?an _ |- context [?an] ] ⇒ rewrite H; simpl
     end).

Instance Subset_morphism_2 X `{OrderedType X}
  : Proper (flip Subset ==> Subset ==> impl) (Subset).

Instance Subset_morphism_3 X `{OrderedType X}
  : Proper (Subset ==> flip Subset ==> flip impl) (Subset).

Lemma minus_single_singleton X `{OrderedType X} (s : set X) (x:X)
: s \ singleton x [=] s \ {x; {}}.

Lemma minus_single_singleton´ X `{OrderedType X} (s : set X) (x:X)
: s \ singleton x ⊆ s \ {x; {}}.

Lemma minus_single_singleton´´ X `{OrderedType X} (s : set X) (x:X)
: s \ {x; {}} ⊆ s \ singleton x.

Lemma fresh_of_list {X} `{OrderedType X} (L:list X) (y:X)
  : Util.fresh y L → y ∉ of_list L.

Hint Extern 20 (?s \ {?x; {}} ⊆ ?s \ singleton ?x) ⇒ eapply minus_single_singleton´´.
Hint Extern 20 (?s \ singleton ?x ⊆ ?s \ {?x; {}}) ⇒ eapply minus_single_singleton´.

Hint Extern 20 (?s \ {?x; {}} [=] ?s \ singleton ?x) ⇒ rewrite minus_single_singleton; reflexivity.
Hint Extern 20 (?s \ singleton ?x [=] ?s \ {?x; {}}) ⇒ rewrite minus_single_singleton; reflexivity.

Hint Extern 20 (Subset (?a \ _) ?a) ⇒ eapply minus_incl.
Hint Extern 20 (Subset (?a \ _) ?a´) ⇒ (is_evar a ; fail 1)
                                        || (has_evar a ; fail 1)
                                        || (is_evar a´ ; fail 1)
                                        || (has_evar a´; fail 1)
                                        || eapply minus_incl.

Hint Extern 10 (Subset ?a (_ ∪ ?a)) ⇒ eapply incl_right.

Instance diff_proper_impl X `{OrderedType X}
: Proper (flip Subset ==> Subset ==> flip Subset) diff.

Definition max_set {X} `{OrderedType X} (a:set X) (b:set X) :=
  if [SetInterface.cardinal a < SetInterface.cardinal b] then
    b
  else
    a.

Lemma cardinal_difference {X} `{OrderedType X} (s t: set X)
: SetInterface.cardinal (s \ t) ≤ SetInterface.cardinal s.

Lemma cardinal_difference´ {X} `{OrderedType X} (s t: set X)
: t ⊆ s
  → SetInterface.cardinal (s \ t) = SetInterface.cardinal s - SetInterface.cardinal t.

Instance cardinal_morph {X} `{OrderedType X}
: Proper (@Subset X _ _ ==> Peano.le) SetInterface.cardinal.

Lemma cardinal_of_list_unique {X} `{OrderedType X} (Z:list X)
: unique Z → SetInterface.cardinal (of_list Z) = length Z.

Lemma cardinal_map {X} `{OrderedType X} {Y} `{OrderedType Y} (s: set X) (f:X → Y) `{Proper _ (_eq ==> _eq) f}
: SetInterface.cardinal (SetConstructs.map f s) ≤ SetInterface.cardinal s.

Hint Extern 20 ( ?v ∈ singleton ?v ) ⇒ eapply singleton_iff; reflexivity.
Hint Extern 20 ( ?s ⊆ ?s ∪ _ ) ⇒ eapply incl_left.
Hint Extern 20 ( ?s ⊆ _ ∪ ?s ) ⇒ eapply incl_right.
Hint Extern 20 ⇒ match goal with
                   | [ H: ?x ∈ ?s, H´: ?x ∉ ?s |- _ ] ⇒ exfalso; eapply H´, H
                 end.

Lemma incl_union_right X `{OrderedType X} s t u
: s ⊆ t → s ⊆ u ++ t.


Lemma incl_union_left X `{OrderedType X} s t u
: s ⊆ t → s ⊆ t ++ u.


Lemma incl_add_right X `{OrderedType X} s t x
: s ⊆ t → s ⊆ {x; t}.

Lemma in_add_left X `{OrderedType X} s x
: x ∈ {x; s}.


Hint Resolve incl_union_left incl_union_right incl_add_right in_add_left
             union_left union_right get_list_union_map : cset.