Qcert.Basic.Data.BrandRelation
Definition brands := list brand.
Definition any : brands := nil.
Definition brand_relation_t := list (string×string).
Section brand_relation_types.
Context (brand_relation_brands:brand_relation_t).
Definition brand_relation_trans_t
:= ∀ a b c, In (a,b) brand_relation_brands →
In (b,c) brand_relation_brands →
In (a,c) brand_relation_brands.
Definition brand_relation_assym_t
:= ∀ a b, In (a,b) brand_relation_brands →
¬ In (b,a) brand_relation_brands.
Section brand_relation_dec.
Lemma brand_relation_trans_dec :
{brand_relation_trans_t}
+ {¬ brand_relation_trans_t}.
Lemma brand_relation_assym_dec :
{brand_relation_assym_t}
+ {¬ brand_relation_assym_t}.
End brand_relation_dec.
End brand_relation_types.
Class brand_relation :=
mkBrand_relation {
brand_relation_brands : list (string×string);
brand_relation_trans_b :
holds (brand_relation_trans_dec brand_relation_brands);
brand_relation_assym_b :
holds (brand_relation_assym_dec brand_relation_brands)
}.
Section brand_relation_prop.
Context {br:brand_relation}.
Lemma brand_relation_trans :
brand_relation_trans_t brand_relation_brands.
Lemma brand_relation_assym :
brand_relation_assym_t brand_relation_brands.
Lemma brand_relation_irrefl a : ¬ In (a,a) brand_relation_brands.
End brand_relation_prop.
Lemma brand_relation_ext b pf1 pf2 pf1' pf2' :
mkBrand_relation b pf1 pf2 = mkBrand_relation b pf1' pf2' .
Lemma brand_relation_fequal {br₁ br₂}:
@brand_relation_brands br₁ = @brand_relation_brands br₂ →
br₁ = br₂.
Section sub_brand.
Definition sub_brand (h:brand_relation_t) (a b:brand)
:= a = b ∨ In (a,b) h.
Definition sub_brand_dec br a b : {sub_brand br a b} + {¬sub_brand br a b}.
Global Instance sub_brand_refl br : Reflexive (sub_brand br).
Global Instance sub_brand_pre `{brand_relation} : PreOrder (sub_brand brand_relation_brands).
Global Instance sub_brand_part `{brand_relation} : PartialOrder eq (sub_brand brand_relation_brands).
Lemma sub_brand_in_trans `{brand_relation} {x y z}:
sub_brand brand_relation_brands x y →
In (y, z) brand_relation_brands →
In (x, z) brand_relation_brands.
Lemma in_sub_brand_trans `{brand_relation} {x y z}:
In (x, y) brand_relation_brands →
sub_brand brand_relation_brands y z →
In (x, z) brand_relation_brands.
Definition sub_brands (h:brand_relation_t) (a b:brands)
:= ∀ y, In y b → ∃ x, In x a ∧ sub_brand h x y.
Definition sub_brands_dec br a b :
{sub_brands br a b} + {¬sub_brands br a b}.
Global Instance sub_brands_pre `{brand_relation} : PreOrder (sub_brands brand_relation_brands).
Lemma incl_sub_brands (hs:brand_relation_t) (a b:brands) :
incl a b → sub_brands hs b a.
Definition equiv_brands (h:brand_relation_t) (a b:brands)
:= sub_brands h a b ∧ sub_brands h b a.
Global Instance equiv_brands_sub_subr (hs:brand_relation_t) :
subrelation (equiv_brands hs) (sub_brands hs).
Global Instance equiv_brands_sub_flip_subr (hs:brand_relation_t) :
subrelation (equiv_brands hs) (flip (sub_brands hs)).
Definition equiv_brands_dec br a b :
{equiv_brands br a b} + {¬equiv_brands br a b}.
Global Instance equiv_brands_equiv `{brand_relation} :
Equivalence (equiv_brands brand_relation_brands).
Global Instance equiv_brands_eqdec `{brand_relation} :
EqDec brands (equiv_brands brand_relation_brands).
Global Instance equivlist_equiv_brands (hs:brand_relation_t)
: subrelation equivlist (equiv_brands hs).
Global Instance sub_brands_part `{brand_relation} : PartialOrder (equiv_brands brand_relation_brands) (sub_brands brand_relation_brands).
Global Instance sub_brands_app_proper `{brand_relation} :
Proper (sub_brands brand_relation_brands ==>
sub_brands brand_relation_brands ==>
sub_brands brand_relation_brands)
(@app brand).
Global Instance equiv_brands_app_proper `{brand_relation} :
Proper (equiv_brands brand_relation_brands ==>
equiv_brands brand_relation_brands ==>
equiv_brands brand_relation_brands)
(@app brand).
Lemma sub_brands_any hs b : sub_brands hs b any.
Lemma any_sub_brands hs b : sub_brands hs any b → b = any.
End sub_brand.
Section brand_ops.
Definition parents (hs:brand_relation_t) (a:brand)
:= map snd
(filter (fun x ⇒ if a == (fst x) then true else false) hs).
Lemma parents_In (hs:brand_relation_t) (s a:brand) :
In s (parents hs a) ↔ In (a,s) hs.
Definition parents_and_self (hs:brand_relation_t) (a:brand)
:= a::(parents hs a).
Lemma parents_and_self_In (hs:brand_relation_t) (s:brand) (a:brand) :
In s (parents_and_self hs a) ↔ sub_brand hs a s.
Definition explode_brands (hs:brand_relation_t) (a:brands)
:= flat_map (parents_and_self hs) a.
Lemma incl_explode_brands (hs:brand_relation_t) (a:brands) :
incl a (explode_brands hs a).
Lemma sub_explode_brands
(hs:brand_relation_t) (a:brands) :
sub_brands hs (explode_brands hs a) a.
Lemma explode_brands_sub
(hs:brand_relation_t) (a:brands) :
sub_brands hs a (explode_brands hs a).
Lemma explode_brands_equivbrands
(hs:brand_relation_t) (a:brands) :
equiv_brands hs (explode_brands hs a) a.
Global Instance explode_brands_proper `{brand_relation} :
Proper (equiv_brands brand_relation_brands ==> equiv_brands brand_relation_brands) (explode_brands brand_relation_brands).
Lemma explode_brands_proper_inv `{brand_relation} (a b:brands) :
equiv_brands brand_relation_brands
(explode_brands brand_relation_brands a)
(explode_brands brand_relation_brands b) →
equiv_brands brand_relation_brands
a
b.
Lemma explode_brands_incl hs b a:
sub_brands hs a b →
incl b (explode_brands hs a).
Global Instance explode_brands_properequiv `{brand_relation} :
Proper (equiv_brands brand_relation_brands ==> equivlist) (explode_brands brand_relation_brands).
Lemma explode_brands_idempotent `{brand_relation} (a:brands) :
equivlist
(explode_brands brand_relation_brands
(explode_brands brand_relation_brands a))
(explode_brands brand_relation_brands a).
Lemma explode_brands_app_incl hs a b :
incl (explode_brands hs a)
(explode_brands hs (a++b)).
Definition has_subtype_in (hs:brand_relation_t) (c:brands) (a:brand)
: bool
:= existsb (fun x ⇒ (if in_dec equiv_dec (x,a) hs then true else false)) c.
Definition collapse_brands (hs:brand_relation_t) (c:brands)
:= filter (fun x ⇒ negb (has_subtype_in hs c x)) c.
Lemma collapse_brands_sublist (hs:brand_relation_t) (a:brands) :
sublist (collapse_brands hs a) a.
Lemma collapse_brands_incl (hs:brand_relation_t) (a:brands) :
incl (collapse_brands hs a) a.
Lemma has_subtype_in_app hs a l1 l2 :
has_subtype_in hs (l1 ++ l2) a =
has_subtype_in hs l1 a ||
has_subtype_in hs l2 a.
Lemma nosub_collapse_brands hs a :
(∀ x y : brand, In x a → In y a → ¬ In (x, y) hs) →
collapse_brands hs a = a.
Lemma collapse_brands_nosub hs a :
collapse_brands hs a = a →
(∀ x y : brand, In x a → In y a → ¬ In (x, y) hs).
Lemma has_subtype_in_single hs a b :
has_subtype_in hs (a::nil) b = if in_dec equiv_dec (a,b) hs then true else false.
Lemma has_subtype_in_not_self `{brand_relation} a :
has_subtype_in brand_relation_brands (a :: nil) a = false.
Lemma collapse_brands_singleton {br:brand_relation} (bb:brand)
: collapse_brands brand_relation_brands (singleton bb) = singleton bb.
Lemma has_subtype_in_cons_self `{brand_relation} a l :
has_subtype_in brand_relation_brands (a :: l) a =
has_subtype_in brand_relation_brands l a.
Lemma has_subtype_in_least `{brand_relation} {x:brand} {a:brands} :
In x a →
{y:brand |
In y a
∧ sub_brand brand_relation_brands y x
∧ has_subtype_in brand_relation_brands a y = false}.
Lemma sub_collapse_brands `{brand_relation} (a:brands) :
sub_brands brand_relation_brands
(collapse_brands brand_relation_brands a)
a.
Lemma collapse_brands_sub
(hs:brand_relation_t) (a:brands) :
sub_brands hs a (collapse_brands hs a).
Lemma collapse_brands_equivbrands
`{brand_relation} (a:brands) :
equiv_brands brand_relation_brands
(collapse_brands brand_relation_brands a)
a.
Lemma collapse_collapses `{brand_relation} (a:brands) :
∀ x y,
In x a →
In y (collapse_brands brand_relation_brands a) →
¬ In (x,y) brand_relation_brands.
Global Instance collapse_brands_proper `{brand_relation} :
Proper (equiv_brands brand_relation_brands ==> equiv_brands brand_relation_brands) (collapse_brands brand_relation_brands).
Lemma collapse_brands_proper_inv `{brand_relation} (a b:brands) :
equiv_brands brand_relation_brands
(collapse_brands brand_relation_brands a)
(collapse_brands brand_relation_brands b) →
equiv_brands brand_relation_brands
a
b.
Lemma existsb_app {A} (f:A→bool) l1 l2 :
existsb f (l1 ++ l2) = existsb f l1 || existsb f l2.
Lemma collapse_brands_idempotent `{brand_relation} (a:brands) :
collapse_brands brand_relation_brands (collapse_brands brand_relation_brands a) = collapse_brands brand_relation_brands a.
Lemma sort_brands_equiv hs a :
equiv_brands hs (insertion_sort StringOrder.lt_dec a) a.
Definition canon_brands (hs:brand_relation_t) (a:brands)
:= insertion_sort StringOrder.lt_dec (collapse_brands hs a).
Lemma canon_brands_singleton {br:brand_relation} (bb:brand)
: canon_brands brand_relation_brands (singleton bb) = singleton bb.
Lemma canon_brands_equiv `{brand_relation} (a:brands)
: equiv_brands
brand_relation_brands
(canon_brands brand_relation_brands a)
a.
Global Instance has_subtype_in_proper_equivlist :
Proper (eq ==> equivlist ==> eq ==> eq) has_subtype_in.
Lemma collapse_sort_brands_commute (hs:brand_relation_t) (a:brands)
: insertion_sort StringOrder.lt_dec (collapse_brands hs a)
= collapse_brands hs (insertion_sort StringOrder.lt_dec a).
Lemma canon_brands_incl (hs:brand_relation_t) (a:brands) :
incl (canon_brands hs a) a.
Definition is_canon_brands (hs:brand_relation_t) (a:brands)
:= is_list_sorted StringOrder.lt_dec a = true
∧ (∀ x y, In x a → In y a → ¬ In (x,y) hs).
Lemma canon_brands_is_canon_brands (hs:brand_relation_t) (a:brands) :
is_canon_brands hs (canon_brands hs a).
Lemma is_canon_brands_canon_brands hs a :
is_canon_brands hs a → canon_brands hs a = a.
Lemma canon_brands_idempotent (hs:brand_relation_t) (a:brands) :
canon_brands hs (canon_brands hs a)
= canon_brands hs a.
Lemma is_canon_brands_dec (hs:brand_relation_t) (a:brands) :
{is_canon_brands hs a} + {¬ is_canon_brands hs a}.
Lemma is_canon_brands_singleton {br:brand_relation} (bb:brand)
: is_canon_brands brand_relation_brands (singleton bb).
Lemma canon_equiv `{brand_relation} (a b:brands) :
equiv_brands brand_relation_brands a b
↔
canon_brands brand_relation_brands a = canon_brands brand_relation_brands b.
Global Instance canon_proper `{brand_relation} :
Proper (equiv_brands brand_relation_brands ==> eq) (canon_brands brand_relation_brands).
Lemma canon_equiv_is_canon_brands `{brand_relation} (a b:brands) :
is_canon_brands brand_relation_brands b →
(equiv_brands brand_relation_brands a b
↔
canon_brands brand_relation_brands a = b).
Definition equiv_brands_dec_alt `{brand_relation} a b :
{equiv_brands brand_relation_brands a b}
+ {¬equiv_brands brand_relation_brands a b}.
Lemma explode_canon_explode `{brand_relation} a :
equivlist (explode_brands brand_relation_brands
(canon_brands brand_relation_brands a))
(explode_brands brand_relation_brands a).
Lemma canon_brands_canon_brands_app1 `{brand_relation} a b :
canon_brands brand_relation_brands
(canon_brands brand_relation_brands a ++ b) =
canon_brands brand_relation_brands (a ++ b).
End brand_ops.
Section brand_join.
Definition brand_join (hs:brand_relation_t) (a b:brands)
:= canon_brands hs
(set_inter string_dec
(explode_brands hs a)
(explode_brands hs b)).
Lemma brand_join_is_canon hs a b :
is_canon_brands hs (brand_join hs a b).
Lemma brand_join_canon_l `{brand_relation} a b :
brand_join brand_relation_brands (canon_brands brand_relation_brands a) b
= brand_join brand_relation_brands a b.
Lemma brand_join_canon_r `{brand_relation} a b :
brand_join brand_relation_brands a (canon_brands brand_relation_brands b)
= brand_join brand_relation_brands a b.
Theorem brand_join_idempotent `{brand_relation} a :
brand_join brand_relation_brands a a
= canon_brands brand_relation_brands a.
Lemma brand_join_idempotent_can `{brand_relation} a :
is_canon_brands brand_relation_brands a →
brand_join brand_relation_brands a a = a.
Theorem brand_join_commutative hs a b :
brand_join hs a b = brand_join hs b a.
Lemma set_inter_preserves_explode_brands `{brand_relation} a b:
equivlist
(explode_brands brand_relation_brands
(set_inter string_dec
(explode_brands brand_relation_brands a)
(explode_brands brand_relation_brands b)))
(set_inter string_dec
(explode_brands brand_relation_brands a)
(explode_brands brand_relation_brands b)).
Theorem brand_join_associative`{brand_relation} a b c:
brand_join brand_relation_brands
(brand_join brand_relation_brands a b)
c
= brand_join brand_relation_brands a
(brand_join brand_relation_brands b c).
Lemma brand_join_consistent1 `{brand_relation} b b2 :
sub_brands brand_relation_brands b b2 →
brand_join brand_relation_brands b b2 =
(canon_brands brand_relation_brands b2).
Lemma brand_join_consistent2 `{brand_relation} b b2 :
brand_join brand_relation_brands b b2
= canon_brands brand_relation_brands b2
→ sub_brands brand_relation_brands b b2.
Theorem brand_join_consistent `{brand_relation} b b2 :
sub_brands brand_relation_brands b b2 ↔
brand_join brand_relation_brands b b2
= canon_brands brand_relation_brands b2.
Lemma brand_join_consistent_can `{brand_relation} b b2 :
is_canon_brands brand_relation_brands b2 →
(sub_brands brand_relation_brands b b2 ↔
brand_join brand_relation_brands b b2 = b2).
End brand_join.
Section brand_meet.
Definition brand_meet (hs:brand_relation_t) (a b:brands)
:= canon_brands hs (a ++ b).
Lemma brand_meet_is_canon hs a b :
is_canon_brands hs (brand_meet hs a b).
Lemma brand_meet_canon_l `{brand_relation} a b :
brand_meet brand_relation_brands (canon_brands brand_relation_brands a) b
= brand_meet brand_relation_brands a b.
Lemma brand_meet_canon_r `{brand_relation} a b :
brand_meet brand_relation_brands a (canon_brands brand_relation_brands b)
= brand_meet brand_relation_brands a b.
Theorem brand_meet_idempotent `{brand_relation} a :
brand_meet brand_relation_brands a a
= canon_brands brand_relation_brands a.
Lemma brand_meet_idempotent_can `{brand_relation} a :
is_canon_brands brand_relation_brands a →
brand_meet brand_relation_brands a a = a.
Theorem brand_meet_commutative `{brand_relation} a b :
brand_meet brand_relation_brands a b = brand_meet brand_relation_brands b a.
Theorem brand_meet_associative`{brand_relation} a b c:
brand_meet brand_relation_brands
(brand_meet brand_relation_brands a b)
c
= brand_meet brand_relation_brands a
(brand_meet brand_relation_brands b c).
Lemma brand_meet_consistent1 `{brand_relation} b b2 :
sub_brands brand_relation_brands b b2 →
brand_meet brand_relation_brands b b2 =
(canon_brands brand_relation_brands b).
Lemma brand_meet_consistent2 `{brand_relation} b b2 :
brand_meet brand_relation_brands b b2
= canon_brands brand_relation_brands b
→ sub_brands brand_relation_brands b b2.
Theorem brand_meet_consistent `{brand_relation} b b2 :
sub_brands brand_relation_brands b b2 ↔
brand_meet brand_relation_brands b b2
= canon_brands brand_relation_brands b.
Lemma brand_meet_consistent_can `{brand_relation} b b2 :
is_canon_brands brand_relation_brands b →
(sub_brands brand_relation_brands b b2 ↔
brand_meet brand_relation_brands b b2 = b).
End brand_meet.
Section meet_join.
Theorem brand_join_absorptive `{brand_relation} a b:
brand_join brand_relation_brands
a
(brand_meet brand_relation_brands a b)
= canon_brands brand_relation_brands a.
Lemma brand_join_absorptive_can `{brand_relation} a b:
is_canon_brands brand_relation_brands a →
brand_join brand_relation_brands
a
(brand_meet brand_relation_brands a b)
= a.
Theorem brand_meet_absorptive `{brand_relation} a b:
brand_meet brand_relation_brands
a
(brand_join brand_relation_brands a b)
= canon_brands brand_relation_brands a.
Lemma brand_meet_absorptive_can `{brand_relation} a b:
is_canon_brands brand_relation_brands a →
brand_meet brand_relation_brands
a
(brand_join brand_relation_brands a b)
= a.
End meet_join.
Section brands_lattice.
Context {br:brand_relation}.
Global Instance brands_lattice : Lattice brands (equiv_brands brand_relation_brands)
:= { meet:=brand_meet brand_relation_brands;
join:=brand_join brand_relation_brands
}.
Global Instance brands_olattice :
OLattice (equiv_brands brand_relation_brands) (sub_brands brand_relation_brands).
End brands_lattice.
Global Instance brand_relation_eqdec : EqDec brand_relation eq.