Lvc.Constr.CSetBasic

Require Export Setoid Coq.Classes.Morphisms.
Require Export Sets SetInterface SetConstructs SetProperties.
Require Import EqDec CSetNotation Util CSetTac.

Section theorems.
  Variable X : Type.
  Context `{OrderedType X}.

  Lemma single_spec_neq (x y:X)
    : x {{ y }}x === y.

  Lemma neq_not_in_single (x y:X)
    : x =/= y¬x {{y}}.

  Lemma minus_empty (s:set X)
    : s \ s.

  Lemma minus_in_in s t (x:X)
    : x (s \ t)x s ¬x t.

  Lemma in_in_minus s t (x:X)
    : x s¬x tx (s \ t).

  Lemma union_comm (s t:set X)
    : s t t s .

  Lemma minus_inane_set (s t:set X)
    : s t (s \ t) s.

  Lemma minus_union_set (s t:set X)
    : s t ((s t) \ t) s.

  Lemma in_minus_neq s (x y:X)
    : x =/= yx s
    → x (s\{{y}}).

  Lemma add_inane s (x:X)
    : x s
    → s ({{x}} s).

  Lemma in_single_union s (y:X)
    : y {{y}} s.

  Lemma minus_union (s t u:set X)
    : (s \ t \ u) s \ (t u).

  Lemma incl_empty (s:set X)
    : s.

  Lemma incl_singleton (x:X) (s:set X)
    : x ssingleton x s.

  Lemma minus_incl (s t:set X)
    : (s\t) s.

  Lemma empty_neutral_union (s:set X)
    : s s.

  Lemma incl_add s (x:X)
    : s ({{x}} s).

  Lemma incl_refl (s:set X)
  : s s.

  Lemma incl_right (s t:set X)
    : s (t s).

  Lemma incl_add´ (s:set X) x
    : s {x; s}.

  Lemma in_add´ (s:set X) x
    : x {x; s}.

  Lemma incl_minus (s t : set X)
    : (s \ t) s.

  Lemma union_assoc (s t u : set X)
    : s t u s (t u).

  Lemma union_minus_incl (s t:set X)
    : ((t s) \ t) s.

  Lemma incl_minus_lr (s t :set X)
    : s t s \ \ t.

  Lemma union_idem (s:set X)
    : s s s.

  Lemma minus_in s t (x:X)
    : x sx tx (s t).

  Lemma union_cases s t (x:X)
    : x (s t)x s x t.

  Lemma not_in_union_comp (s t : set X) x :
    ¬x s ¬x t¬x (s t).

  Lemma not_in_union_decomp s t (x:X)
    : x (s t)x s x t.

  Lemma union_left s t (x:X)
    : x sx (s t).

  Lemma union_right s t (x:X)
    : x tx (s t).

  Lemma set_fact_2 s t (x:X)
    : (s \ ({{x}} t)) \ {{x}} s \ ({{x}} t).

  Lemma incl_union_absorption (s t:set X)
    : s ts t t.

  Lemma incl_union_lr (s t :set X)
    : s t s t .

  Lemma incl_left (s t:set X)
    : s (s t).

  Lemma in_meet (s t:set X) (x:X)
    : x sx tx s t.

  Lemma meet_in (s t:set X) (x:X)
    : x s tx s x t.

  Lemma meet_incl (s t u:set X)
    : s us t u.

  Lemma meet_comm (s t:set X)
    : s t t s.

  Lemma incl_meet (s t:set X)
    : s ts s t.

  Lemma minus_meet (s t u:set X)
    : (s \ t) u s u \ t.

  Lemma set_incl (s t: set X)
    : s tt st s.

  Lemma elements_nil_eset (s : set X) :
    s elements s = nil.

  Lemma union_meet_distr_r (s t u : set X) :
    (s t) u (s u) (t u).

  Lemma union_is_empty (s t : set X) :
    s t → (s t ).

  Lemma smaller_meet_empty (s t u : set X) :
    (s t) u t u .

  Lemma empty_intersection_in_one_not_other (s t : set X) x :
    s t x s¬ x t.

  Lemma meet_assoc (s t u : set X)
    : s t u s (t u).

  Lemma incl_meet_lr (s t :set X)
    : s t s t .

  Lemma meet_in_union (s t : set X)
    : s t s t.

  Lemma minus_dist_union (s t u:set X)
    : (s t) \ u (s \ u) (t \ u).

  Lemma minus_dist_intersection (s t u:set X)
    : (s t) \ u (s \ u) (t \ u).

  Lemma incl_not_member (s t:set X) x
    : s t¬x t¬x s.

  Lemma incl_meet_empty (s t u:set X)
    : s tu t emptyu s empty.

  Lemma union_incl_split (s t u : set X)
    : s ut us t u.

  Lemma union_minus_remove (a b : set X)
        : (a b) \ a b \ a.

  Lemma minus_incl_meet_special2 (c d : set X)
    : c d
    → c
    → c ( \ (c \ d)) c.

  Lemma meet_minus (s t : set X)
    : s (t \ s) .

  Lemma meet_in_left (s t : set X)
    : s t s.

  Lemma not_in_meet_empty (D:set X) x
    : ¬ x D
    → D {{x}} .

  Lemma incl_eq (s t:set X)
    : s tt st s.

  Lemma eq_incl (s t:set X)
    : t ss t t s.

  End theorems.

  Section moretheorems.

  Require Import List.
  Variable X : Type.
  Context `{OrderedType X}.

  Hypothesis equiv_is_eq : _eq = eq.

End moretheorems.

Definition addf {X} `{OrderedType X} {Y} `{OrderedType Y} (f:XY) :=
  (fun x tadd (f x) t).

Add Parametric Morphism {X} `{OrderedType X} {Y} `{OrderedType Y} (f:XY)
  `{Proper _ (_eq ==> _eq) f}
  : (addf f)
  with signature
    _eq ==> Equal ==> Equal as addf_morphism.

Add Parametric Morphism {X} `{OrderedType X} {Y} `{OrderedType Y} (f:XY)
  : (addf f)
  with signature
    eq ==> Equal ==> Equal as addf_morphism2.

Lemma addf_transpose {X} `{OrderedType X} {Y} `{OrderedType Y} (f:XY)
 : transpose Equal (addf f).

Lemma minus_union_both X `{OrderedType X} (s t: set X) x
  : x ss \ t [=] (s {{x}}) \ (t {{x}}).

Lemma list_eq_eq {X} {L :list X}
  : list_eq eq L L = .

Lemma minus_idem X `{OrderedType X} (s t:set X)
: s \ t [=] (s \ t) \ t.

Lemma meet_incl_eq {X} `{OrderedType X} (s t :set X)
: ts t [=] ts [=] .

Lemma InA_in {X} `{OrderedType X} x L
 : InA _eq x L x of_list L.

Lemma minus_minus_eq {X} `{OrderedType X} (s t : set X)
  : s [=] s \ (t \ s).

Lemma union_incl_left {X} `{OrderedType X} (s t u: set X)
: s ts t u.

Lemma of_list_app X `{OrderedType X} (A B: list X)
  : of_list (A ++ B) [=] of_list A of_list B.

Lemma incl_set_left X `{OrderedType X} (s t : set X)
: s [=] ts [<=] t.

Lemma minus_inter_empty X `{OrderedType X} s t u
: s t [=] s u
  → s \ t [=] s \ u.