Commit 6b1c085d authored by Robbert Krebbers's avatar Robbert Krebbers

Remove LeftDistr and LeftDistr classes.

These are hardly used, and confusing since we have so many operations of
different arities that distribute.
parent 068dd357
......@@ -580,10 +580,6 @@ Class LeftAbsorb {A} (R : relation A) (i : A) (f : A → A → A) : Prop :=
left_absorb: x, R (f i x) i.
Class RightAbsorb {A} (R : relation A) (i : A) (f : A A A) : Prop :=
right_absorb: x, R (f x i) i.
Class LeftDistr {A} (R : relation A) (f g : A A A) : Prop :=
left_distr: x y z, R (f x (g y z)) (g (f x y) (f x z)).
Class RightDistr {A} (R : relation A) (f g : A A A) : Prop :=
right_distr: y z x, R (f (g y z) x) (g (f y x) (f z x)).
Class AntiSymmetric {A} (R S : relation A) : Prop :=
anti_symmetric: x y, S x y S y x R x y.
Class Total {A} (R : relation A) := total x y : R x y R y x.
......@@ -604,8 +600,6 @@ Arguments right_id {_ _} _ _ {_} _.
Arguments associative {_ _} _ {_} _ _ _.
Arguments left_absorb {_ _} _ _ {_} _.
Arguments right_absorb {_ _} _ _ {_} _.
Arguments left_distr {_ _} _ _ {_} _ _ _.
Arguments right_distr {_ _} _ _ {_} _ _ _.
Arguments anti_symmetric {_ _} _ {_} _ _ _ _.
Arguments total {_} _ {_} _ _.
Arguments trichotomy {_} _ {_} _ _.
......@@ -635,12 +629,6 @@ Proof. auto. Qed.
Lemma right_absorb_L {A} (i : A) (f : A A A) `{!RightAbsorb (=) i f} x :
f x i = i.
Proof. auto. Qed.
Lemma left_distr_L {A} (f g : A A A) `{!LeftDistr (=) f g} x y z :
f x (g y z) = g (f x y) (f x z).
Proof. auto. Qed.
Lemma right_distr_L {A} (f g : A A A) `{!RightDistr (=) f g} y z x :
f (g y z) x = g (f y x) (f z x).
Proof. auto. Qed.
(** ** Axiomatization of ordered structures *)
(** The classes [PreOrder], [PartialOrder], and [TotalOrder] use an arbitrary
......@@ -965,14 +953,6 @@ Instance: LeftId (↔) True impl.
Proof. unfold impl. red; intuition. Qed.
Instance: RightAbsorb () True impl.
Proof. unfold impl. red; intuition. Qed.
Instance: LeftDistr () () ().
Proof. red; intuition. Qed.
Instance: RightDistr () () ().
Proof. red; intuition. Qed.
Instance: LeftDistr () () ().
Proof. red; intuition. Qed.
Instance: RightDistr () () ().
Proof. red; intuition. Qed.
Lemma not_injective `{Injective A B R R' f} x y : ¬R x y ¬R' (f x) (f y).
Proof. intuition. Qed.
Instance injective_compose {A B C} R1 R2 R3 (f : A B) (g : B C) :
......
......@@ -557,24 +557,23 @@ Section lattice.
Proof. split. by apply intersection_subseteq_l. by apply subseteq_empty. Qed.
Global Instance: RightAbsorb (() : relation A) ().
Proof. intros ?. by rewrite (commutative _), (left_absorb _ _). Qed.
Global Instance: LeftDistr (() : relation A) () ().
Lemma union_intersection_l (X Y Z : A) : X (Y Z) (X Y) (X Z).
Proof.
intros X Y Z. split; [|apply lattice_distr].
apply union_least.
split; [apply union_least|apply lattice_distr].
{ apply intersection_greatest; auto using union_subseteq_l. }
apply intersection_greatest.
* apply union_subseteq_r_transitive, intersection_subseteq_l.
* apply union_subseteq_r_transitive, intersection_subseteq_r.
Qed.
Global Instance: RightDistr (() : relation A) () ().
Proof. intros X Y Z. by rewrite !(commutative _ _ Z), (left_distr _ _). Qed.
Global Instance: LeftDistr (() : relation A) () ().
Lemma union_intersection_r (X Y Z : A) : (X Y) Z (X Z) (Y Z).
Proof. by rewrite !(commutative _ _ Z), union_intersection_l. Qed.
Lemma intersection_union_l (X Y Z : A) : X (Y Z) (X Y) (X Z).
Proof.
intros X Y Z. split.
* rewrite (left_distr () ()).
split.
* rewrite union_intersection_l.
apply intersection_greatest.
{ apply union_subseteq_r_transitive, intersection_subseteq_l. }
rewrite (right_distr () ()).
rewrite union_intersection_r.
apply intersection_preserving; auto using union_subseteq_l.
* apply intersection_greatest.
{ apply union_least; auto using intersection_subseteq_l. }
......@@ -582,8 +581,8 @@ Section lattice.
+ apply intersection_subseteq_r_transitive, union_subseteq_l.
+ apply intersection_subseteq_r_transitive, union_subseteq_r.
Qed.
Global Instance: RightDistr (() : relation A) () ().
Proof. intros X Y Z. by rewrite !(commutative _ _ Z), (left_distr _ _). Qed.
Lemma intersection_union_r (X Y Z : A) : (X Y) Z (X Z) (Y Z).
Proof. by rewrite !(commutative _ _ Z), intersection_union_l. Qed.
Section leibniz.
Context `{!LeibnizEquiv A}.
......@@ -591,13 +590,13 @@ Section lattice.
Proof. intros ?. unfold_leibniz. apply (left_absorb _ _). Qed.
Global Instance: RightAbsorb (=) ().
Proof. intros ?. unfold_leibniz. apply (right_absorb _ _). Qed.
Global Instance: LeftDistr (=) () ().
Proof. intros ???. unfold_leibniz. apply (left_distr _ _). Qed.
Global Instance: RightDistr (=) () ().
Proof. intros ???. unfold_leibniz. apply (right_distr _ _). Qed.
Global Instance: LeftDistr (=) () ().
Proof. intros ???. unfold_leibniz. apply (left_distr _ _). Qed.
Global Instance: RightDistr (=) () ().
Proof. intros ???. unfold_leibniz. apply (right_distr _ _). Qed.
Lemma union_intersection_l_L (X Y Z : A) : X (Y Z) = (X Y) (X Z).
Proof. unfold_leibniz; apply union_intersection_l. Qed.
Lemma union_intersection_r_L (X Y Z : A) : (X Y) Z = (X Z) (Y Z).
Proof. unfold_leibniz; apply union_intersection_r. Qed.
Lemma intersection_union_l_L (X Y Z : A) : X (Y Z) (X Y) (X Z).
Proof. unfold_leibniz; apply intersection_union_l. Qed.
Lemma intersection_union_r_L (X Y Z : A) : (X Y) Z (X Z) (Y Z).
Proof. unfold_leibniz; apply intersection_union_r. Qed.
End leibniz.
End lattice.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment