Require Import String.
Require Import List.
Require Import Bool.
Require Import EquivDec.
Require Import Eqdep_dec.
Require Import Basics.
Require Import ListSet.
Require Import Program.Basics.
Require Import RelationClasses EquivDec Morphisms.
Require Import Utils.
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
:=
forall 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
:=
forall 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}.
Proof.
Lemma brand_relation_assym_dec :
{
brand_relation_assym_t}
+ {~
brand_relation_assym_t}.
Proof.
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.
Proof.
Lemma brand_relation_assym :
brand_relation_assym_t brand_relation_brands.
Proof.
Lemma brand_relation_irrefl a : ~
In (
a,
a)
brand_relation_brands.
Proof.
End brand_relation_prop.
Lemma brand_relation_ext b pf1 pf2 pf1'
pf2' :
mkBrand_relation b pf1 pf2 =
mkBrand_relation b pf1'
pf2' .
Proof.
Lemma brand_relation_fequal {
br₁
br₂}:
@
brand_relation_brands br₁ = @
brand_relation_brands br₂ ->
br₁ =
br₂.
Proof.
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}.
Proof.
unfold sub_brand.
destruct (
a ==
b).
-
left;
intuition.
-
destruct (
in_dec equiv_dec (
a,
b)
br).
*
left;
intuition.
*
right;
intuition.
Defined.
Global Instance sub_brand_refl br :
Reflexive (
sub_brand br).
Proof.
repeat red; intuition.
Qed.
Global Instance sub_brand_pre `{
brand_relation} :
PreOrder (
sub_brand brand_relation_brands).
Proof.
Global Instance sub_brand_part `{
brand_relation} :
PartialOrder eq (
sub_brand brand_relation_brands).
Proof.
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.
Proof.
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.
Proof.
Definition sub_brands (
h:
brand_relation_t) (
a b:
brands)
:=
forall y,
In y b ->
exists 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}.
Proof.
Global Instance sub_brands_pre `{
brand_relation} :
PreOrder (
sub_brands brand_relation_brands).
Proof.
unfold sub_brands.
constructor;
red;
intros.
-
exists y;
intuition.
-
destruct (
H1 _ H2)
as [
y' [
yin ysb]].
destruct (
H0 _ yin)
as [
z' [
zin zsb]].
exists z';
split.
+
intuition.
+
etransitivity;
eauto.
Qed.
Lemma incl_sub_brands (
hs:
brand_relation_t) (
a b:
brands) :
incl a b ->
sub_brands hs b a.
Proof.
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).
Proof.
Global Instance equiv_brands_sub_flip_subr (
hs:
brand_relation_t) :
subrelation (
equiv_brands hs) (
flip (
sub_brands hs)).
Proof.
Definition equiv_brands_dec br a b :
{
equiv_brands br a b} + {~
equiv_brands br a b}.
Proof.
Global Instance equiv_brands_equiv `{
brand_relation} :
Equivalence (
equiv_brands brand_relation_brands).
Proof.
unfold equiv_brands.
constructor;
red;
intros.
-
intuition.
-
intuition.
-
intuition;
etransitivity;
eauto.
Qed.
Global Instance equiv_brands_eqdec `{
brand_relation} :
EqDec brands (
equiv_brands brand_relation_brands).
Proof.
Global Instance equivlist_equiv_brands (
hs:
brand_relation_t)
:
subrelation equivlist (
equiv_brands hs).
Proof.
Global Instance sub_brands_part `{
brand_relation} :
PartialOrder (
equiv_brands brand_relation_brands) (
sub_brands brand_relation_brands).
Proof.
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).
Proof.
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).
Proof.
Lemma sub_brands_any hs b :
sub_brands hs b any.
Proof.
Lemma any_sub_brands hs b :
sub_brands hs any b ->
b =
any.
Proof.
unfold sub_brands,
any.
destruct b;
trivial;
intros.
destruct (
H b);
simpl;
intuition.
Qed.
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.
Proof.
unfold parents.
split.
-
intros inn.
apply in_map_iff in inn.
destruct inn as [[? ?] [?
inn]];
simpl in *;
subst.
apply filter_In in inn.
destruct inn as [??];
unfold brand in *;
match goal with [
H:
context [
match ?
x with _ =>
_ end] |-
_] =>
destruct x end;
trivial;
unfold equiv,
complement in *;
simpl in *;
congruence.
-
intros inn.
apply in_map_iff.
exists (
a,
s);
simpl;
intuition.
apply filter_In;
intuition.
simpl.
unfold brand in *;
match goal with [|-
context [
match ?
x with _ =>
_ end] ] =>
destruct x end;
trivial;
unfold equiv,
complement in *;
simpl in *;
congruence.
Qed.
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.
Proof.
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).
Proof.
Lemma sub_explode_brands
(
hs:
brand_relation_t) (
a:
brands) :
sub_brands hs (
explode_brands hs a)
a.
Proof.
Lemma explode_brands_sub
(
hs:
brand_relation_t) (
a:
brands) :
sub_brands hs a (
explode_brands hs a).
Proof.
Lemma explode_brands_equivbrands
(
hs:
brand_relation_t) (
a:
brands) :
equiv_brands hs (
explode_brands hs a)
a.
Proof.
Global Instance explode_brands_proper `{
brand_relation} :
Proper (
equiv_brands brand_relation_brands ==>
equiv_brands brand_relation_brands) (
explode_brands brand_relation_brands).
Proof.
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.
Proof.
Lemma explode_brands_incl hs b a:
sub_brands hs a b ->
incl b (
explode_brands hs a).
Proof.
Global Instance explode_brands_properequiv `{
brand_relation} :
Proper (
equiv_brands brand_relation_brands ==>
equivlist) (
explode_brands brand_relation_brands).
Proof.
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).
Proof.
Lemma explode_brands_app_incl hs a b :
incl (
explode_brands hs a)
(
explode_brands hs (
a++
b)).
Proof.
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.
Proof.
Lemma collapse_brands_incl (
hs:
brand_relation_t) (
a:
brands) :
incl (
collapse_brands hs a)
a.
Proof.
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.
Proof.
Lemma nosub_collapse_brands hs a :
(
forall x y :
brand,
In x a ->
In y a -> ~
In (
x,
y)
hs) ->
collapse_brands hs a =
a.
Proof.
Lemma collapse_brands_nosub hs a :
collapse_brands hs a =
a ->
(
forall x y :
brand,
In x a ->
In y a -> ~
In (
x,
y)
hs).
Proof.
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.
Proof.
simpl.
rewrite orb_comm;
simpl;
trivial.
Qed.
Lemma has_subtype_in_not_self `{
brand_relation}
a :
has_subtype_in brand_relation_brands (
a ::
nil)
a =
false.
Proof.
Lemma collapse_brands_singleton {
br:
brand_relation} (
bb:
brand)
:
collapse_brands brand_relation_brands (
singleton bb) =
singleton bb.
Proof.
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.
Proof.
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}.
Proof.
Lemma sub_collapse_brands `{
brand_relation} (
a:
brands) :
sub_brands brand_relation_brands
(
collapse_brands brand_relation_brands a)
a.
Proof.
Lemma collapse_brands_sub
(
hs:
brand_relation_t) (
a:
brands) :
sub_brands hs a (
collapse_brands hs a).
Proof.
Lemma collapse_brands_equivbrands
`{
brand_relation} (
a:
brands) :
equiv_brands brand_relation_brands
(
collapse_brands brand_relation_brands a)
a.
Proof.
Lemma collapse_collapses `{
brand_relation} (
a:
brands) :
forall x y,
In x a ->
In y (
collapse_brands brand_relation_brands a) ->
~
In (
x,
y)
brand_relation_brands.
Proof.
Global Instance collapse_brands_proper `{
brand_relation} :
Proper (
equiv_brands brand_relation_brands ==>
equiv_brands brand_relation_brands) (
collapse_brands brand_relation_brands).
Proof.
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.
Proof.
Lemma existsb_app {
A} (
f:
A->
bool)
l1 l2 :
existsb f (
l1 ++
l2) =
existsb f l1 ||
existsb f l2.
Proof.
induction l1;
simpl;
trivial.
rewrite IHl1.
rewrite orb_assoc;
trivial.
Qed.
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.
Proof.
Lemma sort_brands_equiv hs a :
equiv_brands hs (
insertion_sort StringOrder.lt_dec a)
a.
Proof.
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.
Proof.
Lemma canon_brands_equiv `{
brand_relation} (
a:
brands)
:
equiv_brands
brand_relation_brands
(
canon_brands brand_relation_brands a)
a.
Proof.
Global Instance has_subtype_in_proper_equivlist :
Proper (
eq ==>
equivlist ==>
eq ==>
eq)
has_subtype_in.
Proof.
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).
Proof.
Lemma canon_brands_incl (
hs:
brand_relation_t) (
a:
brands) :
incl (
canon_brands hs a)
a.
Proof.
Definition is_canon_brands (
hs:
brand_relation_t) (
a:
brands)
:=
is_list_sorted StringOrder.lt_dec a =
true
/\ (
forall 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).
Proof.
Lemma is_canon_brands_canon_brands hs a :
is_canon_brands hs a ->
canon_brands hs a =
a.
Proof.
Lemma canon_brands_idempotent (
hs:
brand_relation_t) (
a:
brands) :
canon_brands hs (
canon_brands hs a)
=
canon_brands hs a.
Proof.
Lemma is_canon_brands_dec (
hs:
brand_relation_t) (
a:
brands) :
{
is_canon_brands hs a} + {~
is_canon_brands hs a}.
Proof.
Lemma is_canon_brands_singleton {
br:
brand_relation} (
bb:
brand)
:
is_canon_brands brand_relation_brands (
singleton bb).
Proof.
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.
Proof.
Global Instance canon_proper `{
brand_relation} :
Proper (
equiv_brands brand_relation_brands ==>
eq) (
canon_brands brand_relation_brands).
Proof.
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).
Proof.
Definition equiv_brands_dec_alt `{
brand_relation}
a b :
{
equiv_brands brand_relation_brands a b}
+ {~
equiv_brands brand_relation_brands a b}.
Proof.
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).
Proof.
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).
Proof.
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).
Proof.
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.
Proof.
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.
Proof.
Theorem brand_join_idempotent `{
brand_relation}
a :
brand_join brand_relation_brands a a
=
canon_brands brand_relation_brands a.
Proof.
Lemma brand_join_idempotent_can `{
brand_relation}
a :
is_canon_brands brand_relation_brands a ->
brand_join brand_relation_brands a a =
a.
Proof.
Theorem brand_join_commutative hs a b :
brand_join hs a b =
brand_join hs b a.
Proof.
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)).
Proof.
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).
Proof.
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).
Proof.
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.
Proof.
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.
Proof.
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).
Proof.
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).
Proof.
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.
Proof.
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.
Proof.
Theorem brand_meet_idempotent `{
brand_relation}
a :
brand_meet brand_relation_brands a a
=
canon_brands brand_relation_brands a.
Proof.
Lemma brand_meet_idempotent_can `{
brand_relation}
a :
is_canon_brands brand_relation_brands a ->
brand_meet brand_relation_brands a a =
a.
Proof.
Theorem brand_meet_commutative `{
brand_relation}
a b :
brand_meet brand_relation_brands a b =
brand_meet brand_relation_brands b a.
Proof.
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).
Proof.
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).
Proof.
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.
Proof.
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.
Proof.
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).
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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.
Proof.
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
}.
Proof.
Global Instance brands_olattice :
OLattice (
equiv_brands brand_relation_brands) (
sub_brands brand_relation_brands).
Proof.
End brands_lattice.
Global Instance brand_relation_eqdec :
EqDec brand_relation eq.
Proof.
Hint Resolve canon_brands_is_canon_brands.