Commit 932ff6bd by 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 1b35575d
 ... @@ -580,10 +580,6 @@ Class LeftAbsorb {A} (R : relation A) (i : A) (f : A → A → A) : Prop := ... @@ -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. left_absorb: ∀ x, R (f i x) i. Class RightAbsorb {A} (R : relation A) (i : A) (f : A → A → A) : Prop := Class RightAbsorb {A} (R : relation A) (i : A) (f : A → A → A) : Prop := right_absorb: ∀ x, R (f x i) i. 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 := Class AntiSymmetric {A} (R S : relation A) : Prop := anti_symmetric: ∀ x y, S x y → S y x → R x y. 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. Class Total {A} (R : relation A) := total x y : R x y ∨ R y x. ... @@ -604,8 +600,6 @@ Arguments right_id {_ _} _ _ {_} _. ... @@ -604,8 +600,6 @@ Arguments right_id {_ _} _ _ {_} _. Arguments associative {_ _} _ {_} _ _ _. Arguments associative {_ _} _ {_} _ _ _. Arguments left_absorb {_ _} _ _ {_} _. Arguments left_absorb {_ _} _ _ {_} _. Arguments right_absorb {_ _} _ _ {_} _. Arguments right_absorb {_ _} _ _ {_} _. Arguments left_distr {_ _} _ _ {_} _ _ _. Arguments right_distr {_ _} _ _ {_} _ _ _. Arguments anti_symmetric {_ _} _ {_} _ _ _ _. Arguments anti_symmetric {_ _} _ {_} _ _ _ _. Arguments total {_} _ {_} _ _. Arguments total {_} _ {_} _ _. Arguments trichotomy {_} _ {_} _ _. Arguments trichotomy {_} _ {_} _ _. ... @@ -635,12 +629,6 @@ Proof. auto. Qed. ... @@ -635,12 +629,6 @@ Proof. auto. Qed. Lemma right_absorb_L {A} (i : A) (f : A → A → A) `{!RightAbsorb (=) i f} x : Lemma right_absorb_L {A} (i : A) (f : A → A → A) `{!RightAbsorb (=) i f} x : f x i = i. f x i = i. Proof. auto. Qed. 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 *) (** ** Axiomatization of ordered structures *) (** The classes [PreOrder], [PartialOrder], and [TotalOrder] use an arbitrary (** The classes [PreOrder], [PartialOrder], and [TotalOrder] use an arbitrary ... @@ -965,14 +953,6 @@ Instance: LeftId (↔) True impl. ... @@ -965,14 +953,6 @@ Instance: LeftId (↔) True impl. Proof. unfold impl. red; intuition. Qed. Proof. unfold impl. red; intuition. Qed. Instance: RightAbsorb (↔) True impl. Instance: RightAbsorb (↔) True impl. Proof. unfold impl. red; intuition. Qed. 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). Lemma not_injective `{Injective A B R R' f} x y : ¬R x y → ¬R' (f x) (f y). Proof. intuition. Qed. Proof. intuition. Qed. Instance injective_compose {A B C} R1 R2 R3 (f : A → B) (g : B → C) : Instance injective_compose {A B C} R1 R2 R3 (f : A → B) (g : B → C) : ... ...
 ... @@ -557,24 +557,23 @@ Section lattice. ... @@ -557,24 +557,23 @@ Section lattice. Proof. split. by apply intersection_subseteq_l. by apply subseteq_empty. Qed. Proof. split. by apply intersection_subseteq_l. by apply subseteq_empty. Qed. Global Instance: RightAbsorb ((≡) : relation A) ∅ (∩). Global Instance: RightAbsorb ((≡) : relation A) ∅ (∩). Proof. intros ?. by rewrite (commutative _), (left_absorb _ _). Qed. 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. Proof. intros X Y Z. split; [|apply lattice_distr]. split; [apply union_least|apply lattice_distr]. apply union_least. { apply intersection_greatest; auto using union_subseteq_l. } { apply intersection_greatest; auto using union_subseteq_l. } apply intersection_greatest. apply intersection_greatest. * apply union_subseteq_r_transitive, intersection_subseteq_l. * apply union_subseteq_r_transitive, intersection_subseteq_l. * apply union_subseteq_r_transitive, intersection_subseteq_r. * apply union_subseteq_r_transitive, intersection_subseteq_r. Qed. Qed. Global Instance: RightDistr ((≡) : relation A) (∪) (∩). Lemma union_intersection_r (X Y Z : A) : (X ∩ Y) ∪ Z ≡ (X ∪ Z) ∩ (Y ∪ Z). Proof. intros X Y Z. by rewrite !(commutative _ _ Z), (left_distr _ _). Qed. Proof. by rewrite !(commutative _ _ Z), union_intersection_l. Qed. Global Instance: LeftDistr ((≡) : relation A) (∩) (∪). Lemma intersection_union_l (X Y Z : A) : X ∩ (Y ∪ Z) ≡ (X ∩ Y) ∪ (X ∩ Z). Proof. Proof. intros X Y Z. split. split. * rewrite (left_distr (∪) (∩)). * rewrite union_intersection_l. apply intersection_greatest. apply intersection_greatest. { apply union_subseteq_r_transitive, intersection_subseteq_l. } { 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_preserving; auto using union_subseteq_l. * apply intersection_greatest. * apply intersection_greatest. { apply union_least; auto using intersection_subseteq_l. } { apply union_least; auto using intersection_subseteq_l. } ... @@ -582,8 +581,8 @@ Section lattice. ... @@ -582,8 +581,8 @@ Section lattice. + apply intersection_subseteq_r_transitive, union_subseteq_l. + apply intersection_subseteq_r_transitive, union_subseteq_l. + apply intersection_subseteq_r_transitive, union_subseteq_r. + apply intersection_subseteq_r_transitive, union_subseteq_r. Qed. Qed. Global Instance: RightDistr ((≡) : relation A) (∩) (∪). Lemma intersection_union_r (X Y Z : A) : (X ∪ Y) ∩ Z ≡ (X ∩ Z) ∪ (Y ∩ Z). Proof. intros X Y Z. by rewrite !(commutative _ _ Z), (left_distr _ _). Qed. Proof. by rewrite !(commutative _ _ Z), intersection_union_l. Qed. Section leibniz. Section leibniz. Context `{!LeibnizEquiv A}. Context `{!LeibnizEquiv A}. ... @@ -591,13 +590,13 @@ Section lattice. ... @@ -591,13 +590,13 @@ Section lattice. Proof. intros ?. unfold_leibniz. apply (left_absorb _ _). Qed. Proof. intros ?. unfold_leibniz. apply (left_absorb _ _). Qed. Global Instance: RightAbsorb (=) ∅ (∩). Global Instance: RightAbsorb (=) ∅ (∩). Proof. intros ?. unfold_leibniz. apply (right_absorb _ _). Qed. Proof. intros ?. unfold_leibniz. apply (right_absorb _ _). Qed. Global Instance: LeftDistr (=) (∪) (∩). Lemma union_intersection_l_L (X Y Z : A) : X ∪ (Y ∩ Z) = (X ∪ Y) ∩ (X ∪ Z). Proof. intros ???. unfold_leibniz. apply (left_distr _ _). Qed. Proof. unfold_leibniz; apply union_intersection_l. Qed. Global Instance: RightDistr (=) (∪) (∩). Lemma union_intersection_r_L (X Y Z : A) : (X ∩ Y) ∪ Z = (X ∪ Z) ∩ (Y ∪ Z). Proof. intros ???. unfold_leibniz. apply (right_distr _ _). Qed. Proof. unfold_leibniz; apply union_intersection_r. Qed. Global Instance: LeftDistr (=) (∩) (∪). Lemma intersection_union_l_L (X Y Z : A) : X ∩ (Y ∪ Z) ≡ (X ∩ Y) ∪ (X ∩ Z). Proof. intros ???. unfold_leibniz. apply (left_distr _ _). Qed. Proof. unfold_leibniz; apply intersection_union_l. Qed. Global Instance: RightDistr (=) (∩) (∪). Lemma intersection_union_r_L (X Y Z : A) : (X ∪ Y) ∩ Z ≡ (X ∩ Z) ∪ (Y ∩ Z). Proof. intros ???. unfold_leibniz. apply (right_distr _ _). Qed. Proof. unfold_leibniz; apply intersection_union_r. Qed. End leibniz. End leibniz. End lattice. 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