posets.lean

import algebra.order
import standard
import logic
open algebra bool eq.ops

structure poset [class] (A: Type) extends has_le A :=
  (le_refl : ∀a, le a a)
  (le_trans : ∀a b c, le a b → le b c → le a c)

definition weak_order.to_poset [instance] [coercion] [reducible]
           (A : Type) [p : weak_order A]
           : poset A :=
  ⦃ poset
  , le_refl := weak_order.le_refl
  , le_trans := weak_order.le_trans
  ⦄

notation a `≰`:50 b := ¬(a ≤ b)

example {A : Type} (P : A → Prop) : (¬∃x, P x) ↔ ∀x, ¬ P x :=
begin
  apply iff.intro,
  intro H1,
    intro x,
    intro Hpx,
    have Hexpx : ∃ x, P x, from exists.intro x Hpx,
    exact (H1 Hexpx),
  intro H1,
    intro H2,
    exact (exists.elim H2 H1), 
end

example (P Q : Prop) : ¬(P ∧ Q) ↔ (P → ¬Q) := 
begin
  apply iff.intro,
  intro Hnpq,
  intro Hp,
  intro Hq,
  have Hpq : P ∧ Q, by apply and.intro ; exact Hp ; exact Hq,
  exact (Hnpq Hpq),
  intro Hpnq,
  intro Hpq,
  have Hp : P, from and.left Hpq,
  have Hq : Q, from and.right Hpq,
  have Hnq : ¬Q, from Hpnq Hp,
  exact (Hnq Hq)
end

definition has_le.compatible   {A : Type} [p : has_le A] (a b : A) := ∃c : A, c ≤ a ∧ c ≤ b
definition has_le.incompatible {A : Type} [p : has_le A] (a b : A) := ∀c : A, c ≤ a → c ≰ b

infix `∥`:50 := has_le.compatible
infix `⊥`:50 := has_le.incompatible

structure separative_order [class] (A : Type) extends weak_order A :=
  (le_separative : ∀ (p q : A), (∀(x : A), le x p → ∃ c, le c x ∧ le c q) → le p q)

section
  variable A : Type
  variable [s : separative_order A]
  include s

  theorem le.separative {p q : A} : (∀x, x ≤ p → x ∥ q) → p ≤ q := !separative_order.le_separative
  theorem le_iff_compat {p q : A} : p ≤ q ↔ (∀x, x ≤ p → x ∥ q) :=
  begin
    apply iff.intro,
    intro Hpq,
    intro x,
    intro Hxp,
    fapply exists.intro,
      exact x,
      apply and.intro,
      apply le.refl,
      apply le.trans,
      eassumption,
      exact Hpq,
      exact !le.separative
  end
end

structure sup_semilattice [class] (A : Type) extends add_comm_semigroup A :=
   (add_idempotent : ∀x, add x x = x)

definition add.idempotent {A : Type}
           [s : sup_semilattice A] {a : A} : a + a = a := !sup_semilattice.add_idempotent

namespace sup_semilattice
  variable {A : Type}
  variable [s : sup_semilattice A]
  include s

  definition to_weak_order [instance] [coercion] [reducible]
           : weak_order A :=
  ⦃ weak_order A
  , le := λ x y : A, x + y = y
  , le_refl := sup_semilattice.add_idempotent
  , le_trans := λa b c Habb Hbcc,
      calc
         a + c = a + (b + c) : Hbcc
           ... = (a + b) + c : add.assoc
           ... = b + c       : Habb
           ... = c           : Hbcc
  , le_antisymm := λa b Hab Hba,
      calc
          a = b + a               : Hba
        ... = a + b               : add.comm
        ... = b                   : Hab
  ⦄


  theorem le_add_left (a b : A) : a ≤ a + b := 
  calc
    a + (a + b) = (a + a) + b  : add.assoc
            ... = a + b        : add_idempotent

  theorem le_add_right (a b : A) : b ≤ a + b := 
  calc
    b   ≤ b + a : le_add_left
    ... = a + b : add_comm

  theorem add_le_add_left {a b : A} (H : a ≤ b) (c : A) : c + a ≤ c + b :=
  calc
    (c + a) + (c + b) = ((c + a) + c) + b  : add.assoc
                  ... = c + (c + a) + b    : add_comm
                  ... = (c + c) + a + b    : add_assoc
                  ... = c + a + b          : add_idempotent
                  ... = c + (a + b)        : add_assoc
                  ... = c + b              : H

  theorem add_le_add_right {a b : A} (H : a ≤ b) (c : A) : a + c ≤ b + c :=
  add.comm c a ▸ add.comm c b ▸ add_le_add_left H c

  theorem add_le_add {a b c d : A} (Hab : a ≤ b) (Hcd : c ≤ d) : a + c ≤ b + d := 
    le.trans (add_le_add_right Hab c) (add_le_add_left Hcd b)

  theorem add_sup (a b : A) : ∀x, (a ≤ x ∧ b ≤ x) ↔ a + b ≤ x := 
  begin
    intro x,
    apply iff.intro,
    { intro H,
      have Hax : a ≤ x, from and.left H,
      have Hbx : b ≤ x, from and.right H,
      exact calc
        a + b + x = a + (b + x)  : add.assoc
              ... = a + x        : Hbx
              ... = x            : Hax
      },
    { intro H,
      apply and.intro,
      { exact calc
             a ≤ a + b  : le_add_left
           ... ≤ x      : H},
      { exact calc
             b ≤ a + b  : le_add_right
           ... ≤ x      : H}}
  end
end sup_semilattice

structure inf_semilattice [class] (A : Type) extends comm_semigroup A :=
   (mul_idempotent : ∀x, mul x x = x)

definition mul.idempotent (A : Type)
           [s : inf_semilattice A] (a : A) : a * a = a := !inf_semilattice.mul_idempotent

namespace inf_semilattice
  variables {A : Type} [s : inf_semilattice A]
  include s

  definition to_weak_order [instance] [coercion] [reducible]
           : weak_order A :=
  ⦃ weak_order A
  , le := λ x y : A, x * y = x
  , le_refl := inf_semilattice.mul_idempotent
  , le_trans := λa b c Haba Hbcb,
      calc
         a * c = (a * b) * c : Haba
           ... = a * (b * c) : semigroup.mul_assoc
           ... = a * b       : Hbcb
           ... = a           : Haba
  , le_antisymm := λa b Hab Hba,
      calc
          a = a * b               : Hab
        ... = b * a               : comm_semigroup.mul_comm
        ... = b                   : Hba
  ⦄

  theorem mul_le_left (a b : A) : a * b ≤ a :=
  calc
    a * b * a = a * (b * a)  : mul.assoc
          ... = a * (a * b)  : mul.comm
          ... = (a * a) * b  : mul.assoc
          ... = a * b        : mul_idempotent

  theorem mul_le_right (a b : A) : a * b ≤ b :=
  calc
    a * b = b * a : mul_comm
      ... ≤ b     : mul_le_left

  theorem mul_inf (a b : A) : ∀x, (x ≤ a ∧ x ≤ b) ↔ x ≤ a * b := 
  begin
    intro x,
    apply iff.intro,
    { intro H,
      have Hxa : x * a = x, from (and.left H),
      have Hxb : x * b = x, from (and.right H),
      rewrite [▸ (_ = _), -mul.assoc, Hxa, Hxb]
      },
    { intro H
    , apply and.intro,
      { exact (calc
            x ≤ a * b : H
          ... ≤ a     : mul_le_left)},
      { exact (calc
            x ≤ a * b : H
          ... ≤ b     : mul_le_right)}
    }
  end

  theorem mul_le_mul_left {a b : A} (H : a ≤ b) (c : A) : c * a ≤ c * b :=
  calc
    (c * a) * (c * b) = ((c * a) * c) * b  : mul.assoc
                  ... = c * (c * a) * b    : mul_comm
                  ... = (c * c) * a * b    : mul_assoc
                  ... = c * a * b          : mul_idempotent
                  ... = c * (a * b)        : mul_assoc
                  ... = c * a              : H

  theorem mul_le_mul_right {a b : A} (H : a ≤ b) (c : A) : a * c ≤ b * c :=
  mul.comm c a ▸ mul.comm c b ▸ mul_le_mul_left H c

  theorem mul_le_mul {a b c d : A} (Hab : a ≤ b) (Hcd : c ≤ d) : a * c ≤ b * d := 
    le.trans (mul_le_mul_right Hab c) (mul_le_mul_left Hcd b)
end inf_semilattice


structure bounded_sup_semilattice [class] (A : Type) extends sup_semilattice A, add_comm_monoid A

namespace bounded_sup_semilattice
  variables {A : Type} [s : bounded_sup_semilattice A]
  include s
  open sup_semilattice

  definition zero_min
            (a : A) : 0 ≤ a := add_monoid.zero_add a
end bounded_sup_semilattice


structure bounded_inf_semilattice [class] (A : Type) extends inf_semilattice A, comm_monoid A

namespace bounded_inf_semilattice
  variables {A : Type} [s : bounded_inf_semilattice A]
  include s
  open inf_semilattice
  definition one_max (a : A) : a ≤ 1 := monoid.mul_one a
end bounded_inf_semilattice


structure lattice [class] (A : Type) extends sup_semilattice A, inf_semilattice A :=
  (add_mul_absorptive : ∀a b, add a (mul a b) = a)
  (mul_add_absorptive : ∀a b, mul a (add a b) = a)

namespace lattice
  variable {A : Type}
  variable [s : lattice A]
  include s

  open sup_semilattice inf_semilattice

  theorem add.absorves_mul_left  (a b : A) : a + (a * b) = a := !add_mul_absorptive
  theorem add.absorves_mul_right (a b : A) : (a * b) + a = a :=
    by rewrite [add.comm, add.absorves_mul_left]

  theorem mul.absorves_add_left  (a b : A) : a * (a + b) = a := !mul_add_absorptive
  theorem mul.absorves_add_right (a b : A) : (a + b) * a = a :=
    by rewrite [mul.comm, mul.absorves_add_left]

  theorem suple_iff_infle (a b : A) : a + b = b ↔ a * b = a :=
  begin
    apply iff.intro,
    intro Habb,
    rewrite
     (calc
       a * b = a * (a + b) : Habb
         ... = a           : mul_add_absorptive),
    intro Haba,
    rewrite
     (calc
       a + b = (a * b) + b : Haba
         ... = b + (a * b) : add_comm
         ... = b + (b * a) : mul_comm
         ... = b           : add_mul_absorptive)
  end
 
  definition to_weak_order [coercion] [instance] [reducible] : weak_order A :=
    sup_semilattice.to_weak_order

  theorem le_add_left (a b : A) : a ≤ a + b :=
  !sup_semilattice.le_add_left

  theorem le_add_right (a b : A) : b ≤ a + b :=
  !sup_semilattice.le_add_right

  theorem add_sup (a b x : A) :(a ≤ x ∧ b ≤ x) ↔ (a + b ≤ x) :=
  !sup_semilattice.add_sup

  theorem mul_le_left (a b : A) : a * b ≤ a :=
  iff.mp' !suple_iff_infle !inf_semilattice.mul_le_left

  theorem mul_le_right (a b : A) : a * b ≤ b :=
  iff.mp' !suple_iff_infle !inf_semilattice.mul_le_right

  theorem mul_inf (a b x : A) : (x ≤ a ∧ x ≤ b) ↔ x ≤ a * b := 
  begin
    apply iff.intro,
    { intro H,
      have Hxa : x * a = x, from iff.mp !suple_iff_infle (and.left H),
      have Hxb : x * b = x, from iff.mp !suple_iff_infle (and.right H),
      have Hxab : x * (a * b) = x, from iff.mp !inf_semilattice.mul_inf (and.intro Hxa Hxb), 
      exact (iff.mp' !suple_iff_infle Hxab)
      },
    { intro H,
      have Hxab' : x * (a * b) = x, from iff.mp !suple_iff_infle H, 
      have Hxaxb : x * a = x ∧ x * b = x, from iff.mp' !inf_semilattice.mul_inf Hxab',
      exact (and_of_and_of_imp_of_imp Hxaxb (iff.mp' !suple_iff_infle) (iff.mp' !suple_iff_infle))
     }
  end

end lattice

section
  variables {A : Type} [s : lattice A]
  include s
  open lattice
  theorem le_add_left  (a b : A) : a ≤ a + b := !lattice.le_add_left
  theorem le_add_right (a b : A) : b ≤ a + b := !lattice.le_add_right

  theorem add.sup (a b x : A) : (a ≤ x ∧ b ≤ x) ↔ (a + b ≤ x) :=
          !lattice.add_sup

  theorem mul_le_left  (a b : A) : a * b ≤ a := !lattice.mul_le_left
  theorem mul_le_right (a b : A) : a * b ≤ b := !lattice.mul_le_right

  theorem mul.inf (a b x : A) : (x ≤ a ∧ x ≤ b) ↔ (x ≤ a * b) :=
          !lattice.mul_inf

  theorem add_le_add_left {a b : A} (H : a ≤ b) (c : A) : c + a ≤ c + b :=
  sup_semilattice.add_le_add_left H c

  theorem add_le_add_right {a b : A} (H : a ≤ b) (c : A) : a + c ≤ b + c :=
  sup_semilattice.add_le_add_right H c

  theorem add_le_add {a b c d : A} (Hab : a ≤ b) (Hcd : c ≤ d) : a + c ≤ b + d :=
  sup_semilattice.add_le_add Hab Hcd

  theorem mul_le_mul_left {a b : A} (H : a ≤ b) (c : A) : c * a ≤ c * b :=
  iff.mp' !suple_iff_infle (inf_semilattice.mul_le_mul_left (iff.mp !suple_iff_infle H) c)

  theorem mul_le_mul_right {a b : A} (H : a ≤ b) (c : A) : a * c ≤ b * c :=
  iff.mp' !suple_iff_infle (inf_semilattice.mul_le_mul_right (iff.mp !suple_iff_infle H) c)


  theorem mul_le_mul {a b c d : A} (Hab : a ≤ b) (Hcd : c ≤ d) : a * c ≤ b * d :=
  iff.mp' !suple_iff_infle
    (inf_semilattice.mul_le_mul (iff.mp !suple_iff_infle Hab)
                                (iff.mp !suple_iff_infle Hcd))

end


structure distrib_lattice [class] (A : Type) extends lattice A  :=
  (add_mul_distrib: ∀a b c, add a (mul b c) = mul (add a b) (add a c))
  (mul_add_distrib: ∀a b c, mul a (add b c) = add (mul a b) (mul a c))

section
  variable {A : Type}
  variable [s : distrib_lattice A]
  include s
  open distrib_lattice
  theorem mul.distrib_over_add_left {a b c : A}
          : a * (b + c) = a * b + a * c := !mul_add_distrib
  theorem mul.distrib_over_add_right {a b c : A}
          : (a + b) * c = a * c + b * c :=
  begin
    rewrite [mul.comm, mul.distrib_over_add_left, mul.comm, mul.comm c b]
  end

  theorem add.distrib_over_mul_left {a b c : A}
          : a + (b * c) = (a + b) * (a + c) := !add_mul_distrib

  theorem add.distrib_over_mul_right {a b c : A}
          : (a * b) + c = (a + c) * (b + c) :=
  begin
    rewrite [add.comm, add.distrib_over_mul_left, add.comm, add.comm c b]
  end
end


namespace distrib_lattice
  variable {A : Type}
  variable [s : distrib_lattice A]
  include s
  open lattice

  definition to_distrib [instance] [coercion] [reducible] : distrib A :=
  ⦃ distrib
  , left_distrib := λa b c,
      calc
        a * (b + c) = a * b + a * c : mul_add_distrib
  , right_distrib := λa b c,
    calc
      (a + b) * c = c * (a + b)    : mul.comm
              ... = c * a + c * b  : mul_add_distrib
              ... = a * c + c * b  : mul.comm
              ... = a * c + b * c  : mul.comm
  ⦄

end distrib_lattice

structure bounded_lattice [class] (A : Type)
  extends lattice A, bounded_sup_semilattice A,
          bounded_inf_semilattice A

namespace bounded_lattice
  open lattice
  variable {A : Type}
  variable [s : bounded_lattice A]
  include s

  theorem zero_min : ∀a, 0 ≤ a := bounded_sup_semilattice.zero_min
  theorem one_max (a : A) : a ≤ 1 :=
  begin
    fapply (iff.mp' !suple_iff_infle),
    exact !mul_one
  end

  theorem le_zero (a : A) (H : a ≤ 0) : a = 0 := !le.antisymm H !zero_min
  theorem one_le (a : A) (H : 1 ≤ a) : a = 1 := !le.antisymm !one_max H

  theorem zero_mul (a : A) : 0 * a = 0 := 
  begin
    apply !le_zero,
    exact calc
      0 * a + 0 = 0 + 0 * a : add.comm
            ... = 0         : add_mul_absorptive
  end

  theorem mul_zero (a : A) : a * 0 = 0 := 
  calc
    a * 0 = 0 * a : mul.comm
      ... = 0     : zero_mul

  theorem one_add (a : A) : 1 + a = 1 :=
  begin
    apply !one_le,
    apply (iff.mp' !suple_iff_infle),
    exact !mul_add_absorptive
  end

  theorem add_one (a : A) : a + 1 = 1 := 
  calc
    a + 1 = 1 + a : add.comm
      ... = 1     : one_add

end bounded_lattice


structure bounded_distrib_lattice [class] (A : Type) extends distrib_lattice A, bounded_lattice A

-- Structure with relative pseudo complement
structure has_rp_comp [class] (A : Type) :=
   (rp_comp : A → A → A)

infixl `⊸`:65 := has_rp_comp.rp_comp

check @weak_order.le


definition bool.lattice [instance] : lattice bool := 
  ⦃ lattice
  , add := bor
  , mul := band
  , add_idempotent := by intro a; cases a; repeat (exact rfl)
  , mul_idempotent := by intro a; cases a; repeat (exact rfl)
  , add_comm := by intros; cases a; repeat [cases b | exact rfl]
  , mul_comm := by intros; cases a; repeat [cases b | exact rfl]
  , add_assoc := by intros; cases a; repeat [ cases b | cases c | exact rfl ]
  , mul_assoc := by intros; cases a; repeat [ cases b | cases c | exact rfl ]
  , add_mul_absorptive := by intros; cases a; repeat [ cases b | exact rfl ]
  , mul_add_absorptive := by intros; cases a; repeat [ cases b | exact rfl ] 
  ⦄

definition bool.distrib_lattice [instance] : distrib_lattice bool :=
   ⦃ distrib_lattice
   , add_mul_distrib := by intros; cases a; repeat [cases b | cases c | exact rfl]
   , mul_add_distrib := by intros; cases a; repeat [cases b | cases c | exact rfl]
   , bool.lattice
   ⦄

definition bool.monoid [instance] : monoid bool :=
  ⦃ monoid
  , one := tt
  , one_mul := by intro a; cases a; repeat [exact rfl]
  , mul_one := by intro a; cases a; repeat [exact rfl]
  , bool.lattice
  ⦄

definition bool.add_monoid [instance] : add_monoid bool :=
  ⦃ add_monoid
  , zero := ff
  , zero_add := by intro a; cases a; repeat [exact rfl]
  , add_zero := by intro a; cases a; repeat [exact rfl]
  , bool.lattice
  ⦄

definition bool.has_rp_comp [instance] : has_rp_comp bool :=
  ⦃ has_rp_comp, rp_comp := λa b, bnot a || b ⦄

section
  constant A : Type
  hypothesis [l : bounded_distrib_lattice A]

  check ∀{a b : A}, a ≤ b
end


check weak_order.le_antisymm

structure heyting_algebra [class] (A : Type) extends bounded_distrib_lattice A, has_rp_comp A :=
  (rp_comp_inf : let mleq a b := add a b = b in ∀a b x, mleq (mul a x) b ↔ mleq x (rp_comp a b))

section
  variables {A : Type} [s : heyting_algebra A]
  include s
  open bounded_distrib_lattice has_rp_comp

  theorem rp_comp.inf {a b x : A} : (a * x) ≤ b ↔ x ≤ (a ⊸ b) :=
    !heyting_algebra.rp_comp_inf
end

namespace heyting_algebra
  variable {A : Type}
  variable [s : heyting_algebra A]
  include s
  open bounded_lattice
  definition p_comp (a : A) : A := a ⊸ 0
end heyting_algebra

prefix `-` := heyting_algebra.p_comp

namespace heyting_algebra
  variable {A : Type}
  variable [s : heyting_algebra A]
  include s
  open bounded_lattice

  theorem rp_comp_le (a b : A) : a * (a ⊸ b) ≤ b :=
  begin
    apply (iff.mp' rp_comp.inf),
    exact !le.refl
  end

  theorem mul_pcomp (a : A) : a * (- a) = 0 :=
  begin
    fapply le_zero,
    apply rp_comp_le
  end

  theorem pcomp_mul (a : A) : -a * a = 0 := 
  calc
    -a * a = a * -a : mul.comm
       ... = 0      : mul_pcomp

  theorem mul_pcomp_add (a b : A) : a * (-a + b) = a * b :=
  calc
    a * (-a + b) = a * -a + a * b  : mul.distrib_over_add_left
             ... = 0 + a * b       : mul_pcomp
             ... = a * b           : zero_add

  theorem mul_of_add_pcomp (a b : A) : a * (b + -a) = a * b :=
    by rewrite [add.comm, mul_pcomp_add]


  theorem rpcomp_le_rpcomp_right {a b : A} (H : a ≤ b) (c : A) : b ⊸ c ≤ a ⊸ c :=
  begin
    fapply (iff.mp !rp_comp_inf),
    rewrite ▸(_ ≤ _),
    exact calc
      a * (b ⊸ c) ≤ b * (b ⊸ c)  : mul_le_mul_right H (b ⊸ c)
              ... ≤ c             : rp_comp_le
  end

  theorem rpcomp_le_rpcomp_left {a b : A} (H : a ≤ b) (c : A) : c ⊸ a ≤ c ⊸ b :=
  begin
    fapply (iff.mp !rp_comp_inf),
    rewrite ▸(_ ≤ _),
    exact calc
      c * (c ⊸ a) ≤ a  : rp_comp_le
              ... ≤ b   : H
  end

  theorem rpcomp_le_rpcomp {a b c d : A} (Hab : a ≤ b) (Hcd : c ≤ d) : b ⊸ c ≤ a ⊸ d :=
  calc
    b ⊸ c ≤ b ⊸ d  : rpcomp_le_rpcomp_left Hcd b
     ...  ≤ a ⊸ d  :  rpcomp_le_rpcomp_right Hab d

  theorem pcomp_reverse {a b : A} (H : a ≤ b) : -b ≤ -a := rpcomp_le_rpcomp_right H 0

  theorem rpcomp_unique {a b x : A} : (∀y, a * y ≤ b ↔ y ≤ x) → x = a ⊸ b := sorry


end heyting_algebra

structure boolean_algebra [class] (A : Type) extends heyting_algebra A :=
  (add_comp : ∀a, add a (rp_comp a zero) = one)

section
  variables {A : Type} [s : boolean_algebra A]
  include s
  open boolean_algebra

  definition add_comp_one (a : A) : a + -a = 1 := !add_comp
  definition comp_add_one (a : A) : -a + a = 1
    := by rewrite [add.comm, add_comp_one]
end


namespace boolean_algebra
  variable {A : Type}
  variable [s : boolean_algebra A]
  include s
  open heyting_algebra bounded_lattice lattice

  definition symm_diff (a b : A) : A := (a ⊸ b) + (b ⊸ a)
  infixl `▵`:65 := symm_diff

  theorem le_comp_add (a b : A) : -a + b = 1 ↔ a ≤ b :=
  begin
    apply iff.intro,
    { intro H,
      apply (iff.mp' !suple_iff_infle),
      exact calc
        a * b =         0 + a * b  : zero_add
          ... = (a * - a) + a * b  : mul_pcomp
          ... = a * (-a + b)       : mul_add_distrib
          ... = a * 1              : H
          ... = a                  : mul_one
      },
    { intro H,
      apply (le.antisymm (one_max (-a + b))),
      exact calc
          1 = -a + a  : comp_add_one
        ... ≤ -a + b  : add_le_add_left H (-a)
    }
  end

  lemma yuishi_lemma_10 {a b c d : A} (H : a * c ≤ d + b) : c ≤ d + (-a + b) := 
  begin
    apply (iff.mp' !suple_iff_infle),
    rewrite (add.comm (-a) b),
    rewrite -add.assoc,
    rewrite mul.distrib_over_add_left,
    rewrite -(algebra.mul_one c) at {1},
    rewrite -(add_comp_one a),
    rewrite (mul.comm c _),
    rewrite mul.assoc,
    rewrite mul.distrib_over_add_right,
    rewrite -mul.assoc,
    have Hacdb : (a * c) * (d + b) = a * c,
      from iff.mp !suple_iff_infle H,
    rewrite Hacdb,
    rewrite add.assoc,
    rewrite -mul.assoc,
    rewrite (mul.comm c (-a)),
    rewrite add.absorves_mul_right,
    rewrite -mul.distrib_over_add_right,
    rewrite add_comp_one,
    rewrite algebra.one_mul
  end

  theorem rcomp_or (a b : A) : a ⊸ b = -a + b :=
  begin
    apply le.antisymm,
    { have Hp : a ⊸ b ≤ b + (-a + b),
      from by
         apply (@yuishi_lemma_10 _ _ a b (a ⊸ b) b);
         rewrite add.idempotent;
         apply rp_comp_le,
      rewrite -(@add.idempotent _ _ b) at {2},
      rewrite -add.assoc,
      rewrite add.comm,
      exact Hp
      },
    { apply (iff.mp rp_comp.inf),
      exact calc
        a * (-a + b) = a * -a + a * b : mul_add_distrib
                 ... = 0      + a * b : mul_pcomp
                 ... = a * b          : zero_add
                 ... ≤ b              : mul_le_right a b
      }
  end

  /-
  -- Boolean ring from boolean algebra;
  -- we already use + and * for boolean operations
  -- and they do not coincide with ring structure;
  -- hence we don't specify the following as
  -- coercion or instances.
  definition to_boolean_ring : comm_ring A :=
    ⦃ comm_ring
    , add := symm_diff
    , mul := mul
    , !to_comm_monoid
    , add_assoc := λa b c,
      calc
        (a ▵ b) ▵ c = ((a ⊸ b) + (b ⊸ a)) ▵ c : rfl
                ... = ((a ⊸ b) + (b ⊸ a)) ▵ c    : rfl
                ... = a ▵ (b ▵ c)              : sorry

    ⦄
    -/

end boolean_algebra