module Data.Bool.Properties where
open import Data.Bool as Bool
open import Data.Fin
open import Data.Function
open import Algebra
open import Algebra.Structures
import Algebra.RingSolver.Simple as Solver
import Algebra.RingSolver.AlmostCommutativeRing as ACR
open import Relation.Nullary using (_⇔_)
open import Relation.Binary.PropositionalEquality
import Algebra.FunctionProperties as P; open P _≡_
open import Data.Product
open import Data.Sum
open import Data.Empty
import Relation.Binary.EqReasoning as EqR; open EqR Bool.setoid
private
∨-assoc : Associative _∨_
∨-assoc true y z = refl
∨-assoc false y z = refl
∧-assoc : Associative _∧_
∧-assoc true y z = refl
∧-assoc false y z = refl
∨-comm : Commutative _∨_
∨-comm true true = refl
∨-comm true false = refl
∨-comm false true = refl
∨-comm false false = refl
∧-comm : Commutative _∧_
∧-comm true true = refl
∧-comm true false = refl
∧-comm false true = refl
∧-comm false false = refl
∨-identity : Identity false _∨_
∨-identity = (λ _ → refl) , (λ x → ∨-comm x false)
∧-identity : Identity true _∧_
∧-identity = (λ _ → refl) , (λ x → ∧-comm x true)
zero-∧ : Zero false _∧_
zero-∧ = (λ _ → refl) , (λ x → ∧-comm x false)
distrib-∧-∨ : _∧_ DistributesOver _∨_
distrib-∧-∨ = distˡ , distʳ
where
distˡ : _∧_ DistributesOverˡ _∨_
distˡ true y z = refl
distˡ false y z = refl
distʳ : _∧_ DistributesOverʳ _∨_
distʳ x y z =
begin
(y ∨ z) ∧ x
≈⟨ ∧-comm (y ∨ z) x ⟩
x ∧ (y ∨ z)
≈⟨ distˡ x y z ⟩
x ∧ y ∨ x ∧ z
≈⟨ cong₂ _∨_ (∧-comm x y) (∧-comm x z) ⟩
y ∧ x ∨ z ∧ x
∎
isCommutativeSemiring-∨-∧
: IsCommutativeSemiring _≡_ _∨_ _∧_ false true
isCommutativeSemiring-∨-∧ = record
{ isSemiring = record
{ isSemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = record
{ isMonoid = record
{ isSemigroup = record
{ isEquivalence = isEquivalence
; assoc = ∨-assoc
; ∙-pres-≈ = cong₂ _∨_
}
; identity = ∨-identity
}
; comm = ∨-comm
}
; *-isMonoid = record
{ isSemigroup = record
{ isEquivalence = isEquivalence
; assoc = ∧-assoc
; ∙-pres-≈ = cong₂ _∧_
}
; identity = ∧-identity
}
; distrib = distrib-∧-∨
}
; zero = zero-∧
}
; *-comm = ∧-comm
}
commutativeSemiring-∨-∧ : CommutativeSemiring
commutativeSemiring-∨-∧ = record
{ _+_ = _∨_
; _*_ = _∧_
; 0# = false
; 1# = true
; isCommutativeSemiring = isCommutativeSemiring-∨-∧
}
module RingSolver =
Solver (ACR.fromCommutativeSemiring commutativeSemiring-∨-∧)
private
zero-∨ : Zero true _∨_
zero-∨ = (λ _ → refl) , (λ x → ∨-comm x true)
distrib-∨-∧ : _∨_ DistributesOver _∧_
distrib-∨-∧ = distˡ , distʳ
where
distˡ : _∨_ DistributesOverˡ _∧_
distˡ true y z = refl
distˡ false y z = refl
distʳ : _∨_ DistributesOverʳ _∧_
distʳ x y z =
begin
(y ∧ z) ∨ x
≈⟨ ∨-comm (y ∧ z) x ⟩
x ∨ (y ∧ z)
≈⟨ distˡ x y z ⟩
(x ∨ y) ∧ (x ∨ z)
≈⟨ cong₂ _∧_ (∨-comm x y) (∨-comm x z) ⟩
(y ∨ x) ∧ (z ∨ x)
∎
isCommutativeSemiring-∧-∨
: IsCommutativeSemiring _≡_ _∧_ _∨_ true false
isCommutativeSemiring-∧-∨ = record
{ isSemiring = record
{ isSemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = record
{ isMonoid = record
{ isSemigroup = record
{ isEquivalence = isEquivalence
; assoc = ∧-assoc
; ∙-pres-≈ = cong₂ _∧_
}
; identity = ∧-identity
}
; comm = ∧-comm
}
; *-isMonoid = record
{ isSemigroup = record
{ isEquivalence = isEquivalence
; assoc = ∨-assoc
; ∙-pres-≈ = cong₂ _∨_
}
; identity = ∨-identity
}
; distrib = distrib-∨-∧
}
; zero = zero-∨
}
; *-comm = ∨-comm
}
commutativeSemiring-∧-∨ : CommutativeSemiring
commutativeSemiring-∧-∨ = record
{ _+_ = _∧_
; _*_ = _∨_
; 0# = true
; 1# = false
; isCommutativeSemiring = isCommutativeSemiring-∧-∨
}
private
absorptive : Absorptive _∨_ _∧_
absorptive = abs-∨-∧ , abs-∧-∨
where
abs-∨-∧ : _∨_ Absorbs _∧_
abs-∨-∧ true y = refl
abs-∨-∧ false y = refl
abs-∧-∨ : _∧_ Absorbs _∨_
abs-∧-∨ true y = refl
abs-∧-∨ false y = refl
not-∧-inverse : Inverse false not _∧_
not-∧-inverse =
¬x∧x≡⊥ , (λ x → ∧-comm x (not x) ⟨ trans ⟩ ¬x∧x≡⊥ x)
where
¬x∧x≡⊥ : LeftInverse false not _∧_
¬x∧x≡⊥ false = refl
¬x∧x≡⊥ true = refl
not-∨-inverse : Inverse true not _∨_
not-∨-inverse =
¬x∨x≡⊤ , (λ x → ∨-comm x (not x) ⟨ trans ⟩ ¬x∨x≡⊤ x)
where
¬x∨x≡⊤ : LeftInverse true not _∨_
¬x∨x≡⊤ false = refl
¬x∨x≡⊤ true = refl
isBooleanAlgebra : IsBooleanAlgebra _≡_ _∨_ _∧_ not true false
isBooleanAlgebra = record
{ isDistributiveLattice = record
{ isLattice = record
{ isEquivalence = isEquivalence
; ∨-comm = ∨-comm
; ∨-assoc = ∨-assoc
; ∨-pres-≈ = cong₂ _∨_
; ∧-comm = ∧-comm
; ∧-assoc = ∧-assoc
; ∧-pres-≈ = cong₂ _∧_
; absorptive = absorptive
}
; ∨-∧-distribʳ = proj₂ distrib-∨-∧
}
; ∨-complementʳ = proj₂ not-∨-inverse
; ∧-complementʳ = proj₂ not-∧-inverse
; ¬-pres-≈ = cong not
}
booleanAlgebra : BooleanAlgebra
booleanAlgebra = record
{ _∨_ = _∨_
; _∧_ = _∧_
; ¬_ = not
; ⊤ = true
; ⊥ = false
; isBooleanAlgebra = isBooleanAlgebra
}
private
xor-is-ok : ∀ x y → x xor y ≡ (x ∨ y) ∧ not (x ∧ y)
xor-is-ok true y = refl
xor-is-ok false y = sym $ proj₂ ∧-identity _
commutativeRing-xor-∧ : CommutativeRing
commutativeRing-xor-∧ = commutativeRing
where
import Algebra.Props.BooleanAlgebra as BA
open BA booleanAlgebra
open XorRing _xor_ xor-is-ok
module XorRingSolver =
Solver (ACR.fromCommutativeRing commutativeRing-xor-∧)
not-involutive : Involutive not
not-involutive true = refl
not-involutive false = refl
not-¬ : ∀ {x y} → x ≡ y → x ≢ not y
not-¬ {true} refl ()
not-¬ {false} refl ()
¬-not : ∀ {x y} → x ≢ y → x ≡ not y
¬-not {true} {true} x≢y = ⊥-elim (x≢y refl)
¬-not {true} {false} _ = refl
¬-not {false} {true} _ = refl
¬-not {false} {false} x≢y = ⊥-elim (x≢y refl)
⇔→≡ : {b₁ b₂ b : Bool} → b₁ ≡ b ⇔ b₂ ≡ b → b₁ ≡ b₂
⇔→≡ {true } {true } hyp = refl
⇔→≡ {true } {false} {true } hyp = sym (proj₁ hyp refl)
⇔→≡ {true } {false} {false} hyp = proj₂ hyp refl
⇔→≡ {false} {true } {true } hyp = proj₂ hyp refl
⇔→≡ {false} {true } {false} hyp = sym (proj₁ hyp refl)
⇔→≡ {false} {false} hyp = refl
T-≡ : ∀ {b} → T b ⇔ b ≡ true
T-≡ {false} = ((λ ()) , λ ())
T-≡ {true} = (const refl , const _)
T-∧ : ∀ {b₁ b₂} → T (b₁ ∧ b₂) ⇔ (T b₁ × T b₂)
T-∧ {true} {true} = (const (_ , _) , const _)
T-∧ {true} {false} = ((λ ()) , proj₂)
T-∧ {false} {_} = ((λ ()) , proj₁)
T-∨ : ∀ {b₁ b₂} → T (b₁ ∨ b₂) ⇔ (T b₁ ⊎ T b₂)
T-∨ {true} {b₂} = (inj₁ , const _)
T-∨ {false} {true} = (inj₂ , const _)
T-∨ {false} {false} = (inj₁ , [ id , id ])
proof-irrelevance : ∀ {b} (p q : T b) → p ≡ q
proof-irrelevance {true} _ _ = refl
proof-irrelevance {false} () ()