From 6b1c085d9718eb11faadc0dc369a2e841f96982d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 14 Jan 2016 23:21:34 +0100
Subject: [PATCH] Remove LeftDistr and LeftDistr classes.

These are hardly used, and confusing since we have so many operations of
different arities that distribute.
---
 prelude/base.v   | 20 --------------------
 prelude/orders.v | 37 ++++++++++++++++++-------------------
 2 files changed, 18 insertions(+), 39 deletions(-)

diff --git a/prelude/base.v b/prelude/base.v
index f42df42af..5ff6bee7b 100644
--- a/prelude/base.v
+++ b/prelude/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/prelude/orders.v b/prelude/orders.v
index a8b7f2d20..0dd57462b 100644
--- a/prelude/orders.v
+++ b/prelude/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.
-- 
GitLab