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 ∈ t → x ∈ (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 =/= y → x ∈ 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 ∈ s → singleton 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 s´ t t´:set X)
: s ⊆ s´ → t ⊆ t´ → s \ t´ ⊆ s´ \ t.
Lemma union_idem (s:set X)
: s ∪ s ≅ s.
Lemma minus_in s t (x:X)
: x ∉ s → x ∉ t → x ∉ (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 ∈ s → x ∈ (s ∪ t).
Lemma union_right s t (x:X)
: x ∈ t → x ∈ (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 ⊆ t → s ∪ t ≅ t.
Lemma incl_union_lr (s s´ t t´:set X)
: s ⊆ s´ → t ⊆ t´ → s ∪ t ⊆ s´ ∪ t´.
Lemma incl_left (s t:set X)
: s ⊆ (s ∪ t).
Lemma in_meet (s t:set X) (x:X)
: x ∈ s → x ∈ t → x ∈ s ∩ t.
Lemma meet_in (s t:set X) (x:X)
: x ∈ s ∩ t → x ∈ s ∧ x ∈ t.
Lemma meet_incl (s t u:set X)
: s ⊆ u → s ∩ t ⊆ u.
Lemma meet_comm (s t:set X)
: s ∩ t ≅ t ∩ s.
Lemma incl_meet (s t:set X)
: s ⊆ t → s ≅ s ∩ t.
Lemma minus_meet (s t u:set X)
: (s \ t) ∩ u ≅ s ∩ u \ t.
Lemma set_incl (s t: set X)
: s ⊆ t → t ⊆ s → t ≅ 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 s´ t t´:set X)
: s ⊆ s´ → t ⊆ t´ → 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 ⊆ t → u ∩ t ≅ empty → u ∩ s ≅ empty.
Lemma union_incl_split (s t u : set X)
: s ⊆ u → t ⊆ u → s ∪ t ⊆ u.
Lemma union_minus_remove (a b : set X)
: (a ∪ b) \ a ≅ b \ a.
Lemma minus_incl_meet_special2 (c c´ d : set X)
: c ⊆ d
→ c ⊆ c´
→ 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 ⊆ t → t ⊆ s → t ≅ s.
Lemma eq_incl (s t:set X)
: t ≅ s → s ⊆ 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:X→Y) :=
(fun x t ⇒ add (f x) t).
Add Parametric Morphism {X} `{OrderedType X} {Y} `{OrderedType Y} (f:X→Y)
`{Proper _ (_eq ==> _eq) f}
: (addf f)
with signature
_eq ==> Equal ==> Equal as addf_morphism.
Add Parametric Morphism {X} `{OrderedType X} {Y} `{OrderedType Y} (f:X→Y)
: (addf f)
with signature
eq ==> Equal ==> Equal as addf_morphism2.
Lemma addf_transpose {X} `{OrderedType X} {Y} `{OrderedType Y} (f:X→Y)
: transpose Equal (addf f).
Lemma minus_union_both X `{OrderedType X} (s t: set X) x
: x ∉ s → s \ t [=] (s ∪ {{x}}) \ (t ∪ {{x}}).
Lemma list_eq_eq {X} {L L´:list X}
: list_eq eq L L´ ↔ 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 s´ t t´:set X)
: t´ ⊆ t → s ∩ t [=] s´ ∩ t → s ∩ t´ [=] s´ ∩ t´.
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 ⊆ t → s ⊆ 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 [=] t → s [<=] t.
Lemma minus_inter_empty X `{OrderedType X} s t u
: s ∩ t [=] s ∩ u
→ s \ t [=] s \ u.
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 ∈ t → x ∈ (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 =/= y → x ∈ 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 ∈ s → singleton 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 s´ t t´:set X)
: s ⊆ s´ → t ⊆ t´ → s \ t´ ⊆ s´ \ t.
Lemma union_idem (s:set X)
: s ∪ s ≅ s.
Lemma minus_in s t (x:X)
: x ∉ s → x ∉ t → x ∉ (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 ∈ s → x ∈ (s ∪ t).
Lemma union_right s t (x:X)
: x ∈ t → x ∈ (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 ⊆ t → s ∪ t ≅ t.
Lemma incl_union_lr (s s´ t t´:set X)
: s ⊆ s´ → t ⊆ t´ → s ∪ t ⊆ s´ ∪ t´.
Lemma incl_left (s t:set X)
: s ⊆ (s ∪ t).
Lemma in_meet (s t:set X) (x:X)
: x ∈ s → x ∈ t → x ∈ s ∩ t.
Lemma meet_in (s t:set X) (x:X)
: x ∈ s ∩ t → x ∈ s ∧ x ∈ t.
Lemma meet_incl (s t u:set X)
: s ⊆ u → s ∩ t ⊆ u.
Lemma meet_comm (s t:set X)
: s ∩ t ≅ t ∩ s.
Lemma incl_meet (s t:set X)
: s ⊆ t → s ≅ s ∩ t.
Lemma minus_meet (s t u:set X)
: (s \ t) ∩ u ≅ s ∩ u \ t.
Lemma set_incl (s t: set X)
: s ⊆ t → t ⊆ s → t ≅ 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 s´ t t´:set X)
: s ⊆ s´ → t ⊆ t´ → 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 ⊆ t → u ∩ t ≅ empty → u ∩ s ≅ empty.
Lemma union_incl_split (s t u : set X)
: s ⊆ u → t ⊆ u → s ∪ t ⊆ u.
Lemma union_minus_remove (a b : set X)
: (a ∪ b) \ a ≅ b \ a.
Lemma minus_incl_meet_special2 (c c´ d : set X)
: c ⊆ d
→ c ⊆ c´
→ 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 ⊆ t → t ⊆ s → t ≅ s.
Lemma eq_incl (s t:set X)
: t ≅ s → s ⊆ 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:X→Y) :=
(fun x t ⇒ add (f x) t).
Add Parametric Morphism {X} `{OrderedType X} {Y} `{OrderedType Y} (f:X→Y)
`{Proper _ (_eq ==> _eq) f}
: (addf f)
with signature
_eq ==> Equal ==> Equal as addf_morphism.
Add Parametric Morphism {X} `{OrderedType X} {Y} `{OrderedType Y} (f:X→Y)
: (addf f)
with signature
eq ==> Equal ==> Equal as addf_morphism2.
Lemma addf_transpose {X} `{OrderedType X} {Y} `{OrderedType Y} (f:X→Y)
: transpose Equal (addf f).
Lemma minus_union_both X `{OrderedType X} (s t: set X) x
: x ∉ s → s \ t [=] (s ∪ {{x}}) \ (t ∪ {{x}}).
Lemma list_eq_eq {X} {L L´:list X}
: list_eq eq L L´ ↔ 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 s´ t t´:set X)
: t´ ⊆ t → s ∩ t [=] s´ ∩ t → s ∩ t´ [=] s´ ∩ t´.
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 ⊆ t → s ⊆ 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 [=] t → s [<=] t.
Lemma minus_inter_empty X `{OrderedType X} s t u
: s ∩ t [=] s ∩ u
→ s \ t [=] s \ u.