diff --git a/theories/base.v b/theories/base.v index f42df42affd16dcf8734e3f223fec3b0b295509e..5ff6bee7b664e8a6994c05bfef095afa943ffc9e 100644 --- a/theories/base.v +++ b/theories/base.v @@ -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) : diff --git a/theories/orders.v b/theories/orders.v index a8b7f2d20663c0496352813fd2dbbba612c2e995..0dd57462b40c49e54521da8409918aac0cab8397 100644 --- a/theories/orders.v +++ b/theories/orders.v @@ -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.