[Updated the Algebra hierarchy. Nils Anders Danielsson **20071207231200 + Now the Algebra record hierarchy is based on the same principles as those of Relation.Binary and Category. ] hunk ./Algebra.agda 2 --- Some algebraic structures +-- Algebraic structures hunk ./Algebra.agda 5 -open import Relation.Binary +-- Algebraic structures packed up with setoids and operations. hunk ./Algebra.agda 7 -module Algebra (s : Setoid) where +module Algebra where hunk ./Algebra.agda 9 -open import Data.Product -open Setoid s +open import Relation.Binary +import Algebra.FunctionProperties as P +open import Algebra.Structures +open import Data.Function hunk ./Algebra.agda 15 --- Unary and binary operations +-- Semigroups, (commutative) monoids and (abelian) groups hunk ./Algebra.agda 17 -Op₁ : Set -Op₁ = carrier -> carrier +record Semigroup : Set1 where + infixl 7 _•_ + field + setoid : Setoid + _•_ : P.Op₂ setoid + isSemigroup : IsSemigroup setoid _•_ hunk ./Algebra.agda 24 -Op₂ : Set -Op₂ = carrier -> carrier -> carrier + open Setoid setoid public + open IsSemigroup setoid isSemigroup public hunk ./Algebra.agda 27 ------------------------------------------------------------------------- --- Properties of operations +record Monoid : Set1 where + infixl 7 _•_ + field + setoid : Setoid + _•_ : P.Op₂ setoid + ε : Setoid.carrier setoid + isMonoid : IsMonoid setoid _•_ ε hunk ./Algebra.agda 35 -Associative : Op₂ -> Set -Associative _•_ = forall x y z -> (x • (y • z)) ≈ ((x • y) • z) + open Setoid setoid public + open IsMonoid setoid isMonoid public hunk ./Algebra.agda 38 -Commutative : Op₂ -> Set -Commutative _•_ = forall x y -> (x • y) ≈ (y • x) + semigroup : Semigroup + semigroup = record + { setoid = setoid + ; _•_ = _•_ + ; isSemigroup = isSemigroup + } hunk ./Algebra.agda 45 -LeftIdentity : carrier -> Op₂ -> Set -LeftIdentity e _•_ = forall x -> (e • x) ≈ x +record CommutativeMonoid : Set1 where + infixl 7 _•_ + field + setoid : Setoid + _•_ : P.Op₂ setoid + ε : Setoid.carrier setoid + isCommutativeMonoid : IsCommutativeMonoid setoid _•_ ε hunk ./Algebra.agda 53 -RightIdentity : carrier -> Op₂ -> Set -RightIdentity e _•_ = forall x -> (x • e) ≈ x + open Setoid setoid public + open IsCommutativeMonoid setoid isCommutativeMonoid public hunk ./Algebra.agda 56 -Identity : carrier -> Op₂ -> Set -Identity e • = LeftIdentity e • × RightIdentity e • + monoid : Monoid + monoid = record + { setoid = setoid + ; _•_ = _•_ + ; ε = ε + ; isMonoid = isMonoid + } hunk ./Algebra.agda 64 -LeftZero : carrier -> Op₂ -> Set -LeftZero z _•_ = forall x -> (z • x) ≈ z + open Setoid setoid public + open Monoid monoid public using (semigroup) hunk ./Algebra.agda 67 -RightZero : carrier -> Op₂ -> Set -RightZero z _•_ = forall x -> (x • z) ≈ z +record Group : Set1 where + infix 8 _⁻¹ + infixl 7 _•_ + field + setoid : Setoid + _•_ : P.Op₂ setoid + ε : Setoid.carrier setoid + _⁻¹ : P.Op₁ setoid + isGroup : IsGroup setoid _•_ ε _⁻¹ hunk ./Algebra.agda 77 -Zero : carrier -> Op₂ -> Set -Zero z • = LeftZero z • × RightZero z • + open Setoid setoid public + open IsGroup setoid isGroup public hunk ./Algebra.agda 80 -LeftInverse : carrier -> Op₁ -> Op₂ -> Set -LeftInverse e _⁻¹ _•_ = forall x -> (x ⁻¹ • x) ≈ e + monoid : Monoid + monoid = record + { setoid = setoid + ; _•_ = _•_ + ; ε = ε + ; isMonoid = isMonoid + } hunk ./Algebra.agda 88 -RightInverse : carrier -> Op₁ -> Op₂ -> Set -RightInverse e _⁻¹ _•_ = forall x -> (x • (x ⁻¹)) ≈ e + open Monoid monoid public using (semigroup) hunk ./Algebra.agda 90 -Inverse : carrier -> Op₁ -> Op₂ -> Set -Inverse e ⁻¹ • = LeftInverse e ⁻¹ • × RightInverse e ⁻¹ • +record AbelianGroup : Set1 where + infix 8 _⁻¹ + infixl 7 _•_ + field + setoid : Setoid + _•_ : P.Op₂ setoid + ε : Setoid.carrier setoid + _⁻¹ : P.Op₁ setoid + isAbelianGroup : IsAbelianGroup setoid _•_ ε _⁻¹ hunk ./Algebra.agda 100 -_DistributesOverˡ_ : Op₂ -> Op₂ -> Set -_*_ DistributesOverˡ _+_ = - forall x y z -> (x * (y + z)) ≈ ((x * y) + (x * z)) + open Setoid setoid public + open IsAbelianGroup setoid isAbelianGroup public hunk ./Algebra.agda 103 -_DistributesOverʳ_ : Op₂ -> Op₂ -> Set -_*_ DistributesOverʳ _+_ = - forall x y z -> ((y + z) * x) ≈ ((y * x) + (z * x)) + group : Group + group = record + { setoid = setoid + ; _•_ = _•_ + ; ε = ε + ; _⁻¹ = _⁻¹ + ; isGroup = isGroup + } hunk ./Algebra.agda 112 -_DistributesOver_ : Op₂ -> Op₂ -> Set -* DistributesOver + = (* DistributesOverˡ +) × (* DistributesOverʳ +) + open Group group public using (semigroup; monoid) hunk ./Algebra.agda 114 -_IdempotentOn_ : Op₂ -> carrier -> Set -_•_ IdempotentOn x = (x • x) ≈ x + commutativeMonoid : CommutativeMonoid + commutativeMonoid = record + { setoid = setoid + ; _•_ = _•_ + ; ε = ε + ; isCommutativeMonoid = isCommutativeMonoid + } hunk ./Algebra.agda 122 -Idempotent : Op₂ -> Set -Idempotent • = forall x -> • IdempotentOn x +------------------------------------------------------------------------ +-- (Commutative) semirings hunk ./Algebra.agda 125 -Idempotent₁ : Op₁ -> Set -Idempotent₁ f = forall x -> f (f x) ≈ f x +record Semiring : Set1 where + infixl 7 _*_ + infixl 6 _+_ + field + setoid : Setoid + _+_ : P.Op₂ setoid + _*_ : P.Op₂ setoid + 0# : Setoid.carrier setoid + 1# : Setoid.carrier setoid + isSemiring : IsSemiring setoid _+_ _*_ 0# 1# hunk ./Algebra.agda 136 -_Absorbs_ : Op₂ -> Op₂ -> Set -_•_ Absorbs _∘_ = forall x y -> (x • (x ∘ y)) ≈ x + open Setoid setoid public + open IsSemiring setoid isSemiring public hunk ./Algebra.agda 139 -Absorptive : Op₂ -> Op₂ -> Set -Absorptive • ∘ = (• Absorbs ∘) × (∘ Absorbs •) + +-commutativeMonoid : CommutativeMonoid + +-commutativeMonoid = record + { setoid = setoid + ; _•_ = _+_ + ; ε = 0# + ; isCommutativeMonoid = +-isCommutativeMonoid + } hunk ./Algebra.agda 147 -Involutive : Op₁ -> Set -Involutive f = forall x -> f (f x) ≈ x + open CommutativeMonoid +-commutativeMonoid public + using () renaming ( semigroup to +-semigroup + ; monoid to +-monoid + ) hunk ./Algebra.agda 152 ------------------------------------------------------------------------- --- Combinations of properties (one binary operation) + *-monoid : Monoid + *-monoid = record + { setoid = setoid + ; _•_ = _*_ + ; ε = 1# + ; isMonoid = *-isMonoid + } hunk ./Algebra.agda 160 --- First some abbreviations: + open Monoid *-monoid public + using () renaming (semigroup to *-semigroup) hunk ./Algebra.agda 163 -_Preserves-≈ : Op₁ -> Set -• Preserves-≈ = • Preserves _≈_ → _≈_ +record CommutativeSemiring : Set1 where + infixl 7 _*_ + infixl 6 _+_ + field + setoid : Setoid + _+_ : P.Op₂ setoid + _*_ : P.Op₂ setoid + 0# : Setoid.carrier setoid + 1# : Setoid.carrier setoid + isCommutativeSemiring : IsCommutativeSemiring setoid _+_ _*_ 0# 1# hunk ./Algebra.agda 174 -_Preserves₂-≈ : Op₂ -> Set -• Preserves₂-≈ = • Preserves₂ _≈_ → _≈_ → _≈_ + open Setoid setoid public + open IsCommutativeSemiring setoid isCommutativeSemiring public hunk ./Algebra.agda 177 -record Semigroup (• : Op₂) : Set where - field - assoc : Associative • - •-pres-≈ : • Preserves₂-≈ + semiring : Semiring + semiring = record + { setoid = setoid + ; _+_ = _+_ + ; _*_ = _*_ + ; 0# = 0# + ; 1# = 1# + ; isSemiring = isSemiring + } hunk ./Algebra.agda 187 -record Monoid (• : Op₂) (ε : carrier) : Set where - field - semigroup : Semigroup • - identity : Identity ε • + open Semiring semiring public + using ( +-semigroup; +-monoid; +-commutativeMonoid + ; *-semigroup; *-monoid + ) + + *-commutativeMonoid : CommutativeMonoid + *-commutativeMonoid = record + { setoid = setoid + ; _•_ = _*_ + ; ε = 1# + ; isCommutativeMonoid = *-isCommutativeMonoid + } + +------------------------------------------------------------------------ +-- (Commutative) rings hunk ./Algebra.agda 203 -record CommutativeMonoid (• : Op₂) (ε : carrier) : Set where +-- A raw ring is a ring without any laws (except for the underlying +-- equality). + +record RawRing : Set1 where + infix 8 -_ + infixl 7 _*_ + infixl 6 _+_ hunk ./Algebra.agda 211 - monoid : Monoid • ε - comm : Commutative • + setoid : Setoid + _+_ : P.Op₂ setoid + _*_ : P.Op₂ setoid + -_ : P.Op₁ setoid + 0# : Setoid.carrier setoid + 1# : Setoid.carrier setoid + + open Setoid setoid public hunk ./Algebra.agda 220 -record Group (• : Op₂) (ε : carrier) (⁻¹ : Op₁) : Set where +record Ring : Set1 where + infix 8 -_ + infixl 7 _*_ + infixl 6 _+_ hunk ./Algebra.agda 225 - monoid : Monoid • ε - inverse : Inverse ε ⁻¹ • - ⁻¹-pres-≈ : ⁻¹ Preserves-≈ + setoid : Setoid + _+_ : P.Op₂ setoid + _*_ : P.Op₂ setoid + -_ : P.Op₁ setoid + 0# : Setoid.carrier setoid + 1# : Setoid.carrier setoid + isRing : IsRing setoid _+_ _*_ -_ 0# 1# + + open Setoid setoid public + open IsRing setoid isRing public + + +-abelianGroup : AbelianGroup + +-abelianGroup = record + { setoid = setoid + ; _•_ = _+_ + ; ε = 0# + ; _⁻¹ = -_ + ; isAbelianGroup = +-isAbelianGroup + } hunk ./Algebra.agda 245 -record AbelianGroup (• : Op₂) (ε : carrier) (⁻¹ : Op₁) : Set where + semiring : Semiring + semiring = record + { setoid = setoid + ; _+_ = _+_ + ; _*_ = _*_ + ; 0# = 0# + ; 1# = 1# + ; isSemiring = isSemiring + } + + open Semiring semiring public + using ( +-semigroup; +-monoid; +-commutativeMonoid + ; *-semigroup; *-monoid + ) + + rawRing : RawRing + rawRing = record + { setoid = setoid + ; _+_ = _+_ + ; _*_ = _*_ + ; -_ = -_ + ; 0# = 0# + ; 1# = 1# + } + +record CommutativeRing : Set1 where + infix 8 -_ + infixl 7 _*_ + infixl 6 _+_ hunk ./Algebra.agda 275 - group : Group • ε ⁻¹ - comm : Commutative • + setoid : Setoid + _+_ : P.Op₂ setoid + _*_ : P.Op₂ setoid + -_ : P.Op₁ setoid + 0# : Setoid.carrier setoid + 1# : Setoid.carrier setoid + isCommutativeRing : IsCommutativeRing setoid _+_ _*_ -_ 0# 1# + + open Setoid setoid public + open IsCommutativeRing setoid isCommutativeRing public + + ring : Ring + ring = record + { setoid = setoid + ; _+_ = _+_ + ; _*_ = _*_ + ; -_ = -_ + ; 0# = 0# + ; 1# = 1# + ; isRing = isRing + } + + commutativeSemiring : CommutativeSemiring + commutativeSemiring = record + { setoid = setoid + ; _+_ = _+_ + ; _*_ = _*_ + ; 0# = 0# + ; 1# = 1# + ; isCommutativeSemiring = isCommutativeSemiring + } + + open Ring ring public using (rawRing; +-abelianGroup) + open CommutativeSemiring commutativeSemiring public + using ( +-semigroup; +-monoid; +-commutativeMonoid + ; *-semigroup; *-monoid; *-commutativeMonoid + ; semiring + ) hunk ./Algebra.agda 315 --- Combinations of properties (two binary operations) +-- (Distributive) lattices and boolean algebras hunk ./Algebra.agda 317 -record Semiring (+ * : Op₂) (0# 1# : carrier) : Set where +record Lattice : Set1 where + infixr 7 _∧_ + infixr 6 _∨_ hunk ./Algebra.agda 321 - +-monoid : CommutativeMonoid + 0# - *-monoid : Monoid * 1# - distrib : * DistributesOver + - zero : Zero 0# * + setoid : Setoid + _∨_ : P.Op₂ setoid + _∧_ : P.Op₂ setoid + isLattice : IsLattice setoid _∨_ _∧_ hunk ./Algebra.agda 326 -record CommutativeSemiring (+ * : Op₂) (0# 1# : carrier) : Set where - field - semiring : Semiring + * 0# 1# - *-comm : Commutative * + open Setoid setoid public + open IsLattice setoid isLattice public hunk ./Algebra.agda 329 -record Ring (+ * : Op₂) (- : Op₁) (0# 1# : carrier) : Set where +record DistributiveLattice : Set1 where + infixr 7 _∧_ + infixr 6 _∨_ hunk ./Algebra.agda 333 - +-group : AbelianGroup + 0# - - *-monoid : Monoid * 1# - distrib : * DistributesOver + + setoid : Setoid + _∨_ : P.Op₂ setoid + _∧_ : P.Op₂ setoid + isDistributiveLattice : IsDistributiveLattice setoid _∨_ _∧_ hunk ./Algebra.agda 338 -record CommutativeRing (+ * : Op₂) (- : Op₁) (0# 1# : carrier) : Set where - field - ring : Ring + * - 0# 1# - *-comm : Commutative * + open Setoid setoid public + open IsDistributiveLattice setoid isDistributiveLattice public hunk ./Algebra.agda 341 --- A structure which lies somewhere between commutative rings and --- commutative semirings + lattice : Lattice + lattice = record + { setoid = setoid + ; _∨_ = _∨_ + ; _∧_ = _∧_ + ; isLattice = isLattice + } hunk ./Algebra.agda 349 -record AlmostCommRing (_+_ _*_ : Op₂) - (¬_ : Op₁) - (0# 1# : carrier) : Set where +record BooleanAlgebra : Set1 where + infix 8 ¬_ + infixr 7 _∧_ + infixr 6 _∨_ hunk ./Algebra.agda 354 - commSemiring : CommutativeSemiring _+_ _*_ 0# 1# - ¬-pres-≈ : ¬_ Preserves-≈ - ¬-*-distribˡ : forall x y -> ((¬ x) * y) ≈ (¬ (x * y)) - ¬-+-comm : forall x y -> ((¬ x) + (¬ y)) ≈ (¬ (x + y)) + setoid : Setoid + _∨_ : P.Op₂ setoid + _∧_ : P.Op₂ setoid + ¬_ : P.Op₁ setoid + ⊤ : Setoid.carrier setoid + ⊥ : Setoid.carrier setoid + isBooleanAlgebra : IsBooleanAlgebra setoid _∨_ _∧_ ¬_ ⊤ ⊥ hunk ./Algebra.agda 362 -record Lattice (∨ ∧ : Op₂) : Set where - field - ∨-comm : Commutative ∨ - ∨-assoc : Associative ∨ - ∨-pres-≈ : ∨ Preserves₂-≈ - ∧-comm : Commutative ∧ - ∧-assoc : Associative ∧ - ∧-pres-≈ : ∧ Preserves₂-≈ - absorptive : Absorptive ∨ ∧ + open Setoid setoid public + open IsBooleanAlgebra setoid isBooleanAlgebra public hunk ./Algebra.agda 365 -record DistributiveLattice (∨ ∧ : Op₂) : Set where - field - lattice : Lattice ∨ ∧ - ∨-∧-distribˡ : ∨ DistributesOverˡ ∧ + distributiveLattice : DistributiveLattice + distributiveLattice = record + { setoid = setoid + ; _∨_ = _∨_ + ; _∧_ = _∧_ + ; isDistributiveLattice = isDistributiveLattice + } hunk ./Algebra.agda 373 -record BooleanAlgebra (∨ ∧ : Op₂) (¬ : Op₁) (⊤ ⊥ : carrier) : Set where - field - distLattice : DistributiveLattice ∨ ∧ - ∨-complementʳ : RightInverse ⊤ ¬ ∨ - ∧-complementʳ : RightInverse ⊥ ¬ ∧ - ¬-pres-≈ : ¬ Preserves-≈ + open DistributiveLattice distributiveLattice public + using (lattice) addfile ./Algebra/FunctionProperties.agda hunk ./Algebra/FunctionProperties.agda 1 +------------------------------------------------------------------------ +-- Properties of functions, such as associativity and commutativity +------------------------------------------------------------------------ + +-- These properties can (for instance) be used to define algebraic +-- structures. + +open import Relation.Binary + +-- The properties are specified using the equality in the given +-- setoid. + +module Algebra.FunctionProperties (s : Setoid) where + +open import Data.Product +open Setoid s + +------------------------------------------------------------------------ +-- Unary and binary operations + +Op₁ : Set +Op₁ = carrier -> carrier + +Op₂ : Set +Op₂ = carrier -> carrier -> carrier + +------------------------------------------------------------------------ +-- Properties of operations + +Associative : Op₂ -> Set +Associative _•_ = forall x y z -> (x • (y • z)) ≈ ((x • y) • z) + +Commutative : Op₂ -> Set +Commutative _•_ = forall x y -> (x • y) ≈ (y • x) + +LeftIdentity : carrier -> Op₂ -> Set +LeftIdentity e _•_ = forall x -> (e • x) ≈ x + +RightIdentity : carrier -> Op₂ -> Set +RightIdentity e _•_ = forall x -> (x • e) ≈ x + +Identity : carrier -> Op₂ -> Set +Identity e • = LeftIdentity e • × RightIdentity e • + +LeftZero : carrier -> Op₂ -> Set +LeftZero z _•_ = forall x -> (z • x) ≈ z + +RightZero : carrier -> Op₂ -> Set +RightZero z _•_ = forall x -> (x • z) ≈ z + +Zero : carrier -> Op₂ -> Set +Zero z • = LeftZero z • × RightZero z • + +LeftInverse : carrier -> Op₁ -> Op₂ -> Set +LeftInverse e _⁻¹ _•_ = forall x -> (x ⁻¹ • x) ≈ e + +RightInverse : carrier -> Op₁ -> Op₂ -> Set +RightInverse e _⁻¹ _•_ = forall x -> (x • (x ⁻¹)) ≈ e + +Inverse : carrier -> Op₁ -> Op₂ -> Set +Inverse e ⁻¹ • = LeftInverse e ⁻¹ • × RightInverse e ⁻¹ • + +_DistributesOverˡ_ : Op₂ -> Op₂ -> Set +_*_ DistributesOverˡ _+_ = + forall x y z -> (x * (y + z)) ≈ ((x * y) + (x * z)) + +_DistributesOverʳ_ : Op₂ -> Op₂ -> Set +_*_ DistributesOverʳ _+_ = + forall x y z -> ((y + z) * x) ≈ ((y * x) + (z * x)) + +_DistributesOver_ : Op₂ -> Op₂ -> Set +* DistributesOver + = (* DistributesOverˡ +) × (* DistributesOverʳ +) + +_IdempotentOn_ : Op₂ -> carrier -> Set +_•_ IdempotentOn x = (x • x) ≈ x + +Idempotent : Op₂ -> Set +Idempotent • = forall x -> • IdempotentOn x + +IdempotentFun : Op₁ -> Set +IdempotentFun f = forall x -> f (f x) ≈ f x + +_Absorbs_ : Op₂ -> Op₂ -> Set +_•_ Absorbs _∘_ = forall x y -> (x • (x ∘ y)) ≈ x + +Absorptive : Op₂ -> Op₂ -> Set +Absorptive • ∘ = (• Absorbs ∘) × (∘ Absorbs •) + +Involutive : Op₁ -> Set +Involutive f = forall x -> f (f x) ≈ x hunk ./Algebra/Morphism.agda 2 --- Definitions of morphisms +-- Morphisms between algebraic structures hunk ./Algebra/Morphism.agda 5 -open import Relation.Binary - -module Algebra.Morphism (from to : Setoid) where +module Algebra.Morphism where hunk ./Algebra/Morphism.agda 7 -import Algebra as Alg -private - module F = Setoid from - module F = Alg from - module T = Setoid to - module T = Alg to -open Setoid to using (_≈_) +open import Relation.Binary +open import Algebra +open import Algebra.FunctionProperties +open import Data.Function hunk ./Algebra/Morphism.agda 15 -Morphism : Set -Morphism = F.carrier -> T.carrier +module Definitions (from : Set) (to : Setoid) where + open Setoid to renaming (carrier to to-carrier) hunk ./Algebra/Morphism.agda 18 -Homomorphic₀ : Morphism -> F.carrier -> T.carrier -> Set -Homomorphic₀ ⟦_⟧ • •' = ⟦ • ⟧ ≈ •' + Morphism : Set + Morphism = from -> to-carrier hunk ./Algebra/Morphism.agda 21 -Homomorphic₁ : Morphism -> F.Op₁ -> T.Op₁ -> Set -Homomorphic₁ ⟦_⟧ •_ •'_ = forall x -> ⟦ • x ⟧ ≈ •' ⟦ x ⟧ + Homomorphic₀ : Morphism -> from -> to-carrier -> Set + Homomorphic₀ ⟦_⟧ • ∘ = ⟦ • ⟧ ≈ ∘ hunk ./Algebra/Morphism.agda 24 -Homomorphic₂ : Morphism -> F.Op₂ -> T.Op₂ -> Set -Homomorphic₂ ⟦_⟧ _•_ _•'_ = - forall x y -> ⟦ x • y ⟧ ≈ (⟦ x ⟧ •' ⟦ y ⟧) + Homomorphic₁ : Morphism -> Fun₁ from -> Op₁ to -> Set + Homomorphic₁ ⟦_⟧ •_ ∘_ = forall x -> ⟦ • x ⟧ ≈ ∘ ⟦ x ⟧ + + Homomorphic₂ : Morphism -> Fun₂ from -> Op₂ to -> Set + Homomorphic₂ ⟦_⟧ _•_ _∘_ = + forall x y -> ⟦ x • y ⟧ ≈ (⟦ x ⟧ ∘ ⟦ y ⟧) hunk ./Algebra/Morphism.agda 34 -record RingHomomorphism - (F+ F* : F.Op₂) (F- : F.Op₁) (F0# F1# : F.carrier) - (T+ T* : T.Op₂) (T- : T.Op₁) (T0# T1# : T.carrier) - : Set where +-- Other morphisms could of course be defined. + +record _-RawRing⟶_ (from to : RawRing) : Set where + open RawRing + open Definitions (carrier from) (setoid to) hunk ./Algebra/Morphism.agda 41 - +-homo : Homomorphic₂ ⟦_⟧ F+ T+ - *-homo : Homomorphic₂ ⟦_⟧ F* T* - ¬-homo : Homomorphic₁ ⟦_⟧ F- T- - 0-homo : Homomorphic₀ ⟦_⟧ F0# T0# - 1-homo : Homomorphic₀ ⟦_⟧ F1# T1# + +-homo : Homomorphic₂ ⟦_⟧ (_+_ from) (_+_ to) + *-homo : Homomorphic₂ ⟦_⟧ (_*_ from) (_*_ to) + --homo : Homomorphic₁ ⟦_⟧ (-_ from) (-_ to) + 0-homo : Homomorphic₀ ⟦_⟧ (0# from) (0# to) + 1-homo : Homomorphic₀ ⟦_⟧ (1# from) (1# to) + +_-Ring⟶_ : Ring -> Ring -> Set +from -Ring⟶ to = rawRing from -RawRing⟶ rawRing to + where open Ring hunk ./Algebra/Operations.agda 2 --- Some defined operations +-- Some defined operations (multiplication by natural number and +-- exponentiation) hunk ./Algebra/Operations.agda 6 -open import Algebra.Packaged +open import Algebra hunk ./Algebra/Operations.agda 8 -module Algebra.Operations (s : Semiringoid) where +module Algebra.Operations (s : Semiring) where hunk ./Algebra/Operations.agda 10 +open Semiring s hiding (zero) +open import Data.Nat using (zero; suc; ℕ) +open import Data.Function +open import Logic hunk ./Algebra/Operations.agda 16 -open import Logic -open import Data.Function -open import Data.Nat using (zero; suc; ℕ) -import Algebra -import Relation.Binary.EqReasoning -open Semiringoid s -open Algebra setoid -open Setoid setoid -private - module R = Semiring semiring - module A = CommutativeMonoid R.+-monoid - module A = Monoid A.monoid - module A = Semigroup A.semigroup - module M = Monoid R.*-monoid - module M = Semigroup M.semigroup -open Relation.Binary.EqReasoning preorder +import Relation.Binary.EqReasoning as EqR +open EqR setoid hunk ./Algebra/Operations.agda 24 +infixr 7 _×_ + hunk ./Algebra/Operations.agda 28 -suc n × x = x + (n × x) +suc n × x = x + n × x hunk ./Algebra/Operations.agda 32 +infixr 8 _^_ + hunk ./Algebra/Operations.agda 36 -x ^ suc n = x * (x ^ n) +x ^ suc n = x * x ^ n hunk ./Algebra/Operations.agda 44 - ×-pres-≈ {n} {n'} {x} {x'} n≡n' x≈x' = - begin - n × x - ∼⟨ refl $ ≡-cong (\n -> n × x) n≡n' ⟩ - n' × x - ∼⟨ ×-pres-≈ʳ n' x≈x' ⟩ - n' × x' - ∎ + ×-pres-≈ {n} {n'} {x} {x'} n≡n' x≈x' = begin + n × x ≈⟨ reflexive $ ≡-cong (\n -> n × x) n≡n' ⟩ + n' × x ≈⟨ ×-pres-≈ʳ n' x≈x' ⟩ + n' × x' ∎ hunk ./Algebra/Operations.agda 49 - ×-pres-≈ʳ : forall n -> (_×_ n) Preserves-≈ + ×-pres-≈ʳ : forall n -> (_×_ n) Preserves _≈_ → _≈_ hunk ./Algebra/Operations.agda 51 - ×-pres-≈ʳ (suc n) x≈x' = x≈x' ⟨ A.•-pres-≈ ⟩ ×-pres-≈ʳ n x≈x' + ×-pres-≈ʳ (suc n) x≈x' = x≈x' ⟨ +-pres-≈ ⟩ ×-pres-≈ʳ n x≈x' hunk ./Algebra/Operations.agda 54 - ^-pres-≈ {x} {x'} {n} {n'} x≈x' n≡n' = - begin - x ^ n - ∼⟨ refl $ ≡-cong (_^_ x) n≡n' ⟩ - x ^ n' - ∼⟨ ^-pres-≈ˡ n' x≈x' ⟩ - x' ^ n' - ∎ + ^-pres-≈ {x} {x'} {n} {n'} x≈x' n≡n' = begin + x ^ n ≈⟨ reflexive $ ≡-cong (_^_ x) n≡n' ⟩ + x ^ n' ≈⟨ ^-pres-≈ˡ n' x≈x' ⟩ + x' ^ n' ∎ hunk ./Algebra/Operations.agda 59 - ^-pres-≈ˡ : forall n -> (\x -> x ^ n) Preserves-≈ + ^-pres-≈ˡ : forall n -> (\x -> x ^ n) Preserves _≈_ → _≈_ hunk ./Algebra/Operations.agda 61 - ^-pres-≈ˡ (suc n) x≈x' = x≈x' ⟨ M.•-pres-≈ ⟩ ^-pres-≈ˡ n x≈x' + ^-pres-≈ˡ (suc n) x≈x' = x≈x' ⟨ *-pres-≈ ⟩ ^-pres-≈ˡ n x≈x' hunk ./Algebra/Packaged.agda 1 ------------------------------------------------------------------------- --- Algebraic properties packaged up with operations ------------------------------------------------------------------------- - -module Algebra.Packaged where - -open import Relation.Binary -open import Algebra -import Algebra.Morphism as M -open Setoid - --- I know that groupoid really means something else... - -record Groupoid : Set1 where - field - setoid : Setoid - _+_ : Op₂ setoid - -_ : Op₁ setoid - 0# : carrier setoid - group : Group setoid _+_ 0# -_ - -record AbelianGroupoid : Set1 where - field - setoid : Setoid - _+_ : Op₂ setoid - -_ : Op₁ setoid - 0# : carrier setoid - abelianGroup : AbelianGroup setoid _+_ 0# -_ - -record Semiringoid : Set1 where - field - setoid : Setoid - _+_ : Op₂ setoid - _*_ : Op₂ setoid - 0# : carrier setoid - 1# : carrier setoid - semiring : Semiring setoid _+_ _*_ 0# 1# - -record CommutativeSemiringoid : Set1 where - field - setoid : Setoid - _+_ : Op₂ setoid - _*_ : Op₂ setoid - 0# : carrier setoid - 1# : carrier setoid - commSemiring : CommutativeSemiring setoid _+_ _*_ 0# 1# - -record BareRingoid : Set1 where - field - setoid : Setoid - _+_ : Op₂ setoid - _*_ : Op₂ setoid - -_ : Op₁ setoid - 0# : carrier setoid - 1# : carrier setoid - -private - module Bare where - open BareRingoid - - record Ringoid : Set1 where - field - bare : BareRingoid - ring : Ring (setoid bare) - (_+_ bare) (_*_ bare) (-_ bare) - (0# bare) (1# bare) - - record CommutativeRingoid : Set1 where - field - bare : BareRingoid - commRing : CommutativeRing (setoid bare) - (_+_ bare) (_*_ bare) (-_ bare) - (0# bare) (1# bare) - - record AlmostCommRingoid : Set1 where - field - bare : BareRingoid - almostCommRing : AlmostCommRing (setoid bare) - (_+_ bare) (_*_ bare) (-_ bare) - (0# bare) (1# bare) - -open Bare public - -record Latticoid : Set1 where - field - setoid : Setoid - _∨_ : Op₂ setoid - _∧_ : Op₂ setoid - lattice : Lattice setoid _∨_ _∧_ - -record DistributiveLatticoid : Set1 where - field - setoid : Setoid - _∨_ : Op₂ setoid - _∧_ : Op₂ setoid - distLattice : DistributiveLattice setoid _∨_ _∧_ - -record BooleanAlgebraoid : Set1 where - field - setoid : Setoid - _∨_ : Op₂ setoid - _∧_ : Op₂ setoid - ¬_ : Op₁ setoid - ⊤ : carrier setoid - ⊥ : carrier setoid - booleanAlgebra : BooleanAlgebra setoid _∨_ _∧_ ¬_ ⊤ ⊥ - ------------------------------------------------------------------------- --- Some morphisms - -_-Bare-AlmostComm⟶_ : BareRingoid -> AlmostCommRingoid -> Set -b -Bare-AlmostComm⟶ a = - RingHomomorphism B._+_ B._*_ B.-_ B.0# B.1# - A._+_ A._*_ A.-_ A.0# A.1# - where - module B = BareRingoid b - module A = AlmostCommRingoid a - module A = BareRingoid A.bare - open M B.setoid A.setoid rmfile ./Algebra/Packaged.agda hunk ./Algebra/Props/AbelianGroup.agda 5 -open import Algebra.Packaged +open import Algebra hunk ./Algebra/Props/AbelianGroup.agda 7 -module Algebra.Props.AbelianGroup - (g : AbelianGroupoid) - where +module Algebra.Props.AbelianGroup (g : AbelianGroup) where hunk ./Algebra/Props/AbelianGroup.agda 9 -open import Relation.Binary +open AbelianGroup g +import Relation.Binary.EqReasoning as EqR; open EqR setoid hunk ./Algebra/Props/AbelianGroup.agda 13 -import Relation.Binary.EqReasoning -import Algebra -import Algebra.Props.Group -open AbelianGroupoid g -open Setoid setoid -open Relation.Binary.EqReasoning preorder -open Algebra setoid -open AbelianGroup abelianGroup -open Group group -open Monoid monoid -open Semigroup semigroup - ------------------------------------------------------------------------- --- An abelian group is a group - -groupoid : Groupoid -groupoid = record - { setoid = setoid - ; _+_ = _+_ - ; -_ = -_ - ; 0# = 0# - ; group = group - } - -open Algebra.Props.Group groupoid public - ------------------------------------------------------------------------- --- Some properties hunk ./Algebra/Props/AbelianGroup.agda 17 - lemma : forall x y -> ((x + y) + - x) ≈ y - lemma x y = - begin - (x + y) + - x - ∼⟨ comm _ _ ⟨ •-pres-≈ ⟩ byDef ⟩ - (y + x) + - x - ∼⟨ sym $ assoc _ _ _ ⟩ - y + (x + - x) - ∼⟨ byDef ⟨ •-pres-≈ ⟩ proj₂ inverse _ ⟩ - y + 0# - ∼⟨ proj₂ identity _ ⟩ - y - ∎ + lemma : forall x y -> x • y • x ⁻¹ ≈ y + lemma x y = begin + x • y • x ⁻¹ ≈⟨ comm _ _ ⟨ •-pres-≈ ⟩ byDef ⟩ + y • x • x ⁻¹ ≈⟨ sym $ assoc _ _ _ ⟩ + y • (x • x ⁻¹) ≈⟨ byDef ⟨ •-pres-≈ ⟩ proj₂ inverse _ ⟩ + y • ε ≈⟨ proj₂ identity _ ⟩ + y ∎ hunk ./Algebra/Props/AbelianGroup.agda 25 - ¬-+-comm : forall x y -> ((- x) + (- y)) ≈ (- (x + y)) - ¬-+-comm x y = - begin - (- x) + - y - ∼⟨ comm _ _ ⟩ - (- y) + - x - ∼⟨ sym $ lem ⟨ •-pres-≈ ⟩ byDef ⟩ - (x + ((y + (- (x + y))) + - y)) + - x - ∼⟨ lemma _ _ ⟩ - (y + (- (x + y))) + - y - ∼⟨ lemma _ _ ⟩ - (- (x + y)) - ∎ + --•-comm : forall x y -> x ⁻¹ • y ⁻¹ ≈ (x • y) ⁻¹ + --•-comm x y = begin + x ⁻¹ • y ⁻¹ ≈⟨ comm _ _ ⟩ + y ⁻¹ • x ⁻¹ ≈⟨ sym $ lem ⟨ •-pres-≈ ⟩ byDef ⟩ + x • (y • (x • y) ⁻¹ • y ⁻¹) • x ⁻¹ ≈⟨ lemma _ _ ⟩ + y • (x • y) ⁻¹ • y ⁻¹ ≈⟨ lemma _ _ ⟩ + (x • y) ⁻¹ ∎ hunk ./Algebra/Props/AbelianGroup.agda 33 - lem = - begin - x + ((y + (- (x + y))) + - y) - ∼⟨ assoc _ _ _ ⟩ - (x + (y + (- (x + y)))) + - y - ∼⟨ assoc _ _ _ ⟨ •-pres-≈ ⟩ byDef ⟩ - ((x + y) + (- (x + y))) + - y - ∼⟨ proj₂ inverse _ ⟨ •-pres-≈ ⟩ byDef ⟩ - 0# + (- y) - ∼⟨ proj₁ identity _ ⟩ - - y - ∎ + lem = begin + x • (y • (x • y) ⁻¹ • y ⁻¹) ≈⟨ assoc _ _ _ ⟩ + x • (y • (x • y) ⁻¹) • y ⁻¹ ≈⟨ assoc _ _ _ ⟨ •-pres-≈ ⟩ byDef ⟩ + x • y • (x • y) ⁻¹ • y ⁻¹ ≈⟨ proj₂ inverse _ ⟨ •-pres-≈ ⟩ byDef ⟩ + ε • y ⁻¹ ≈⟨ proj₁ identity _ ⟩ + y ⁻¹ ∎ hunk ./Algebra/Props/AlmostCommRing.agda 1 ------------------------------------------------------------------------- --- Some derivable properties ------------------------------------------------------------------------- - -open import Algebra.Packaged - -module Algebra.Props.AlmostCommRing - (r : AlmostCommRingoid) - where - -open import Data.Function -open import Relation.Binary -import Algebra -import Algebra.Props.CommutativeSemiring as CSProp -import Relation.Binary.EqReasoning as PP -open AlmostCommRingoid r -open BareRingoid bare -open Algebra setoid -open AlmostCommRing almostCommRing -open PP (Setoid.preorder setoid) - ------------------------------------------------------------------------- --- An "almost commutative ring" is a commutative semiring - -commSemiringoid : CommutativeSemiringoid -commSemiringoid = record - { setoid = setoid - ; _+_ = _+_ - ; _*_ = _*_ - ; 0# = 0# - ; 1# = 1# - ; commSemiring = commSemiring - } - -open CSProp commSemiringoid public hiding (bareRingoid) - ------------------------------------------------------------------------- --- An "almost commutative ring" is a bare ring - -bareRingoid : BareRingoid -bareRingoid = bare - --bare-almostComm⟶ : bareRingoid -Bare-AlmostComm⟶ r --bare-almostComm⟶ = record - { ⟦_⟧ = id - ; +-homo = \_ _ -> byDef - ; *-homo = \_ _ -> byDef - ; ¬-homo = \_ -> byDef - ; 0-homo = byDef - ; 1-homo = byDef - } rmfile ./Algebra/Props/AlmostCommRing.agda hunk ./Algebra/Props/BooleanAlgebra.agda 5 -open import Algebra.Packaged +open import Algebra hunk ./Algebra/Props/BooleanAlgebra.agda 7 -module Algebra.Props.BooleanAlgebra - (b : BooleanAlgebraoid) - where +module Algebra.Props.BooleanAlgebra (b : BooleanAlgebra) where hunk ./Algebra/Props/BooleanAlgebra.agda 9 +open BooleanAlgebra b +import Algebra.Props.DistributiveLattice as DL +open DL distributiveLattice public +import Algebra.Structures as S; open S setoid +import Algebra.FunctionProperties as P; open P setoid +import Relation.Binary.EqReasoning as EqR; open EqR setoid hunk ./Algebra/Props/BooleanAlgebra.agda 18 -import Relation.Binary.EqReasoning -import Algebra -import Algebra.Props.Lattice -import Algebra.Props.DistributiveLattice -open BooleanAlgebraoid b -open Algebra setoid -open BooleanAlgebra booleanAlgebra -open DistributiveLattice distLattice -open Lattice lattice -open Setoid setoid -open Relation.Binary.EqReasoning preorder - ------------------------------------------------------------------------- --- A boolean algebra is a distributive lattice - -distLatticoid : DistributiveLatticoid -distLatticoid = record - { setoid = setoid - ; _∨_ = _∨_ - ; _∧_ = _∧_ - ; distLattice = distLattice - } - -open Algebra.Props.DistributiveLattice distLatticoid public hunk ./Algebra/Props/BooleanAlgebra.agda 27 - ∨-complementˡ x = - begin - (¬ x) ∨ x - ∼⟨ ∨-comm _ _ ⟩ - x ∨ (¬ x) - ∼⟨ ∨-complementʳ _ ⟩ - ⊤ - ∎ + ∨-complementˡ x = begin + ¬ x ∨ x ≈⟨ ∨-comm _ _ ⟩ + x ∨ ¬ x ≈⟨ ∨-complementʳ _ ⟩ + ⊤ ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 36 - ∧-complementˡ x = - begin - (¬ x) ∧ x - ∼⟨ ∧-comm _ _ ⟩ - x ∧ (¬ x) - ∼⟨ ∧-complementʳ _ ⟩ - ⊥ - ∎ + ∧-complementˡ x = begin + ¬ x ∧ x ≈⟨ ∧-comm _ _ ⟩ + x ∧ ¬ x ≈⟨ ∧-complementʳ _ ⟩ + ⊥ ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 46 - ∧-∨-boolAlg : BooleanAlgebra _∧_ _∨_ ¬_ ⊥ ⊤ - ∧-∨-boolAlg = record - { distLattice = ∧-∨-distLattice - ; ∨-complementʳ = proj₂ ∧-complement - ; ∧-complementʳ = proj₂ ∨-complement - ; ¬-pres-≈ = ¬-pres-≈ + ∧-∨-isBooleanAlgebra : IsBooleanAlgebra _∧_ _∨_ ¬_ ⊥ ⊤ + ∧-∨-isBooleanAlgebra = record + { isDistributiveLattice = ∧-∨-isDistributiveLattice + ; ∨-complementʳ = proj₂ ∧-complement + ; ∧-complementʳ = proj₂ ∨-complement + ; ¬-pres-≈ = ¬-pres-≈ hunk ./Algebra/Props/BooleanAlgebra.agda 54 +∧-∨-booleanAlgebra : BooleanAlgebra +∧-∨-booleanAlgebra = record + { setoid = setoid + ; _∧_ = _∨_ + ; _∨_ = _∧_ + ; ¬_ = ¬_ + ; ⊤ = ⊥ + ; ⊥ = ⊤ + ; isBooleanAlgebra = ∧-∨-isBooleanAlgebra + } + + hunk ./Algebra/Props/BooleanAlgebra.agda 75 - x∧⊤=x : forall x -> (x ∧ ⊤) ≈ x - x∧⊤=x x = - begin - x ∧ ⊤ - ∼⟨ byDef ⟨ ∧-pres-≈ ⟩ sym (proj₂ ∨-complement _) ⟩ - x ∧ (x ∨ ¬ x) - ∼⟨ proj₂ absorptive _ _ ⟩ - x - ∎ + x∧⊤=x : forall x -> x ∧ ⊤ ≈ x + x∧⊤=x x = begin + x ∧ ⊤ ≈⟨ byDef ⟨ ∧-pres-≈ ⟩ sym (proj₂ ∨-complement _) ⟩ + x ∧ (x ∨ ¬ x) ≈⟨ proj₂ absorptive _ _ ⟩ + x ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 84 - x∨⊥=x : forall x -> (x ∨ ⊥) ≈ x - x∨⊥=x x = - begin - x ∨ ⊥ - ∼⟨ byDef ⟨ ∨-pres-≈ ⟩ sym (proj₂ ∧-complement _) ⟩ - x ∨ (x ∧ ¬ x) - ∼⟨ proj₁ absorptive _ _ ⟩ - x - ∎ + x∨⊥=x : forall x -> x ∨ ⊥ ≈ x + x∨⊥=x x = begin + x ∨ ⊥ ≈⟨ byDef ⟨ ∨-pres-≈ ⟩ sym (proj₂ ∧-complement _) ⟩ + x ∨ x ∧ ¬ x ≈⟨ proj₁ absorptive _ _ ⟩ + x ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 93 - x∧⊥=⊥ : forall x -> (x ∧ ⊥) ≈ ⊥ - x∧⊥=⊥ x = - begin - x ∧ ⊥ - ∼⟨ byDef ⟨ ∧-pres-≈ ⟩ sym (proj₂ ∧-complement _) ⟩ - x ∧ (x ∧ ¬ x) - ∼⟨ ∧-assoc _ _ _ ⟩ - (x ∧ x) ∧ ¬ x - ∼⟨ ∧-idempotent _ ⟨ ∧-pres-≈ ⟩ byDef ⟩ - x ∧ ¬ x - ∼⟨ proj₂ ∧-complement _ ⟩ - ⊥ - ∎ + x∧⊥=⊥ : forall x -> x ∧ ⊥ ≈ ⊥ + x∧⊥=⊥ x = begin + x ∧ ⊥ ≈⟨ byDef ⟨ ∧-pres-≈ ⟩ sym (proj₂ ∧-complement _) ⟩ + x ∧ x ∧ ¬ x ≈⟨ ∧-assoc _ _ _ ⟩ + (x ∧ x) ∧ ¬ x ≈⟨ ∧-idempotent _ ⟨ ∧-pres-≈ ⟩ byDef ⟩ + x ∧ ¬ x ≈⟨ proj₂ ∧-complement _ ⟩ + ⊥ ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 103 - ∨-∧-commSemiring : CommutativeSemiring _∨_ _∧_ ⊥ ⊤ - ∨-∧-commSemiring = record - { semiring = record - { +-monoid = record - { monoid = record - { semigroup = record + ∨-∧-isCommutativSemiring : IsCommutativeSemiring _∨_ _∧_ ⊥ ⊤ + ∨-∧-isCommutativSemiring = record + { isSemiring = record + { +-isCommutativeMonoid = record + { isMonoid = record + { isSemigroup = record hunk ./Algebra/Props/BooleanAlgebra.agda 116 - ; *-monoid = record - { semigroup = record + ; *-isMonoid = record + { isSemigroup = record hunk ./Algebra/Props/BooleanAlgebra.agda 129 +∨-∧-commutativeSemiring : CommutativeSemiring +∨-∧-commutativeSemiring = record + { setoid = setoid + ; _+_ = _∨_ + ; _*_ = _∧_ + ; 0# = ⊥ + ; 1# = ⊤ + ; isCommutativeSemiring = ∨-∧-isCommutativSemiring + } + hunk ./Algebra/Props/BooleanAlgebra.agda 148 - x∨⊤=⊤ : forall x -> (x ∨ ⊤) ≈ ⊤ - x∨⊤=⊤ x = - begin - x ∨ ⊤ - ∼⟨ byDef ⟨ ∨-pres-≈ ⟩ sym (proj₂ ∨-complement _) ⟩ - x ∨ (x ∨ ¬ x) - ∼⟨ ∨-assoc _ _ _ ⟩ - (x ∨ x) ∨ ¬ x - ∼⟨ ∨-idempotent _ ⟨ ∨-pres-≈ ⟩ byDef ⟩ - x ∨ ¬ x - ∼⟨ proj₂ ∨-complement _ ⟩ - ⊤ - ∎ + x∨⊤=⊤ : forall x -> x ∨ ⊤ ≈ ⊤ + x∨⊤=⊤ x = begin + x ∨ ⊤ ≈⟨ byDef ⟨ ∨-pres-≈ ⟩ sym (proj₂ ∨-complement _) ⟩ + x ∨ x ∨ ¬ x ≈⟨ ∨-assoc _ _ _ ⟩ + (x ∨ x) ∨ ¬ x ≈⟨ ∨-idempotent _ ⟨ ∨-pres-≈ ⟩ byDef ⟩ + x ∨ ¬ x ≈⟨ proj₂ ∨-complement _ ⟩ + ⊤ ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 158 - ∧-∨-commSemiring : CommutativeSemiring _∧_ _∨_ ⊤ ⊥ - ∧-∨-commSemiring = record - { semiring = record - { +-monoid = record - { monoid = record - { semigroup = record + ∧-∨-isCommutativeSemiring : IsCommutativeSemiring _∧_ _∨_ ⊤ ⊥ + ∧-∨-isCommutativeSemiring = record + { isSemiring = record + { +-isCommutativeMonoid = record + { isMonoid = record + { isSemigroup = record hunk ./Algebra/Props/BooleanAlgebra.agda 171 - ; *-monoid = record - { semigroup = record + ; *-isMonoid = record + { isSemigroup = record hunk ./Algebra/Props/BooleanAlgebra.agda 184 +∧-∨-commutativeSemiring : CommutativeSemiring +∧-∨-commutativeSemiring = record + { setoid = setoid + ; _+_ = _∧_ + ; _*_ = _∨_ + ; 0# = ⊤ + ; 1# = ⊥ + ; isCommutativeSemiring = ∧-∨-isCommutativeSemiring + } + hunk ./Algebra/Props/BooleanAlgebra.agda 204 - lemma : forall x y -> (x ∧ y) ≈ ⊥ -> (x ∨ y) ≈ ⊤ -> (¬ x) ≈ y - lemma x y x∧y=⊥ x∨y=⊤ = - begin - (¬ x) - ∼⟨ sym $ proj₂ ∧-identity _ ⟩ - (¬ x) ∧ ⊤ - ∼⟨ byDef ⟨ ∧-pres-≈ ⟩ sym x∨y=⊤ ⟩ - (¬ x) ∧ (x ∨ y) - ∼⟨ proj₁ ∧-∨-distrib _ _ _ ⟩ - ((¬ x) ∧ x) ∨ ((¬ x) ∧ y) - ∼⟨ proj₁ ∧-complement _ ⟨ ∨-pres-≈ ⟩ byDef ⟩ - ⊥ ∨ ((¬ x) ∧ y) - ∼⟨ sym x∧y=⊥ ⟨ ∨-pres-≈ ⟩ byDef ⟩ - (x ∧ y) ∨ ((¬ x) ∧ y) - ∼⟨ sym $ proj₂ ∧-∨-distrib _ _ _ ⟩ - (x ∨ ¬ x) ∧ y - ∼⟨ proj₂ ∨-complement _ ⟨ ∧-pres-≈ ⟩ byDef ⟩ - ⊤ ∧ y - ∼⟨ proj₁ ∧-identity _ ⟩ - y - ∎ + lemma : forall x y -> x ∧ y ≈ ⊥ -> x ∨ y ≈ ⊤ -> ¬ x ≈ y + lemma x y x∧y=⊥ x∨y=⊤ = begin + ¬ x ≈⟨ sym $ proj₂ ∧-identity _ ⟩ + ¬ x ∧ ⊤ ≈⟨ byDef ⟨ ∧-pres-≈ ⟩ sym x∨y=⊤ ⟩ + ¬ x ∧ (x ∨ y) ≈⟨ proj₁ ∧-∨-distrib _ _ _ ⟩ + ¬ x ∧ x ∨ ¬ x ∧ y ≈⟨ proj₁ ∧-complement _ ⟨ ∨-pres-≈ ⟩ byDef ⟩ + ⊥ ∨ ¬ x ∧ y ≈⟨ sym x∧y=⊥ ⟨ ∨-pres-≈ ⟩ byDef ⟩ + x ∧ y ∨ ¬ x ∧ y ≈⟨ sym $ proj₂ ∧-∨-distrib _ _ _ ⟩ + (x ∨ ¬ x) ∧ y ≈⟨ proj₂ ∨-complement _ ⟨ ∧-pres-≈ ⟩ byDef ⟩ + ⊤ ∧ y ≈⟨ proj₁ ∧-identity _ ⟩ + y ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 225 - deMorgan₁ : forall x y -> ¬ (x ∧ y) ≈ ((¬ x) ∨ (¬ y)) - deMorgan₁ x y = lemma (x ∧ y) ((¬ x) ∨ (¬ y)) lem₁ lem₂ + deMorgan₁ : forall x y -> ¬ (x ∧ y) ≈ ¬ x ∨ ¬ y + deMorgan₁ x y = lemma (x ∧ y) (¬ x ∨ ¬ y) lem₁ lem₂ hunk ./Algebra/Props/BooleanAlgebra.agda 228 - lem₁ = - begin - (x ∧ y) ∧ ((¬ x) ∨ (¬ y)) - ∼⟨ proj₁ ∧-∨-distrib _ _ _ ⟩ - ((x ∧ y) ∧ (¬ x)) ∨ ((x ∧ y) ∧ (¬ y)) - ∼⟨ (∧-comm _ _ ⟨ ∧-pres-≈ ⟩ byDef) ⟨ ∨-pres-≈ ⟩ byDef ⟩ - ((y ∧ x) ∧ (¬ x)) ∨ ((x ∧ y) ∧ (¬ y)) - ∼⟨ sym (∧-assoc _ _ _) ⟨ ∨-pres-≈ ⟩ sym (∧-assoc _ _ _) ⟩ - (y ∧ (x ∧ (¬ x))) ∨ (x ∧ (y ∧ (¬ y))) - ∼⟨ (byDef ⟨ ∧-pres-≈ ⟩ proj₂ ∧-complement _) ⟨ ∨-pres-≈ ⟩ - (byDef ⟨ ∧-pres-≈ ⟩ proj₂ ∧-complement _) ⟩ - (y ∧ ⊥) ∨ (x ∧ ⊥) - ∼⟨ proj₂ ∧-zero _ ⟨ ∨-pres-≈ ⟩ proj₂ ∧-zero _ ⟩ - ⊥ ∨ ⊥ - ∼⟨ proj₂ ∨-identity _ ⟩ - ⊥ - ∎ + lem₁ = begin + (x ∧ y) ∧ (¬ x ∨ ¬ y) ≈⟨ proj₁ ∧-∨-distrib _ _ _ ⟩ + (x ∧ y) ∧ ¬ x ∨ (x ∧ y) ∧ ¬ y ≈⟨ (∧-comm _ _ ⟨ ∧-pres-≈ ⟩ byDef) ⟨ ∨-pres-≈ ⟩ byDef ⟩ + (y ∧ x) ∧ ¬ x ∨ (x ∧ y) ∧ ¬ y ≈⟨ sym (∧-assoc _ _ _) ⟨ ∨-pres-≈ ⟩ sym (∧-assoc _ _ _) ⟩ + y ∧ (x ∧ ¬ x) ∨ x ∧ (y ∧ ¬ y) ≈⟨ (byDef ⟨ ∧-pres-≈ ⟩ proj₂ ∧-complement _) ⟨ ∨-pres-≈ ⟩ + (byDef ⟨ ∧-pres-≈ ⟩ proj₂ ∧-complement _) ⟩ + (y ∧ ⊥) ∨ (x ∧ ⊥) ≈⟨ proj₂ ∧-zero _ ⟨ ∨-pres-≈ ⟩ proj₂ ∧-zero _ ⟩ + ⊥ ∨ ⊥ ≈⟨ proj₂ ∨-identity _ ⟩ + ⊥ ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 238 - lem₃ = - begin - (x ∧ y) ∨ (¬ x) - ∼⟨ proj₂ ∨-∧-distrib _ _ _ ⟩ - (x ∨ (¬ x)) ∧ (y ∨ (¬ x)) - ∼⟨ proj₂ ∨-complement _ ⟨ ∧-pres-≈ ⟩ byDef ⟩ - ⊤ ∧ (y ∨ (¬ x)) - ∼⟨ proj₁ ∧-identity _ ⟩ - y ∨ (¬ x) - ∼⟨ ∨-comm _ _ ⟩ - (¬ x) ∨ y - ∎ + lem₃ = begin + (x ∧ y) ∨ ¬ x ≈⟨ proj₂ ∨-∧-distrib _ _ _ ⟩ + (x ∨ ¬ x) ∧ (y ∨ ¬ x) ≈⟨ proj₂ ∨-complement _ ⟨ ∧-pres-≈ ⟩ byDef ⟩ + ⊤ ∧ (y ∨ ¬ x) ≈⟨ proj₁ ∧-identity _ ⟩ + y ∨ ¬ x ≈⟨ ∨-comm _ _ ⟩ + ¬ x ∨ y ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 245 - lem₂ = - begin - (x ∧ y) ∨ ((¬ x) ∨ (¬ y)) - ∼⟨ ∨-assoc _ _ _ ⟩ - ((x ∧ y) ∨ (¬ x)) ∨ (¬ y) - ∼⟨ lem₃ ⟨ ∨-pres-≈ ⟩ byDef ⟩ - ((¬ x) ∨ y) ∨ (¬ y) - ∼⟨ sym $ ∨-assoc _ _ _ ⟩ - (¬ x) ∨ (y ∨ (¬ y)) - ∼⟨ byDef ⟨ ∨-pres-≈ ⟩ proj₂ ∨-complement _ ⟩ - (¬ x) ∨ ⊤ - ∼⟨ proj₂ ∨-zero _ ⟩ - ⊤ - ∎ + lem₂ = begin + (x ∧ y) ∨ (¬ x ∨ ¬ y) ≈⟨ ∨-assoc _ _ _ ⟩ + ((x ∧ y) ∨ ¬ x) ∨ ¬ y ≈⟨ lem₃ ⟨ ∨-pres-≈ ⟩ byDef ⟩ + (¬ x ∨ y) ∨ ¬ y ≈⟨ sym $ ∨-assoc _ _ _ ⟩ + ¬ x ∨ (y ∨ ¬ y) ≈⟨ byDef ⟨ ∨-pres-≈ ⟩ proj₂ ∨-complement _ ⟩ + ¬ x ∨ ⊤ ≈⟨ proj₂ ∨-zero _ ⟩ + ⊤ ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 253 - deMorgan₂ : forall x y -> ¬ (x ∨ y) ≈ ((¬ x) ∧ (¬ y)) - deMorgan₂ x y = - begin - ¬ (x ∨ y) - ∼⟨ ¬-pres-≈ $ sym (¬-involutive _) ⟨ ∨-pres-≈ ⟩ - sym (¬-involutive _) ⟩ - ¬ ((¬ ¬ x) ∨ (¬ ¬ y)) - ∼⟨ ¬-pres-≈ $ sym $ deMorgan₁ _ _ ⟩ - ¬ ¬ ((¬ x) ∧ (¬ y)) - ∼⟨ ¬-involutive _ ⟩ - (¬ x) ∧ (¬ y) - ∎ + deMorgan₂ : forall x y -> ¬ (x ∨ y) ≈ ¬ x ∧ ¬ y + deMorgan₂ x y = begin + ¬ (x ∨ y) ≈⟨ ¬-pres-≈ $ sym (¬-involutive _) ⟨ ∨-pres-≈ ⟩ + sym (¬-involutive _) ⟩ + ¬ (¬ ¬ x ∨ ¬ ¬ y) ≈⟨ ¬-pres-≈ $ sym $ deMorgan₁ _ _ ⟩ + ¬ ¬ (¬ x ∧ ¬ y) ≈⟨ ¬-involutive _ ⟩ + ¬ x ∧ ¬ y ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 267 - (_⊕_ : Op₂) - (⊕-def : forall x y -> (x ⊕ y) ≈ ((x ∨ y) ∧ ¬ (x ∧ y))) + (xor : Op₂) + (⊕-def : forall x y -> xor x y ≈ (x ∨ y) ∧ ¬ (x ∧ y)) hunk ./Algebra/Props/BooleanAlgebra.agda 271 + private + infixl 6 _⊕_ + + _⊕_ : Op₂ + _⊕_ = xor + hunk ./Algebra/Props/BooleanAlgebra.agda 280 - -> x ≈ y -> u ≈ v -> (x ∧ ¬ u) ≈ (y ∧ ¬ v) + -> x ≈ y -> u ≈ v -> x ∧ ¬ u ≈ y ∧ ¬ v hunk ./Algebra/Props/BooleanAlgebra.agda 283 - ⊕-¬-distribˡ : forall x y -> ¬ (x ⊕ y) ≈ ((¬ x) ⊕ y) - ⊕-¬-distribˡ x y = - begin - ¬ (x ⊕ y) - ∼⟨ ¬-pres-≈ $ ⊕-def _ _ ⟩ - ¬ ((x ∨ y) ∧ (¬ (x ∧ y))) - ∼⟨ ¬-pres-≈ (proj₂ ∧-∨-distrib _ _ _) ⟩ - ¬ ((x ∧ ¬ (x ∧ y)) ∨ (y ∧ ¬ (x ∧ y))) - ∼⟨ ¬-pres-≈ $ + ⊕-¬-distribˡ : forall x y -> ¬ (x ⊕ y) ≈ ¬ x ⊕ y + ⊕-¬-distribˡ x y = begin + ¬ (x ⊕ y) ≈⟨ ¬-pres-≈ $ ⊕-def _ _ ⟩ + ¬ ((x ∨ y) ∧ (¬ (x ∧ y))) ≈⟨ ¬-pres-≈ (proj₂ ∧-∨-distrib _ _ _) ⟩ + ¬ ((x ∧ ¬ (x ∧ y)) ∨ (y ∧ ¬ (x ∧ y))) ≈⟨ ¬-pres-≈ $ hunk ./Algebra/Props/BooleanAlgebra.agda 291 - ¬ ((x ∧ ¬ (x ∧ y)) ∨ (y ∧ ¬ (y ∧ x))) - ∼⟨ ¬-pres-≈ $ lem _ _ ⟨ ∨-pres-≈ ⟩ lem _ _ ⟩ - ¬ ((x ∧ ¬ y) ∨ (y ∧ ¬ x)) - ∼⟨ deMorgan₂ _ _ ⟩ - (¬ (x ∧ ¬ y) ∧ ¬ (y ∧ ¬ x)) - ∼⟨ deMorgan₁ _ _ ⟨ ∧-pres-≈ ⟩ byDef ⟩ - (((¬ x) ∨ (¬ ¬ y)) ∧ ¬ (y ∧ ¬ x)) - ∼⟨ helper (byDef ⟨ ∨-pres-≈ ⟩ ¬-involutive _) - (∧-comm _ _) ⟩ - (((¬ x) ∨ y) ∧ ¬ ((¬ x) ∧ y)) - ∼⟨ sym $ ⊕-def _ _ ⟩ - ((¬ x) ⊕ y) - ∎ + ¬ ((x ∧ ¬ (x ∧ y)) ∨ (y ∧ ¬ (y ∧ x))) ≈⟨ ¬-pres-≈ $ lem _ _ ⟨ ∨-pres-≈ ⟩ lem _ _ ⟩ + ¬ ((x ∧ ¬ y) ∨ (y ∧ ¬ x)) ≈⟨ deMorgan₂ _ _ ⟩ + ¬ (x ∧ ¬ y) ∧ ¬ (y ∧ ¬ x) ≈⟨ deMorgan₁ _ _ ⟨ ∧-pres-≈ ⟩ byDef ⟩ + (¬ x ∨ (¬ ¬ y)) ∧ ¬ (y ∧ ¬ x) ≈⟨ helper (byDef ⟨ ∨-pres-≈ ⟩ ¬-involutive _) + (∧-comm _ _) ⟩ + (¬ x ∨ y) ∧ ¬ (¬ x ∧ y) ≈⟨ sym $ ⊕-def _ _ ⟩ + ¬ x ⊕ y ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 299 - lem : forall x y -> (x ∧ ¬ (x ∧ y)) ≈ (x ∧ (¬ y)) - lem x y = - begin - x ∧ ¬ (x ∧ y) - ∼⟨ byDef ⟨ ∧-pres-≈ ⟩ deMorgan₁ _ _ ⟩ - x ∧ ((¬ x) ∨ (¬ y)) - ∼⟨ proj₁ ∧-∨-distrib _ _ _ ⟩ - (x ∧ (¬ x)) ∨ (x ∧ (¬ y)) - ∼⟨ proj₂ ∧-complement _ ⟨ ∨-pres-≈ ⟩ byDef ⟩ - ⊥ ∨ (x ∧ (¬ y)) - ∼⟨ proj₁ ∨-identity _ ⟩ - x ∧ (¬ y) - ∎ + lem : forall x y -> x ∧ ¬ (x ∧ y) ≈ x ∧ ¬ y + lem x y = begin + x ∧ ¬ (x ∧ y) ≈⟨ byDef ⟨ ∧-pres-≈ ⟩ deMorgan₁ _ _ ⟩ + x ∧ (¬ x ∨ ¬ y) ≈⟨ proj₁ ∧-∨-distrib _ _ _ ⟩ + (x ∧ ¬ x) ∨ (x ∧ ¬ y) ≈⟨ proj₂ ∧-complement _ ⟨ ∨-pres-≈ ⟩ byDef ⟩ + ⊥ ∨ (x ∧ ¬ y) ≈⟨ proj₁ ∨-identity _ ⟩ + x ∧ ¬ y ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 309 - ⊕-comm x y = - begin - x ⊕ y - ∼⟨ ⊕-def _ _ ⟩ - (x ∨ y) ∧ ¬ (x ∧ y) - ∼⟨ helper (∨-comm _ _) (∧-comm _ _) ⟩ - (y ∨ x) ∧ ¬ (y ∧ x) - ∼⟨ sym $ ⊕-def _ _ ⟩ - y ⊕ x - ∎ + ⊕-comm x y = begin + x ⊕ y ≈⟨ ⊕-def _ _ ⟩ + (x ∨ y) ∧ ¬ (x ∧ y) ≈⟨ helper (∨-comm _ _) (∧-comm _ _) ⟩ + (y ∨ x) ∧ ¬ (y ∧ x) ≈⟨ sym $ ⊕-def _ _ ⟩ + y ⊕ x ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 315 - ⊕-¬-distribʳ : forall x y -> ¬ (x ⊕ y) ≈ (x ⊕ (¬ y)) - ⊕-¬-distribʳ x y = - begin - ¬ (x ⊕ y) - ∼⟨ ¬-pres-≈ $ ⊕-comm _ _ ⟩ - ¬ (y ⊕ x) - ∼⟨ ⊕-¬-distribˡ _ _ ⟩ - ((¬ y) ⊕ x) - ∼⟨ ⊕-comm _ _ ⟩ - (x ⊕ (¬ y)) - ∎ + ⊕-¬-distribʳ : forall x y -> ¬ (x ⊕ y) ≈ x ⊕ ¬ y + ⊕-¬-distribʳ x y = begin + ¬ (x ⊕ y) ≈⟨ ¬-pres-≈ $ ⊕-comm _ _ ⟩ + ¬ (y ⊕ x) ≈⟨ ⊕-¬-distribˡ _ _ ⟩ + ¬ y ⊕ x ≈⟨ ⊕-comm _ _ ⟩ + x ⊕ ¬ y ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 322 - ⊕-annihilates-¬ : forall x y -> (x ⊕ y) ≈ ((¬ x) ⊕ (¬ y)) - ⊕-annihilates-¬ x y = - begin - x ⊕ y - ∼⟨ sym $ ¬-involutive _ ⟩ - ¬ ¬ (x ⊕ y) - ∼⟨ ¬-pres-≈ $ ⊕-¬-distribˡ _ _ ⟩ - ¬ ((¬ x) ⊕ y) - ∼⟨ ⊕-¬-distribʳ _ _ ⟩ - ((¬ x) ⊕ (¬ y)) - ∎ + ⊕-annihilates-¬ : forall x y -> x ⊕ y ≈ ¬ x ⊕ ¬ y + ⊕-annihilates-¬ x y = begin + x ⊕ y ≈⟨ sym $ ¬-involutive _ ⟩ + ¬ ¬ (x ⊕ y) ≈⟨ ¬-pres-≈ $ ⊕-¬-distribˡ _ _ ⟩ + ¬ (¬ x ⊕ y) ≈⟨ ⊕-¬-distribʳ _ _ ⟩ + ¬ x ⊕ ¬ y ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 330 - ⊕-pres : _⊕_ Preserves₂-≈ - ⊕-pres {x} {y} {u} {v} x≈y u≈v = - begin - x ⊕ u - ∼⟨ ⊕-def _ _ ⟩ - (x ∨ u) ∧ ¬ (x ∧ u) - ∼⟨ helper (x≈y ⟨ ∨-pres-≈ ⟩ u≈v) + ⊕-pres : _⊕_ Preserves₂ _≈_ → _≈_ → _≈_ + ⊕-pres {x} {y} {u} {v} x≈y u≈v = begin + x ⊕ u ≈⟨ ⊕-def _ _ ⟩ + (x ∨ u) ∧ ¬ (x ∧ u) ≈⟨ helper (x≈y ⟨ ∨-pres-≈ ⟩ u≈v) hunk ./Algebra/Props/BooleanAlgebra.agda 335 - (y ∨ v) ∧ ¬ (y ∧ v) - ∼⟨ sym $ ⊕-def _ _ ⟩ - y ⊕ v - ∎ + (y ∨ v) ∧ ¬ (y ∧ v) ≈⟨ sym $ ⊕-def _ _ ⟩ + y ⊕ v ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 341 - ⊥⊕x=x : forall x -> (⊥ ⊕ x) ≈ x - ⊥⊕x=x x = - begin - ⊥ ⊕ x - ∼⟨ ⊕-def _ _ ⟩ - (⊥ ∨ x) ∧ ¬ (⊥ ∧ x) - ∼⟨ helper (proj₁ ∨-identity _) + ⊥⊕x=x : forall x -> ⊥ ⊕ x ≈ x + ⊥⊕x=x x = begin + ⊥ ⊕ x ≈⟨ ⊕-def _ _ ⟩ + (⊥ ∨ x) ∧ ¬ (⊥ ∧ x) ≈⟨ helper (proj₁ ∨-identity _) hunk ./Algebra/Props/BooleanAlgebra.agda 346 - x ∧ ¬ ⊥ - ∼⟨ byDef ⟨ ∧-pres-≈ ⟩ ¬⊥=⊤ ⟩ - x ∧ ⊤ - ∼⟨ proj₂ ∧-identity _ ⟩ - x - ∎ + x ∧ ¬ ⊥ ≈⟨ byDef ⟨ ∧-pres-≈ ⟩ ¬⊥=⊤ ⟩ + x ∧ ⊤ ≈⟨ proj₂ ∧-identity _ ⟩ + x ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 353 - x⊕x=⊥ : forall x -> (x ⊕ x) ≈ ⊥ - x⊕x=⊥ x = - begin - x ⊕ x - ∼⟨ ⊕-def _ _ ⟩ - (x ∨ x) ∧ ¬ (x ∧ x) - ∼⟨ helper (∨-idempotent _) + x⊕x=⊥ : forall x -> x ⊕ x ≈ ⊥ + x⊕x=⊥ x = begin + x ⊕ x ≈⟨ ⊕-def _ _ ⟩ + (x ∨ x) ∧ ¬ (x ∧ x) ≈⟨ helper (∨-idempotent _) hunk ./Algebra/Props/BooleanAlgebra.agda 358 - x ∧ ¬ x - ∼⟨ proj₂ ∧-complement _ ⟩ - ⊥ - ∎ + x ∧ ¬ x ≈⟨ proj₂ ∧-complement _ ⟩ + ⊥ ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 365 - distˡ x y z = - begin - x ∧ (y ⊕ z) - ∼⟨ byDef ⟨ ∧-pres-≈ ⟩ ⊕-def _ _ ⟩ - x ∧ ((y ∨ z) ∧ ¬ (y ∧ z)) - ∼⟨ ∧-assoc _ _ _ ⟩ - (x ∧ (y ∨ z)) ∧ ¬ (y ∧ z) - ∼⟨ byDef ⟨ ∧-pres-≈ ⟩ deMorgan₁ _ _ ⟩ + distˡ x y z = begin + x ∧ (y ⊕ z) ≈⟨ byDef ⟨ ∧-pres-≈ ⟩ ⊕-def _ _ ⟩ + x ∧ ((y ∨ z) ∧ ¬ (y ∧ z)) ≈⟨ ∧-assoc _ _ _ ⟩ + (x ∧ (y ∨ z)) ∧ ¬ (y ∧ z) ≈⟨ byDef ⟨ ∧-pres-≈ ⟩ deMorgan₁ _ _ ⟩ hunk ./Algebra/Props/BooleanAlgebra.agda 370 - ((¬ y) ∨ (¬ z)) - ∼⟨ sym $ proj₁ ∨-identity _ ⟩ + (¬ y ∨ ¬ z) ≈⟨ sym $ proj₁ ∨-identity _ ⟩ hunk ./Algebra/Props/BooleanAlgebra.agda 373 - ((¬ y) ∨ (¬ z))) - ∼⟨ lem₃ ⟨ ∨-pres-≈ ⟩ byDef ⟩ - ((x ∧ (y ∨ z)) ∧ (¬ x)) ∨ + (¬ y ∨ ¬ z)) ≈⟨ lem₃ ⟨ ∨-pres-≈ ⟩ byDef ⟩ + ((x ∧ (y ∨ z)) ∧ ¬ x) ∨ hunk ./Algebra/Props/BooleanAlgebra.agda 376 - ((¬ y) ∨ (¬ z))) - ∼⟨ sym $ proj₁ ∧-∨-distrib _ _ _ ⟩ + (¬ y ∨ ¬ z)) ≈⟨ sym $ proj₁ ∧-∨-distrib _ _ _ ⟩ hunk ./Algebra/Props/BooleanAlgebra.agda 378 - ((¬ x) ∨ ((¬ y) ∨ (¬ z))) - ∼⟨ byDef ⟨ ∧-pres-≈ ⟩ + (¬ x ∨ (¬ y ∨ ¬ z)) ≈⟨ byDef ⟨ ∧-pres-≈ ⟩ hunk ./Algebra/Props/BooleanAlgebra.agda 381 - ((¬ x) ∨ ¬ (y ∧ z)) - ∼⟨ byDef ⟨ ∧-pres-≈ ⟩ sym (deMorgan₁ _ _) ⟩ + (¬ x ∨ ¬ (y ∧ z)) ≈⟨ byDef ⟨ ∧-pres-≈ ⟩ sym (deMorgan₁ _ _) ⟩ hunk ./Algebra/Props/BooleanAlgebra.agda 383 - ¬ (x ∧ (y ∧ z)) - ∼⟨ helper byDef lem₁ ⟩ + ¬ (x ∧ (y ∧ z)) ≈⟨ helper byDef lem₁ ⟩ hunk ./Algebra/Props/BooleanAlgebra.agda 385 - ¬ ((x ∧ y) ∧ (x ∧ z)) - ∼⟨ proj₁ ∧-∨-distrib _ _ _ ⟨ ∧-pres-≈ ⟩ + ¬ ((x ∧ y) ∧ (x ∧ z)) ≈⟨ proj₁ ∧-∨-distrib _ _ _ ⟨ ∧-pres-≈ ⟩ hunk ./Algebra/Props/BooleanAlgebra.agda 388 - ¬ ((x ∧ y) ∧ (x ∧ z)) - ∼⟨ sym $ ⊕-def _ _ ⟩ - (x ∧ y) ⊕ (x ∧ z) - ∎ + ¬ ((x ∧ y) ∧ (x ∧ z)) ≈⟨ sym $ ⊕-def _ _ ⟩ + (x ∧ y) ⊕ (x ∧ z) ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 391 - lem₂ = - begin - x ∧ (y ∧ z) - ∼⟨ ∧-assoc _ _ _ ⟩ - (x ∧ y) ∧ z - ∼⟨ ∧-comm _ _ ⟨ ∧-pres-≈ ⟩ byDef ⟩ - (y ∧ x) ∧ z - ∼⟨ sym $ ∧-assoc _ _ _ ⟩ - y ∧ (x ∧ z) - ∎ + lem₂ = begin + x ∧ (y ∧ z) ≈⟨ ∧-assoc _ _ _ ⟩ + (x ∧ y) ∧ z ≈⟨ ∧-comm _ _ ⟨ ∧-pres-≈ ⟩ byDef ⟩ + (y ∧ x) ∧ z ≈⟨ sym $ ∧-assoc _ _ _ ⟩ + y ∧ (x ∧ z) ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 397 - lem₁ = - begin - x ∧ (y ∧ z) - ∼⟨ sym (∧-idempotent _) ⟨ ∧-pres-≈ ⟩ byDef ⟩ - (x ∧ x) ∧ (y ∧ z) - ∼⟨ sym $ ∧-assoc _ _ _ ⟩ - x ∧ (x ∧ (y ∧ z)) - ∼⟨ byDef ⟨ ∧-pres-≈ ⟩ lem₂ ⟩ - x ∧ (y ∧ (x ∧ z)) - ∼⟨ ∧-assoc _ _ _ ⟩ - (x ∧ y) ∧ (x ∧ z) - ∎ + lem₁ = begin + x ∧ (y ∧ z) ≈⟨ sym (∧-idempotent _) ⟨ ∧-pres-≈ ⟩ byDef ⟩ + (x ∧ x) ∧ (y ∧ z) ≈⟨ sym $ ∧-assoc _ _ _ ⟩ + x ∧ (x ∧ (y ∧ z)) ≈⟨ byDef ⟨ ∧-pres-≈ ⟩ lem₂ ⟩ + x ∧ (y ∧ (x ∧ z)) ≈⟨ ∧-assoc _ _ _ ⟩ + (x ∧ y) ∧ (x ∧ z) ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 404 - lem₃ = - begin - ⊥ - ∼⟨ sym $ proj₂ ∧-zero _ ⟩ - (y ∨ z) ∧ ⊥ - ∼⟨ byDef ⟨ ∧-pres-≈ ⟩ sym (proj₂ ∧-complement _) ⟩ - (y ∨ z) ∧ (x ∧ (¬ x)) - ∼⟨ ∧-assoc _ _ _ ⟩ - ((y ∨ z) ∧ x) ∧ (¬ x) - ∼⟨ ∧-comm _ _ ⟨ ∧-pres-≈ ⟩ byDef ⟩ - (x ∧ (y ∨ z)) ∧ (¬ x) - ∎ + lem₃ = begin + ⊥ ≈⟨ sym $ proj₂ ∧-zero _ ⟩ + (y ∨ z) ∧ ⊥ ≈⟨ byDef ⟨ ∧-pres-≈ ⟩ sym (proj₂ ∧-complement _) ⟩ + (y ∨ z) ∧ (x ∧ ¬ x) ≈⟨ ∧-assoc _ _ _ ⟩ + ((y ∨ z) ∧ x) ∧ ¬ x ≈⟨ ∧-comm _ _ ⟨ ∧-pres-≈ ⟩ byDef ⟩ + (x ∧ (y ∨ z)) ∧ ¬ x ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 412 - distʳ x y z = - begin - (y ⊕ z) ∧ x - ∼⟨ ∧-comm _ _ ⟩ - x ∧ (y ⊕ z) - ∼⟨ distˡ _ _ _ ⟩ - (x ∧ y) ⊕ (x ∧ z) - ∼⟨ ∧-comm _ _ ⟨ ⊕-pres ⟩ ∧-comm _ _ ⟩ - (y ∧ x) ⊕ (z ∧ x) - ∎ + distʳ x y z = begin + (y ⊕ z) ∧ x ≈⟨ ∧-comm _ _ ⟩ + x ∧ (y ⊕ z) ≈⟨ distˡ _ _ _ ⟩ + (x ∧ y) ⊕ (x ∧ z) ≈⟨ ∧-comm _ _ ⟨ ⊕-pres ⟩ ∧-comm _ _ ⟩ + (y ∧ x) ⊕ (z ∧ x) ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 419 - -> ((x ∧ y) ∨ (u ∧ v)) ≈ - (((x ∨ u) ∧ (y ∨ u)) ∧ - ((x ∨ v) ∧ (y ∨ v))) - lemma₂ x y u v = - begin - (x ∧ y) ∨ (u ∧ v) - ∼⟨ proj₁ ∨-∧-distrib _ _ _ ⟩ - ((x ∧ y) ∨ u) ∧ ((x ∧ y) ∨ v) - ∼⟨ proj₂ ∨-∧-distrib _ _ _ ⟨ ∧-pres-≈ ⟩ proj₂ ∨-∧-distrib _ _ _ ⟩ - ((x ∨ u) ∧ (y ∨ u)) ∧ ((x ∨ v) ∧ (y ∨ v)) - ∎ + -> (x ∧ y) ∨ (u ∧ v) ≈ + ((x ∨ u) ∧ (y ∨ u)) ∧ + ((x ∨ v) ∧ (y ∨ v)) + lemma₂ x y u v = begin + (x ∧ y) ∨ (u ∧ v) ≈⟨ proj₁ ∨-∧-distrib _ _ _ ⟩ + ((x ∧ y) ∨ u) ∧ ((x ∧ y) ∨ v) ≈⟨ proj₂ ∨-∧-distrib _ _ _ + ⟨ ∧-pres-≈ ⟩ + proj₂ ∨-∧-distrib _ _ _ ⟩ + ((x ∨ u) ∧ (y ∨ u)) ∧ + ((x ∨ v) ∧ (y ∨ v)) ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 431 - ⊕-assoc x y z = - begin - x ⊕ (y ⊕ z) - ∼⟨ byDef ⟨ ⊕-pres ⟩ ⊕-def _ _ ⟩ - x ⊕ ((y ∨ z) ∧ ¬ (y ∧ z)) - ∼⟨ ⊕-def _ _ ⟩ + ⊕-assoc x y z = begin + x ⊕ (y ⊕ z) ≈⟨ byDef ⟨ ⊕-pres ⟩ ⊕-def _ _ ⟩ + x ⊕ ((y ∨ z) ∧ ¬ (y ∧ z)) ≈⟨ ⊕-def _ _ ⟩ hunk ./Algebra/Props/BooleanAlgebra.agda 435 - ¬ (x ∧ ((y ∨ z) ∧ ¬ (y ∧ z))) - ∼⟨ lem₃ ⟨ ∧-pres-≈ ⟩ lem₄ ⟩ - (((x ∨ y) ∨ z) ∧ ((x ∨ (¬ y)) ∨ (¬ z))) ∧ - ((((¬ x) ∨ (¬ y)) ∨ z) ∧ (((¬ x) ∨ y) ∨ (¬ z))) - ∼⟨ sym $ ∧-assoc _ _ _ ⟩ + ¬ (x ∧ ((y ∨ z) ∧ ¬ (y ∧ z))) ≈⟨ lem₃ ⟨ ∧-pres-≈ ⟩ lem₄ ⟩ + (((x ∨ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z)) ∧ + (((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z)) ≈⟨ sym $ ∧-assoc _ _ _ ⟩ hunk ./Algebra/Props/BooleanAlgebra.agda 439 - (((x ∨ (¬ y)) ∨ (¬ z)) ∧ - ((((¬ x) ∨ (¬ y)) ∨ z) ∧ (((¬ x) ∨ y) ∨ (¬ z)))) - ∼⟨ byDef ⟨ ∧-pres-≈ ⟩ lem₅ ⟩ + (((x ∨ ¬ y) ∨ ¬ z) ∧ + (((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z))) ≈⟨ byDef ⟨ ∧-pres-≈ ⟩ lem₅ ⟩ hunk ./Algebra/Props/BooleanAlgebra.agda 442 - ((((¬ x) ∨ (¬ y)) ∨ z) ∧ - (((x ∨ (¬ y)) ∨ ¬ z) ∧ (((¬ x) ∨ y) ∨ ¬ z))) - ∼⟨ ∧-assoc _ _ _ ⟩ - (((x ∨ y) ∨ z) ∧ (((¬ x) ∨ (¬ y)) ∨ z)) ∧ - (((x ∨ (¬ y)) ∨ ¬ z) ∧ (((¬ x) ∨ y) ∨ ¬ z)) - ∼⟨ lem₁ ⟨ ∧-pres-≈ ⟩ lem₂ ⟩ + (((¬ x ∨ ¬ y) ∨ z) ∧ + (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z))) ≈⟨ ∧-assoc _ _ _ ⟩ + (((x ∨ y) ∨ z) ∧ ((¬ x ∨ ¬ y) ∨ z)) ∧ + (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z)) ≈⟨ lem₁ ⟨ ∧-pres-≈ ⟩ lem₂ ⟩ hunk ./Algebra/Props/BooleanAlgebra.agda 447 - ¬ (((x ∨ y) ∧ ¬ (x ∧ y)) ∧ z) - ∼⟨ sym $ ⊕-def _ _ ⟩ - ((x ∨ y) ∧ ¬ (x ∧ y)) ⊕ z - ∼⟨ sym $ ⊕-def _ _ ⟨ ⊕-pres ⟩ byDef ⟩ - (x ⊕ y) ⊕ z - ∎ + ¬ (((x ∨ y) ∧ ¬ (x ∧ y)) ∧ z) ≈⟨ sym $ ⊕-def _ _ ⟩ + ((x ∨ y) ∧ ¬ (x ∧ y)) ⊕ z ≈⟨ sym $ ⊕-def _ _ ⟨ ⊕-pres ⟩ byDef ⟩ + (x ⊕ y) ⊕ z ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 451 - lem₁ = - begin - ((x ∨ y) ∨ z) ∧ (((¬ x) ∨ (¬ y)) ∨ z) - ∼⟨ sym $ proj₂ ∨-∧-distrib _ _ _ ⟩ - ((x ∨ y) ∧ ((¬ x) ∨ (¬ y))) ∨ z - ∼⟨ (byDef ⟨ ∧-pres-≈ ⟩ sym (deMorgan₁ _ _)) + lem₁ = begin + ((x ∨ y) ∨ z) ∧ ((¬ x ∨ ¬ y) ∨ z) ≈⟨ sym $ proj₂ ∨-∧-distrib _ _ _ ⟩ + ((x ∨ y) ∧ (¬ x ∨ ¬ y)) ∨ z ≈⟨ (byDef ⟨ ∧-pres-≈ ⟩ sym (deMorgan₁ _ _)) hunk ./Algebra/Props/BooleanAlgebra.agda 455 - ((x ∨ y) ∧ ¬ (x ∧ y)) ∨ z - ∎ + ((x ∨ y) ∧ ¬ (x ∧ y)) ∨ z ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 457 - lem₂' = - begin - (x ∨ (¬ y)) ∧ ((¬ x) ∨ y) - ∼⟨ sym $ - proj₁ ∧-identity _ - ⟨ ∧-pres-≈ ⟩ - proj₂ ∧-identity _ ⟩ - (⊤ ∧ (x ∨ (¬ y))) ∧ (((¬ x) ∨ y) ∧ ⊤) - ∼⟨ sym $ - (proj₁ ∨-complement _ ⟨ ∧-pres-≈ ⟩ ∨-comm _ _) - ⟨ ∧-pres-≈ ⟩ - (byDef ⟨ ∧-pres-≈ ⟩ proj₁ ∨-complement _) ⟩ - (((¬ x) ∨ x) ∧ ((¬ y) ∨ x)) ∧ - (((¬ x) ∨ y) ∧ ((¬ y) ∨ y)) - ∼⟨ sym $ lemma₂ _ _ _ _ ⟩ - ((¬ x) ∧ (¬ y)) ∨ (x ∧ y) - ∼⟨ sym $ deMorgan₂ _ _ ⟨ ∨-pres-≈ ⟩ ¬-involutive _ ⟩ - ¬ (x ∨ y) ∨ ¬ ¬ (x ∧ y) - ∼⟨ sym (deMorgan₁ _ _) ⟩ - ¬ ((x ∨ y) ∧ ¬ (x ∧ y)) - ∎ + lem₂' = begin + (x ∨ ¬ y) ∧ (¬ x ∨ y) ≈⟨ sym $ + proj₁ ∧-identity _ + ⟨ ∧-pres-≈ ⟩ + proj₂ ∧-identity _ ⟩ + (⊤ ∧ (x ∨ ¬ y)) ∧ ((¬ x ∨ y) ∧ ⊤) ≈⟨ sym $ + (proj₁ ∨-complement _ ⟨ ∧-pres-≈ ⟩ ∨-comm _ _) + ⟨ ∧-pres-≈ ⟩ + (byDef ⟨ ∧-pres-≈ ⟩ proj₁ ∨-complement _) ⟩ + ((¬ x ∨ x) ∧ (¬ y ∨ x)) ∧ + ((¬ x ∨ y) ∧ (¬ y ∨ y)) ≈⟨ sym $ lemma₂ _ _ _ _ ⟩ + (¬ x ∧ ¬ y) ∨ (x ∧ y) ≈⟨ sym $ deMorgan₂ _ _ ⟨ ∨-pres-≈ ⟩ ¬-involutive _ ⟩ + ¬ (x ∨ y) ∨ ¬ ¬ (x ∧ y) ≈⟨ sym (deMorgan₁ _ _) ⟩ + ¬ ((x ∨ y) ∧ ¬ (x ∧ y)) ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 472 - lem₂ = - begin - ((x ∨ (¬ y)) ∨ ¬ z) ∧ (((¬ x) ∨ y) ∨ ¬ z) - ∼⟨ sym $ proj₂ ∨-∧-distrib _ _ _ ⟩ - ((x ∨ (¬ y)) ∧ ((¬ x) ∨ y)) ∨ ¬ z - ∼⟨ lem₂' ⟨ ∨-pres-≈ ⟩ byDef ⟩ - ¬ ((x ∨ y) ∧ ¬ (x ∧ y)) ∨ ¬ z - ∼⟨ sym $ deMorgan₁ _ _ ⟩ - ¬ (((x ∨ y) ∧ ¬ (x ∧ y)) ∧ z) - ∎ + lem₂ = begin + ((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z) ≈⟨ sym $ proj₂ ∨-∧-distrib _ _ _ ⟩ + ((x ∨ ¬ y) ∧ (¬ x ∨ y)) ∨ ¬ z ≈⟨ lem₂' ⟨ ∨-pres-≈ ⟩ byDef ⟩ + ¬ ((x ∨ y) ∧ ¬ (x ∧ y)) ∨ ¬ z ≈⟨ sym $ deMorgan₁ _ _ ⟩ + ¬ (((x ∨ y) ∧ ¬ (x ∧ y)) ∧ z) ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 478 - lem₃ = - begin - x ∨ ((y ∨ z) ∧ ¬ (y ∧ z)) - ∼⟨ byDef ⟨ ∨-pres-≈ ⟩ - (byDef ⟨ ∧-pres-≈ ⟩ deMorgan₁ _ _) ⟩ - x ∨ ((y ∨ z) ∧ ((¬ y) ∨ (¬ z))) - ∼⟨ proj₁ ∨-∧-distrib _ _ _ ⟩ - (x ∨ (y ∨ z)) ∧ (x ∨ ((¬ y) ∨ (¬ z))) - ∼⟨ ∨-assoc _ _ _ ⟨ ∧-pres-≈ ⟩ ∨-assoc _ _ _ ⟩ - ((x ∨ y) ∨ z) ∧ ((x ∨ (¬ y)) ∨ (¬ z)) - ∎ + lem₃ = begin + x ∨ ((y ∨ z) ∧ ¬ (y ∧ z)) ≈⟨ byDef ⟨ ∨-pres-≈ ⟩ + (byDef ⟨ ∧-pres-≈ ⟩ deMorgan₁ _ _) ⟩ + x ∨ ((y ∨ z) ∧ (¬ y ∨ ¬ z)) ≈⟨ proj₁ ∨-∧-distrib _ _ _ ⟩ + (x ∨ (y ∨ z)) ∧ (x ∨ (¬ y ∨ ¬ z)) ≈⟨ ∨-assoc _ _ _ ⟨ ∧-pres-≈ ⟩ ∨-assoc _ _ _ ⟩ + ((x ∨ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z) ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 485 - lem₄' = - begin - ¬ ((y ∨ z) ∧ ¬ (y ∧ z)) - ∼⟨ deMorgan₁ _ _ ⟩ - ¬ (y ∨ z) ∨ ¬ ¬ (y ∧ z) - ∼⟨ deMorgan₂ _ _ ⟨ ∨-pres-≈ ⟩ ¬-involutive _ ⟩ - ((¬ y) ∧ (¬ z)) ∨ (y ∧ z) - ∼⟨ lemma₂ _ _ _ _ ⟩ - (((¬ y) ∨ y) ∧ ((¬ z) ∨ y)) ∧ - (((¬ y) ∨ z) ∧ ((¬ z) ∨ z)) - ∼⟨ (proj₁ ∨-complement _ ⟨ ∧-pres-≈ ⟩ ∨-comm _ _) - ⟨ ∧-pres-≈ ⟩ - (byDef ⟨ ∧-pres-≈ ⟩ proj₁ ∨-complement _) ⟩ - (⊤ ∧ (y ∨ (¬ z))) ∧ - (((¬ y) ∨ z) ∧ ⊤) - ∼⟨ proj₁ ∧-identity _ ⟨ ∧-pres-≈ ⟩ - proj₂ ∧-identity _ ⟩ - (y ∨ (¬ z)) ∧ ((¬ y) ∨ z) - ∎ + lem₄' = begin + ¬ ((y ∨ z) ∧ ¬ (y ∧ z)) ≈⟨ deMorgan₁ _ _ ⟩ + ¬ (y ∨ z) ∨ ¬ ¬ (y ∧ z) ≈⟨ deMorgan₂ _ _ ⟨ ∨-pres-≈ ⟩ ¬-involutive _ ⟩ + (¬ y ∧ ¬ z) ∨ (y ∧ z) ≈⟨ lemma₂ _ _ _ _ ⟩ + ((¬ y ∨ y) ∧ (¬ z ∨ y)) ∧ + ((¬ y ∨ z) ∧ (¬ z ∨ z)) ≈⟨ (proj₁ ∨-complement _ ⟨ ∧-pres-≈ ⟩ ∨-comm _ _) + ⟨ ∧-pres-≈ ⟩ + (byDef ⟨ ∧-pres-≈ ⟩ proj₁ ∨-complement _) ⟩ + (⊤ ∧ (y ∨ ¬ z)) ∧ + ((¬ y ∨ z) ∧ ⊤) ≈⟨ proj₁ ∧-identity _ ⟨ ∧-pres-≈ ⟩ + proj₂ ∧-identity _ ⟩ + (y ∨ ¬ z) ∧ (¬ y ∨ z) ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 498 - lem₄ = - begin - ¬ (x ∧ ((y ∨ z) ∧ ¬ (y ∧ z))) - ∼⟨ deMorgan₁ _ _ ⟩ - (¬ x) ∨ ¬ ((y ∨ z) ∧ ¬ (y ∧ z)) - ∼⟨ byDef ⟨ ∨-pres-≈ ⟩ lem₄' ⟩ - (¬ x) ∨ ((y ∨ (¬ z)) ∧ ((¬ y) ∨ z)) - ∼⟨ proj₁ ∨-∧-distrib _ _ _ ⟩ - ((¬ x) ∨ (y ∨ (¬ z))) ∧ - ((¬ x) ∨ ((¬ y) ∨ z)) - ∼⟨ ∨-assoc _ _ _ ⟨ ∧-pres-≈ ⟩ ∨-assoc _ _ _ ⟩ - (((¬ x) ∨ y) ∨ (¬ z)) ∧ - (((¬ x) ∨ (¬ y)) ∨ z) - ∼⟨ ∧-comm _ _ ⟩ - (((¬ x) ∨ (¬ y)) ∨ z) ∧ - (((¬ x) ∨ y) ∨ (¬ z)) - ∎ + lem₄ = begin + ¬ (x ∧ ((y ∨ z) ∧ ¬ (y ∧ z))) ≈⟨ deMorgan₁ _ _ ⟩ + ¬ x ∨ ¬ ((y ∨ z) ∧ ¬ (y ∧ z)) ≈⟨ byDef ⟨ ∨-pres-≈ ⟩ lem₄' ⟩ + ¬ x ∨ ((y ∨ ¬ z) ∧ (¬ y ∨ z)) ≈⟨ proj₁ ∨-∧-distrib _ _ _ ⟩ + (¬ x ∨ (y ∨ ¬ z)) ∧ + (¬ x ∨ (¬ y ∨ z)) ≈⟨ ∨-assoc _ _ _ ⟨ ∧-pres-≈ ⟩ ∨-assoc _ _ _ ⟩ + ((¬ x ∨ y) ∨ ¬ z) ∧ + ((¬ x ∨ ¬ y) ∨ z) ≈⟨ ∧-comm _ _ ⟩ + ((¬ x ∨ ¬ y) ∨ z) ∧ + ((¬ x ∨ y) ∨ ¬ z) ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 509 - lem₅ = - begin - ((x ∨ (¬ y)) ∨ (¬ z)) ∧ - ((((¬ x) ∨ (¬ y)) ∨ z) ∧ (((¬ x) ∨ y) ∨ (¬ z))) - ∼⟨ ∧-assoc _ _ _ ⟩ - (((x ∨ (¬ y)) ∨ (¬ z)) ∧ (((¬ x) ∨ (¬ y)) ∨ z)) ∧ - (((¬ x) ∨ y) ∨ (¬ z)) - ∼⟨ ∧-comm _ _ ⟨ ∧-pres-≈ ⟩ byDef ⟩ - ((((¬ x) ∨ (¬ y)) ∨ z) ∧ ((x ∨ (¬ y)) ∨ (¬ z))) ∧ - (((¬ x) ∨ y) ∨ (¬ z)) - ∼⟨ sym $ ∧-assoc _ _ _ ⟩ - (((¬ x) ∨ (¬ y)) ∨ z) ∧ - (((x ∨ (¬ y)) ∨ ¬ z) ∧ (((¬ x) ∨ y) ∨ ¬ z)) - ∎ + lem₅ = begin + ((x ∨ ¬ y) ∨ ¬ z) ∧ + (((¬ x ∨ ¬ y) ∨ z) ∧ ((¬ x ∨ y) ∨ ¬ z)) ≈⟨ ∧-assoc _ _ _ ⟩ + (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ ¬ y) ∨ z)) ∧ + ((¬ x ∨ y) ∨ ¬ z) ≈⟨ ∧-comm _ _ ⟨ ∧-pres-≈ ⟩ byDef ⟩ + (((¬ x ∨ ¬ y) ∨ z) ∧ ((x ∨ ¬ y) ∨ ¬ z)) ∧ + ((¬ x ∨ y) ∨ ¬ z) ≈⟨ sym $ ∧-assoc _ _ _ ⟩ + ((¬ x ∨ ¬ y) ∨ z) ∧ + (((x ∨ ¬ y) ∨ ¬ z) ∧ ((¬ x ∨ y) ∨ ¬ z)) ∎ hunk ./Algebra/Props/BooleanAlgebra.agda 519 - commRing : CommutativeRing _⊕_ _∧_ id ⊥ ⊤ - commRing = record - { ring = record - { +-group = record - { group = record - { monoid = record - { semigroup = record + isCommutativeRing : IsCommutativeRing _⊕_ _∧_ id ⊥ ⊤ + isCommutativeRing = record + { isRing = record + { +-isAbelianGroup = record + { isGroup = record + { isMonoid = record + { isSemigroup = record hunk ./Algebra/Props/BooleanAlgebra.agda 536 - ; *-monoid = record - { semigroup = record + ; *-isMonoid = record + { isSemigroup = record hunk ./Algebra/Props/BooleanAlgebra.agda 548 - commRingoid : CommutativeRingoid - commRingoid = record - { bare = record - { setoid = setoid - ; _+_ = _⊕_ - ; _*_ = _∧_ - ; -_ = id - ; 0# = ⊥ - ; 1# = ⊤ - } - ; commRing = commRing + commutativeRing : CommutativeRing + commutativeRing = record + { setoid = setoid + ; _+_ = _⊕_ + ; _*_ = _∧_ + ; -_ = id + ; 0# = ⊥ + ; 1# = ⊤ + ; isCommutativeRing = isCommutativeRing hunk ./Algebra/Props/BooleanAlgebra.agda 559 +infixl 6 _⊕_ + hunk ./Algebra/Props/CommutativeRing.agda 1 ------------------------------------------------------------------------- --- Some derivable properties ------------------------------------------------------------------------- - -open import Algebra.Packaged - -module Algebra.Props.CommutativeRing - (r : CommutativeRingoid) - where - -import Algebra -import Algebra.Props.Ring -open CommutativeRingoid r -open BareRingoid bare -open Algebra setoid -open CommutativeRing commRing - ------------------------------------------------------------------------- --- A commutative ring is a ring - -ringoid : Ringoid -ringoid = record - { bare = record - { setoid = setoid - ; _+_ = _+_ - ; _*_ = _*_ - ; -_ = -_ - ; 0# = 0# - ; 1# = 1# - } - ; ring = ring - } - -open Algebra.Props.Ring ringoid public - ------------------------------------------------------------------------- --- A commutative ring is a commutative semiring - -abstract - - commSemiring : CommutativeSemiring _+_ _*_ 0# 1# - commSemiring = record - { semiring = semiring - ; *-comm = *-comm - } - -commSemiringoid : CommutativeSemiringoid -commSemiringoid = record - { setoid = setoid - ; _+_ = _+_ - ; _*_ = _*_ - ; 0# = 0# - ; 1# = 1# - ; commSemiring = commSemiring - } - ------------------------------------------------------------------------- --- A commutative ring is an "almost commutative ring" - -abstract - - almostCommRing : AlmostCommRing _+_ _*_ -_ 0# 1# - almostCommRing = record - { commSemiring = commSemiring - ; ¬-pres-≈ = Group.⁻¹-pres-≈ (AbelianGroup.group (Ring.+-group ring)) - ; ¬-*-distribˡ = ¬-*-distribˡ - ; ¬-+-comm = ¬-+-comm - } - -almostCommRingoid : AlmostCommRingoid -almostCommRingoid = record - { bare = record - { setoid = setoid - ; _+_ = _+_ - ; _*_ = _*_ - ; -_ = -_ - ; 0# = 0# - ; 1# = 1# - } - ; almostCommRing = almostCommRing - } rmfile ./Algebra/Props/CommutativeRing.agda hunk ./Algebra/Props/CommutativeSemiring.agda 1 ------------------------------------------------------------------------- --- Some derivable properties ------------------------------------------------------------------------- - -open import Algebra.Packaged - -module Algebra.Props.CommutativeSemiring - (r : CommutativeSemiringoid) - where - -import Algebra -import Relation.Binary.EqReasoning -open import Relation.Binary -open import Data.Function -import Algebra.Props.Semiring as SProp -open CommutativeSemiringoid r -open Algebra setoid -open CommutativeSemiring commSemiring -open Relation.Binary.EqReasoning (Setoid.preorder setoid) - ------------------------------------------------------------------------- --- A commutative semiring is a semiring - -semiringoid : Semiringoid -semiringoid = record - { setoid = setoid - ; _+_ = _+_ - ; _*_ = _*_ - ; 0# = 0# - ; 1# = 1# - ; semiring = semiring - } - -open SProp semiringoid public - ------------------------------------------------------------------------- --- Commutative semirings can be viewed as almost commutative rings by --- using identity as the "almost negation" - -almostCommRingoid : AlmostCommRingoid -almostCommRingoid = record - { bare = bareRingoid - ; almostCommRing = record - { commSemiring = commSemiring - ; ¬-pres-≈ = id - ; ¬-*-distribˡ = \_ _ -> byDef - ; ¬-+-comm = \_ _ -> byDef - } - } rmfile ./Algebra/Props/CommutativeSemiring.agda hunk ./Algebra/Props/DistributiveLattice.agda 5 -open import Algebra.Packaged +open import Algebra hunk ./Algebra/Props/DistributiveLattice.agda 8 - (dl : DistributiveLatticoid) - where + (dl : DistributiveLattice) + where hunk ./Algebra/Props/DistributiveLattice.agda 11 -open import Relation.Binary +open DistributiveLattice dl +import Algebra.Props.Lattice as L; open L lattice public +import Algebra.Structures as S; open S setoid +import Algebra.FunctionProperties as P; open P setoid +import Relation.Binary.EqReasoning as EqR; open EqR setoid hunk ./Algebra/Props/DistributiveLattice.agda 18 -import Relation.Binary.EqReasoning -import Algebra -import Algebra.Props.Lattice -open DistributiveLatticoid dl -open Algebra setoid -open DistributiveLattice distLattice -open Lattice lattice -open Setoid setoid -open Relation.Binary.EqReasoning preorder - ------------------------------------------------------------------------- --- A distributive lattice is a lattice - -latticoid : Latticoid -latticoid = record - { setoid = setoid - ; _∨_ = _∨_ - ; _∧_ = _∧_ - ; lattice = lattice - } - -open Algebra.Props.Lattice latticoid public - ------------------------------------------------------------------------- --- Some properties hunk ./Algebra/Props/DistributiveLattice.agda 25 - ∨-∧-distribʳ x y z = - begin - (y ∧ z) ∨ x - ∼⟨ ∨-comm _ _ ⟩ - x ∨ (y ∧ z) - ∼⟨ ∨-∧-distribˡ _ _ _ ⟩ - (x ∨ y) ∧ (x ∨ z) - ∼⟨ ∨-comm _ _ ⟨ ∧-pres-≈ ⟩ ∨-comm _ _ ⟩ - (y ∨ x) ∧ (z ∨ x) - ∎ + ∨-∧-distribʳ x y z = begin + y ∧ z ∨ x ≈⟨ ∨-comm _ _ ⟩ + x ∨ y ∧ z ≈⟨ ∨-∧-distribˡ _ _ _ ⟩ + (x ∨ y) ∧ (x ∨ z) ≈⟨ ∨-comm _ _ ⟨ ∧-pres-≈ ⟩ ∨-comm _ _ ⟩ + (y ∨ x) ∧ (z ∨ x) ∎ hunk ./Algebra/Props/DistributiveLattice.agda 35 - ∧-∨-distribˡ x y z = - begin - x ∧ (y ∨ z) - ∼⟨ sym (proj₂ absorptive _ _) ⟨ ∧-pres-≈ ⟩ byDef ⟩ - (x ∧ (x ∨ y)) ∧ (y ∨ z) - ∼⟨ (byDef ⟨ ∧-pres-≈ ⟩ ∨-comm _ _) ⟨ ∧-pres-≈ ⟩ byDef ⟩ - (x ∧ (y ∨ x)) ∧ (y ∨ z) - ∼⟨ sym $ ∧-assoc _ _ _ ⟩ - x ∧ ((y ∨ x) ∧ (y ∨ z)) - ∼⟨ byDef ⟨ ∧-pres-≈ ⟩ sym (proj₁ ∨-∧-distrib _ _ _) ⟩ - x ∧ (y ∨ (x ∧ z)) - ∼⟨ sym (proj₁ absorptive _ _) ⟨ ∧-pres-≈ ⟩ byDef ⟩ - (x ∨ (x ∧ z)) ∧ (y ∨ (x ∧ z)) - ∼⟨ sym $ proj₂ ∨-∧-distrib _ _ _ ⟩ - (x ∧ y) ∨ (x ∧ z) - ∎ + ∧-∨-distribˡ x y z = begin + x ∧ (y ∨ z) ≈⟨ sym (proj₂ absorptive _ _) ⟨ ∧-pres-≈ ⟩ byDef ⟩ + (x ∧ (x ∨ y)) ∧ (y ∨ z) ≈⟨ (byDef ⟨ ∧-pres-≈ ⟩ ∨-comm _ _) ⟨ ∧-pres-≈ ⟩ byDef ⟩ + (x ∧ (y ∨ x)) ∧ (y ∨ z) ≈⟨ sym $ ∧-assoc _ _ _ ⟩ + x ∧ ((y ∨ x) ∧ (y ∨ z)) ≈⟨ byDef ⟨ ∧-pres-≈ ⟩ sym (proj₁ ∨-∧-distrib _ _ _) ⟩ + x ∧ (y ∨ x ∧ z) ≈⟨ sym (proj₁ absorptive _ _) ⟨ ∧-pres-≈ ⟩ byDef ⟩ + (x ∨ x ∧ z) ∧ (y ∨ x ∧ z) ≈⟨ sym $ proj₂ ∨-∧-distrib _ _ _ ⟩ + x ∧ y ∨ x ∧ z ∎ hunk ./Algebra/Props/DistributiveLattice.agda 45 - ∧-∨-distribʳ x y z = - begin - (y ∨ z) ∧ x - ∼⟨ ∧-comm _ _ ⟩ - x ∧ (y ∨ z) - ∼⟨ ∧-∨-distribˡ _ _ _ ⟩ - (x ∧ y) ∨ (x ∧ z) - ∼⟨ ∧-comm _ _ ⟨ ∨-pres-≈ ⟩ ∧-comm _ _ ⟩ - (y ∧ x) ∨ (z ∧ x) - ∎ + ∧-∨-distribʳ x y z = begin + (y ∨ z) ∧ x ≈⟨ ∧-comm _ _ ⟩ + x ∧ (y ∨ z) ≈⟨ ∧-∨-distribˡ _ _ _ ⟩ + x ∧ y ∨ x ∧ z ≈⟨ ∧-comm _ _ ⟨ ∨-pres-≈ ⟩ ∧-comm _ _ ⟩ + y ∧ x ∨ z ∧ x ∎ hunk ./Algebra/Props/DistributiveLattice.agda 53 - ∧-∨-distLattice : DistributiveLattice _∧_ _∨_ - ∧-∨-distLattice = record - { lattice = ∧-∨-lattice + ∧-∨-isDistributiveLattice : IsDistributiveLattice _∧_ _∨_ + ∧-∨-isDistributiveLattice = record + { isLattice = ∧-∨-isLattice hunk ./Algebra/Props/DistributiveLattice.agda 59 +∧-∨-distributiveLattice : DistributiveLattice +∧-∨-distributiveLattice = record + { setoid = setoid + ; _∧_ = _∨_ + ; _∨_ = _∧_ + ; isDistributiveLattice = ∧-∨-isDistributiveLattice + } + hunk ./Algebra/Props/Group.agda 5 -open import Algebra.Packaged +open import Algebra hunk ./Algebra/Props/Group.agda 7 -module Algebra.Props.Group (g : Groupoid) where +module Algebra.Props.Group (g : Group) where hunk ./Algebra/Props/Group.agda 9 -open import Relation.Binary +open Group g +import Relation.Binary.EqReasoning as EqR; open EqR setoid hunk ./Algebra/Props/Group.agda 13 -import Relation.Binary.EqReasoning -import Algebra -open Groupoid g -open Setoid setoid -open Relation.Binary.EqReasoning preorder -open Algebra setoid -open Group group -open Monoid monoid -open Semigroup semigroup - ------------------------------------------------------------------------- --- Some properties hunk ./Algebra/Props/Group.agda 16 - ¬-involutive : forall x -> (- - x) ≈ x - ¬-involutive x = - begin - - - x - ∼⟨ sym $ proj₂ identity _ ⟩ - (- - x) + 0# - ∼⟨ byDef ⟨ •-pres-≈ ⟩ sym (proj₁ inverse _) ⟩ - (- - x) + ((- x) + x) - ∼⟨ assoc _ _ _ ⟩ - ((- - x) + - x) + x - ∼⟨ proj₁ inverse _ ⟨ •-pres-≈ ⟩ byDef ⟩ - 0# + x - ∼⟨ proj₁ identity _ ⟩ - x - ∎ + ⁻¹-involutive : forall x -> x ⁻¹ ⁻¹ ≈ x + ⁻¹-involutive x = begin + x ⁻¹ ⁻¹ ≈⟨ sym $ proj₂ identity _ ⟩ + x ⁻¹ ⁻¹ • ε ≈⟨ byDef ⟨ •-pres-≈ ⟩ sym (proj₁ inverse _) ⟩ + x ⁻¹ ⁻¹ • (x ⁻¹ • x) ≈⟨ assoc _ _ _ ⟩ + x ⁻¹ ⁻¹ • x ⁻¹ • x ≈⟨ proj₁ inverse _ ⟨ •-pres-≈ ⟩ byDef ⟩ + ε • x ≈⟨ proj₁ identity _ ⟩ + x ∎ hunk ./Algebra/Props/Lattice.agda 5 -open import Algebra.Packaged +open import Algebra hunk ./Algebra/Props/Lattice.agda 7 -module Algebra.Props.Lattice (l : Latticoid) where +module Algebra.Props.Lattice (l : Lattice) where hunk ./Algebra/Props/Lattice.agda 9 -open import Relation.Binary +open Lattice l +import Algebra.Structures as S; open S setoid +import Algebra.FunctionProperties as P; open P setoid +import Relation.Binary.EqReasoning as EqR; open EqR setoid hunk ./Algebra/Props/Lattice.agda 15 -import Relation.Binary.EqReasoning -import Algebra -open Latticoid l -open Algebra setoid -open Lattice lattice -open Setoid setoid -open Relation.Binary.EqReasoning preorder hunk ./Algebra/Props/Lattice.agda 18 + ∧-idempotent : Idempotent _∧_ + ∧-idempotent x = begin + x ∧ x ≈⟨ byDef ⟨ ∧-pres-≈ ⟩ sym (proj₁ absorptive _ _) ⟩ + x ∧ (x ∨ x ∧ x) ≈⟨ proj₂ absorptive _ _ ⟩ + x ∎ + + ∨-idempotent : Idempotent _∨_ + ∨-idempotent x = begin + x ∨ x ≈⟨ byDef ⟨ ∨-pres-≈ ⟩ sym (∧-idempotent _) ⟩ + x ∨ x ∧ x ≈⟨ proj₁ absorptive _ _ ⟩ + x ∎ + hunk ./Algebra/Props/Lattice.agda 32 - ∧-∨-lattice : Lattice _∧_ _∨_ - ∧-∨-lattice = record + ∧-∨-isLattice : IsLattice _∧_ _∨_ + ∧-∨-isLattice = record hunk ./Algebra/Props/Lattice.agda 43 - ∧-idempotent : Idempotent _∧_ - ∧-idempotent x = - begin - x ∧ x - ∼⟨ byDef ⟨ ∧-pres-≈ ⟩ sym (proj₁ absorptive _ _) ⟩ - x ∧ (x ∨ (x ∧ x)) - ∼⟨ proj₂ absorptive _ _ ⟩ - x - ∎ - - ∨-idempotent : Idempotent _∨_ - ∨-idempotent x = - begin - x ∨ x - ∼⟨ byDef ⟨ ∨-pres-≈ ⟩ sym (∧-idempotent _) ⟩ - x ∨ (x ∧ x) - ∼⟨ proj₁ absorptive _ _ ⟩ - x - ∎ +∧-∨-lattice : Lattice +∧-∨-lattice = record + { setoid = setoid + ; _∧_ = _∨_ + ; _∨_ = _∧_ + ; isLattice = ∧-∨-isLattice + } hunk ./Algebra/Props/Ring.agda 5 -open import Algebra.Packaged +open import Algebra hunk ./Algebra/Props/Ring.agda 7 -module Algebra.Props.Ring (r : Ringoid) where +module Algebra.Props.Ring (r : Ring) where hunk ./Algebra/Props/Ring.agda 9 -open import Relation.Binary +open Ring r +import Relation.Binary.EqReasoning as EqR; open EqR setoid hunk ./Algebra/Props/Ring.agda 13 -import Relation.Binary.EqReasoning -import Algebra -import Algebra.Props.AbelianGroup -open Ringoid r -open BareRingoid bare -open Setoid setoid -open Relation.Binary.EqReasoning preorder -open Algebra setoid -private - module R = Ring ring - module A = AbelianGroup R.+-group - module A = Group A.group - module A = Monoid A.monoid - module A = Semigroup A.semigroup - module M = Monoid R.*-monoid - module M = Semigroup M.semigroup - ------------------------------------------------------------------------- --- A ring is a semiring - -abstract - zero : Zero 0# _*_ - zero = zeroˡ , zeroʳ - where - zeroˡ : LeftZero 0# _*_ - zeroˡ x = - begin - 0# * x - ∼⟨ sym $ proj₂ A.identity _ ⟩ - (0# * x) + 0# - ∼⟨ byDef ⟨ A.•-pres-≈ ⟩ sym (proj₂ A.inverse _) ⟩ - (0# * x) + ((0# * x) + - (0# * x)) - ∼⟨ A.assoc _ _ _ ⟩ - ((0# * x) + (0# * x)) + - (0# * x) - ∼⟨ sym (proj₂ R.distrib _ _ _) ⟨ A.•-pres-≈ ⟩ byDef ⟩ - ((0# + 0#) * x) + - (0# * x) - ∼⟨ (proj₂ A.identity _ ⟨ M.•-pres-≈ ⟩ byDef) - ⟨ A.•-pres-≈ ⟩ - byDef ⟩ - (0# * x) + - (0# * x) - ∼⟨ proj₂ A.inverse _ ⟩ - 0# - ∎ - - zeroʳ : RightZero 0# _*_ - zeroʳ x = - begin - x * 0# - ∼⟨ sym $ proj₂ A.identity _ ⟩ - (x * 0#) + 0# - ∼⟨ byDef ⟨ A.•-pres-≈ ⟩ sym (proj₂ A.inverse _) ⟩ - (x * 0#) + ((x * 0#) + - (x * 0#)) - ∼⟨ A.assoc _ _ _ ⟩ - ((x * 0#) + (x * 0#)) + - (x * 0#) - ∼⟨ sym (proj₁ R.distrib _ _ _) ⟨ A.•-pres-≈ ⟩ byDef ⟩ - (x * (0# + 0#)) + - (x * 0#) - ∼⟨ (byDef ⟨ M.•-pres-≈ ⟩ proj₂ A.identity _) - ⟨ A.•-pres-≈ ⟩ - byDef ⟩ - (x * 0#) + - (x * 0#) - ∼⟨ proj₂ A.inverse _ ⟩ - 0# - ∎ - - semiring : Semiring _+_ _*_ 0# 1# - semiring = record - { +-monoid = record - { monoid = A.monoid - ; comm = A.comm - } - ; *-monoid = R.*-monoid - ; distrib = R.distrib - ; zero = zero - } - -semiringoid : Semiringoid -semiringoid = record - { setoid = setoid - ; _+_ = _+_ - ; _*_ = _*_ - ; 0# = 0# - ; 1# = 1# - ; semiring = semiring - } - ------------------------------------------------------------------------- --- (+, -_, 0#) is an abelian group - -abelianGroupoid : AbelianGroupoid -abelianGroupoid = record - { setoid = setoid - ; _+_ = _+_ - ; -_ = -_ - ; 0# = 0# - ; abelianGroup = R.+-group - } - -open Algebra.Props.AbelianGroup abelianGroupoid public - ------------------------------------------------------------------------- --- Some properties hunk ./Algebra/Props/Ring.agda 16 - ¬-*-distribˡ : forall x y -> ((- x) * y) ≈ (- (x * y)) - ¬-*-distribˡ x y = - begin - (- x) * y - ∼⟨ sym $ proj₂ A.identity _ ⟩ - ((- x) * y) + 0# - ∼⟨ byDef ⟨ A.•-pres-≈ ⟩ sym (proj₂ A.inverse _) ⟩ - ((- x) * y) + ((x * y) + - (x * y)) - ∼⟨ A.assoc _ _ _ ⟩ - (((- x) * y) + (x * y)) + - (x * y) - ∼⟨ sym (proj₂ R.distrib _ _ _) ⟨ A.•-pres-≈ ⟩ byDef ⟩ - (((- x) + x) * y) + - (x * y) - ∼⟨ (proj₁ A.inverse _ ⟨ M.•-pres-≈ ⟩ byDef) - ⟨ A.•-pres-≈ ⟩ - byDef ⟩ - (0# * y) + - (x * y) - ∼⟨ proj₁ zero _ ⟨ A.•-pres-≈ ⟩ byDef ⟩ - 0# + - (x * y) - ∼⟨ proj₁ A.identity _ ⟩ - - (x * y) - ∎ + --*-distribˡ : forall x y -> - x * y ≈ - (x * y) + --*-distribˡ x y = begin + - x * y ≈⟨ sym $ proj₂ +-identity _ ⟩ + - x * y + 0# ≈⟨ byDef ⟨ +-pres-≈ ⟩ sym (proj₂ --inverse _) ⟩ + - x * y + (x * y + - (x * y)) ≈⟨ +-assoc _ _ _ ⟩ + - x * y + x * y + - (x * y) ≈⟨ sym (proj₂ distrib _ _ _) ⟨ +-pres-≈ ⟩ byDef ⟩ + (- x + x) * y + - (x * y) ≈⟨ (proj₁ --inverse _ ⟨ *-pres-≈ ⟩ byDef) + ⟨ +-pres-≈ ⟩ + byDef ⟩ + 0# * y + - (x * y) ≈⟨ proj₁ zero _ ⟨ +-pres-≈ ⟩ byDef ⟩ + 0# + - (x * y) ≈⟨ proj₁ +-identity _ ⟩ + - (x * y) ∎ hunk ./Algebra/Props/Ring.agda 29 - ¬-*-distribʳ : forall x y -> (x * (- y)) ≈ (- (x * y)) - ¬-*-distribʳ x y = - begin - x * (- y) - ∼⟨ sym $ proj₁ A.identity _ ⟩ - 0# + (x * (- y)) - ∼⟨ sym (proj₁ A.inverse _) ⟨ A.•-pres-≈ ⟩ byDef ⟩ - (- (x * y) + (x * y)) + (x * (- y)) - ∼⟨ sym $ A.assoc _ _ _ ⟩ - - (x * y) + ((x * y) + (x * (- y))) - ∼⟨ byDef ⟨ A.•-pres-≈ ⟩ sym (proj₁ R.distrib _ _ _) ⟩ - - (x * y) + (x * (y + - y)) - ∼⟨ byDef ⟨ A.•-pres-≈ ⟩ (byDef ⟨ M.•-pres-≈ ⟩ proj₂ A.inverse _) ⟩ - - (x * y) + (x * 0#) - ∼⟨ byDef ⟨ A.•-pres-≈ ⟩ proj₂ zero _ ⟩ - - (x * y) + 0# - ∼⟨ proj₂ A.identity _ ⟩ - - (x * y) - ∎ + --*-distribʳ : forall x y -> x * - y ≈ - (x * y) + --*-distribʳ x y = begin + x * - y ≈⟨ sym $ proj₁ +-identity _ ⟩ + 0# + x * - y ≈⟨ sym (proj₁ --inverse _) ⟨ +-pres-≈ ⟩ byDef ⟩ + - (x * y) + x * y + x * - y ≈⟨ sym $ +-assoc _ _ _ ⟩ + - (x * y) + (x * y + x * - y) ≈⟨ byDef ⟨ +-pres-≈ ⟩ sym (proj₁ distrib _ _ _) ⟩ + - (x * y) + x * (y + - y) ≈⟨ byDef ⟨ +-pres-≈ ⟩ (byDef ⟨ *-pres-≈ ⟩ proj₂ --inverse _) ⟩ + - (x * y) + x * 0# ≈⟨ byDef ⟨ +-pres-≈ ⟩ proj₂ zero _ ⟩ + - (x * y) + 0# ≈⟨ proj₂ +-identity _ ⟩ + - (x * y) ∎ hunk ./Algebra/Props/Semiring.agda 1 ------------------------------------------------------------------------- --- Some derivable properties ------------------------------------------------------------------------- - -open import Algebra.Packaged - -module Algebra.Props.Semiring (r : Semiringoid) where - -open import Data.Function -open Semiringoid r - ------------------------------------------------------------------------- --- A semiring is a bare ring (using identity as the "almost negation") - -bareRingoid : BareRingoid -bareRingoid = record - { setoid = setoid - ; _+_ = _+_ - ; _*_ = _*_ - ; -_ = id - ; 0# = 0# - ; 1# = 1# - } rmfile ./Algebra/Props/Semiring.agda hunk ./Algebra/RingSolver.agda 9 -open import Algebra.Packaged +open import Algebra +open import Algebra.RingSolver.AlmostCommutativeRing hunk ./Algebra/RingSolver.agda 13 - (coeff : BareRingoid) -- Coefficient "ring". - (r : AlmostCommRingoid) -- Main "ring". - (morphism : coeff -Bare-AlmostComm⟶ r) + (coeff : RawRing) -- Coefficient "ring". + (r : AlmostCommutativeRing) -- Main "ring". + (morphism : coeff -Raw-AlmostCommutative⟶ r) hunk ./Algebra/RingSolver.agda 18 -open import Relation.Binary +import Algebra.RingSolver.Lemmas as L; open L coeff r morphism +private module C = RawRing coeff +open AlmostCommutativeRing r hiding (zero) +import Algebra.FunctionProperties as P; open P setoid +open import Algebra.Morphism +open _-RawRing⟶_ morphism renaming (⟦_⟧ to ⟦_⟧') +import Algebra.Operations as Ops; open Ops semiring + hunk ./Algebra/RingSolver.agda 27 -open import Data.Nat hiding (_*_) renaming (_+_ to _ℕ-+_) -open import Data.Function hiding (const) -open import Data.Product -import Relation.Binary.EqReasoning -import Algebra -import Algebra.Morphism as Morphism -import Algebra.Operations -import Algebra.Props.AlmostCommRing -import Algebra.RingSolver.Lemmas -open Algebra.RingSolver.Lemmas coeff r morphism -open AlmostCommRingoid r -open BareRingoid bare -open Algebra.Props.AlmostCommRing r -open Setoid setoid -open Algebra setoid -open AlmostCommRing almostCommRing -open CommutativeSemiring commSemiring -private - module I = Semiring semiring - module A = Monoid (CommutativeMonoid.monoid I.+-monoid) - module A = Semigroup A.semigroup - module M = Semigroup (Monoid.semigroup I.*-monoid) -open Algebra.Operations semiringoid -private - module C = BareRingoid coeff - module C = Setoid C.setoid -open Morphism C.setoid setoid -open RingHomomorphism morphism renaming (⟦_⟧ to ⟦_⟧') -open Relation.Binary.EqReasoning preorder -open import Data.Vec.Core +open import Relation.Binary + +open import Data.Nat using (ℕ; suc; zero) renaming (_+_ to _ℕ-+_) hunk ./Algebra/RingSolver.agda 31 +open import Data.Vec.Core +open import Data.Function hunk ./Algebra/RingSolver.agda 34 -infix 9 _↑-NF :-_ ¬-NF_ +infix 9 _↑-NF :-_ --NF_ hunk ./Algebra/RingSolver.agda 132 - (p₁ ∷-NF eq₁) +-NF (p₂ ∷-NF eq₂) = p₁ +-NF p₂ ∷-NF eq₁ ⟨ A.•-pres-≈ ⟩ eq₂ - (p₁ ∷-NF eq) +-NF p₂ = p₁ +-NF p₂ ∷-NF eq ⟨ A.•-pres-≈ ⟩ byDef - p₁ +-NF (p₂ ∷-NF eq) = p₁ +-NF p₂ ∷-NF byDef ⟨ A.•-pres-≈ ⟩ eq + (p₁ ∷-NF eq₁) +-NF (p₂ ∷-NF eq₂) = p₁ +-NF p₂ ∷-NF eq₁ ⟨ +-pres-≈ ⟩ eq₂ + (p₁ ∷-NF eq) +-NF p₂ = p₁ +-NF p₂ ∷-NF eq ⟨ +-pres-≈ ⟩ refl + p₁ +-NF (p₂ ∷-NF eq) = p₁ +-NF p₂ ∷-NF refl ⟨ +-pres-≈ ⟩ eq hunk ./Algebra/RingSolver.agda 136 - p₁ ↑-NF +-NF p₂ ↑-NF = (p₁ +-NF p₂) ↑-NF ∷-NF byDef - p₁ *x+ c₁ +-NF p₂ ↑-NF = p₁ *x+ (c₁ +-NF p₂) ∷-NF A.assoc _ _ _ + p₁ ↑-NF +-NF p₂ ↑-NF = (p₁ +-NF p₂) ↑-NF ∷-NF refl + p₁ *x+ c₁ +-NF p₂ ↑-NF = p₁ *x+ (c₁ +-NF p₂) ∷-NF +-assoc _ _ _ hunk ./Algebra/RingSolver.agda 154 - (p₁ ∷-NF eq) *-NF-↑ p₂ = p₁ *-NF-↑ p₂ ∷-NF eq ⟨ M.•-pres-≈ ⟩ byDef - p₁ ↑-NF *-NF-↑ p₂ = (p₁ *-NF p₂) ↑-NF ∷-NF byDef + (p₁ ∷-NF eq) *-NF-↑ p₂ = p₁ *-NF-↑ p₂ ∷-NF eq ⟨ *-pres-≈ ⟩ refl + p₁ ↑-NF *-NF-↑ p₂ = (p₁ *-NF p₂) ↑-NF ∷-NF refl hunk ./Algebra/RingSolver.agda 162 - p₁ ↑-*-NF (p₂ ∷-NF eq) = p₁ ↑-*-NF p₂ ∷-NF byDef ⟨ M.•-pres-≈ ⟩ eq - p₁ ↑-*-NF p₂ ↑-NF = (p₁ *-NF p₂) ↑-NF ∷-NF byDef + p₁ ↑-*-NF (p₂ ∷-NF eq) = p₁ ↑-*-NF p₂ ∷-NF refl ⟨ *-pres-≈ ⟩ eq + p₁ ↑-*-NF p₂ ↑-NF = (p₁ *-NF p₂) ↑-NF ∷-NF refl hunk ./Algebra/RingSolver.agda 170 - (p₁ ∷-NF eq₁) *-NF (p₂ ∷-NF eq₂) = p₁ *-NF p₂ ∷-NF eq₁ ⟨ M.•-pres-≈ ⟩ eq₂ - (p₁ ∷-NF eq) *-NF p₂ = p₁ *-NF p₂ ∷-NF eq ⟨ M.•-pres-≈ ⟩ byDef - p₁ *-NF (p₂ ∷-NF eq) = p₁ *-NF p₂ ∷-NF byDef ⟨ M.•-pres-≈ ⟩ eq + (p₁ ∷-NF eq₁) *-NF (p₂ ∷-NF eq₂) = p₁ *-NF p₂ ∷-NF eq₁ ⟨ *-pres-≈ ⟩ eq₂ + (p₁ ∷-NF eq) *-NF p₂ = p₁ *-NF p₂ ∷-NF eq ⟨ *-pres-≈ ⟩ refl + p₁ *-NF (p₂ ∷-NF eq) = p₁ *-NF p₂ ∷-NF refl ⟨ *-pres-≈ ⟩ eq hunk ./Algebra/RingSolver.agda 174 - p₁ ↑-NF *-NF p₂ ↑-NF = (p₁ *-NF p₂) ↑-NF ∷-NF byDef + p₁ ↑-NF *-NF p₂ ↑-NF = (p₁ *-NF p₂) ↑-NF ∷-NF refl hunk ./Algebra/RingSolver.agda 181 - ¬-NF_ : forall {n p} -> Normal n p -> Normal n (:- p) - ¬-NF_ (p ∷-NF eq) = ¬-NF_ p ∷-NF ¬-pres-≈ eq - ¬-NF_ (con-NF c) = con-NF (C.-_ c) ∷-NF ¬-homo _ - ¬-NF_ (p ↑-NF) = ¬-NF_ p ↑-NF - ¬-NF_ (p *x+ c) = ¬-NF_ p *x+ ¬-NF_ c ∷-NF lemma₆ _ _ _ + --NF_ : forall {n p} -> Normal n p -> Normal n (:- p) + --NF_ (p ∷-NF eq) = --NF_ p ∷-NF --pres-≈ eq + --NF_ (con-NF c) = con-NF (C.-_ c) ∷-NF --homo _ + --NF_ (p ↑-NF) = --NF_ p ↑-NF + --NF_ (p *x+ c) = --NF_ p *x+ --NF_ c ∷-NF lemma₆ _ _ _ hunk ./Algebra/RingSolver.agda 193 - p ^-NF suc n = p *-NF p ^-NF n ∷-NF byDef + p ^-NF suc n = p *-NF p ^-NF n ∷-NF refl hunk ./Algebra/RingSolver.agda 207 - normalise (:- p) = ¬-NF normalise p + normalise (:- p) = --NF normalise p hunk ./Algebra/RingSolver.agda 217 - sem-pres-≈ : forall op -> sem op Preserves₂-≈ - sem-pres-≈ [+] = A.•-pres-≈ - sem-pres-≈ [*] = M.•-pres-≈ + sem-pres-≈ : forall op -> sem op Preserves₂ _≈_ → _≈_ → _≈_ + sem-pres-≈ [+] = +-pres-≈ + sem-pres-≈ [*] = *-pres-≈ hunk ./Algebra/RingSolver.agda 225 - raise-sem (con c) ρ = byDef - raise-sem (var x) ρ = byDef + raise-sem (con c) ρ = refl + raise-sem (var x) ρ = refl hunk ./Algebra/RingSolver.agda 228 - raise-sem (:- p) ρ = ¬-pres-≈ (raise-sem p ρ) + raise-sem (:- p) ρ = --pres-≈ (raise-sem p ρ) hunk ./Algebra/RingSolver.agda 233 - nf-sound (con-NF c) ρ = byDef + nf-sound (con-NF c) ρ = refl hunk ./Algebra/RingSolver.agda 237 - (nf-sound nf₁ (x ∷ ρ) ⟨ M.•-pres-≈ ⟩ byDef) - ⟨ A.•-pres-≈ ⟩ + (nf-sound nf₁ (x ∷ ρ) ⟨ *-pres-≈ ⟩ refl) + ⟨ +-pres-≈ ⟩ addfile ./Algebra/RingSolver/AlmostCommutativeRing.agda hunk ./Algebra/RingSolver/AlmostCommutativeRing.agda 1 +------------------------------------------------------------------------ +-- Commutative semirings with some additional structure ("almost" +-- commutative rings), used by the ring solver +------------------------------------------------------------------------ + +module Algebra.RingSolver.AlmostCommutativeRing where + +open import Relation.Binary +open import Algebra +open import Algebra.Structures +import Algebra.FunctionProperties as P +open import Algebra.Morphism +open import Data.Function + +------------------------------------------------------------------------ +-- Definitions + +record IsAlmostCommutativeRing (s : Setoid) + (_+_ _*_ : P.Op₂ s) + (-_ : P.Op₁ s) + (0# 1# : Setoid.carrier s) : Set where + open Setoid s + field + isCommutativeSemiring : IsCommutativeSemiring s _+_ _*_ 0# 1# + --pres-≈ : -_ Preserves _≈_ → _≈_ + --*-distribˡ : forall x y -> (- x) * y ≈ - (x * y) + --+-comm : forall x y -> (- x) + (- y) ≈ - (x + y) + + open IsCommutativeSemiring s isCommutativeSemiring public + +record AlmostCommutativeRing : Set1 where + infix 8 -_ + infixl 7 _*_ + infixl 6 _+_ + field + setoid : Setoid + _+_ : P.Op₂ setoid + _*_ : P.Op₂ setoid + -_ : P.Op₁ setoid + 0# : Setoid.carrier setoid + 1# : Setoid.carrier setoid + isAlmostCommutativeRing : + IsAlmostCommutativeRing setoid _+_ _*_ -_ 0# 1# + + open Setoid setoid public + open IsAlmostCommutativeRing isAlmostCommutativeRing public + + commutativeSemiring : CommutativeSemiring + commutativeSemiring = record + { setoid = setoid + ; _+_ = _+_ + ; _*_ = _*_ + ; 0# = 0# + ; 1# = 1# + ; isCommutativeSemiring = isCommutativeSemiring + } + + open CommutativeSemiring commutativeSemiring public + using ( +-semigroup; +-monoid; +-commutativeMonoid + ; *-semigroup; *-monoid; *-commutativeMonoid + ; semiring + ) + + rawRing : RawRing + rawRing = record + { setoid = setoid + ; _+_ = _+_ + ; _*_ = _*_ + ; -_ = -_ + ; 0# = 0# + ; 1# = 1# + } + +------------------------------------------------------------------------ +-- Homomorphisms + +_-Raw-AlmostCommutative⟶_ : RawRing -> AlmostCommutativeRing -> Set +from -Raw-AlmostCommutative⟶ to = from -RawRing⟶ rawRing to + where open AlmostCommutativeRing + +-raw-almostCommutative⟶ + : forall r -> + AlmostCommutativeRing.rawRing r -Raw-AlmostCommutative⟶ r +-raw-almostCommutative⟶ r = record + { ⟦_⟧ = id + ; +-homo = \_ _ -> refl + ; *-homo = \_ _ -> refl + ; --homo = \_ -> refl + ; 0-homo = refl + ; 1-homo = refl + } + where open AlmostCommutativeRing r + +------------------------------------------------------------------------ +-- Conversions + +-- Commutative rings are almost commutative rings. + +fromCommutativeRing : CommutativeRing -> AlmostCommutativeRing +fromCommutativeRing cr = record + { setoid = setoid + ; _+_ = _+_ + ; _*_ = _*_ + ; -_ = -_ + ; 0# = 0# + ; 1# = 1# + ; isAlmostCommutativeRing = record + { isCommutativeSemiring = isCommutativeSemiring + ; --pres-≈ = --pres-≈ + ; --*-distribˡ = --*-distribˡ + ; --+-comm = --•-comm + } + } + where + open CommutativeRing cr + import Algebra.Props.Ring as R; open R ring + import Algebra.Props.AbelianGroup as AG; open AG +-abelianGroup + +-- Commutative semirings can be viewed as almost commutative rings by +-- using identity as the "almost negation". + +fromCommutativeSemiring : CommutativeSemiring -> AlmostCommutativeRing +fromCommutativeSemiring cs = record + { setoid = setoid + ; _+_ = _+_ + ; _*_ = _*_ + ; -_ = id + ; 0# = 0# + ; 1# = 1# + ; isAlmostCommutativeRing = record + { isCommutativeSemiring = isCommutativeSemiring + ; --pres-≈ = id + ; --*-distribˡ = \_ _ -> refl + ; --+-comm = \_ _ -> refl + } + } + where open CommutativeSemiring cs hunk ./Algebra/RingSolver/Examples.agda 8 -open import Data.Function hunk ./Algebra/RingSolver/Examples.agda 14 -import Algebra.Operations as Op -import Algebra.RingSolver as S -import Algebra.Props.CommutativeSemiring as CSProp -import Algebra.Props.CommutativeRing as CRProp -import Algebra.Props.AlmostCommRing as ACRProp -open Op (CSProp.semiringoid ℕ-commSemiringoid) using (_^_) -open Op (CRProp.semiringoid Bool-commRingoid-xor-∧) +open import Algebra +import Algebra.Operations as Ops +open Ops (CommutativeSemiring.semiring ℕ-commutativeSemiring) + using (_^_) +open Ops (CommutativeRing.semiring Bool-commutativeRing-xor-∧) hunk ./Algebra/RingSolver/Examples.agda 37 - example₂ - : forall x y - -> (x xor y) ↑ 3 ≡ x ↑ 3 xor x ↑ 2 ∧ y xor x ∧ y ↑ 2 xor y ↑ 3 - example₂ x y = - prove (x ∷ y ∷ []) - ((X :+ Y) :^ 3) - (X :^ 3 :+ (X :^ 2 :* Y :+ (X :* Y :^ 2 :+ Y :^ 3))) - ≡-refl - where - open Bool-xor-ringSolver - X = var fz - Y = var (fs fz) + -- The following example is commented out because it is (currently) + -- too slow. + + -- example₂ + -- : forall x y + -- -> (x xor y) ↑ 3 ≡ + -- (x ↑ 3) xor ((x ↑ 2) ∧ y) xor (x ∧ (y ↑ 2)) xor (y ↑ 3) + -- example₂ x y = + -- prove (x ∷ y ∷ []) + -- ((X :+ Y) :^ 3) + -- (X :^ 3 :+ (X :^ 2 :* Y :+ (X :* Y :^ 2 :+ Y :^ 3))) + -- ≡-refl + -- where + -- open Bool-xor-ringSolver + -- X = var fz + -- Y = var (fs fz) hunk ./Algebra/RingSolver/Lemmas.agda 8 -open import Algebra.Packaged +open import Algebra +open import Algebra.RingSolver.AlmostCommutativeRing hunk ./Algebra/RingSolver/Lemmas.agda 12 - (coeff : BareRingoid) - (r : AlmostCommRingoid) - (morphism : coeff -Bare-AlmostComm⟶ r) + (coeff : RawRing) + (r : AlmostCommutativeRing) + (morphism : coeff -Raw-AlmostCommutative⟶ r) hunk ./Algebra/RingSolver/Lemmas.agda 17 -open import Relation.Binary +private + module C = RawRing coeff +open AlmostCommutativeRing r +open import Algebra.Morphism +open _-RawRing⟶_ morphism +import Relation.Binary.EqReasoning as EqR; open EqR setoid hunk ./Algebra/RingSolver/Lemmas.agda 25 -import Relation.Binary.EqReasoning -import Algebra -import Algebra.Morphism as Morphism -open AlmostCommRingoid r -open BareRingoid bare -open Setoid setoid -open Relation.Binary.EqReasoning preorder -open Algebra setoid -open AlmostCommRing almostCommRing -open CommutativeSemiring commSemiring -open Semiring semiring -private - module A = CommutativeMonoid +-monoid - module A = Monoid A.monoid - module A = Semigroup A.semigroup - module M = Monoid *-monoid - module M = Semigroup M.semigroup - module C = BareRingoid coeff - module C = Setoid C.setoid -open Morphism C.setoid setoid -open RingHomomorphism morphism hunk ./Algebra/RingSolver/Lemmas.agda 28 - lemma₀ : forall x -> (x + ⟦ C.0# ⟧) ≈ x - lemma₀ x = - begin - x + ⟦ C.0# ⟧ - ∼⟨ byDef ⟨ A.•-pres-≈ ⟩ 0-homo ⟩ - x + 0# - ∼⟨ proj₂ A.identity _ ⟩ - x - ∎ + lemma₀ : forall x -> x + ⟦ C.0# ⟧ ≈ x + lemma₀ x = begin + x + ⟦ C.0# ⟧ ≈⟨ byDef ⟨ +-pres-≈ ⟩ 0-homo ⟩ + x + 0# ≈⟨ proj₂ +-identity _ ⟩ + x ∎ hunk ./Algebra/RingSolver/Lemmas.agda 35 - -> (((a + b) * x) + (c + d)) ≈ (((a * x) + c) + ((b * x) + d)) - lemma₁ a b c d x = - begin - ((a + b) * x) + (c + d) - ∼⟨ proj₂ distrib _ _ _ ⟨ A.•-pres-≈ ⟩ byDef ⟩ - ((a * x) + (b * x)) + (c + d) - ∼⟨ sym $ A.assoc _ _ _ ⟩ - (a * x) + ((b * x) + (c + d)) - ∼⟨ byDef ⟨ A.•-pres-≈ ⟩ A.assoc _ _ _ ⟩ - (a * x) + (((b * x) + c) + d) - ∼⟨ byDef ⟨ A.•-pres-≈ ⟩ (A.comm _ _ ⟨ A.•-pres-≈ ⟩ byDef) ⟩ - (a * x) + ((c + (b * x)) + d) - ∼⟨ byDef ⟨ A.•-pres-≈ ⟩ sym (A.assoc _ _ _) ⟩ - (a * x) + (c + ((b * x) + d)) - ∼⟨ A.assoc _ _ _ ⟩ - ((a * x) + c) + ((b * x) + d) - ∎ + -> (a + b) * x + (c + d) ≈ (a * x + c) + (b * x + d) + lemma₁ a b c d x = begin + (a + b) * x + (c + d) ≈⟨ proj₂ distrib _ _ _ ⟨ +-pres-≈ ⟩ byDef ⟩ + (a * x + b * x) + (c + d) ≈⟨ sym $ +-assoc _ _ _ ⟩ + a * x + (b * x + (c + d)) ≈⟨ byDef ⟨ +-pres-≈ ⟩ +-assoc _ _ _ ⟩ + a * x + ((b * x + c) + d) ≈⟨ byDef ⟨ +-pres-≈ ⟩ (+-comm _ _ ⟨ +-pres-≈ ⟩ byDef) ⟩ + a * x + ((c + b * x) + d) ≈⟨ byDef ⟨ +-pres-≈ ⟩ sym (+-assoc _ _ _) ⟩ + a * x + (c + (b * x + d)) ≈⟨ +-assoc _ _ _ ⟩ + (a * x + c) + (b * x + d) ∎ hunk ./Algebra/RingSolver/Lemmas.agda 45 - lemma₂ : forall x y z -> (x + (y + z)) ≈ (y + (x + z)) - lemma₂ x y z = - begin - x + (y + z) - ∼⟨ A.assoc _ _ _ ⟩ - (x + y) + z - ∼⟨ A.comm _ _ ⟨ A.•-pres-≈ ⟩ byDef ⟩ - (y + x) + z - ∼⟨ sym $ A.assoc _ _ _ ⟩ - y + (x + z) - ∎ + lemma₂ : forall x y z -> x + (y + z) ≈ y + (x + z) + lemma₂ x y z = begin + x + (y + z) ≈⟨ +-assoc _ _ _ ⟩ + (x + y) + z ≈⟨ +-comm _ _ ⟨ +-pres-≈ ⟩ byDef ⟩ + (y + x) + z ≈⟨ sym $ +-assoc _ _ _ ⟩ + y + (x + z) ∎ hunk ./Algebra/RingSolver/Lemmas.agda 53 - -> (((a * c) * x) + (b * c)) ≈ (((a * x) + b) * c) - lemma₃ a b c x = - begin - ((a * c) * x) + (b * c) - ∼⟨ lem ⟨ A.•-pres-≈ ⟩ byDef ⟩ - ((a * x) * c) + (b * c) - ∼⟨ sym $ proj₂ distrib _ _ _ ⟩ - ((a * x) + b) * c - ∎ + -> a * c * x + b * c ≈ (a * x + b) * c + lemma₃ a b c x = begin + a * c * x + b * c ≈⟨ lem ⟨ +-pres-≈ ⟩ byDef ⟩ + a * x * c + b * c ≈⟨ sym $ proj₂ distrib _ _ _ ⟩ + (a * x + b) * c ∎ hunk ./Algebra/RingSolver/Lemmas.agda 59 - lem = - begin - (a * c) * x - ∼⟨ sym (M.assoc _ _ _) ⟩ - a * (c * x) - ∼⟨ byDef ⟨ M.•-pres-≈ ⟩ *-comm _ _ ⟩ - a * (x * c) - ∼⟨ M.assoc _ _ _ ⟩ - (a * x) * c - ∎ + lem = begin + a * c * x ≈⟨ sym (*-assoc _ _ _) ⟩ + a * (c * x) ≈⟨ byDef ⟨ *-pres-≈ ⟩ *-comm _ _ ⟩ + a * (x * c) ≈⟨ *-assoc _ _ _ ⟩ + a * x * c ∎ hunk ./Algebra/RingSolver/Lemmas.agda 66 - -> (((a * b) * x) + (a * c)) ≈ (a * ((b * x) + c)) - lemma₄ a b c x = - begin - ((a * b) * x) + (a * c) - ∼⟨ sym (M.assoc _ _ _) - ⟨ A.•-pres-≈ ⟩ - byDef ⟩ - (a * (b * x)) + (a * c) - ∼⟨ sym $ proj₁ distrib _ _ _ ⟩ - a * ((b * x) + c) - ∎ + -> a * b * x + a * c ≈ a * (b * x + c) + lemma₄ a b c x = begin + a * b * x + a * c ≈⟨ sym (*-assoc _ _ _) + ⟨ +-pres-≈ ⟩ + byDef ⟩ + a * (b * x) + a * c ≈⟨ sym $ proj₁ distrib _ _ _ ⟩ + a * (b * x + c) ∎ hunk ./Algebra/RingSolver/Lemmas.agda 75 - -> ((((a * c) * x) * x) + - ((((a * d) + (b * c)) * x) + (b * d))) ≈ - (((a * x) + b) * ((c * x) + d)) - lemma₅ a b c d x = - begin - (((a * c) * x) * x) + - ((((a * d) + (b * c)) * x) + (b * d)) - ∼⟨ lem₁ ⟨ A.•-pres-≈ ⟩ - (lem₂ ⟨ A.•-pres-≈ ⟩ byDef) ⟩ - ((a * x) * (c * x)) + - ((((a * x) * d) + (b * (c * x))) + - (b * d)) - ∼⟨ byDef ⟨ A.•-pres-≈ ⟩ sym (A.assoc _ _ _) ⟩ - ((a * x) * (c * x)) + - (((a * x) * d) + - ((b * (c * x)) + (b * d))) - ∼⟨ A.assoc _ _ _ ⟩ - (((a * x) * (c * x)) + ((a * x) * d)) + - ((b * (c * x)) + (b * d)) - ∼⟨ sym $ proj₁ distrib _ _ _ - ⟨ A.•-pres-≈ ⟩ - proj₁ distrib _ _ _ ⟩ - ((a * x) * ((c * x) + d)) + - (b * ((c * x) + d)) - ∼⟨ sym $ proj₂ distrib _ _ _ ⟩ - ((a * x) + b) * ((c * x) + d) - ∎ + -> a * c * x * x + ((a * d + b * c) * x + b * d) ≈ + (a * x + b) * (c * x + d) + lemma₅ a b c d x = begin + a * c * x * x + + ((a * d + b * c) * x + b * d) ≈⟨ lem₁ ⟨ +-pres-≈ ⟩ + (lem₂ ⟨ +-pres-≈ ⟩ byDef) ⟩ + a * x * (c * x) + + (a * x * d + b * (c * x) + b * d) ≈⟨ byDef ⟨ +-pres-≈ ⟩ sym (+-assoc _ _ _) ⟩ + a * x * (c * x) + + (a * x * d + (b * (c * x) + b * d)) ≈⟨ +-assoc _ _ _ ⟩ + a * x * (c * x) + a * x * d + + (b * (c * x) + b * d) ≈⟨ sym $ proj₁ distrib _ _ _ + ⟨ +-pres-≈ ⟩ + proj₁ distrib _ _ _ ⟩ + a * x * (c * x + d) + b * (c * x + d) ≈⟨ sym $ proj₂ distrib _ _ _ ⟩ + (a * x + b) * (c * x + d) ∎ hunk ./Algebra/RingSolver/Lemmas.agda 92 - lem₁' = - begin - (a * c) * x - ∼⟨ sym $ M.assoc _ _ _ ⟩ - a * (c * x) - ∼⟨ byDef ⟨ M.•-pres-≈ ⟩ *-comm _ _ ⟩ - a * (x * c) - ∼⟨ M.assoc _ _ _ ⟩ - (a * x) * c - ∎ + lem₁' = begin + a * c * x ≈⟨ sym $ *-assoc _ _ _ ⟩ + a * (c * x) ≈⟨ byDef ⟨ *-pres-≈ ⟩ *-comm _ _ ⟩ + a * (x * c) ≈⟨ *-assoc _ _ _ ⟩ + a * x * c ∎ hunk ./Algebra/RingSolver/Lemmas.agda 98 - lem₁ = - begin - ((a * c) * x) * x - ∼⟨ lem₁' ⟨ M.•-pres-≈ ⟩ byDef ⟩ - ((a * x) * c) * x - ∼⟨ sym $ M.assoc _ _ _ ⟩ - (a * x) * (c * x) - ∎ + lem₁ = begin + a * c * x * x ≈⟨ lem₁' ⟨ *-pres-≈ ⟩ byDef ⟩ + a * x * c * x ≈⟨ sym $ *-assoc _ _ _ ⟩ + a * x * (c * x) ∎ hunk ./Algebra/RingSolver/Lemmas.agda 103 - lem₂ = - begin - ((a * d) + (b * c)) * x - ∼⟨ proj₂ distrib _ _ _ ⟩ - ((a * d) * x) + ((b * c) * x) - ∼⟨ sym $ M.assoc _ _ _ ⟨ A.•-pres-≈ ⟩ M.assoc _ _ _ ⟩ - (a * (d * x)) + (b * (c * x)) - ∼⟨ (byDef ⟨ M.•-pres-≈ ⟩ *-comm _ _) - ⟨ A.•-pres-≈ ⟩ byDef ⟩ - (a * (x * d)) + (b * (c * x)) - ∼⟨ M.assoc _ _ _ ⟨ A.•-pres-≈ ⟩ byDef ⟩ - ((a * x) * d) + (b * (c * x)) - ∎ + lem₂ = begin + (a * d + b * c) * x ≈⟨ proj₂ distrib _ _ _ ⟩ + a * d * x + b * c * x ≈⟨ sym $ *-assoc _ _ _ ⟨ +-pres-≈ ⟩ *-assoc _ _ _ ⟩ + a * (d * x) + b * (c * x) ≈⟨ (byDef ⟨ *-pres-≈ ⟩ *-comm _ _) + ⟨ +-pres-≈ ⟩ byDef ⟩ + a * (x * d) + b * (c * x) ≈⟨ *-assoc _ _ _ ⟨ +-pres-≈ ⟩ byDef ⟩ + a * x * d + b * (c * x) ∎ hunk ./Algebra/RingSolver/Lemmas.agda 111 - lemma₆ : forall a b x -> (((- a) * x) + (- b)) ≈ (- ((a * x) + b)) - lemma₆ a b x = - begin - ((- a) * x) + (- b) - ∼⟨ ¬-*-distribˡ _ _ ⟨ A.•-pres-≈ ⟩ byDef ⟩ - (- (a * x)) + (- b) - ∼⟨ ¬-+-comm _ _ ⟩ - - ((a * x) + b) - ∎ + lemma₆ : forall a b x -> - a * x + - b ≈ - (a * x + b) + lemma₆ a b x = begin + - a * x + - b ≈⟨ --*-distribˡ _ _ ⟨ +-pres-≈ ⟩ byDef ⟩ + - (a * x) + - b ≈⟨ --+-comm _ _ ⟩ + - (a * x + b) ∎ hunk ./Algebra/RingSolver/Lemmas.agda 117 - lemma₇ : forall x -> ((⟦ C.1# ⟧ * x) + ⟦ C.0# ⟧) ≈ x - lemma₇ x = - begin - ((⟦ C.1# ⟧ * x) + ⟦ C.0# ⟧) - ∼⟨ (1-homo ⟨ M.•-pres-≈ ⟩ byDef) ⟨ A.•-pres-≈ ⟩ 0-homo ⟩ - (1# * x) + 0# - ∼⟨ proj₂ A.identity _ ⟩ - 1# * x - ∼⟨ proj₁ M.identity _ ⟩ - x - ∎ + lemma₇ : forall x -> ⟦ C.1# ⟧ * x + ⟦ C.0# ⟧ ≈ x + lemma₇ x = begin + ⟦ C.1# ⟧ * x + ⟦ C.0# ⟧ ≈⟨ (1-homo ⟨ *-pres-≈ ⟩ byDef) ⟨ +-pres-≈ ⟩ 0-homo ⟩ + 1# * x + 0# ≈⟨ proj₂ +-identity _ ⟩ + 1# * x ≈⟨ proj₁ *-identity _ ⟩ + x ∎ hunk ./Algebra/RingSolver/Simple.agda 5 -open import Algebra.Packaged +open import Algebra.RingSolver.AlmostCommutativeRing hunk ./Algebra/RingSolver/Simple.agda 7 -module Algebra.RingSolver.Simple (r : AlmostCommRingoid) where +module Algebra.RingSolver.Simple (r : AlmostCommutativeRing) where hunk ./Algebra/RingSolver/Simple.agda 9 +open AlmostCommutativeRing r hunk ./Algebra/RingSolver/Simple.agda 11 -import Algebra.Props.AlmostCommRing as A -open A r -open R bareRingoid r -bare-almostComm⟶ public +open R rawRing r (-raw-almostCommutative⟶ r) public addfile ./Algebra/Structures.agda hunk ./Algebra/Structures.agda 1 +------------------------------------------------------------------------ +-- Some algebraic structures (not packed up with setoids and +-- operations) +------------------------------------------------------------------------ + +open import Relation.Binary + +-- The structures are parameterised on an underlying equality. + +module Algebra.Structures (s : Setoid) where + +open Setoid s +import Algebra.FunctionProperties as P +open P s +import Relation.Binary.EqReasoning as EqR +open EqR s +open import Data.Function +open import Data.Product + +private + + -- Some abbreviations: + + _Preserves-≈ : Op₁ -> Set + • Preserves-≈ = • Preserves _≈_ → _≈_ + + _Preserves₂-≈ : Op₂ -> Set + • Preserves₂-≈ = • Preserves₂ _≈_ → _≈_ → _≈_ + +---------------------------------------------------------------------- +-- One binary operation + +record IsSemigroup (• : Op₂) : Set where + field + assoc : Associative • + •-pres-≈ : • Preserves₂-≈ + +record IsMonoid (• : Op₂) (ε : carrier) : Set where + field + isSemigroup : IsSemigroup • + identity : Identity ε • + + open IsSemigroup isSemigroup public + +record IsCommutativeMonoid (• : Op₂) (ε : carrier) : Set where + field + isMonoid : IsMonoid • ε + comm : Commutative • + + open IsMonoid isMonoid public + +record IsGroup (• : Op₂) (ε : carrier) (⁻¹ : Op₁) : Set where + field + isMonoid : IsMonoid • ε + inverse : Inverse ε ⁻¹ • + ⁻¹-pres-≈ : ⁻¹ Preserves-≈ + + open IsMonoid isMonoid public + +record IsAbelianGroup (• : Op₂) (ε : carrier) (⁻¹ : Op₁) : Set where + field + isGroup : IsGroup • ε ⁻¹ + comm : Commutative • + + open IsGroup isGroup public + + isCommutativeMonoid : IsCommutativeMonoid • ε + isCommutativeMonoid = record + { isMonoid = isMonoid + ; comm = comm + } + +---------------------------------------------------------------------- +-- Two binary operations + +record IsSemiring (+ * : Op₂) (0# 1# : carrier) : Set where + field + +-isCommutativeMonoid : IsCommutativeMonoid + 0# + *-isMonoid : IsMonoid * 1# + distrib : * DistributesOver + + zero : Zero 0# * + + open IsCommutativeMonoid +-isCommutativeMonoid public + renaming ( assoc to +-assoc + ; •-pres-≈ to +-pres-≈ + ; isSemigroup to +-isSemigroup + ; identity to +-identity + ; isMonoid to +-isMonoid + ; comm to +-comm + ) + + open IsMonoid *-isMonoid public + renaming ( assoc to *-assoc + ; •-pres-≈ to *-pres-≈ + ; isSemigroup to *-isSemigroup + ; identity to *-identity + ) + +record IsCommutativeSemiring (+ * : Op₂) (0# 1# : carrier) : Set where + field + isSemiring : IsSemiring + * 0# 1# + *-comm : Commutative * + + open IsSemiring isSemiring public + + *-isCommutativeMonoid : IsCommutativeMonoid * 1# + *-isCommutativeMonoid = record + { isMonoid = *-isMonoid + ; comm = *-comm + } + +record IsRing (_+_ _*_ : Op₂) (-_ : Op₁) (0# 1# : carrier) : Set where + field + +-isAbelianGroup : IsAbelianGroup _+_ 0# -_ + *-isMonoid : IsMonoid _*_ 1# + distrib : _*_ DistributesOver _+_ + + open IsAbelianGroup +-isAbelianGroup public + renaming ( assoc to +-assoc + ; •-pres-≈ to +-pres-≈ + ; isSemigroup to +-isSemigroup + ; identity to +-identity + ; isMonoid to +-isMonoid + ; inverse to --inverse + ; ⁻¹-pres-≈ to --pres-≈ + ; isGroup to +-isGroup + ; comm to +-comm + ; isCommutativeMonoid to +-isCommutativeMonoid + ) + + open IsMonoid *-isMonoid public + renaming ( assoc to *-assoc + ; •-pres-≈ to *-pres-≈ + ; isSemigroup to *-isSemigroup + ; identity to *-identity + ) + + zero : Zero 0# _*_ + zero = (zeroˡ , zeroʳ) + where + zeroˡ : LeftZero 0# _*_ + zeroˡ x = begin + 0# * x ≈⟨ sym $ proj₂ +-identity _ ⟩ + (0# * x) + 0# ≈⟨ byDef ⟨ +-pres-≈ ⟩ sym (proj₂ --inverse _) ⟩ + (0# * x) + ((0# * x) + - (0# * x)) ≈⟨ +-assoc _ _ _ ⟩ + ((0# * x) + (0# * x)) + - (0# * x) ≈⟨ sym (proj₂ distrib _ _ _) ⟨ +-pres-≈ ⟩ byDef ⟩ + ((0# + 0#) * x) + - (0# * x) ≈⟨ (proj₂ +-identity _ ⟨ *-pres-≈ ⟩ byDef) + ⟨ +-pres-≈ ⟩ + byDef ⟩ + (0# * x) + - (0# * x) ≈⟨ proj₂ --inverse _ ⟩ + 0# ∎ + + zeroʳ : RightZero 0# _*_ + zeroʳ x = begin + x * 0# ≈⟨ sym $ proj₂ +-identity _ ⟩ + (x * 0#) + 0# ≈⟨ byDef ⟨ +-pres-≈ ⟩ sym (proj₂ --inverse _) ⟩ + (x * 0#) + ((x * 0#) + - (x * 0#)) ≈⟨ +-assoc _ _ _ ⟩ + ((x * 0#) + (x * 0#)) + - (x * 0#) ≈⟨ sym (proj₁ distrib _ _ _) ⟨ +-pres-≈ ⟩ byDef ⟩ + (x * (0# + 0#)) + - (x * 0#) ≈⟨ (byDef ⟨ *-pres-≈ ⟩ proj₂ +-identity _) + ⟨ +-pres-≈ ⟩ + byDef ⟩ + (x * 0#) + - (x * 0#) ≈⟨ proj₂ --inverse _ ⟩ + 0# ∎ + + isSemiring : IsSemiring _+_ _*_ 0# 1# + isSemiring = record + { +-isCommutativeMonoid = +-isCommutativeMonoid + ; *-isMonoid = *-isMonoid + ; distrib = distrib + ; zero = zero + } + +record IsCommutativeRing (+ * : Op₂) (- : Op₁) (0# 1# : carrier) + : Set where + field + isRing : IsRing + * - 0# 1# + *-comm : Commutative * + + open IsRing isRing public + + isCommutativeSemiring : IsCommutativeSemiring + * 0# 1# + isCommutativeSemiring = record + { isSemiring = isSemiring + ; *-comm = *-comm + } + +record IsLattice (∨ ∧ : Op₂) : Set where + field + ∨-comm : Commutative ∨ + ∨-assoc : Associative ∨ + ∨-pres-≈ : ∨ Preserves₂-≈ + ∧-comm : Commutative ∧ + ∧-assoc : Associative ∧ + ∧-pres-≈ : ∧ Preserves₂-≈ + absorptive : Absorptive ∨ ∧ + +record IsDistributiveLattice (∨ ∧ : Op₂) : Set where + field + isLattice : IsLattice ∨ ∧ + ∨-∧-distribˡ : ∨ DistributesOverˡ ∧ + + open IsLattice isLattice public + +record IsBooleanAlgebra (∨ ∧ : Op₂) (¬ : Op₁) (⊤ ⊥ : carrier) : Set where + field + isDistributiveLattice : IsDistributiveLattice ∨ ∧ + ∨-complementʳ : RightInverse ⊤ ¬ ∨ + ∧-complementʳ : RightInverse ⊥ ¬ ∧ + ¬-pres-≈ : ¬ Preserves-≈ + + open IsDistributiveLattice isDistributiveLattice public hunk ./Data/Bool/Properties.agda 12 -import Algebra -import Algebra.Props.CommutativeSemiring as CSProp -import Algebra.Props.CommutativeRing as CRProp -open Algebra Bool-setoid -open import Algebra.Packaged +open import Algebra +import Algebra.FunctionProperties as P; open P Bool-setoid +open import Algebra.Structures +import Algebra.RingSolver.Simple as Solver +import Algebra.RingSolver.AlmostCommutativeRing as ACR hunk ./Data/Bool/Properties.agda 19 -import Algebra.RingSolver.Simple as Solver hunk ./Data/Bool/Properties.agda 83 - Bool-semiring-∨-∧ : Semiring _∨_ _∧_ false true - Bool-semiring-∨-∧ = record - { +-monoid = record - { monoid = record - { semigroup = record - { assoc = ∨-assoc - ; •-pres-≈ = ≡-cong₂ _∨_ + Bool-isCommutativeSemiring-∨-∧ + : IsCommutativeSemiring Bool-setoid _∨_ _∧_ false true + Bool-isCommutativeSemiring-∨-∧ = record + { isSemiring = record + { +-isCommutativeMonoid = record + { isMonoid = record + { isSemigroup = record + { assoc = ∨-assoc + ; •-pres-≈ = ≡-cong₂ _∨_ + } + ; identity = ∨-identity hunk ./Data/Bool/Properties.agda 95 - ; identity = ∨-identity + ; comm = ∨-comm hunk ./Data/Bool/Properties.agda 97 - ; comm = ∨-comm - } - ; *-monoid = record - { semigroup = record - { assoc = ∧-assoc - ; •-pres-≈ = ≡-cong₂ _∧_ + ; *-isMonoid = record + { isSemigroup = record + { assoc = ∧-assoc + ; •-pres-≈ = ≡-cong₂ _∧_ + } + ; identity = ∧-identity hunk ./Data/Bool/Properties.agda 104 - ; identity = ∧-identity + ; distrib = distrib-∧-∨ + ; zero = zero-∧ hunk ./Data/Bool/Properties.agda 107 - ; distrib = distrib-∧-∨ - ; zero = zero-∧ - } - - Bool-commSemiring-∨-∧ : CommutativeSemiring _∨_ _∧_ false true - Bool-commSemiring-∨-∧ = record - { semiring = Bool-semiring-∨-∧ - ; *-comm = ∧-comm + ; *-comm = ∧-comm hunk ./Data/Bool/Properties.agda 110 -Bool-commSemiringoid-∨-∧ : CommutativeSemiringoid -Bool-commSemiringoid-∨-∧ = record - { setoid = Bool-setoid - ; _+_ = _∨_ - ; _*_ = _∧_ - ; 0# = false - ; 1# = true - ; commSemiring = Bool-commSemiring-∨-∧ +Bool-commutativeSemiring-∨-∧ : CommutativeSemiring +Bool-commutativeSemiring-∨-∧ = record + { setoid = Bool-setoid + ; _+_ = _∨_ + ; _*_ = _∧_ + ; 0# = false + ; 1# = true + ; isCommutativeSemiring = Bool-isCommutativeSemiring-∨-∧ hunk ./Data/Bool/Properties.agda 121 - Solver (CSProp.almostCommRingoid Bool-commSemiringoid-∨-∧) + Solver (ACR.fromCommutativeSemiring Bool-commutativeSemiring-∨-∧) hunk ./Data/Bool/Properties.agda 153 - Bool-semiring-∧-∨ : Semiring _∧_ _∨_ true false - Bool-semiring-∧-∨ = record - { +-monoid = record - { monoid = record - { semigroup = record - { assoc = ∧-assoc - ; •-pres-≈ = ≡-cong₂ _∧_ + Bool-isCommutativeSemiring-∧-∨ + : IsCommutativeSemiring Bool-setoid _∧_ _∨_ true false + Bool-isCommutativeSemiring-∧-∨ = record + { isSemiring = record + { +-isCommutativeMonoid = record + { isMonoid = record + { isSemigroup = record + { assoc = ∧-assoc + ; •-pres-≈ = ≡-cong₂ _∧_ + } + ; identity = ∧-identity hunk ./Data/Bool/Properties.agda 165 - ; identity = ∧-identity + ; comm = ∧-comm hunk ./Data/Bool/Properties.agda 167 - ; comm = ∧-comm - } - ; *-monoid = record - { semigroup = record - { assoc = ∨-assoc - ; •-pres-≈ = ≡-cong₂ _∨_ + ; *-isMonoid = record + { isSemigroup = record + { assoc = ∨-assoc + ; •-pres-≈ = ≡-cong₂ _∨_ + } + ; identity = ∨-identity hunk ./Data/Bool/Properties.agda 174 - ; identity = ∨-identity + ; distrib = distrib-∨-∧ + ; zero = zero-∨ hunk ./Data/Bool/Properties.agda 177 - ; distrib = distrib-∨-∧ - ; zero = zero-∨ - } - - Bool-commSemiring-∧-∨ : CommutativeSemiring _∧_ _∨_ true false - Bool-commSemiring-∧-∨ = record - { semiring = Bool-semiring-∧-∨ - ; *-comm = ∨-comm + ; *-comm = ∨-comm hunk ./Data/Bool/Properties.agda 180 -Bool-commSemiringoid-∧-∨ : CommutativeSemiringoid -Bool-commSemiringoid-∧-∨ = record - { setoid = Bool-setoid - ; _+_ = _∧_ - ; _*_ = _∨_ - ; 0# = true - ; 1# = false - ; commSemiring = Bool-commSemiring-∧-∨ +Bool-commutativeSemiring-∧-∨ : CommutativeSemiring +Bool-commutativeSemiring-∧-∨ = record + { setoid = Bool-setoid + ; _+_ = _∧_ + ; _*_ = _∨_ + ; 0# = true + ; 1# = false + ; isCommutativeSemiring = Bool-isCommutativeSemiring-∧-∨ hunk ./Data/Bool/Properties.agda 191 --- (Bool, ∨, ∧) is a distributive lattice +-- (Bool, ∨, ∧, not, true, false) is a boolean algebra hunk ./Data/Bool/Properties.agda 207 -abstract - - Bool-lattice : Lattice _∨_ _∧_ - Bool-lattice = record - { ∨-comm = ∨-comm - ; ∨-assoc = ∨-assoc - ; ∨-pres-≈ = ≡-cong₂ _∨_ - ; ∧-comm = ∧-comm - ; ∧-assoc = ∧-assoc - ; ∧-pres-≈ = ≡-cong₂ _∧_ - ; absorptive = absorptive - } - - Bool-distLattice : DistributiveLattice _∨_ _∧_ - Bool-distLattice = record - { lattice = Bool-lattice - ; ∨-∧-distribˡ = proj₁ distrib-∨-∧ - } - ------------------------------------------------------------------------- --- (Bool, ∨, ∧, not, true, false) is a boolean algebra - -abstract - private hunk ./Data/Bool/Properties.agda 225 - Bool-booleanAlgebra : BooleanAlgebra _∨_ _∧_ not true false - Bool-booleanAlgebra = record - { distLattice = Bool-distLattice + Bool-isBooleanAlgebra + : IsBooleanAlgebra Bool-setoid _∨_ _∧_ not true false + Bool-isBooleanAlgebra = record + { isDistributiveLattice = record + { isLattice = record + { ∨-comm = ∨-comm + ; ∨-assoc = ∨-assoc + ; ∨-pres-≈ = ≡-cong₂ _∨_ + ; ∧-comm = ∧-comm + ; ∧-assoc = ∧-assoc + ; ∧-pres-≈ = ≡-cong₂ _∧_ + ; absorptive = absorptive + } + ; ∨-∧-distribˡ = proj₁ distrib-∨-∧ + } hunk ./Data/Bool/Properties.agda 245 -Bool-booleanAlgebraoid : BooleanAlgebraoid -Bool-booleanAlgebraoid = record - { setoid = Bool-setoid - ; _∨_ = _∨_ - ; _∧_ = _∧_ - ; ¬_ = not - ; ⊤ = true - ; ⊥ = false - ; booleanAlgebra = Bool-booleanAlgebra +Bool-booleanAlgebra : BooleanAlgebra +Bool-booleanAlgebra = record + { setoid = Bool-setoid + ; _∨_ = _∨_ + ; _∧_ = _∧_ + ; ¬_ = not + ; ⊤ = true + ; ⊥ = false + ; isBooleanAlgebra = Bool-isBooleanAlgebra hunk ./Data/Bool/Properties.agda 266 -Bool-commRingoid-xor-∧ : CommutativeRingoid -Bool-commRingoid-xor-∧ = record - { bare = record - { setoid = Bool-setoid - ; _+_ = _xor_ - ; _*_ = _∧_ - ; -_ = id - ; 0# = false - ; 1# = true - } - ; commRing = R.commRing - } +Bool-commutativeRing-xor-∧ : CommutativeRing +Bool-commutativeRing-xor-∧ = commutativeRing hunk ./Data/Bool/Properties.agda 269 - import Algebra.Props.BooleanAlgebra - module P = Algebra.Props.BooleanAlgebra - Bool-booleanAlgebraoid - module R = P.XorRing _xor_ xor-is-ok + import Algebra.Props.BooleanAlgebra as BA + open BA Bool-booleanAlgebra + open XorRing _xor_ xor-is-ok hunk ./Data/Bool/Properties.agda 274 - Solver (CRProp.almostCommRingoid Bool-commRingoid-xor-∧) + Solver (ACR.fromCommutativeRing Bool-commutativeRing-xor-∧) hunk ./Data/List/Properties.agda 13 -import Algebra -open Algebra ℕ-setoid +open import Algebra hunk ./Data/List/Properties.agda 30 - where - +-assoc = Semigroup.assoc (Monoid.semigroup (CommutativeMonoid.monoid - (Semiring.+-monoid ℕ-semiring))) + where open CommutativeSemiring ℕ-commutativeSemiring hiding (_+_) hunk ./Data/Nat/Properties.agda 11 -import Algebra -import Algebra.Props.CommutativeSemiring as CSProp -open Algebra ℕ-setoid -open import Algebra.Packaged +open import Algebra +open import Algebra.Structures +import Algebra.FunctionProperties as P; open P ℕ-setoid hunk ./Data/Nat/Properties.agda 17 -import Algebra.RingSolver.Simple as Solver hunk ./Data/Nat/Properties.agda 170 - ℕ-semiring : Semiring _+_ _*_ 0 1 - ℕ-semiring = record - { +-monoid = record - { monoid = record - { semigroup = record - { assoc = +-assoc - ; •-pres-≈ = ≡-cong₂ _+_ + ℕ-isCommutativeSemiring : IsCommutativeSemiring ℕ-setoid _+_ _*_ 0 1 + ℕ-isCommutativeSemiring = record + { isSemiring = record + { +-isCommutativeMonoid = record + { isMonoid = record + { isSemigroup = record + { assoc = +-assoc + ; •-pres-≈ = ≡-cong₂ _+_ + } + ; identity = +-identity hunk ./Data/Nat/Properties.agda 181 - ; identity = +-identity + ; comm = +-comm hunk ./Data/Nat/Properties.agda 183 - ; comm = +-comm - } - ; *-monoid = record - { semigroup = record - { assoc = *-assoc - ; •-pres-≈ = ≡-cong₂ _*_ + ; *-isMonoid = record + { isSemigroup = record + { assoc = *-assoc + ; •-pres-≈ = ≡-cong₂ _*_ + } + ; identity = *-identity hunk ./Data/Nat/Properties.agda 190 - ; identity = *-identity + ; distrib = distrib-*-+ + ; zero = *-zero hunk ./Data/Nat/Properties.agda 193 - ; distrib = distrib-*-+ - ; zero = *-zero - } - - ℕ-commSemiring : CommutativeSemiring _+_ _*_ 0 1 - ℕ-commSemiring = record - { semiring = ℕ-semiring - ; *-comm = *-comm + ; *-comm = *-comm hunk ./Data/Nat/Properties.agda 196 -ℕ-commSemiringoid : CommutativeSemiringoid -ℕ-commSemiringoid = record - { setoid = ℕ-setoid - ; _+_ = _+_ - ; _*_ = _*_ - ; 0# = 0 - ; 1# = 1 - ; commSemiring = ℕ-commSemiring +ℕ-commutativeSemiring : CommutativeSemiring +ℕ-commutativeSemiring = record + { setoid = ℕ-setoid + ; _+_ = _+_ + ; _*_ = _*_ + ; 0# = 0 + ; 1# = 1 + ; isCommutativeSemiring = ℕ-isCommutativeSemiring hunk ./Data/Nat/Properties.agda 206 +import Algebra.RingSolver.Simple as Solver +import Algebra.RingSolver.AlmostCommutativeRing as ACR hunk ./Data/Nat/Properties.agda 209 - Solver (CSProp.almostCommRingoid ℕ-commSemiringoid) + Solver (ACR.fromCommutativeSemiring ℕ-commutativeSemiring) hunk ./Data/Nat/Properties.agda 308 - ℕ-lattice : Lattice _⊔_ _⊓_ - ℕ-lattice = record - { ∨-comm = ⊔-comm - ; ∨-assoc = ⊔-assoc - ; ∨-pres-≈ = ≡-cong₂ _⊔_ - ; ∧-comm = ⊓-comm - ; ∧-assoc = ⊓-assoc - ; ∧-pres-≈ = ≡-cong₂ _⊓_ - ; absorptive = absorptive-⊔-⊓ - } - - ℕ-distLattice : DistributiveLattice _⊔_ _⊓_ - ℕ-distLattice = record - { lattice = ℕ-lattice + ℕ-isDistributiveLattice : IsDistributiveLattice ℕ-setoid _⊔_ _⊓_ + ℕ-isDistributiveLattice = record + { isLattice = record + { ∨-comm = ⊔-comm + ; ∨-assoc = ⊔-assoc + ; ∨-pres-≈ = ≡-cong₂ _⊔_ + ; ∧-comm = ⊓-comm + ; ∧-assoc = ⊓-assoc + ; ∧-pres-≈ = ≡-cong₂ _⊓_ + ; absorptive = absorptive-⊔-⊓ + } hunk ./Data/Nat/Properties.agda 322 -ℕ-distLatticoid : DistributiveLatticoid -ℕ-distLatticoid = record - { setoid = ℕ-setoid - ; _∨_ = _⊔_ - ; _∧_ = _⊓_ - ; distLattice = ℕ-distLattice +ℕ-distributiveLattice : DistributiveLattice +ℕ-distributiveLattice = record + { setoid = ℕ-setoid + ; _∨_ = _⊔_ + ; _∧_ = _⊓_ + ; isDistributiveLattice = ℕ-isDistributiveLattice hunk ./Everything.agda 14 +import Algebra.FunctionProperties hunk ./Everything.agda 17 -import Algebra.Packaged hunk ./Everything.agda 18 -import Algebra.Props.AlmostCommRing hunk ./Everything.agda 19 -import Algebra.Props.CommutativeRing -import Algebra.Props.CommutativeSemiring hunk ./Everything.agda 23 -import Algebra.Props.Semiring hunk ./Everything.agda 24 +import Algebra.RingSolver.AlmostCommutativeRing hunk ./Everything.agda 28 +import Algebra.Structures