{-# OPTIONS --without-K --safe #-}
module Algebra.Consequences.Propositional
{a} {A : Set a} where
open import Data.Sum.Base using (inj₁; inj₂)
open import Relation.Binary using (Rel; Setoid; Symmetric; Total)
open import Relation.Binary.PropositionalEquality
open import Relation.Unary using (Pred)
open import Algebra.Core
open import Algebra.Definitions {A = A} _≡_
import Algebra.Consequences.Setoid (setoid A) as Base
open Base public
hiding
( assoc+distribʳ+idʳ+invʳ⇒zeˡ
; assoc+distribˡ+idʳ+invʳ⇒zeʳ
; assoc+id+invʳ⇒invˡ-unique
; assoc+id+invˡ⇒invʳ-unique
; comm+distrˡ⇒distrʳ
; comm+distrʳ⇒distrˡ
; comm⇒sym[distribˡ]
; subst+comm⇒sym
; wlog
; sel⇒idem
)
module _ {_•_ _⁻¹ ε} where
assoc+id+invʳ⇒invˡ-unique : Associative _•_ → Identity ε _•_ →
RightInverse ε _⁻¹ _•_ →
∀ x y → (x • y) ≡ ε → x ≡ (y ⁻¹)
assoc+id+invʳ⇒invˡ-unique = Base.assoc+id+invʳ⇒invˡ-unique (cong₂ _)
assoc+id+invˡ⇒invʳ-unique : Associative _•_ → Identity ε _•_ →
LeftInverse ε _⁻¹ _•_ →
∀ x y → (x • y) ≡ ε → y ≡ (x ⁻¹)
assoc+id+invˡ⇒invʳ-unique = Base.assoc+id+invˡ⇒invʳ-unique (cong₂ _)
module _ {_+_ _*_ -_ 0#} where
assoc+distribʳ+idʳ+invʳ⇒zeˡ : Associative _+_ → _*_ DistributesOverʳ _+_ →
RightIdentity 0# _+_ → RightInverse 0# -_ _+_ →
LeftZero 0# _*_
assoc+distribʳ+idʳ+invʳ⇒zeˡ =
Base.assoc+distribʳ+idʳ+invʳ⇒zeˡ (cong₂ _+_) (cong₂ _*_)
assoc+distribˡ+idʳ+invʳ⇒zeʳ : Associative _+_ → _*_ DistributesOverˡ _+_ →
RightIdentity 0# _+_ → RightInverse 0# -_ _+_ →
RightZero 0# _*_
assoc+distribˡ+idʳ+invʳ⇒zeʳ =
Base.assoc+distribˡ+idʳ+invʳ⇒zeʳ (cong₂ _+_) (cong₂ _*_)
module _ {_•_ _◦_ : Op₂ A} (•-comm : Commutative _•_) where
comm+distrˡ⇒distrʳ : _•_ DistributesOverˡ _◦_ → _•_ DistributesOverʳ _◦_
comm+distrˡ⇒distrʳ = Base.comm+distrˡ⇒distrʳ (cong₂ _) •-comm
comm+distrʳ⇒distrˡ : _•_ DistributesOverʳ _◦_ → _•_ DistributesOverˡ _◦_
comm+distrʳ⇒distrˡ = Base.comm+distrʳ⇒distrˡ (cong₂ _) •-comm
comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y • z)) ≡ ((x ◦ y) • (x ◦ z)))
comm⇒sym[distribˡ] = Base.comm⇒sym[distribˡ] (cong₂ _◦_) •-comm
module _ {_•_ : Op₂ A} where
sel⇒idem : Selective _•_ → Idempotent _•_
sel⇒idem = Base.sel⇒idem _≡_
module _ {p} {P : Pred A p} where
subst+comm⇒sym : ∀ {f} (f-comm : Commutative f) →
Symmetric (λ a b → P (f a b))
subst+comm⇒sym = Base.subst+comm⇒sym {P = P} subst
wlog : ∀ {f} (f-comm : Commutative f) →
∀ {r} {_R_ : Rel _ r} → Total _R_ →
(∀ a b → a R b → P (f a b)) →
∀ a b → P (f a b)
wlog = Base.wlog {P = P} subst