------------------------------------------------------------------------
-- The Agda standard library
--
-- A bunch of properties
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Bool.Properties where
open import Algebra.Bundles
using (Magma; Semigroup; Band; CommutativeMonoid
; IdempotentCommutativeMonoid; CommutativeSemiring; CommutativeRing)
open import Algebra.Lattice.Bundles
using (Lattice; DistributiveLattice; BooleanAlgebra; Semilattice)
import Algebra.Lattice.Properties.BooleanAlgebra as BooleanAlgebraProperties
open import Data.Bool.Base
using (Bool; true; false; not; _∧_; _∨_; _xor_ ; if_then_else_; T; _≤_; _<_
; b≤b; f≤t; f<t)
open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
open import Function.Base using (_⟨_⟩_; const; id)
open import Function.Bundles hiding (Inverse; LeftInverse; RightInverse)
open import Induction.WellFounded using (Acc; WellFounded; acc)
open import Level using (0ℓ; Level)
open import Relation.Binary.Bundles using (DecSetoid; DecTotalOrder; Poset;
Preorder; Setoid; StrictPartialOrder; StrictTotalOrder; TotalOrder)
open import Relation.Binary.Core using (_⇒_)
open import Relation.Binary.Structures
using (IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder
; IsStrictPartialOrder; IsStrictTotalOrder)
open import Relation.Binary.Bundles
using (Setoid; DecSetoid; Poset; Preorder; TotalOrder; DecTotalOrder
; StrictPartialOrder; StrictTotalOrder)
open import Relation.Binary.Definitions
using (Decidable; DecidableEquality ; Reflexive; Transitive; Antisymmetric
; Minimum; Maximum; Total; Irrelevant ; Irreflexive; Asymmetric; Trans
; Trichotomous; tri≈; tri<; tri>; _Respects₂_)
open import Relation.Binary.PropositionalEquality.Core
using (_≡_; refl; sym; cong; cong₂; subst; trans; _≢_)
open import Relation.Binary.PropositionalEquality.Properties
using (module ≡-Reasoning; setoid; decSetoid; isEquivalence)
open import Relation.Nullary.Decidable.Core
using (True; yes; no; fromWitness ; toWitness)
open import Relation.Nullary.Negation.Core using (contradiction)
import Relation.Unary as U
open import Algebra.Definitions {A = Bool} _≡_
open import Algebra.Structures {A = Bool} _≡_
open import Algebra.Lattice.Structures {A = Bool} _≡_
open ≡-Reasoning
private
variable
a b : Level
A : Set a
B : Set b
------------------------------------------------------------------------
-- Properties of _≡_
infix 4 _≟_
_≟_ : DecidableEquality Bool
true ≟ true = yes refl
false ≟ false = yes refl
true ≟ false = no λ()
false ≟ true = no λ()
≡-setoid : Setoid 0ℓ 0ℓ
≡-setoid = setoid Bool
≡-decSetoid : DecSetoid 0ℓ 0ℓ
≡-decSetoid = decSetoid _≟_
------------------------------------------------------------------------
-- Properties of _≤_
-- Relational properties
≤-reflexive : _≡_ ⇒ _≤_
≤-reflexive refl = b≤b
≤-refl : Reflexive _≤_
≤-refl = ≤-reflexive refl
≤-trans : Transitive _≤_
≤-trans b≤b p = p
≤-trans f≤t b≤b = f≤t
≤-antisym : Antisymmetric _≡_ _≤_
≤-antisym b≤b _ = refl
≤-minimum : Minimum _≤_ false
≤-minimum false = b≤b
≤-minimum true = f≤t
≤-maximum : Maximum _≤_ true
≤-maximum false = f≤t
≤-maximum true = b≤b
≤-total : Total _≤_
≤-total false b = inj₁ (≤-minimum b)
≤-total true b = inj₂ (≤-maximum b)
infix 4 _≤?_
_≤?_ : Decidable _≤_
false ≤? b = yes (≤-minimum b)
true ≤? false = no λ ()
true ≤? true = yes b≤b
≤-irrelevant : Irrelevant _≤_
≤-irrelevant {_} f≤t f≤t = refl
≤-irrelevant {false} b≤b b≤b = refl
≤-irrelevant {true} b≤b b≤b = refl
-- Structures
≤-isPreorder : IsPreorder _≡_ _≤_
≤-isPreorder = record
{ isEquivalence = isEquivalence
; reflexive = ≤-reflexive
; trans = ≤-trans
}
≤-isPartialOrder : IsPartialOrder _≡_ _≤_
≤-isPartialOrder = record
{ isPreorder = ≤-isPreorder
; antisym = ≤-antisym
}
≤-isTotalOrder : IsTotalOrder _≡_ _≤_
≤-isTotalOrder = record
{ isPartialOrder = ≤-isPartialOrder
; total = ≤-total
}
≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_
≤-isDecTotalOrder = record
{ isTotalOrder = ≤-isTotalOrder
; _≟_ = _≟_
; _≤?_ = _≤?_
}
-- Bundles
≤-poset : Poset 0ℓ 0ℓ 0ℓ
≤-poset = record
{ isPartialOrder = ≤-isPartialOrder
}
≤-preorder : Preorder 0ℓ 0ℓ 0ℓ
≤-preorder = record
{ isPreorder = ≤-isPreorder
}
≤-totalOrder : TotalOrder 0ℓ 0ℓ 0ℓ
≤-totalOrder = record
{ isTotalOrder = ≤-isTotalOrder
}
≤-decTotalOrder : DecTotalOrder 0ℓ 0ℓ 0ℓ
≤-decTotalOrder = record
{ isDecTotalOrder = ≤-isDecTotalOrder
}
------------------------------------------------------------------------
-- Properties of _<_
-- Relational properties
<-irrefl : Irreflexive _≡_ _<_
<-irrefl refl ()
<-asym : Asymmetric _<_
<-asym f<t ()
<-trans : Transitive _<_
<-trans f<t ()
<-transʳ : Trans _≤_ _<_ _<_
<-transʳ b≤b f<t = f<t
<-transˡ : Trans _<_ _≤_ _<_
<-transˡ f<t b≤b = f<t
<-cmp : Trichotomous _≡_ _<_
<-cmp false false = tri≈ (λ()) refl (λ())
<-cmp false true = tri< f<t (λ()) (λ())
<-cmp true false = tri> (λ()) (λ()) f<t
<-cmp true true = tri≈ (λ()) refl (λ())
infix 4 _<?_
_<?_ : Decidable _<_
false <? false = no (λ())
false <? true = yes f<t
true <? _ = no (λ())
<-resp₂-≡ : _<_ Respects₂ _≡_
<-resp₂-≡ = subst (_ <_) , subst (_< _)
<-irrelevant : Irrelevant _<_
<-irrelevant f<t f<t = refl
<-wellFounded : WellFounded _<_
<-wellFounded _ = acc <-acc
where
<-acc : ∀ {x y} → y < x → Acc _<_ y
<-acc f<t = acc λ ()
-- Structures
<-isStrictPartialOrder : IsStrictPartialOrder _≡_ _<_
<-isStrictPartialOrder = record
{ isEquivalence = isEquivalence
; irrefl = <-irrefl
; trans = <-trans
; <-resp-≈ = <-resp₂-≡
}
<-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
<-isStrictTotalOrder = record
{ isStrictPartialOrder = <-isStrictPartialOrder
; compare = <-cmp
}
-- Bundles
<-strictPartialOrder : StrictPartialOrder 0ℓ 0ℓ 0ℓ
<-strictPartialOrder = record
{ isStrictPartialOrder = <-isStrictPartialOrder
}
<-strictTotalOrder : StrictTotalOrder 0ℓ 0ℓ 0ℓ
<-strictTotalOrder = record
{ isStrictTotalOrder = <-isStrictTotalOrder
}
------------------------------------------------------------------------
-- Properties of _∨_
∨-assoc : Associative _∨_
∨-assoc true y z = refl
∨-assoc false y z = refl
∨-comm : Commutative _∨_
∨-comm true true = refl
∨-comm true false = refl
∨-comm false true = refl
∨-comm false false = refl
∨-identityˡ : LeftIdentity false _∨_
∨-identityˡ _ = refl
∨-identityʳ : RightIdentity false _∨_
∨-identityʳ false = refl
∨-identityʳ true = refl
∨-identity : Identity false _∨_
∨-identity = ∨-identityˡ , ∨-identityʳ
∨-zeroˡ : LeftZero true _∨_
∨-zeroˡ _ = refl
∨-zeroʳ : RightZero true _∨_
∨-zeroʳ false = refl
∨-zeroʳ true = refl
∨-zero : Zero true _∨_
∨-zero = ∨-zeroˡ , ∨-zeroʳ
∨-inverseˡ : LeftInverse true not _∨_
∨-inverseˡ false = refl
∨-inverseˡ true = refl
∨-inverseʳ : RightInverse true not _∨_
∨-inverseʳ x = ∨-comm x (not x) ⟨ trans ⟩ ∨-inverseˡ x
∨-inverse : Inverse true not _∨_
∨-inverse = ∨-inverseˡ , ∨-inverseʳ
∨-idem : Idempotent _∨_
∨-idem false = refl
∨-idem true = refl
∨-sel : Selective _∨_
∨-sel false y = inj₂ refl
∨-sel true y = inj₁ refl
∨-conicalˡ : LeftConical false _∨_
∨-conicalˡ false false _ = refl
∨-conicalʳ : RightConical false _∨_
∨-conicalʳ false false _ = refl
∨-conical : Conical false _∨_
∨-conical = ∨-conicalˡ , ∨-conicalʳ
∨-isMagma : IsMagma _∨_
∨-isMagma = record
{ isEquivalence = isEquivalence
; ∙-cong = cong₂ _∨_
}
∨-magma : Magma 0ℓ 0ℓ
∨-magma = record
{ isMagma = ∨-isMagma
}
∨-isSemigroup : IsSemigroup _∨_
∨-isSemigroup = record
{ isMagma = ∨-isMagma
; assoc = ∨-assoc
}
∨-semigroup : Semigroup 0ℓ 0ℓ
∨-semigroup = record
{ isSemigroup = ∨-isSemigroup
}
∨-isBand : IsBand _∨_
∨-isBand = record
{ isSemigroup = ∨-isSemigroup
; idem = ∨-idem
}
∨-band : Band 0ℓ 0ℓ
∨-band = record
{ isBand = ∨-isBand
}
∨-isSemilattice : IsSemilattice _∨_
∨-isSemilattice = record
{ isBand = ∨-isBand
; comm = ∨-comm
}
∨-semilattice : Semilattice 0ℓ 0ℓ
∨-semilattice = record
{ isSemilattice = ∨-isSemilattice
}
∨-isMonoid : IsMonoid _∨_ false
∨-isMonoid = record
{ isSemigroup = ∨-isSemigroup
; identity = ∨-identity
}
∨-isCommutativeMonoid : IsCommutativeMonoid _∨_ false
∨-isCommutativeMonoid = record
{ isMonoid = ∨-isMonoid
; comm = ∨-comm
}
∨-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
∨-commutativeMonoid = record
{ isCommutativeMonoid = ∨-isCommutativeMonoid
}
∨-isIdempotentCommutativeMonoid :
IsIdempotentCommutativeMonoid _∨_ false
∨-isIdempotentCommutativeMonoid = record
{ isCommutativeMonoid = ∨-isCommutativeMonoid
; idem = ∨-idem
}
∨-idempotentCommutativeMonoid : IdempotentCommutativeMonoid 0ℓ 0ℓ
∨-idempotentCommutativeMonoid = record
{ isIdempotentCommutativeMonoid = ∨-isIdempotentCommutativeMonoid
}
------------------------------------------------------------------------
-- Properties of _∧_
∧-assoc : Associative _∧_
∧-assoc true y z = refl
∧-assoc false y z = refl
∧-comm : Commutative _∧_
∧-comm true true = refl
∧-comm true false = refl
∧-comm false true = refl
∧-comm false false = refl
∧-identityˡ : LeftIdentity true _∧_
∧-identityˡ _ = refl
∧-identityʳ : RightIdentity true _∧_
∧-identityʳ false = refl
∧-identityʳ true = refl
∧-identity : Identity true _∧_
∧-identity = ∧-identityˡ , ∧-identityʳ
∧-zeroˡ : LeftZero false _∧_
∧-zeroˡ _ = refl
∧-zeroʳ : RightZero false _∧_
∧-zeroʳ false = refl
∧-zeroʳ true = refl
∧-zero : Zero false _∧_
∧-zero = ∧-zeroˡ , ∧-zeroʳ
∧-inverseˡ : LeftInverse false not _∧_
∧-inverseˡ false = refl
∧-inverseˡ true = refl
∧-inverseʳ : RightInverse false not _∧_
∧-inverseʳ x = ∧-comm x (not x) ⟨ trans ⟩ ∧-inverseˡ x
∧-inverse : Inverse false not _∧_
∧-inverse = ∧-inverseˡ , ∧-inverseʳ
∧-idem : Idempotent _∧_
∧-idem false = refl
∧-idem true = refl
∧-sel : Selective _∧_
∧-sel false y = inj₁ refl
∧-sel true y = inj₂ refl
∧-conicalˡ : LeftConical true _∧_
∧-conicalˡ true true _ = refl
∧-conicalʳ : RightConical true _∧_
∧-conicalʳ true true _ = refl
∧-conical : Conical true _∧_
∧-conical = ∧-conicalˡ , ∧-conicalʳ
∧-distribˡ-∨ : _∧_ DistributesOverˡ _∨_
∧-distribˡ-∨ true y z = refl
∧-distribˡ-∨ false y z = refl
∧-distribʳ-∨ : _∧_ DistributesOverʳ _∨_
∧-distribʳ-∨ x y z = begin
(y ∨ z) ∧ x ≡⟨ ∧-comm (y ∨ z) x ⟩
x ∧ (y ∨ z) ≡⟨ ∧-distribˡ-∨ x y z ⟩
x ∧ y ∨ x ∧ z ≡⟨ cong₂ _∨_ (∧-comm x y) (∧-comm x z) ⟩
y ∧ x ∨ z ∧ x ∎
∧-distrib-∨ : _∧_ DistributesOver _∨_
∧-distrib-∨ = ∧-distribˡ-∨ , ∧-distribʳ-∨
∨-distribˡ-∧ : _∨_ DistributesOverˡ _∧_
∨-distribˡ-∧ true y z = refl
∨-distribˡ-∧ false y z = refl
∨-distribʳ-∧ : _∨_ DistributesOverʳ _∧_
∨-distribʳ-∧ x y z = begin
(y ∧ z) ∨ x ≡⟨ ∨-comm (y ∧ z) x ⟩
x ∨ (y ∧ z) ≡⟨ ∨-distribˡ-∧ x y z ⟩
(x ∨ y) ∧ (x ∨ z) ≡⟨ cong₂ _∧_ (∨-comm x y) (∨-comm x z) ⟩
(y ∨ x) ∧ (z ∨ x) ∎
∨-distrib-∧ : _∨_ DistributesOver _∧_
∨-distrib-∧ = ∨-distribˡ-∧ , ∨-distribʳ-∧
∧-abs-∨ : _∧_ Absorbs _∨_
∧-abs-∨ true y = refl
∧-abs-∨ false y = refl
∨-abs-∧ : _∨_ Absorbs _∧_
∨-abs-∧ true y = refl
∨-abs-∧ false y = refl
∨-∧-absorptive : Absorptive _∨_ _∧_
∨-∧-absorptive = ∨-abs-∧ , ∧-abs-∨
∧-isMagma : IsMagma _∧_
∧-isMagma = record
{ isEquivalence = isEquivalence
; ∙-cong = cong₂ _∧_
}
∧-magma : Magma 0ℓ 0ℓ
∧-magma = record
{ isMagma = ∧-isMagma
}
∧-isSemigroup : IsSemigroup _∧_
∧-isSemigroup = record
{ isMagma = ∧-isMagma
; assoc = ∧-assoc
}
∧-semigroup : Semigroup 0ℓ 0ℓ
∧-semigroup = record
{ isSemigroup = ∧-isSemigroup
}
∧-isBand : IsBand _∧_
∧-isBand = record
{ isSemigroup = ∧-isSemigroup
; idem = ∧-idem
}
∧-band : Band 0ℓ 0ℓ
∧-band = record
{ isBand = ∧-isBand
}
∧-isSemilattice : IsSemilattice _∧_
∧-isSemilattice = record
{ isBand = ∧-isBand
; comm = ∧-comm
}
∧-semilattice : Semilattice 0ℓ 0ℓ
∧-semilattice = record
{ isSemilattice = ∧-isSemilattice
}
∧-isMonoid : IsMonoid _∧_ true
∧-isMonoid = record
{ isSemigroup = ∧-isSemigroup
; identity = ∧-identity
}
∧-isCommutativeMonoid : IsCommutativeMonoid _∧_ true
∧-isCommutativeMonoid = record
{ isMonoid = ∧-isMonoid
; comm = ∧-comm
}
∧-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
∧-commutativeMonoid = record
{ isCommutativeMonoid = ∧-isCommutativeMonoid
}
∧-isIdempotentCommutativeMonoid :
IsIdempotentCommutativeMonoid _∧_ true
∧-isIdempotentCommutativeMonoid = record
{ isCommutativeMonoid = ∧-isCommutativeMonoid
; idem = ∧-idem
}
∧-idempotentCommutativeMonoid : IdempotentCommutativeMonoid 0ℓ 0ℓ
∧-idempotentCommutativeMonoid = record
{ isIdempotentCommutativeMonoid = ∧-isIdempotentCommutativeMonoid
}
∨-∧-isSemiring : IsSemiring _∨_ _∧_ false true
∨-∧-isSemiring = record
{ isSemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = ∨-isCommutativeMonoid
; *-cong = cong₂ _∧_
; *-assoc = ∧-assoc
; *-identity = ∧-identity
; distrib = ∧-distrib-∨
}
; zero = ∧-zero
}
∨-∧-isCommutativeSemiring
: IsCommutativeSemiring _∨_ _∧_ false true
∨-∧-isCommutativeSemiring = record
{ isSemiring = ∨-∧-isSemiring
; *-comm = ∧-comm
}
∨-∧-commutativeSemiring : CommutativeSemiring 0ℓ 0ℓ
∨-∧-commutativeSemiring = record
{ _+_ = _∨_
; _*_ = _∧_
; 0# = false
; 1# = true
; isCommutativeSemiring = ∨-∧-isCommutativeSemiring
}
∧-∨-isSemiring : IsSemiring _∧_ _∨_ true false
∧-∨-isSemiring = record
{ isSemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = ∧-isCommutativeMonoid
; *-cong = cong₂ _∨_
; *-assoc = ∨-assoc
; *-identity = ∨-identity
; distrib = ∨-distrib-∧
}
; zero = ∨-zero
}
∧-∨-isCommutativeSemiring
: IsCommutativeSemiring _∧_ _∨_ true false
∧-∨-isCommutativeSemiring = record
{ isSemiring = ∧-∨-isSemiring
; *-comm = ∨-comm
}
∧-∨-commutativeSemiring : CommutativeSemiring 0ℓ 0ℓ
∧-∨-commutativeSemiring = record
{ _+_ = _∧_
; _*_ = _∨_
; 0# = true
; 1# = false
; isCommutativeSemiring = ∧-∨-isCommutativeSemiring
}
∨-∧-isLattice : IsLattice _∨_ _∧_
∨-∧-isLattice = record
{ isEquivalence = isEquivalence
; ∨-comm = ∨-comm
; ∨-assoc = ∨-assoc
; ∨-cong = cong₂ _∨_
; ∧-comm = ∧-comm
; ∧-assoc = ∧-assoc
; ∧-cong = cong₂ _∧_
; absorptive = ∨-∧-absorptive
}
∨-∧-lattice : Lattice 0ℓ 0ℓ
∨-∧-lattice = record
{ isLattice = ∨-∧-isLattice
}
∨-∧-isDistributiveLattice : IsDistributiveLattice _∨_ _∧_
∨-∧-isDistributiveLattice = record
{ isLattice = ∨-∧-isLattice
; ∨-distrib-∧ = ∨-distrib-∧
; ∧-distrib-∨ = ∧-distrib-∨
}
∨-∧-distributiveLattice : DistributiveLattice 0ℓ 0ℓ
∨-∧-distributiveLattice = record
{ isDistributiveLattice = ∨-∧-isDistributiveLattice
}
∨-∧-isBooleanAlgebra : IsBooleanAlgebra _∨_ _∧_ not true false
∨-∧-isBooleanAlgebra = record
{ isDistributiveLattice = ∨-∧-isDistributiveLattice
; ∨-complement = ∨-inverse
; ∧-complement = ∧-inverse
; ¬-cong = cong not
}
∨-∧-booleanAlgebra : BooleanAlgebra 0ℓ 0ℓ
∨-∧-booleanAlgebra = record
{ isBooleanAlgebra = ∨-∧-isBooleanAlgebra
}
------------------------------------------------------------------------
-- Properties of not
not-involutive : Involutive not
not-involutive true = refl
not-involutive false = refl
not-injective : ∀ {x y} → not x ≡ not y → x ≡ y
not-injective {false} {false} nx≢ny = refl
not-injective {true} {true} nx≢ny = refl
not-¬ : ∀ {x y} → x ≡ y → x ≢ not y
not-¬ {true} refl ()
not-¬ {false} refl ()
¬-not : ∀ {x y} → x ≢ y → x ≡ not y
¬-not {true} {true} x≢y = contradiction refl x≢y
¬-not {true} {false} _ = refl
¬-not {false} {true} _ = refl
¬-not {false} {false} x≢y = contradiction refl x≢y
------------------------------------------------------------------------
-- Properties of _xor_
xor-is-ok : ∀ x y → x xor y ≡ (x ∨ y) ∧ not (x ∧ y)
xor-is-ok true y = refl
xor-is-ok false y = sym (∧-identityʳ _)
true-xor : ∀ x → true xor x ≡ not x
true-xor false = refl
true-xor true = refl
xor-same : ∀ x → x xor x ≡ false
xor-same false = refl
xor-same true = refl
not-distribˡ-xor : ∀ x y → not (x xor y) ≡ (not x) xor y
not-distribˡ-xor false y = refl
not-distribˡ-xor true y = not-involutive _
not-distribʳ-xor : ∀ x y → not (x xor y) ≡ x xor (not y)
not-distribʳ-xor false y = refl
not-distribʳ-xor true y = refl
xor-assoc : Associative _xor_
xor-assoc true y z = sym (not-distribˡ-xor y z)
xor-assoc false y z = refl
xor-comm : Commutative _xor_
xor-comm false false = refl
xor-comm false true = refl
xor-comm true false = refl
xor-comm true true = refl
xor-identityˡ : LeftIdentity false _xor_
xor-identityˡ _ = refl
xor-identityʳ : RightIdentity false _xor_
xor-identityʳ false = refl
xor-identityʳ true = refl
xor-identity : Identity false _xor_
xor-identity = xor-identityˡ , xor-identityʳ
xor-inverseˡ : LeftInverse true not _xor_
xor-inverseˡ false = refl
xor-inverseˡ true = refl
xor-inverseʳ : RightInverse true not _xor_
xor-inverseʳ x = xor-comm x (not x) ⟨ trans ⟩ xor-inverseˡ x
xor-inverse : Inverse true not _xor_
xor-inverse = xor-inverseˡ , xor-inverseʳ
∧-distribˡ-xor : _∧_ DistributesOverˡ _xor_
∧-distribˡ-xor false y z = refl
∧-distribˡ-xor true y z = refl
∧-distribʳ-xor : _∧_ DistributesOverʳ _xor_
∧-distribʳ-xor x false z = refl
∧-distribʳ-xor x true false = sym (xor-identityʳ x)
∧-distribʳ-xor x true true = sym (xor-same x)
∧-distrib-xor : _∧_ DistributesOver _xor_
∧-distrib-xor = ∧-distribˡ-xor , ∧-distribʳ-xor
xor-annihilates-not : ∀ x y → (not x) xor (not y) ≡ x xor y
xor-annihilates-not false y = not-involutive _
xor-annihilates-not true y = refl
xor-∧-commutativeRing : CommutativeRing 0ℓ 0ℓ
xor-∧-commutativeRing = ⊕-∧-commutativeRing
where
open BooleanAlgebraProperties ∨-∧-booleanAlgebra
open XorRing _xor_ xor-is-ok
------------------------------------------------------------------------
-- Properties of if_then_else_
if-float : ∀ (f : A → B) b {x y} →
f (if b then x else y) ≡ (if b then f x else f y)
if-float _ true = refl
if-float _ false = refl
if-eta : ∀ b {x : A} →
(if b then x else x) ≡ x
if-eta false = refl
if-eta true = refl
if-idem-then : ∀ b {x y : A} →
(if b then (if b then x else y) else y)
≡ (if b then x else y)
if-idem-then false = refl
if-idem-then true = refl
if-idem-else : ∀ b {x y : A} →
(if b then x else (if b then x else y))
≡ (if b then x else y)
if-idem-else false = refl
if-idem-else true = refl
if-swap-then : ∀ b c {x y : A} →
(if b then (if c then x else y) else y)
≡ (if c then (if b then x else y) else y)
if-swap-then false false = refl
if-swap-then false true = refl
if-swap-then true _ = refl
if-swap-else : ∀ b c {x y : A} →
(if b then x else (if c then x else y))
≡ (if c then x else (if b then x else y))
if-swap-else false _ = refl
if-swap-else true false = refl
if-swap-else true true = refl
if-not : ∀ b {x y : A} →
(if not b then x else y) ≡ (if b then y else x)
if-not false = refl
if-not true = refl
if-∧ : ∀ b {c} {x y : A} →
(if b ∧ c then x else y) ≡ (if b then (if c then x else y) else y)
if-∧ false = refl
if-∧ true = refl
if-∨ : ∀ b {c} {x y : A} →
(if b ∨ c then x else y) ≡ (if b then x else (if c then x else y))
if-∨ false = refl
if-∨ true = refl
if-xor : ∀ b {c} {x y : A} →
(if b xor c then x else y)
≡ (if b then (if c then y else x) else (if c then x else y))
if-xor false = refl
if-xor true {false} = refl
if-xor true {true } = refl
-- The following congruence lemmas are short hands for
-- cong (if_then x else y)
-- cong (if b then_else y)
-- cong (if b then x else_)
-- cong (if b then_else_)
-- on the different sub-terms in an if_then_else_ expression.
-- With these short hands, the branches x and y can be inferred
-- automatically (i.e., they are implicit arguments) whereas
-- the branches have to be spelled out explicitly when using cong.
-- (Using underscores as in "cong (if b then _ else_)"
-- unfortunately fails to resolve the omitted argument.)
if-cong : ∀ {b c} {x y : A} → b ≡ c →
(if b then x else y)
≡ (if c then x else y)
if-cong refl = refl
if-cong-then : ∀ b {x y z : A} → x ≡ z →
(if b then x else y)
≡ (if b then z else y)
if-cong-then _ refl = refl
if-cong-else : ∀ b {x y z : A} → y ≡ z →
(if b then x else y)
≡ (if b then x else z)
if-cong-else _ refl = refl
if-cong₂ : ∀ b {x y z w : A} → x ≡ z → y ≡ w →
(if b then x else y)
≡ (if b then z else w)
if-cong₂ _ refl refl = refl
------------------------------------------------------------------------
-- Properties of T
open Relation.Nullary.Decidable.Core public using (T?)
T-≡ : ∀ {x} → T x ⇔ x ≡ true
T-≡ {false} = mk⇔ (λ ()) (λ ())
T-≡ {true} = mk⇔ (const refl) (const _)
T-not-≡ : ∀ {x} → T (not x) ⇔ x ≡ false
T-not-≡ {false} = mk⇔ (const refl) (const _)
T-not-≡ {true} = mk⇔ (λ ()) (λ ())
T-∧ : ∀ {x y} → T (x ∧ y) ⇔ (T x × T y)
T-∧ {true} {true} = mk⇔ (const (_ , _)) (const _)
T-∧ {true} {false} = mk⇔ (λ ()) proj₂
T-∧ {false} {_} = mk⇔ (λ ()) proj₁
T-∨ : ∀ {x y} → T (x ∨ y) ⇔ (T x ⊎ T y)
T-∨ {true} {_} = mk⇔ inj₁ (const _)
T-∨ {false} {true} = mk⇔ inj₂ (const _)
T-∨ {false} {false} = mk⇔ inj₁ [ id , id ]
T-irrelevant : U.Irrelevant T
T-irrelevant {true} _ _ = refl
T?-diag : ∀ b → T b → True (T? b)
T?-diag b = fromWitness
------------------------------------------------------------------------
-- Miscellaneous other properties
⇔→≡ : {x y z : Bool} → x ≡ z ⇔ y ≡ z → x ≡ y
⇔→≡ {true } {true } hyp = refl
⇔→≡ {true } {false} {true } hyp = sym (Equivalence.to hyp refl)
⇔→≡ {true } {false} {false} hyp = Equivalence.from hyp refl
⇔→≡ {false} {true } {true } hyp = Equivalence.from hyp refl
⇔→≡ {false} {true } {false} hyp = sym (Equivalence.to hyp refl)
⇔→≡ {false} {false} hyp = refl
------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.
-- Version 2.0
push-function-into-if = if-float
{-# WARNING_ON_USAGE push-function-into-if
"Warning: push-function-into-if was deprecated in v2.0.
Please use if-float instead."
#-}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4