From 65ac8887f40ca8ad2fcde525e7e4f8e2616db7c5 Mon Sep 17 00:00:00 2001 From: Freek Date: Wed, 7 Aug 2024 18:43:20 +0200 Subject: [PATCH 1/6] Add Boolean Rings --- Cubical/Algebra/BooleanRing.agda | 4 + Cubical/Algebra/BooleanRing/Base.agda | 246 ++++++++++++++++++++++++++ 2 files changed, 250 insertions(+) create mode 100644 Cubical/Algebra/BooleanRing.agda create mode 100644 Cubical/Algebra/BooleanRing/Base.agda diff --git a/Cubical/Algebra/BooleanRing.agda b/Cubical/Algebra/BooleanRing.agda new file mode 100644 index 000000000..32d528503 --- /dev/null +++ b/Cubical/Algebra/BooleanRing.agda @@ -0,0 +1,4 @@ +{-# OPTIONS --safe #-} +module Cubical.Algebra.BooleanRing where + +open import Cubical.Algebra.BooleanRing.Base public diff --git a/Cubical/Algebra/BooleanRing/Base.agda b/Cubical/Algebra/BooleanRing/Base.agda new file mode 100644 index 000000000..7cfb3fe14 --- /dev/null +++ b/Cubical/Algebra/BooleanRing/Base.agda @@ -0,0 +1,246 @@ +{-# OPTIONS --safe #-} +module Cubical.Algebra.BooleanRing.Base where + +open import Cubical.Foundations.Prelude hiding (_∧_;_∨_) +open import Cubical.Foundations.Structure +open import Cubical.Data.Empty as ⊥ +open import Cubical.Algebra.Ring +open import Cubical.Algebra.AbGroup.Base +open import Cubical.Algebra.CommRing +open import Cubical.Tactics.CommRingSolver + + +private + variable + ℓ ℓ' : Level + +record IsBooleanRing {B : Type ℓ} + (𝟘 𝟙 : B) (_+_ _·_ : B → B → B) (-_ : B → B) : Type ℓ where + + field + isCommRing : IsCommRing 𝟘 𝟙 _+_ _·_ -_ + ·IsIdempotent : (x : B) → x · x ≡ x + + open IsCommRing isCommRing public + +record BooleanStr (A : Type ℓ) : Type (ℓ-suc ℓ) where + field + 𝟘 : A + 𝟙 : A + _+_ : A → A → A + _·_ : A → A → A + -_ : A → A + isBooleanRing : IsBooleanRing 𝟘 𝟙 _+_ _·_ -_ + + infix 8 -_ + infixl 7 _·_ + infixl 6 _+_ + + open IsBooleanRing isBooleanRing public + +BooleanRing : ∀ ℓ → Type (ℓ-suc ℓ) +BooleanRing ℓ = TypeWithStr ℓ BooleanStr + +BooleanStrToCommRingStr : { A : Type ℓ } → BooleanStr A → CommRingStr A +BooleanStrToCommRingStr x = record { isCommRing = IsBooleanRing.isCommRing (BooleanStr.isBooleanRing x) } + +BooleanRingToCommRing : BooleanRing ℓ → CommRing ℓ +BooleanRingToCommRing (carrier , structure ) = carrier , BooleanStrToCommRingStr structure + +module BooleanAlgebraStr (A : BooleanRing ℓ) where + open BooleanStr (A . snd) + _∨_ : ⟨ A ⟩ → ⟨ A ⟩ → ⟨ A ⟩ + a ∨ b = (a + b) + (a · b) + _∧_ : ⟨ A ⟩ → ⟨ A ⟩ → ⟨ A ⟩ + a ∧ b = (a · b) + ¬_ : ⟨ A ⟩ → ⟨ A ⟩ + ¬ a = 𝟙 + a + + variable x y z : ⟨ A ⟩ + + ∧IsIdempotent : x ∧ x ≡ x + ∧IsIdempotent = ·IsIdempotent _ + + ∧Assoc : x ∧ ( y ∧ z ) ≡ ( x ∧ y ) ∧ z + ∧Assoc = ·Assoc _ _ _ + + ∧Comm : (x ∧ y) ≡ (y ∧ x) + ∧Comm = ·Comm _ _ + + ∨Assoc : (x ∨ ( y ∨ z ) ≡ ( x ∨ y ) ∨ z ) + ∨Assoc = solve! (BooleanRingToCommRing A) + + ∨Comm : (x ∨ y ) ≡ (y ∨ x) + ∨Comm = solve! (BooleanRingToCommRing A) + + 0∨IdR : x ∨ 𝟘 ≡ x + 0∨IdR = solve! (BooleanRingToCommRing A) + + 0∨IdL : 𝟘 ∨ x ≡ x + 0∨IdL = solve! (BooleanRingToCommRing A) + + 1∧IdR : x ∧ 𝟙 ≡ x + 1∧IdR = ·IdR _ + + 1∧IdL : 𝟙 ∧ x ≡ x + 1∧IdL = ·IdL _ + + 0∧RightAnnihilates : x ∧ 𝟘 ≡ 𝟘 + 0∧RightAnnihilates = RingTheory.0RightAnnihilates (CommRing→Ring (BooleanRingToCommRing A)) _ + + 0∧LeftAnnihilates : 𝟘 ∧ x ≡ 𝟘 + 0∧LeftAnnihilates = RingTheory.0LeftAnnihilates (CommRing→Ring (BooleanRingToCommRing A)) _ + + -IsId : x + x ≡ 𝟘 + -IsId {x = x} = RingTheory.+Idempotency→0 (CommRing→Ring (BooleanRingToCommRing A)) (x + x) 2x≡4x + where + 2x≡4x : x + x ≡ (x + x) + (x + x) + 2x≡4x = + (x + x) + ≡⟨ sym (·IsIdempotent (x + x)) ⟩ + (x + x) · (x + x) + ≡⟨ solve! (BooleanRingToCommRing A) ⟩ + ((x · x) + (x · x)) + ((x · x) + (x · x)) + ≡⟨ cong₂ _+_ (cong₂ _+_ (·IsIdempotent x) (·IsIdempotent x)) (cong₂ _+_ (·IsIdempotent x) (·IsIdempotent x)) ⟩ + (x + x) + (x + x) ∎ + + ∨IsIdempotent : x ∨ x ≡ x + ∨IsIdempotent { x = x } = + x + x + x · x + ≡⟨ cong (λ y → y + x · x) -IsId ⟩ + 𝟘 + x · x + ≡⟨ +IdL (x · x) ⟩ + x · x + ≡⟨ ·IsIdempotent x ⟩ + x ∎ + + 1Absorbs∨R : x ∨ 𝟙 ≡ 𝟙 + 1Absorbs∨R {x = x} = + (x + 𝟙) + (x · 𝟙) + ≡⟨ solve! (BooleanRingToCommRing A) ⟩ + 𝟙 + (x + x) + ≡⟨ cong (λ y → 𝟙 + y) -IsId ⟩ + 𝟙 + 𝟘 + ≡⟨ +IdR 𝟙 ⟩ + 𝟙 ∎ + + 1Absorbs∨L : 𝟙 ∨ x ≡ 𝟙 + 1Absorbs∨L {x = x} = ∨Comm ∙ 1Absorbs∨R + + ∧Distr∨L : x ∧ ( y ∨ z) ≡ (x ∧ y) ∨ (x ∧ z) + ∧Distr∨L {x = x} {y = y} { z = z} = + x · ((y + z) + (y · z)) + ≡⟨ solve! (BooleanRingToCommRing A) ⟩ + x · y + x · z + x · (y · z) + ≡⟨ cong (λ a → x · y + x · z + a · (y · z)) (sym (·IsIdempotent x)) ⟩ + x · y + x · z + x · x · (y · z) + ≡⟨ solve! (BooleanRingToCommRing A) ⟩ + x · y + x · z + (x · y) · (x · z) ∎ + + ∧Distr∨R : (x ∨ y) ∧ z ≡ (x ∧ z) ∨ (y ∧ z) + ∧Distr∨R = ∧Comm ∙ ∧Distr∨L ∙ cong₂ _∨_ ∧Comm ∧Comm + + ∨Distr∧L : x ∨ (y ∧ z) ≡ (x ∨ y) ∧ (x ∨ z) + ∨Distr∧L {x = x} {y = y} {z = z} = + x + (y · z) + x · (y · z) + ≡⟨ solve! (BooleanRingToCommRing A) ⟩ + x + 𝟘 + 𝟘 + y · z + 𝟘 + x · y · z + ≡⟨ cong (λ a → a + 𝟘 + 𝟘 + y · z + 𝟘 + a · y · z) (sym (·IsIdempotent x)) ⟩ + x · x + 𝟘 + 𝟘 + y · z + 𝟘 + x · x · y · z + ≡⟨ cong (λ a → x · x + 𝟘 + 𝟘 + y · z + a + x · x · y · z) (sym (-IsId {x = (x · y) · z})) ⟩ + x · x + 𝟘 + 𝟘 + y · z + (x · y · z + x · y · z) + x · x · y · z + ≡⟨ (cong₂ (λ a b → x · x + a + b + y · z + (x · y · z + x · y · z) + x · x · y · z)) (xa-xxa≡0 z) (xa-xxa≡0 y) ⟩ + x · x + (x · z + x · x · z) + (x · y + x · x · y) + y · z + (x · y · z + x · y · z) + x · x · y · z + ≡⟨ solve! (BooleanRingToCommRing A) ⟩ + (x + y + x · y) · (x + z + x · z) ∎ where + xa≡xxa : (a : ⟨ A ⟩) → x · a ≡ (x · x ) · a + xa≡xxa a = cong (λ y → y · a) (sym (·IsIdempotent x)) + xa-xxa≡0 : (a : ⟨ A ⟩) → 𝟘 ≡ x · a + x · x · a + xa-xxa≡0 a = + 𝟘 + ≡⟨ sym -IsId ⟩ + x · a + x · a + ≡⟨ cong (λ y → x · a + y · a) (sym (·IsIdempotent x)) ⟩ + x · a + x · x · a ∎ + + ∨Distr∧R : (x ∧ y) ∨ z ≡ (x ∨ z) ∧ (y ∨ z) + ∨Distr∧R = ∨Comm ∙ ∨Distr∧L ∙ cong₂ _∧_ ∨Comm ∨Comm + + ∨Absorps∧L : x ∧ (x ∨ y) ≡ x + ∨Absorps∧L {x = x} {y = y} = + x · ((x + y) + (x · y)) + ≡⟨ solve! (BooleanRingToCommRing A) ⟩ + x · x + (x · y + x · x · y) + ≡⟨ cong (λ z → z + ((x · y) + (z · y))) (·IsIdempotent x) ⟩ + x + (x · y + x · y) + ≡⟨ cong (_+_ x) -IsId ⟩ + (x + 𝟘) + ≡⟨ +IdR x ⟩ + x ∎ + + ∧Absorps∨L : x ∨ (x ∧ y) ≡ x + ∧Absorps∨L {x = x} { y = y} = + x + x · y + x · (x · y) + ≡⟨ solve! (BooleanRingToCommRing A) ⟩ + x + (x · y + x · x · y) + ≡⟨ cong (λ z → x + (x · y + z · y)) (·IsIdempotent x) ⟩ + x + (x · y + x · y) + ≡⟨ cong (_+_ x) -IsId ⟩ + x + 𝟘 + ≡⟨ +IdR x ⟩ + x ∎ + + ¬Cancels∧R : (x ∧ (¬ x)) ≡ 𝟘 + ¬Cancels∧R {x = x} = + x · (𝟙 + x) + ≡⟨ solve! (BooleanRingToCommRing A) ⟩ + x + x · x + ≡⟨ cong (λ y → x + y) (·IsIdempotent x) ⟩ + x + x + ≡⟨ -IsId ⟩ + 𝟘 ∎ + + ¬Cancels∧L : ((¬ x) ∧ x) ≡ 𝟘 + ¬Cancels∧L = ∧Comm ∙ ¬Cancels∧R + + ¬Completes∨R : (x ∨ (¬ x)) ≡ 𝟙 + ¬Completes∨R {x = x} = + x + (¬ x) + (x ∧ (¬ x)) + ≡⟨ cong (λ z → x + ¬ x + z) ¬Cancels∧R ⟩ + x + ¬ x + 𝟘 + ≡⟨ solve! (BooleanRingToCommRing A) ⟩ + x ∨ 𝟙 + ≡⟨ 1Absorbs∨R ⟩ + 𝟙 ∎ + + ¬Completes∨L : (¬ x) ∨ x ≡ 𝟙 + ¬Completes∨L = ∨Comm ∙ ¬Completes∨R + + ¬¬ : ¬ ¬ x ≡ x + ¬¬ {x = x} = + 𝟙 + (𝟙 + x) + ≡⟨ +Assoc 𝟙 𝟙 x ⟩ + (𝟙 + 𝟙) + x + ≡⟨ cong (λ y → y + x) ( -IsId {x = 𝟙}) ⟩ + 𝟘 + x + ≡⟨ +IdL x ⟩ + x ∎ + + ¬0≡1 : ¬ 𝟘 ≡ 𝟙 + ¬0≡1 = +IdR 𝟙 + + ¬1≡0 : ¬ 𝟙 ≡ 𝟘 + ¬1≡0 = -IsId {x = 𝟙} + + DeMorgan¬∨ : ¬ (x ∨ y) ≡ (¬ x) ∧ (¬ y) + DeMorgan¬∨ = solve! (BooleanRingToCommRing A) + + DeMorgan¬∧ : ¬ (x ∧ y) ≡ (¬ x) ∨ (¬ y) + DeMorgan¬∧ {x = x} {y = y} = + 𝟙 + x · y + ≡⟨ solve! (BooleanRingToCommRing A) ⟩ + 𝟘 + 𝟘 + 𝟙 + x · y + ≡⟨ cong₂ (λ a b → ((a + b) + 𝟙) + (x · y)) (sym (-IsId {x = 𝟙 + x})) (sym (-IsId {x = y})) ⟩ + ((𝟙 + x) + (𝟙 + x)) + (y + y) + 𝟙 + x · y + ≡⟨ solve! (BooleanRingToCommRing A) ⟩ + ((¬ x) ∨ (¬ y)) ∎ From 1165d7ea2f8a696d884330ddac833cf72138b92f Mon Sep 17 00:00:00 2001 From: Freek Date: Wed, 4 Sep 2024 20:19:52 +0200 Subject: [PATCH 2/6] Changed To to an arrow per Felix' comment. --- Cubical/Algebra/BooleanRing/Base.agda | 48 +++++++++++++-------------- 1 file changed, 24 insertions(+), 24 deletions(-) diff --git a/Cubical/Algebra/BooleanRing/Base.agda b/Cubical/Algebra/BooleanRing/Base.agda index 7cfb3fe14..5e85b2605 100644 --- a/Cubical/Algebra/BooleanRing/Base.agda +++ b/Cubical/Algebra/BooleanRing/Base.agda @@ -41,11 +41,11 @@ record BooleanStr (A : Type ℓ) : Type (ℓ-suc ℓ) where BooleanRing : ∀ ℓ → Type (ℓ-suc ℓ) BooleanRing ℓ = TypeWithStr ℓ BooleanStr -BooleanStrToCommRingStr : { A : Type ℓ } → BooleanStr A → CommRingStr A -BooleanStrToCommRingStr x = record { isCommRing = IsBooleanRing.isCommRing (BooleanStr.isBooleanRing x) } +BooleanStr→CommRingStr : { A : Type ℓ } → BooleanStr A → CommRingStr A +BooleanStr→CommRingStr x = record { isCommRing = IsBooleanRing.isCommRing (BooleanStr.isBooleanRing x) } -BooleanRingToCommRing : BooleanRing ℓ → CommRing ℓ -BooleanRingToCommRing (carrier , structure ) = carrier , BooleanStrToCommRingStr structure +BooleanRing→CommRing : BooleanRing ℓ → CommRing ℓ +BooleanRing→CommRing (carrier , structure ) = carrier , BooleanStr→CommRingStr structure module BooleanAlgebraStr (A : BooleanRing ℓ) where open BooleanStr (A . snd) @@ -68,16 +68,16 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where ∧Comm = ·Comm _ _ ∨Assoc : (x ∨ ( y ∨ z ) ≡ ( x ∨ y ) ∨ z ) - ∨Assoc = solve! (BooleanRingToCommRing A) + ∨Assoc = solve! (BooleanRing→CommRing A) ∨Comm : (x ∨ y ) ≡ (y ∨ x) - ∨Comm = solve! (BooleanRingToCommRing A) + ∨Comm = solve! (BooleanRing→CommRing A) 0∨IdR : x ∨ 𝟘 ≡ x - 0∨IdR = solve! (BooleanRingToCommRing A) + 0∨IdR = solve! (BooleanRing→CommRing A) 0∨IdL : 𝟘 ∨ x ≡ x - 0∨IdL = solve! (BooleanRingToCommRing A) + 0∨IdL = solve! (BooleanRing→CommRing A) 1∧IdR : x ∧ 𝟙 ≡ x 1∧IdR = ·IdR _ @@ -86,20 +86,20 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where 1∧IdL = ·IdL _ 0∧RightAnnihilates : x ∧ 𝟘 ≡ 𝟘 - 0∧RightAnnihilates = RingTheory.0RightAnnihilates (CommRing→Ring (BooleanRingToCommRing A)) _ + 0∧RightAnnihilates = RingTheory.0RightAnnihilates (CommRing→Ring (BooleanRing→CommRing A)) _ 0∧LeftAnnihilates : 𝟘 ∧ x ≡ 𝟘 - 0∧LeftAnnihilates = RingTheory.0LeftAnnihilates (CommRing→Ring (BooleanRingToCommRing A)) _ + 0∧LeftAnnihilates = RingTheory.0LeftAnnihilates (CommRing→Ring (BooleanRing→CommRing A)) _ -IsId : x + x ≡ 𝟘 - -IsId {x = x} = RingTheory.+Idempotency→0 (CommRing→Ring (BooleanRingToCommRing A)) (x + x) 2x≡4x + -IsId {x = x} = RingTheory.+Idempotency→0 (CommRing→Ring (BooleanRing→CommRing A)) (x + x) 2x≡4x where 2x≡4x : x + x ≡ (x + x) + (x + x) 2x≡4x = (x + x) ≡⟨ sym (·IsIdempotent (x + x)) ⟩ (x + x) · (x + x) - ≡⟨ solve! (BooleanRingToCommRing A) ⟩ + ≡⟨ solve! (BooleanRing→CommRing A) ⟩ ((x · x) + (x · x)) + ((x · x) + (x · x)) ≡⟨ cong₂ _+_ (cong₂ _+_ (·IsIdempotent x) (·IsIdempotent x)) (cong₂ _+_ (·IsIdempotent x) (·IsIdempotent x)) ⟩ (x + x) + (x + x) ∎ @@ -117,7 +117,7 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where 1Absorbs∨R : x ∨ 𝟙 ≡ 𝟙 1Absorbs∨R {x = x} = (x + 𝟙) + (x · 𝟙) - ≡⟨ solve! (BooleanRingToCommRing A) ⟩ + ≡⟨ solve! (BooleanRing→CommRing A) ⟩ 𝟙 + (x + x) ≡⟨ cong (λ y → 𝟙 + y) -IsId ⟩ 𝟙 + 𝟘 @@ -130,11 +130,11 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where ∧Distr∨L : x ∧ ( y ∨ z) ≡ (x ∧ y) ∨ (x ∧ z) ∧Distr∨L {x = x} {y = y} { z = z} = x · ((y + z) + (y · z)) - ≡⟨ solve! (BooleanRingToCommRing A) ⟩ + ≡⟨ solve! (BooleanRing→CommRing A) ⟩ x · y + x · z + x · (y · z) ≡⟨ cong (λ a → x · y + x · z + a · (y · z)) (sym (·IsIdempotent x)) ⟩ x · y + x · z + x · x · (y · z) - ≡⟨ solve! (BooleanRingToCommRing A) ⟩ + ≡⟨ solve! (BooleanRing→CommRing A) ⟩ x · y + x · z + (x · y) · (x · z) ∎ ∧Distr∨R : (x ∨ y) ∧ z ≡ (x ∧ z) ∨ (y ∧ z) @@ -143,7 +143,7 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where ∨Distr∧L : x ∨ (y ∧ z) ≡ (x ∨ y) ∧ (x ∨ z) ∨Distr∧L {x = x} {y = y} {z = z} = x + (y · z) + x · (y · z) - ≡⟨ solve! (BooleanRingToCommRing A) ⟩ + ≡⟨ solve! (BooleanRing→CommRing A) ⟩ x + 𝟘 + 𝟘 + y · z + 𝟘 + x · y · z ≡⟨ cong (λ a → a + 𝟘 + 𝟘 + y · z + 𝟘 + a · y · z) (sym (·IsIdempotent x)) ⟩ x · x + 𝟘 + 𝟘 + y · z + 𝟘 + x · x · y · z @@ -151,7 +151,7 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where x · x + 𝟘 + 𝟘 + y · z + (x · y · z + x · y · z) + x · x · y · z ≡⟨ (cong₂ (λ a b → x · x + a + b + y · z + (x · y · z + x · y · z) + x · x · y · z)) (xa-xxa≡0 z) (xa-xxa≡0 y) ⟩ x · x + (x · z + x · x · z) + (x · y + x · x · y) + y · z + (x · y · z + x · y · z) + x · x · y · z - ≡⟨ solve! (BooleanRingToCommRing A) ⟩ + ≡⟨ solve! (BooleanRing→CommRing A) ⟩ (x + y + x · y) · (x + z + x · z) ∎ where xa≡xxa : (a : ⟨ A ⟩) → x · a ≡ (x · x ) · a xa≡xxa a = cong (λ y → y · a) (sym (·IsIdempotent x)) @@ -169,7 +169,7 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where ∨Absorps∧L : x ∧ (x ∨ y) ≡ x ∨Absorps∧L {x = x} {y = y} = x · ((x + y) + (x · y)) - ≡⟨ solve! (BooleanRingToCommRing A) ⟩ + ≡⟨ solve! (BooleanRing→CommRing A) ⟩ x · x + (x · y + x · x · y) ≡⟨ cong (λ z → z + ((x · y) + (z · y))) (·IsIdempotent x) ⟩ x + (x · y + x · y) @@ -181,7 +181,7 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where ∧Absorps∨L : x ∨ (x ∧ y) ≡ x ∧Absorps∨L {x = x} { y = y} = x + x · y + x · (x · y) - ≡⟨ solve! (BooleanRingToCommRing A) ⟩ + ≡⟨ solve! (BooleanRing→CommRing A) ⟩ x + (x · y + x · x · y) ≡⟨ cong (λ z → x + (x · y + z · y)) (·IsIdempotent x) ⟩ x + (x · y + x · y) @@ -193,7 +193,7 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where ¬Cancels∧R : (x ∧ (¬ x)) ≡ 𝟘 ¬Cancels∧R {x = x} = x · (𝟙 + x) - ≡⟨ solve! (BooleanRingToCommRing A) ⟩ + ≡⟨ solve! (BooleanRing→CommRing A) ⟩ x + x · x ≡⟨ cong (λ y → x + y) (·IsIdempotent x) ⟩ x + x @@ -208,7 +208,7 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where x + (¬ x) + (x ∧ (¬ x)) ≡⟨ cong (λ z → x + ¬ x + z) ¬Cancels∧R ⟩ x + ¬ x + 𝟘 - ≡⟨ solve! (BooleanRingToCommRing A) ⟩ + ≡⟨ solve! (BooleanRing→CommRing A) ⟩ x ∨ 𝟙 ≡⟨ 1Absorbs∨R ⟩ 𝟙 ∎ @@ -233,14 +233,14 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where ¬1≡0 = -IsId {x = 𝟙} DeMorgan¬∨ : ¬ (x ∨ y) ≡ (¬ x) ∧ (¬ y) - DeMorgan¬∨ = solve! (BooleanRingToCommRing A) + DeMorgan¬∨ = solve! (BooleanRing→CommRing A) DeMorgan¬∧ : ¬ (x ∧ y) ≡ (¬ x) ∨ (¬ y) DeMorgan¬∧ {x = x} {y = y} = 𝟙 + x · y - ≡⟨ solve! (BooleanRingToCommRing A) ⟩ + ≡⟨ solve! (BooleanRing→CommRing A) ⟩ 𝟘 + 𝟘 + 𝟙 + x · y ≡⟨ cong₂ (λ a b → ((a + b) + 𝟙) + (x · y)) (sym (-IsId {x = 𝟙 + x})) (sym (-IsId {x = y})) ⟩ ((𝟙 + x) + (𝟙 + x)) + (y + y) + 𝟙 + x · y - ≡⟨ solve! (BooleanRingToCommRing A) ⟩ + ≡⟨ solve! (BooleanRing→CommRing A) ⟩ ((¬ x) ∨ (¬ y)) ∎ From 4ade01fb48ec0edf52ceea45023716c9f972ddba Mon Sep 17 00:00:00 2001 From: Freek Date: Wed, 4 Sep 2024 20:26:23 +0200 Subject: [PATCH 3/6] Removed superfluous brackets per Felix' comment. --- Cubical/Algebra/BooleanRing/Base.agda | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/Cubical/Algebra/BooleanRing/Base.agda b/Cubical/Algebra/BooleanRing/Base.agda index 5e85b2605..cf696bdec 100644 --- a/Cubical/Algebra/BooleanRing/Base.agda +++ b/Cubical/Algebra/BooleanRing/Base.agda @@ -15,7 +15,8 @@ private ℓ ℓ' : Level record IsBooleanRing {B : Type ℓ} - (𝟘 𝟙 : B) (_+_ _·_ : B → B → B) (-_ : B → B) : Type ℓ where + (𝟘 𝟙 : B) (_+_ _·_ : B → B → B) (-_ : B → B) : Type ℓ where + no-eta-equality field isCommRing : IsCommRing 𝟘 𝟙 _+_ _·_ -_ @@ -52,7 +53,7 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where _∨_ : ⟨ A ⟩ → ⟨ A ⟩ → ⟨ A ⟩ a ∨ b = (a + b) + (a · b) _∧_ : ⟨ A ⟩ → ⟨ A ⟩ → ⟨ A ⟩ - a ∧ b = (a · b) + a ∧ b = a · b ¬_ : ⟨ A ⟩ → ⟨ A ⟩ ¬ a = 𝟙 + a @@ -64,13 +65,13 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where ∧Assoc : x ∧ ( y ∧ z ) ≡ ( x ∧ y ) ∧ z ∧Assoc = ·Assoc _ _ _ - ∧Comm : (x ∧ y) ≡ (y ∧ x) + ∧Comm : x ∧ y ≡ y ∧ x ∧Comm = ·Comm _ _ ∨Assoc : (x ∨ ( y ∨ z ) ≡ ( x ∨ y ) ∨ z ) ∨Assoc = solve! (BooleanRing→CommRing A) - ∨Comm : (x ∨ y ) ≡ (y ∨ x) + ∨Comm : x ∨ y ≡ y ∨ x ∨Comm = solve! (BooleanRing→CommRing A) 0∨IdR : x ∨ 𝟘 ≡ x @@ -200,10 +201,10 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where ≡⟨ -IsId ⟩ 𝟘 ∎ - ¬Cancels∧L : ((¬ x) ∧ x) ≡ 𝟘 + ¬Cancels∧L : (¬ x) ∧ x ≡ 𝟘 ¬Cancels∧L = ∧Comm ∙ ¬Cancels∧R - ¬Completes∨R : (x ∨ (¬ x)) ≡ 𝟙 + ¬Completes∨R : x ∨ (¬ x) ≡ 𝟙 ¬Completes∨R {x = x} = x + (¬ x) + (x ∧ (¬ x)) ≡⟨ cong (λ z → x + ¬ x + z) ¬Cancels∧R ⟩ From be588a69ac7b68a199ef8b9ef8e111d42818ae62 Mon Sep 17 00:00:00 2001 From: Freek Date: Wed, 4 Sep 2024 20:27:58 +0200 Subject: [PATCH 4/6] missed on parenthesis. --- Cubical/Algebra/BooleanRing/Base.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cubical/Algebra/BooleanRing/Base.agda b/Cubical/Algebra/BooleanRing/Base.agda index cf696bdec..da2421c03 100644 --- a/Cubical/Algebra/BooleanRing/Base.agda +++ b/Cubical/Algebra/BooleanRing/Base.agda @@ -191,7 +191,7 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where ≡⟨ +IdR x ⟩ x ∎ - ¬Cancels∧R : (x ∧ (¬ x)) ≡ 𝟘 + ¬Cancels∧R : x ∧ (¬ x) ≡ 𝟘 ¬Cancels∧R {x = x} = x · (𝟙 + x) ≡⟨ solve! (BooleanRing→CommRing A) ⟩ From 1d02daf508e36656b92695c01c9a092d19c2cf69 Mon Sep 17 00:00:00 2001 From: Freek Date: Wed, 4 Sep 2024 20:47:46 +0200 Subject: [PATCH 5/6] Changed names to comply with NAMING.md --- Cubical/Algebra/BooleanRing/Base.agda | 80 +++++++++++++-------------- 1 file changed, 40 insertions(+), 40 deletions(-) diff --git a/Cubical/Algebra/BooleanRing/Base.agda b/Cubical/Algebra/BooleanRing/Base.agda index da2421c03..a64914ebd 100644 --- a/Cubical/Algebra/BooleanRing/Base.agda +++ b/Cubical/Algebra/BooleanRing/Base.agda @@ -20,7 +20,7 @@ record IsBooleanRing {B : Type ℓ} field isCommRing : IsCommRing 𝟘 𝟙 _+_ _·_ -_ - ·IsIdempotent : (x : B) → x · x ≡ x + ·Idem : (x : B) → x · x ≡ x open IsCommRing isCommRing public @@ -59,8 +59,8 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where variable x y z : ⟨ A ⟩ - ∧IsIdempotent : x ∧ x ≡ x - ∧IsIdempotent = ·IsIdempotent _ + ∧Idem : x ∧ x ≡ x + ∧Idem = ·Idem _ ∧Assoc : x ∧ ( y ∧ z ) ≡ ( x ∧ y ) ∧ z ∧Assoc = ·Assoc _ _ _ @@ -74,23 +74,23 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where ∨Comm : x ∨ y ≡ y ∨ x ∨Comm = solve! (BooleanRing→CommRing A) - 0∨IdR : x ∨ 𝟘 ≡ x - 0∨IdR = solve! (BooleanRing→CommRing A) + ∨IdR : x ∨ 𝟘 ≡ x + ∨IdR = solve! (BooleanRing→CommRing A) - 0∨IdL : 𝟘 ∨ x ≡ x - 0∨IdL = solve! (BooleanRing→CommRing A) + ∨IdL : 𝟘 ∨ x ≡ x + ∨IdL = solve! (BooleanRing→CommRing A) - 1∧IdR : x ∧ 𝟙 ≡ x - 1∧IdR = ·IdR _ + ∧IdR : x ∧ 𝟙 ≡ x + ∧IdR = ·IdR _ - 1∧IdL : 𝟙 ∧ x ≡ x - 1∧IdL = ·IdL _ + ∧IdL : 𝟙 ∧ x ≡ x + ∧IdL = ·IdL _ - 0∧RightAnnihilates : x ∧ 𝟘 ≡ 𝟘 - 0∧RightAnnihilates = RingTheory.0RightAnnihilates (CommRing→Ring (BooleanRing→CommRing A)) _ + ∧AnnihilR : x ∧ 𝟘 ≡ 𝟘 + ∧AnnihilR = RingTheory.0RightAnnihilates (CommRing→Ring (BooleanRing→CommRing A)) _ - 0∧LeftAnnihilates : 𝟘 ∧ x ≡ 𝟘 - 0∧LeftAnnihilates = RingTheory.0LeftAnnihilates (CommRing→Ring (BooleanRing→CommRing A)) _ + ∧AnnihilL : 𝟘 ∧ x ≡ 𝟘 + ∧AnnihilL = RingTheory.0LeftAnnihilates (CommRing→Ring (BooleanRing→CommRing A)) _ -IsId : x + x ≡ 𝟘 -IsId {x = x} = RingTheory.+Idempotency→0 (CommRing→Ring (BooleanRing→CommRing A)) (x + x) 2x≡4x @@ -98,21 +98,21 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where 2x≡4x : x + x ≡ (x + x) + (x + x) 2x≡4x = (x + x) - ≡⟨ sym (·IsIdempotent (x + x)) ⟩ + ≡⟨ sym (·Idem (x + x)) ⟩ (x + x) · (x + x) ≡⟨ solve! (BooleanRing→CommRing A) ⟩ ((x · x) + (x · x)) + ((x · x) + (x · x)) - ≡⟨ cong₂ _+_ (cong₂ _+_ (·IsIdempotent x) (·IsIdempotent x)) (cong₂ _+_ (·IsIdempotent x) (·IsIdempotent x)) ⟩ + ≡⟨ cong₂ _+_ (cong₂ _+_ (·Idem x) (·Idem x)) (cong₂ _+_ (·Idem x) (·Idem x)) ⟩ (x + x) + (x + x) ∎ - ∨IsIdempotent : x ∨ x ≡ x - ∨IsIdempotent { x = x } = + ∨Idem : x ∨ x ≡ x + ∨Idem { x = x } = x + x + x · x ≡⟨ cong (λ y → y + x · x) -IsId ⟩ 𝟘 + x · x ≡⟨ +IdL (x · x) ⟩ x · x - ≡⟨ ·IsIdempotent x ⟩ + ≡⟨ ·Idem x ⟩ x ∎ 1Absorbs∨R : x ∨ 𝟙 ≡ 𝟙 @@ -128,25 +128,25 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where 1Absorbs∨L : 𝟙 ∨ x ≡ 𝟙 1Absorbs∨L {x = x} = ∨Comm ∙ 1Absorbs∨R - ∧Distr∨L : x ∧ ( y ∨ z) ≡ (x ∧ y) ∨ (x ∧ z) - ∧Distr∨L {x = x} {y = y} { z = z} = + ∧DistR∨ : x ∧ ( y ∨ z) ≡ (x ∧ y) ∨ (x ∧ z) + ∧DistR∨ {x = x} {y = y} { z = z} = x · ((y + z) + (y · z)) ≡⟨ solve! (BooleanRing→CommRing A) ⟩ x · y + x · z + x · (y · z) - ≡⟨ cong (λ a → x · y + x · z + a · (y · z)) (sym (·IsIdempotent x)) ⟩ + ≡⟨ cong (λ a → x · y + x · z + a · (y · z)) (sym (·Idem x)) ⟩ x · y + x · z + x · x · (y · z) ≡⟨ solve! (BooleanRing→CommRing A) ⟩ x · y + x · z + (x · y) · (x · z) ∎ - ∧Distr∨R : (x ∨ y) ∧ z ≡ (x ∧ z) ∨ (y ∧ z) - ∧Distr∨R = ∧Comm ∙ ∧Distr∨L ∙ cong₂ _∨_ ∧Comm ∧Comm + ∧DistL∨ : (x ∨ y) ∧ z ≡ (x ∧ z) ∨ (y ∧ z) + ∧DistL∨ = ∧Comm ∙ ∧DistR∨ ∙ cong₂ _∨_ ∧Comm ∧Comm - ∨Distr∧L : x ∨ (y ∧ z) ≡ (x ∨ y) ∧ (x ∨ z) - ∨Distr∧L {x = x} {y = y} {z = z} = + ∨DistR∧ : x ∨ (y ∧ z) ≡ (x ∨ y) ∧ (x ∨ z) + ∨DistR∧ {x = x} {y = y} {z = z} = x + (y · z) + x · (y · z) ≡⟨ solve! (BooleanRing→CommRing A) ⟩ x + 𝟘 + 𝟘 + y · z + 𝟘 + x · y · z - ≡⟨ cong (λ a → a + 𝟘 + 𝟘 + y · z + 𝟘 + a · y · z) (sym (·IsIdempotent x)) ⟩ + ≡⟨ cong (λ a → a + 𝟘 + 𝟘 + y · z + 𝟘 + a · y · z) (sym (·Idem x)) ⟩ x · x + 𝟘 + 𝟘 + y · z + 𝟘 + x · x · y · z ≡⟨ cong (λ a → x · x + 𝟘 + 𝟘 + y · z + a + x · x · y · z) (sym (-IsId {x = (x · y) · z})) ⟩ x · x + 𝟘 + 𝟘 + y · z + (x · y · z + x · y · z) + x · x · y · z @@ -155,36 +155,36 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where ≡⟨ solve! (BooleanRing→CommRing A) ⟩ (x + y + x · y) · (x + z + x · z) ∎ where xa≡xxa : (a : ⟨ A ⟩) → x · a ≡ (x · x ) · a - xa≡xxa a = cong (λ y → y · a) (sym (·IsIdempotent x)) + xa≡xxa a = cong (λ y → y · a) (sym (·Idem x)) xa-xxa≡0 : (a : ⟨ A ⟩) → 𝟘 ≡ x · a + x · x · a xa-xxa≡0 a = 𝟘 ≡⟨ sym -IsId ⟩ x · a + x · a - ≡⟨ cong (λ y → x · a + y · a) (sym (·IsIdempotent x)) ⟩ + ≡⟨ cong (λ y → x · a + y · a) (sym (·Idem x)) ⟩ x · a + x · x · a ∎ ∨Distr∧R : (x ∧ y) ∨ z ≡ (x ∨ z) ∧ (y ∨ z) - ∨Distr∧R = ∨Comm ∙ ∨Distr∧L ∙ cong₂ _∧_ ∨Comm ∨Comm + ∨Distr∧R = ∨Comm ∙ ∨DistR∧ ∙ cong₂ _∧_ ∨Comm ∨Comm - ∨Absorps∧L : x ∧ (x ∨ y) ≡ x - ∨Absorps∧L {x = x} {y = y} = + ∧AbsorbL∨ : x ∧ (x ∨ y) ≡ x + ∧AbsorbL∨ {x = x} {y = y} = x · ((x + y) + (x · y)) ≡⟨ solve! (BooleanRing→CommRing A) ⟩ x · x + (x · y + x · x · y) - ≡⟨ cong (λ z → z + ((x · y) + (z · y))) (·IsIdempotent x) ⟩ + ≡⟨ cong (λ z → z + ((x · y) + (z · y))) (·Idem x) ⟩ x + (x · y + x · y) ≡⟨ cong (_+_ x) -IsId ⟩ (x + 𝟘) ≡⟨ +IdR x ⟩ x ∎ - ∧Absorps∨L : x ∨ (x ∧ y) ≡ x - ∧Absorps∨L {x = x} { y = y} = + ∨AbsorbL∧ : x ∨ (x ∧ y) ≡ x + ∨AbsorbL∧ {x = x} { y = y} = x + x · y + x · (x · y) ≡⟨ solve! (BooleanRing→CommRing A) ⟩ x + (x · y + x · x · y) - ≡⟨ cong (λ z → x + (x · y + z · y)) (·IsIdempotent x) ⟩ + ≡⟨ cong (λ z → x + (x · y + z · y)) (·Idem x) ⟩ x + (x · y + x · y) ≡⟨ cong (_+_ x) -IsId ⟩ x + 𝟘 @@ -196,7 +196,7 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where x · (𝟙 + x) ≡⟨ solve! (BooleanRing→CommRing A) ⟩ x + x · x - ≡⟨ cong (λ y → x + y) (·IsIdempotent x) ⟩ + ≡⟨ cong (λ y → x + y) (·Idem x) ⟩ x + x ≡⟨ -IsId ⟩ 𝟘 ∎ @@ -217,8 +217,8 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where ¬Completes∨L : (¬ x) ∨ x ≡ 𝟙 ¬Completes∨L = ∨Comm ∙ ¬Completes∨R - ¬¬ : ¬ ¬ x ≡ x - ¬¬ {x = x} = + ¬Invol : ¬ ¬ x ≡ x + ¬Invol {x = x} = 𝟙 + (𝟙 + x) ≡⟨ +Assoc 𝟙 𝟙 x ⟩ (𝟙 + 𝟙) + x From 433f1bcb1267edd1cdb3e43694d782789911e937 Mon Sep 17 00:00:00 2001 From: Freek Date: Thu, 5 Sep 2024 17:56:47 +0200 Subject: [PATCH 6/6] Added fixities for /\,\/ and neg and removed parentheses --- Cubical/Algebra/BooleanRing/Base.agda | 22 +++++++++++++--------- 1 file changed, 13 insertions(+), 9 deletions(-) diff --git a/Cubical/Algebra/BooleanRing/Base.agda b/Cubical/Algebra/BooleanRing/Base.agda index a64914ebd..cc9c389a4 100644 --- a/Cubical/Algebra/BooleanRing/Base.agda +++ b/Cubical/Algebra/BooleanRing/Base.agda @@ -57,6 +57,10 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where ¬_ : ⟨ A ⟩ → ⟨ A ⟩ ¬ a = 𝟙 + a + infix 8 ¬_ + infixl 7 _∧_ + infixl 6 _∨_ + variable x y z : ⟨ A ⟩ ∧Idem : x ∧ x ≡ x @@ -97,7 +101,7 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where where 2x≡4x : x + x ≡ (x + x) + (x + x) 2x≡4x = - (x + x) + x + x ≡⟨ sym (·Idem (x + x)) ⟩ (x + x) · (x + x) ≡⟨ solve! (BooleanRing→CommRing A) ⟩ @@ -175,7 +179,7 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where ≡⟨ cong (λ z → z + ((x · y) + (z · y))) (·Idem x) ⟩ x + (x · y + x · y) ≡⟨ cong (_+_ x) -IsId ⟩ - (x + 𝟘) + x + 𝟘 ≡⟨ +IdR x ⟩ x ∎ @@ -191,7 +195,7 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where ≡⟨ +IdR x ⟩ x ∎ - ¬Cancels∧R : x ∧ (¬ x) ≡ 𝟘 + ¬Cancels∧R : x ∧ ¬ x ≡ 𝟘 ¬Cancels∧R {x = x} = x · (𝟙 + x) ≡⟨ solve! (BooleanRing→CommRing A) ⟩ @@ -201,12 +205,12 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where ≡⟨ -IsId ⟩ 𝟘 ∎ - ¬Cancels∧L : (¬ x) ∧ x ≡ 𝟘 + ¬Cancels∧L : ¬ x ∧ x ≡ 𝟘 ¬Cancels∧L = ∧Comm ∙ ¬Cancels∧R - ¬Completes∨R : x ∨ (¬ x) ≡ 𝟙 + ¬Completes∨R : x ∨ ¬ x ≡ 𝟙 ¬Completes∨R {x = x} = - x + (¬ x) + (x ∧ (¬ x)) + x + ¬ x + (x ∧ ¬ x) ≡⟨ cong (λ z → x + ¬ x + z) ¬Cancels∧R ⟩ x + ¬ x + 𝟘 ≡⟨ solve! (BooleanRing→CommRing A) ⟩ @@ -233,10 +237,10 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where ¬1≡0 : ¬ 𝟙 ≡ 𝟘 ¬1≡0 = -IsId {x = 𝟙} - DeMorgan¬∨ : ¬ (x ∨ y) ≡ (¬ x) ∧ (¬ y) + DeMorgan¬∨ : ¬ (x ∨ y) ≡ ¬ x ∧ ¬ y DeMorgan¬∨ = solve! (BooleanRing→CommRing A) - DeMorgan¬∧ : ¬ (x ∧ y) ≡ (¬ x) ∨ (¬ y) + DeMorgan¬∧ : ¬ (x ∧ y) ≡ ¬ x ∨ ¬ y DeMorgan¬∧ {x = x} {y = y} = 𝟙 + x · y ≡⟨ solve! (BooleanRing→CommRing A) ⟩ @@ -244,4 +248,4 @@ module BooleanAlgebraStr (A : BooleanRing ℓ) where ≡⟨ cong₂ (λ a b → ((a + b) + 𝟙) + (x · y)) (sym (-IsId {x = 𝟙 + x})) (sym (-IsId {x = y})) ⟩ ((𝟙 + x) + (𝟙 + x)) + (y + y) + 𝟙 + x · y ≡⟨ solve! (BooleanRing→CommRing A) ⟩ - ((¬ x) ∨ (¬ y)) ∎ + ¬ x ∨ ¬ y ∎