open import Tools.Bool using (Bool; true; false; if_then_else_; T)
module Graded.Modality.Instances.Zero-one-many
(πβ€π : Bool)
where
import Tools.Algebra
open import Tools.Function
open import Tools.Level
open import Tools.Nullary
open import Tools.Product
open import Tools.PropositionalEquality as PE
import Tools.Reasoning.PartialOrder
import Tools.Reasoning.PropositionalEquality
open import Tools.Sum using (_β_; injβ; injβ)
import Graded.Modality
import Graded.Modality.Instances.LowerBounded as LowerBounded
import Graded.Modality.Properties.Addition as Addition
import Graded.Modality.Properties.Meet as Meet
import Graded.Modality.Properties.Multiplication as Multiplication
import Graded.Modality.Properties.PartialOrder as PartialOrder
import Graded.Modality.Properties.Star as Star
open import Graded.Modality.Variant lzero
data Zero-one-many : Set where
π π Ο : Zero-one-many
private variable
p pβ pβ q r : Zero-one-many
open Graded.Modality Zero-one-many
open Tools.Algebra Zero-one-many
Meet-requirements :
(Zero-one-many β Zero-one-many β Zero-one-many) β Set
Meet-requirements _β§_ =
(π β§ π β‘ π) Γ
(π β§ π β‘ π) Γ
(Ο β§ Ο β‘ Ο) Γ
(π β§ Ο β‘ Ο) Γ
(Ο β§ π β‘ Ο) Γ
(π β§ Ο β‘ Ο) Γ
(Ο β§ π β‘ Ο) Γ
(π β§ π β’ π) Γ
(π β§ π β’ π)
Meet-requirements-required :
(M : Semiring-with-meet) β
Semiring-with-meet.π M β‘ π β
Semiring-with-meet.π M β‘ π β
Semiring-with-meet._β§_ M π π β’ π β
(β p β Semiring-with-meet._β€_ M Ο p) β
Meet-requirements (Semiring-with-meet._β§_ M)
Meet-requirements-required M refl refl πβ§πβ’π Οβ€ =
(π β§ π β‘β¨ β§-idem _ β©
π β)
, (π β§ π β‘β¨ β§-idem _ β©
π β)
, (Ο β§ Ο β‘β¨ β§-idem _ β©
Ο β)
, (π β§ Ο β‘β¨ β§-comm _ _ β©
Ο β§ π β‘Λβ¨ Οβ€ π β©
Ο β)
, (Ο β§ π β‘Λβ¨ Οβ€ π β©
Ο β)
, (π β§ Ο β‘β¨ β§-comm _ _ β©
Ο β§ π β‘Λβ¨ Οβ€ π β©
Ο β)
, (Ο β§ π β‘Λβ¨ Οβ€ π β©
Ο β)
, πβ§πβ’π
, (Ξ» πβ§πβ‘π β πβ§πβ’π (
π β§ π β‘β¨ β§-comm _ _ β©
π β§ π β‘β¨ πβ§πβ‘π β©
π β))
where
open Semiring-with-meet M hiding (π; π)
open Meet M
open PartialOrder M
open Tools.Reasoning.PropositionalEquality
πβ§π : Zero-one-many
πβ§π = if πβ€π then π else Ο
infixr 40 _β§_
_β§_ : Zero-one-many β Zero-one-many β Zero-one-many
π β§ π = π
π β§ π = π
π β§ π = πβ§π
π β§ π = πβ§π
_ β§ _ = Ο
πβ§πβ‘π : T πβ€π β πβ§π β‘ π
πβ§πβ‘π = lemma _
where
lemma : β b β T b β (if b then π else Ο) β‘ π
lemma true _ = refl
πβ§πβ‘Ο : Β¬ T πβ€π β πβ§π β‘ Ο
πβ§πβ‘Ο = lemma _
where
lemma : β b β Β¬ T b β (if b then π else Ο) β‘ Ο
lemma false _ = refl
lemma true Β¬β€ = β₯-elim (Β¬β€ _)
πβ§πβ’π : πβ§π β’ π
πβ§πβ’π = lemma _
where
lemma : β b β (if b then π else Ο) β’ π
lemma false ()
lemma true ()
πβ§π-elim :
β {p} (P : Zero-one-many β Set p) β
(πβ§π β‘ π β P π) β
(πβ§π β‘ Ο β P Ο) β
P πβ§π
πβ§π-elim P one omega = lemma _ refl
where
lemma : β p β πβ§π β‘ p β P p
lemma π πβ§πβ‘π = β₯-elim (πβ§πβ’π πβ§πβ‘π)
lemma π πβ§πβ‘π = one πβ§πβ‘π
lemma Ο πβ§πβ‘Ο = omega πβ§πβ‘Ο
πβ§[πβ§π] : π β§ πβ§π β‘ πβ§π
πβ§[πβ§π] = πβ§π-elim
(Ξ» p β π β§ p β‘ p)
(Ξ» πβ§πβ‘π β πβ§πβ‘π)
(Ξ» _ β refl)
πβ§[πβ§π] : π β§ πβ§π β‘ πβ§π
πβ§[πβ§π] = πβ§π-elim
(Ξ» p β π β§ p β‘ p)
(Ξ» _ β refl)
(Ξ» _ β refl)
Order-requirements : (Zero-one-many β Zero-one-many β Set) β Set
Order-requirements _β€_ = (Ο β€ π) Γ (Ο β€ π) Γ Β¬ (π β€ π)
Order-requirements-required :
(M : Semiring-with-meet) β
Semiring-with-meet.π M β‘ π β
Semiring-with-meet.π M β‘ π β
Semiring-with-meet._β§_ M π π β’ π β
(β p β Semiring-with-meet._β€_ M Ο p) β
Order-requirements (Semiring-with-meet._β€_ M)
Order-requirements-required M refl refl πβ§πβ’π Οβ€ =
case Meet-requirements-required M refl refl πβ§πβ’π Οβ€ of Ξ» where
(_ , _ , _ , _ , Οβπβ‘Ο , _ , Οβπβ‘Ο , πβπβ’π , _) β
(Ο β‘Λβ¨ Οβπβ‘Ο β©
Ο β π β)
, (Ο β‘Λβ¨ Οβπβ‘Ο β©
Ο β π β)
, (Ξ» πβ‘πβπ β πβπβ’π (
π β π β‘Λβ¨ πβ‘πβπ β©
π β))
where
open Semiring-with-meet M using () renaming (_β§_ to _β_)
open Tools.Reasoning.PropositionalEquality
infix 10 _β€_
_β€_ : Zero-one-many β Zero-one-many β Set
p β€ q = p β‘ p β§ q
Οβ€ : β p β Ο β€ p
Οβ€ _ = refl
π-maximal : π β€ p β p β‘ π
π-maximal {p = π} refl = refl
π-maximal {p = π} = πβ§π-elim
(Ξ» q β π β‘ q β π β‘ π)
(Ξ» _ β sym)
(Ξ» _ ())
πβ°πβ§π : Β¬ π β€ πβ§π
πβ°πβ§π = πβ§πβ’π ββ π-maximal
πβ€πβπβ€π : T πβ€π β π β€ π
πβ€πβπβ€π πβ€π =
π β‘Λβ¨ πβ§πβ‘π πβ€π β©
π β§ π β
where
open Tools.Reasoning.PropositionalEquality
π-maximal : Β¬ T πβ€π β π β€ p β p β‘ π
π-maximal {p = π} _ refl = refl
π-maximal {p = π} πβ°π πβ€π = β₯-elim (
case
π β‘β¨ πβ€π β©
π β§ π β‘β¨ πβ§πβ‘Ο πβ°π β©
Ο β
of Ξ» ())
where
open Tools.Reasoning.PropositionalEquality
infixr 40 _+_
_+_ : Zero-one-many β Zero-one-many β Zero-one-many
π + q = q
π + π = π
_ + _ = Ο
+-decreasingΛ‘ : T πβ€π β β p q β p + q β€ p
+-decreasingΛ‘ πβ€π = Ξ» where
π π β refl
π π β πβ€πβπβ€π πβ€π
π Ο β refl
π π β refl
π π β refl
π Ο β refl
Ο _ β refl
Β¬-+-decreasingΛ‘ : Β¬ T πβ€π β Β¬ (β p q β p + q β€ p)
Β¬-+-decreasingΛ‘ πβ°π hyp =
case π-maximal {p = π} πβ°π (hyp π π) of Ξ» ()
β’π+β’π : p β’ π β q β’ π β p + q β‘ Ο
β’π+β’π {p = π} πβ’π _ = β₯-elim (πβ’π refl)
β’π+β’π {p = π} {q = π} _ πβ’π = β₯-elim (πβ’π refl)
β’π+β’π {p = π} {q = π} _ _ = refl
β’π+β’π {p = π} {q = Ο} _ _ = refl
β’π+β’π {p = Ο} _ _ = refl
+-zeroΚ³ : RightZero Ο _+_
+-zeroΚ³ π = refl
+-zeroΚ³ π = refl
+-zeroΚ³ Ο = refl
+-zero : Zero Ο _+_
+-zero = (Ξ» _ β refl) , +-zeroΚ³
infixr 45 _Β·_
_Β·_ : Zero-one-many β Zero-one-many β Zero-one-many
π Β· _ = π
_ Β· π = π
π Β· π = π
_ Β· _ = Ο
Β·-idempotent : Idempotent _Β·_
Β·-idempotent π = refl
Β·-idempotent π = refl
Β·-idempotent Ο = refl
Β·-comm : Commutative _Β·_
Β·-comm = Ξ» where
π π β refl
π π β refl
π Ο β refl
π π β refl
π π β refl
π Ο β refl
Ο π β refl
Ο π β refl
Ο Ο β refl
ΟΒ·β’π : p β’ π β Ο Β· p β‘ Ο
ΟΒ·β’π {p = π} πβ’π = β₯-elim (πβ’π refl)
ΟΒ·β’π {p = π} _ = refl
ΟΒ·β’π {p = Ο} _ = refl
πΒ·β’π : p β’ π β π Β· p β’ π
πΒ·β’π {p = π} πβ’π = πβ’π
πΒ·β’π {p = π} πβ’π = πβ’π
πΒ·β’π {p = Ο} Οβ’π = Οβ’π
zero-one-many-semiring-with-meet : Semiring-with-meet
zero-one-many-semiring-with-meet = record
{ _+_ = _+_
; _Β·_ = _Β·_
; _β§_ = _β§_
; π = π
; π = π
; +-Β·-Semiring = record
{ isSemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = record
{ isMonoid = record
{ isSemigroup = record
{ isMagma = record
{ isEquivalence = PE.isEquivalence
; β-cong = congβ _+_
}
; assoc = Ξ» where
π _ _ β refl
π π _ β refl
π π π β refl
π π π β refl
π π Ο β refl
π Ο _ β refl
Ο _ _ β refl
}
; identity =
(Ξ» _ β refl)
, comm+idΛ‘βidΚ³ +-comm (Ξ» _ β refl)
}
; comm = +-comm
}
; *-isMonoid = record
{ isSemigroup = record
{ isMagma = record
{ isEquivalence = PE.isEquivalence
; β-cong = congβ _Β·_
}
; assoc = Ξ» where
π _ _ β refl
π π _ β refl
π π π β refl
π π π β refl
π π Ο β refl
π Ο π β refl
π Ο π β refl
π Ο Ο β refl
Ο π _ β refl
Ο π π β refl
Ο π π β refl
Ο π Ο β refl
Ο Ο π β refl
Ο Ο π β refl
Ο Ο Ο β refl
}
; identity =
Β·-identityΛ‘
, comm+idΛ‘βidΚ³ Β·-comm Β·-identityΛ‘
}
; distrib =
Β·-distrib-+Λ‘
, comm+distrΛ‘βdistrΚ³ Β·-comm Β·-distrib-+Λ‘
}
; zero =
(Ξ» _ β refl)
, comm+zeΛ‘βzeΚ³ Β·-comm (Ξ» _ β refl)
}
; β§-Semilattice = record
{ isBand = record
{ isSemigroup = record
{ isMagma = record
{ isEquivalence = PE.isEquivalence
; β-cong = congβ _β§_
}
; assoc = Ξ» where
π π π β refl
π π π β
πβ§π β‘Λβ¨ πβ§[πβ§π] β©
π β§ πβ§π β
π π Ο β refl
π π π β
πβ§π β§ π β‘β¨β©
πβ§π β§ π β‘β¨ β§-comm πβ§π _ β©
π β§ πβ§π β
π π π β
πβ§π β§ π β‘β¨ β§-comm πβ§π _ β©
π β§ πβ§π β‘β¨ πβ§[πβ§π] β©
πβ§π β
π π Ο β
πβ§π β§ Ο β‘β¨ β§-comm πβ§π _ β©
Ο β§ πβ§π β‘β¨β©
Ο β
π Ο _ β refl
π π π β
πβ§π β§ π β‘β¨ β§-comm πβ§π _ β©
π β§ πβ§π β‘β¨ πβ§[πβ§π] β©
πβ§π β
π π π β
πβ§π β§ π β‘β¨β©
πβ§π β§ π β‘β¨ β§-comm πβ§π _ β©
π β§ πβ§π β
π π Ο β
πβ§π β§ Ο β‘β¨ β§-comm πβ§π _ β©
Ο β§ πβ§π β‘β¨β©
Ο β
π π π β
πβ§π β‘Λβ¨ πβ§[πβ§π] β©
π β§ πβ§π β
π π π β refl
π π Ο β refl
π Ο _ β refl
Ο _ _ β refl
}
; idem = Ξ» where
π β refl
π β refl
Ο β refl
}
; comm = β§-comm
}
; Β·-distrib-β§ =
Β·-distrib-β§Λ‘
, comm+distrΛ‘βdistrΚ³ Β·-comm Β·-distrib-β§Λ‘
; +-distrib-β§ =
+-distrib-β§Λ‘
, comm+distrΛ‘βdistrΚ³ +-comm +-distrib-β§Λ‘
}
where
open Tools.Reasoning.PropositionalEquality
+-comm : Commutative _+_
+-comm = Ξ» where
π π β refl
π π β refl
π Ο β refl
π π β refl
π π β refl
π Ο β refl
Ο π β refl
Ο π β refl
Ο Ο β refl
Β·-identityΛ‘ : LeftIdentity π _Β·_
Β·-identityΛ‘ = Ξ» where
π β refl
π β refl
Ο β refl
Β·-distrib-+Λ‘ : _Β·_ DistributesOverΛ‘ _+_
Β·-distrib-+Λ‘ = Ξ» where
π _ _ β refl
π π _ β refl
π π π β refl
π π π β refl
π π Ο β refl
π Ο _ β refl
Ο π _ β refl
Ο π π β refl
Ο π π β refl
Ο π Ο β refl
Ο Ο _ β refl
β§-comm : Commutative _β§_
β§-comm = Ξ» where
π π β refl
π π β refl
π Ο β refl
π π β refl
π π β refl
π Ο β refl
Ο π β refl
Ο π β refl
Ο Ο β refl
Β·-distrib-β§Λ‘ : _Β·_ DistributesOverΛ‘ _β§_
Β·-distrib-β§Λ‘ = Ξ» where
π _ _ β refl
π π π β refl
π π π β
π Β· πβ§π β‘β¨ Β·-identityΛ‘ _ β©
πβ§π β
π π Ο β refl
π π π β
π Β· πβ§π β‘β¨ Β·-identityΛ‘ _ β©
πβ§π β
π π π β refl
π π Ο β refl
π Ο _ β refl
Ο π π β refl
Ο π π β
Ο Β· πβ§π β‘β¨ ΟΒ·β’π πβ§πβ’π β©
Ο β
Ο π Ο β refl
Ο π π β
Ο Β· πβ§π β‘β¨ ΟΒ·β’π πβ§πβ’π β©
Ο β
Ο π π β refl
Ο π Ο β refl
Ο Ο _ β refl
+-distrib-β§Λ‘ : _+_ DistributesOverΛ‘ _β§_
+-distrib-β§Λ‘ = Ξ» where
π _ _ β refl
π π π β refl
π π π β
π + πβ§π β‘β¨ β’π+β’π (Ξ» ()) πβ§πβ’π β©
Ο β
π π Ο β refl
π π π β
π + πβ§π β‘β¨ β’π+β’π (Ξ» ()) πβ§πβ’π β©
Ο β
π π π β refl
π π Ο β refl
π Ο _ β refl
Ο _ _ β refl
zero-one-many-has-well-behaved-zero : Has-well-behaved-zero zero-one-many-semiring-with-meet
zero-one-many-has-well-behaved-zero = record
{ πβ’π = Ξ» ()
; is-π? = Ξ» where
π β yes refl
π β no (Ξ» ())
Ο β no (Ξ» ())
; zero-product = Ξ» where
{p = π} _ β injβ refl
{q = π} _ β injβ refl
; +-positiveΛ‘ = Ξ» where
{p = π} {q = π} _ β refl
{p = π} {q = π} ()
{p = π} {q = Ο} ()
; β§-positiveΛ‘ = Ξ» where
{p = π} {q = π} _ β refl
{p = π} {q = π} _ β refl
{p = π} {q = π} πβ§πβ‘π β
PE.β₯-elim (
case
π β‘β¨ π-maximal (sym πβ§πβ‘π) β©
π β
of Ξ» ())
}
where open Tools.Reasoning.PropositionalEquality
Star-requirements :
(Zero-one-many β Zero-one-many β Zero-one-many β Zero-one-many) β
(Zero-one-many β Zero-one-many β Zero-one-many) β
Set
Star-requirements _β_β·_ _β§_ =
let _β€_ : Zero-one-many β Zero-one-many β Set
p β€ q = p β‘ (p β§ q)
in
(β {q r} β (Ο β q β· r) β‘ Ο) Γ
(β {p r} β (p β Ο β· r) β‘ Ο) Γ
(β {p q} β Β¬ (p β‘ π Γ q β‘ π) β (p β q β· Ο) β‘ Ο) Γ
(β {r} β (π β π β· r) β‘ π) Γ
(β {p} β (p β π β· π) β‘ Ο) Γ
((π β π β· π) β€ (π β§ π)) Γ
((π β π β· π) β€ (π β§ π)) Γ
((π β π β· π) β€ π) Γ
((π β π β· π) β€ π)
Star-requirements-requiredβ² :
(M : Semiring-with-meet) β
Semiring-with-meet.π M β‘ π β
Semiring-with-meet.π M β‘ π β
Semiring-with-meet._+_ M β‘ _+_ β
Semiring-with-meet._Β·_ M β‘ _Β·_ β
Semiring-with-meet._β§_ M β‘ _β§_ β
(_β_β·_ :
Zero-one-many β Zero-one-many β Zero-one-many β Zero-one-many) β
(β p q r β (p β q β· r) β€ q + r Β· (p β q β· r)) β
(β p q r β (p β q β· r) β€ p) β
(β r β _Β·_ SubDistributesOverΚ³ (_β_β· r) by _β€_) β
Star-requirements _β_β·_ _β§_
Star-requirements-requiredβ²
M refl refl refl refl refl star β-ineqβ β-ineqβ Β·-sub-distribΚ³-β =
case Meet-requirements-required M refl refl πβ§πβ’π Οβ€ of Ξ» where
(_ , _ , ΟβΟβ‘Ο , _ , Οβπβ‘Ο , _ , Οβπβ‘Ο , _ , _) β
(Ξ» {_ _} β Οββ·)
, (Ξ» {_ _} β βΟβ·)
, (Ξ» {_ _} β ββ·Ο _ _)
, (Ξ» {r = r} β β€-antisym
(begin
π β π β· r β€β¨ β-ineqβ _ _ _ β©
π β)
(begin
π β‘Λβ¨ Β·-zeroΚ³ _ β©
π β π β· r Β· π β€β¨ Β·-sub-distribΚ³-β _ _ _ _ β©
π β π β· r β))
, (Ξ» {p = p} β β€-antisym
(begin
p β π β· π β€β¨ β-ineqβ _ _ _ β©
π + π Β· p β π β· π ββ¨ β’π+β’π (Ξ» ()) (πΒ·β’π βπβ·) β©
Ο β)
(Οβ€ (p β π β· π)))
, β§-greatest-lower-bound
(β-ineqβ _ _ _)
(begin
π β π β· π β€β¨ β-ineqβ _ _ _ β©
π + π Β· π β π β· π β‘β¨β©
π β)
, β§-greatest-lower-bound
(begin
π β π β· π β€β¨ β-ineqβ _ _ _ β©
π + π Β· π β π β· π β‘β¨β©
π β)
(β-ineqβ _ _ _)
, β-ineqβ _ _ _
, β-ineqβ _ _ _
where
open Semiring-with-meet M hiding (π; π; _+_; _Β·_; _β§_; _β€_)
open PartialOrder M
open Meet M
open Tools.Reasoning.PartialOrder β€-poset
infix 50 _β_β·_
_β_β·_ : Zero-one-many β Zero-one-many β Zero-one-many β Zero-one-many
_β_β·_ = star
Οββ· : Ο β q β· r β‘ Ο
Οββ· {q = q} {r = r} = β€-antisym
(begin
Ο β q β· r β€β¨ β-ineqβ _ _ _ β©
Ο β)
(Οβ€ (Ο β q β· r))
βΟβ· : p β Ο β· r β‘ Ο
βΟβ· {p = p} {r = r} = β€-antisym
(begin
p β Ο β· r β€β¨ β-ineqβ _ _ _ β©
Ο + r Β· p β Ο β· r β‘β¨β©
Ο β)
(Οβ€ (p β Ο β· r))
πββ· : π β q β· r β’ π
πββ· {q = q} {r = r} πββ·β‘π =
case begin
π β‘β¨β©
π Β· Ο β‘Λβ¨ Β·-congΚ³ πββ·β‘π β©
π β q β· r Β· Ο β€β¨ Β·-sub-distribΚ³-β _ _ _ _ β©
Ο β q Β· Ο β· r β‘β¨ Οββ· β©
Ο β
of Ξ» ()
βπβ· : p β π β· r β’ π
βπβ· {p = p} {r = r} βπβ·β‘π =
case begin
π β‘β¨β©
π Β· Ο β‘Λβ¨ Β·-congΚ³ βπβ·β‘π β©
p β π β· r Β· Ο β€β¨ Β·-sub-distribΚ³-β _ _ _ _ β©
(p Β· Ο) β Ο β· r β‘β¨ βΟβ· β©
Ο β
of Ξ» ()
ββ·Ο : β p q β Β¬ (p β‘ π Γ q β‘ π) β (p β q β· Ο) β‘ Ο
ββ·Ο _ Ο _ = βΟβ·
ββ·Ο Ο _ _ = Οββ·
ββ·Ο π π Β¬β‘πΓβ‘π = β₯-elim (Β¬β‘πΓβ‘π (refl , refl))
ββ·Ο p π _ = β€-antisym
(begin
p β π β· Ο β€β¨ β-ineqβ _ _ _ β©
π + Ο Β· p β π β· Ο ββ¨ +-congΛ‘ (ΟΒ·β’π βπβ·) β©
π + Ο β‘β¨β©
Ο β)
(Οβ€ (p β π β· Ο))
ββ·Ο π π _ = β€-antisym
(begin
π β π β· Ο β€β¨ β-ineqβ _ _ _ β©
Ο Β· π β π β· Ο ββ¨ ΟΒ·β’π πββ· β©
Ο β)
(Οβ€ (π β π β· Ο))
Star-requirements-required :
(has-star : Has-star zero-one-many-semiring-with-meet) β
Star-requirements (Has-star._β_β·_ has-star) _β§_
Star-requirements-required has-star =
Star-requirements-requiredβ²
zero-one-many-semiring-with-meet refl refl refl refl refl
_β_β·_
β-ineqβ
β-ineqβ
Β·-sub-distribΚ³-β
where
open Has-star has-star
zero-one-many-lower-bounded-star :
Has-star zero-one-many-semiring-with-meet
zero-one-many-lower-bounded-star =
LowerBounded.has-star zero-one-many-semiring-with-meet Ο Οβ€
zero-one-many-lower-bounded-β :
let open Has-star zero-one-many-lower-bounded-star in
(β r β π β π β· r β‘ π) Γ
(β p q r β Β¬ (p β‘ π Γ q β‘ π) β p β q β· r β‘ Ο)
zero-one-many-lower-bounded-β =
(Ξ» _ β refl)
, (Ξ» where
π π _ Β¬β‘πΓβ‘π β β₯-elim (Β¬β‘πΓβ‘π (refl , refl))
π π _ _ β
Ο Β· πβ§π β‘β¨ ΟΒ·β’π πβ§πβ’π β©
Ο β
π Ο _ _ β refl
π π _ _ β
Ο Β· πβ§π β‘β¨ ΟΒ·β’π πβ§πβ’π β©
Ο β
π π _ _ β refl
π Ο _ _ β refl
Ο _ _ _ β refl)
where
open Has-star zero-one-many-lower-bounded-star
open Tools.Reasoning.PropositionalEquality
zero-one-many-lower-bounded :
(variant : Modality-variant) β
let open Modality-variant variant in
(T πα΅-allowed β Β¬ β-available β T πβ€π) β
Modality
zero-one-many-lower-bounded variant hyp = record
{ variant = variant
; semiring-with-meet = zero-one-many-semiring-with-meet
; π-well-behaved = Ξ» _ β zero-one-many-has-well-behaved-zero
; has-star = Ξ» _ β zero-one-many-lower-bounded-star
; +-decreasingΛ‘ = Ξ» ok no-star β +-decreasingΛ‘ (hyp ok no-star)
}
infix 50 _β_β·_
_β_β·_ : Zero-one-many β Zero-one-many β Zero-one-many β Zero-one-many
p β q β· π = p β§ q
p β q β· π = p + Ο Β· q
p β q β· Ο = Ο Β· (p β§ q)
lower-boundedβ’greatest :
Has-star._β_β·_ zero-one-many-lower-bounded-star β’ _β_β·_
lower-boundedβ’greatest hyp =
case cong (Ξ» f β f π π π) hyp of Ξ» ()
Οββ· : β r β Ο β q β· r β‘ Ο
Οββ· π = refl
Οββ· π = refl
Οββ· Ο = refl
βΟβ· : β r β p β Ο β· r β‘ Ο
βΟβ· {p = p} = Ξ» where
π β
p β§ Ο β‘β¨ M.β§-comm p _ β©
Ο β§ p β‘β¨β©
Ο β
π β
p + Ο β‘β¨ M.+-comm p _ β©
Ο + p β‘β¨β©
Ο β
Ο β
Ο Β· (p β§ Ο) β‘β¨ cong (_ Β·_) (M.β§-comm p _) β©
Ο Β· (Ο β§ p) β‘β¨β©
Ο β
where
open Tools.Reasoning.PropositionalEquality
module M = Semiring-with-meet zero-one-many-semiring-with-meet
πβπβ· : β r β π β π β· r β‘ π
πβπβ· π = refl
πβπβ· π = refl
πβπβ· Ο = refl
ββ·Ο : β p q β Β¬ (p β‘ π Γ q β‘ π) β (p β q β· Ο) β‘ Ο
ββ·Ο p Ο _ = βΟβ· {p = p} Ο
ββ·Ο Ο _ _ = refl
ββ·Ο π π Β¬β‘πΓβ‘π = β₯-elim (Β¬β‘πΓβ‘π (refl , refl))
ββ·Ο π π _ = ΟΒ·β’π πβ§πβ’π
ββ·Ο π π _ = refl
ββ·Ο π π _ = ΟΒ·β’π πβ§πβ’π
βπβ·π : β p β p β π β· π β‘ Ο
βπβ·π π = refl
βπβ·π π = refl
βπβ·π Ο = refl
βπβ§πβ·π : β p β p β πβ§π β· π β‘ Ο
βπβ§πβ·π π = πβ§π-elim (Ξ» q β π β q β· π β‘ Ο) (Ξ» _ β refl) (Ξ» _ β refl)
βπβ§πβ·π π = πβ§π-elim (Ξ» q β π β q β· π β‘ Ο) (Ξ» _ β refl) (Ξ» _ β refl)
βπβ§πβ·π Ο = refl
πβπβ§πβ·π : π β πβ§π β· π β‘ πβ§π
πβπβ§πβ·π = πβ§π-elim
(Ξ» q β π β q β· π β‘ q)
(Ξ» πβ§πβ‘π β πβ§πβ‘π)
(Ξ» _ β refl)
πβπβ§πβ·π : π β πβ§π β· π β‘ πβ§π
πβπβ§πβ·π = πβ§π-elim
(Ξ» q β π β q β· π β‘ q)
(Ξ» _ β refl)
(Ξ» _ β refl)
β-greatest :
(has-star : Has-star zero-one-many-semiring-with-meet) β
β p q r β Has-star._β_β·_ has-star p q r β€ p β q β· r
β-greatest has-star =
case Star-requirements-required has-star of Ξ» where
(Οββ·β² , βΟβ·β² , ββ·β²Ο ,
πβπβ·β² , βπβ·β²π , πβπβ·β²π , πβπβ·β²π , πβπβ·β²π , πβπβ·β²π) β Ξ» where
Ο q r β begin
Ο β q β·β² r ββ¨ Οββ·β² β©
Ο βΛβ¨ Οββ· r β©
Ο β q β· r β
p Ο r β begin
p β Ο β·β² r ββ¨ βΟβ·β² β©
Ο βΛβ¨ βΟβ· r β©
p β Ο β· r β
π π r β begin
π β π β·β² r ββ¨ πβπβ·β² β©
π βΛβ¨ πβπβ· r β©
π β π β· r β
π π Ο β begin
π β π β·β² Ο ββ¨ ββ·β²Ο (Ξ» { (_ , ()) }) β©
Ο βΛβ¨ ββ·Ο π π (Ξ» { (_ , ()) }) β©
π β π β· Ο β
π q Ο β begin
π β q β·β² Ο ββ¨ ββ·β²Ο (Ξ» { (() , _) }) β©
Ο βΛβ¨ ββ·Ο π q (Ξ» { (() , _) }) β©
π β q β· Ο β
p π π β begin
p β π β·β² π ββ¨ βπβ·β²π β©
Ο βΛβ¨ βπβ·π p β©
p β π β· π β
π π π β begin
π β π β·β² π β€β¨ πβπβ·β²π β©
π β§ π β
π π π β begin
π β π β·β² π β€β¨ πβπβ·β²π β©
π β§ π β
π π π β begin
π β π β·β² π β€β¨ πβπβ·β²π β©
π β
π π π β begin
π β π β·β² π β€β¨ πβπβ·β²π β©
π β
where
open Has-star has-star renaming (_β_β·_ to _β_β·β²_)
open PartialOrder zero-one-many-semiring-with-meet
open Tools.Reasoning.PartialOrder β€-poset
zero-one-many-greatest-star : Has-star zero-one-many-semiring-with-meet
zero-one-many-greatest-star = record
{ _β_β·_ = _β_β·_
; β-ineq = β-ineqβ , β-ineqβ
; +-sub-interchangeable-β = +-sub-interchangeable-β
; Β·-sub-distribΚ³-β = Ξ» r _ _ _ β
β€-reflexive (Β·-distribΚ³-β r _ _ _)
; β-sub-distrib-β§ = Ξ» r β
(Ξ» _ _ _ β β€-reflexive (β-distribΛ‘-β§ r _ _ _))
, (Ξ» _ _ _ β β€-reflexive (β-distribΚ³-β§ r _ _ _))
}
where
semiring-with-meet = zero-one-many-semiring-with-meet
open Semiring-with-meet semiring-with-meet
hiding (π; π; _+_; _Β·_; _β§_; _β€_)
open PartialOrder semiring-with-meet
open Addition semiring-with-meet
open Meet semiring-with-meet
open Multiplication semiring-with-meet
β-ineqβ : β p q r β p β q β· r β€ q + r Β· p β q β· r
β-ineqβ p = Ξ» where
q π β begin
p β§ q β€β¨ β§-decreasingΚ³ p _ β©
q βΛβ¨ +-identityΚ³ _ β©
q + π β
π π β begin
p β π β· π βΛβ¨ Β·-identityΛ‘ _ β©
π Β· p β π β· π β
π π β begin
p + Ο ββ¨ +-zeroΚ³ _ β©
Ο β‘β¨β©
π + π Β· Ο βΛβ¨ cong (Ξ» p β π + π Β· p) (+-zeroΚ³ p) β©
π + π Β· (p + Ο) β
Ο π β begin
p + Ο ββ¨ +-zeroΚ³ _ β©
Ο β
π Ο β begin
Ο Β· (p β§ π) β‘β¨β©
(Ο Β· Ο) Β· (p β§ π) ββ¨ Β·-assoc _ _ _ β©
Ο Β· Ο Β· (p β§ π) β
π Ο β begin
Ο Β· (p β§ π) ββ¨ Β·-distribΛ‘-β§ _ p _ β©
Ο Β· p β§ Ο ββ¨ β§-comm (Ο Β· p) _ β©
Ο β§ Ο Β· p β‘β¨β©
Ο β‘β¨β©
π + Ο Β· Ο ββ¨ cong (Ξ» p β _ + Ο Β· p) (β§-comm _ (Ο Β· p)) β©
π + Ο Β· (Ο Β· p β§ Ο) βΛβ¨ cong (Ξ» p β _ + Ο Β· p) (Β·-distribΛ‘-β§ Ο p _) β©
π + Ο Β· Ο Β· (p β§ π) β
Ο Ο β begin
Ο Β· (p β§ Ο) ββ¨ Β·-distribΛ‘-β§ _ p _ β©
Ο Β· p β§ Ο β€β¨ β§-decreasingΚ³ (Ο Β· p) _ β©
Ο β
where
open Tools.Reasoning.PartialOrder β€-poset
β-ineqβ : β p q r β (p β q β· r) β€ p
β-ineqβ p = Ξ» where
q π β begin
p β§ q β€β¨ β§-decreasingΛ‘ p _ β©
p β
π π β begin
p + π ββ¨ +-identityΚ³ _ β©
p β
π π β begin
p + Ο ββ¨ +-zeroΚ³ _ β©
Ο β€β¨ Οβ€ p β©
p β
Ο π β begin
p + Ο ββ¨ +-zeroΚ³ _ β©
Ο β€β¨ Οβ€ p β©
p β
q Ο β begin
Ο Β· (p β§ q) ββ¨ Β·-distribΛ‘-β§ _ p _ β©
Ο Β· p β§ Ο Β· q β€β¨ β§-decreasingΛ‘ (Ο Β· p) _ β©
Ο Β· p β€β¨ Β·-monotoneΛ‘ (Οβ€ π) β©
π Β· p ββ¨ Β·-identityΛ‘ _ β©
p β
where
open Tools.Reasoning.PartialOrder β€-poset
+-sub-interchangeable-β : β r β _+_ SubInterchangeable (_β_β· r) by _β€_
+-sub-interchangeable-β = Ξ» where
π p q pβ² qβ² β begin
(p β§ q) + (pβ² β§ qβ²) β€β¨ +-sub-interchangeable-β§ p _ _ _ β©
(p + pβ²) β§ (q + qβ²) β
π p q pβ² qβ² β begin
(p + Ο Β· q) + (pβ² + Ο Β· qβ²) ββ¨ +-assoc p _ _ β©
p + (Ο Β· q + (pβ² + Ο Β· qβ²)) βΛβ¨ cong (p +_) (+-assoc (Ο Β· q) _ _) β©
p + ((Ο Β· q + pβ²) + Ο Β· qβ²) ββ¨ cong (Ξ» q β p + (q + _)) (+-comm _ pβ²) β©
p + ((pβ² + Ο Β· q) + Ο Β· qβ²) ββ¨ cong (p +_) (+-assoc pβ² _ _) β©
p + (pβ² + (Ο Β· q + Ο Β· qβ²)) βΛβ¨ +-assoc p _ _ β©
(p + pβ²) + (Ο Β· q + Ο Β· qβ²) βΛβ¨ cong (_ +_) (Β·-distribΛ‘-+ Ο q _) β©
(p + pβ²) + Ο Β· (q + qβ²) β
Ο p q pβ² qβ² β begin
Ο Β· (p β§ q) + Ο Β· (pβ² β§ qβ²) βΛβ¨ Β·-distribΛ‘-+ Ο (p β§ q) (pβ² β§ qβ²) β©
Ο Β· ((p β§ q) + (pβ² β§ qβ²)) β€β¨ Β·-monotoneΚ³ (+-sub-interchangeable-β§ p q pβ² qβ²) β©
Ο Β· ((p + pβ²) β§ (q + qβ²)) β
where
open Tools.Reasoning.PartialOrder β€-poset
Β·-distribΚ³-β : β r β _Β·_ DistributesOverΚ³ (_β_β· r)
Β·-distribΚ³-β = Ξ» where
π q p pβ² β
(p β§ pβ²) Β· q β‘β¨ Β·-distribΚ³-β§ _ p _ β©
p Β· q β§ pβ² Β· q β
π q p pβ² β
(p + Ο Β· pβ²) Β· q β‘β¨ Β·-distribΚ³-+ _ p _ β©
p Β· q + (Ο Β· pβ²) Β· q β‘β¨ cong (_ +_) (Β·-assoc Ο pβ² _) β©
p Β· q + Ο Β· pβ² Β· q β
Ο q p pβ² β
(Ο Β· (p β§ pβ²)) Β· q β‘β¨ Β·-assoc _ _ _ β©
Ο Β· (p β§ pβ²) Β· q β‘β¨ cong (_ Β·_) (Β·-distribΚ³-β§ _ p _) β©
Ο Β· (p Β· q β§ pβ² Β· q) β
where
open Tools.Reasoning.PropositionalEquality
β-distribΛ‘-β§ : β r β (_β_β· r) DistributesOverΛ‘ _β§_
β-distribΛ‘-β§ = Ξ» where
π p _ _ β
lemma p _ _
π p q qβ² β
p + Ο Β· (q β§ qβ²) β‘β¨ cong (_ +_) (Β·-distribΛ‘-β§ Ο q _) β©
p + (Ο Β· q β§ Ο Β· qβ²) β‘β¨ +-distribΛ‘-β§ p _ _ β©
(p + Ο Β· q) β§ p + Ο Β· qβ² β
Ο p q qβ² β
Ο Β· (p β§ q β§ qβ²) β‘β¨ cong (_ Β·_) (lemma p _ _) β©
Ο Β· ((p β§ q) β§ (p β§ qβ²)) β‘β¨ Β·-distribΛ‘-β§ Ο (p β§ _) _ β©
Ο Β· (p β§ q) β§ Ο Β· (p β§ qβ²) β
where
open Tools.Reasoning.PropositionalEquality
lemma = Ξ» p q qβ² β
p β§ (q β§ qβ²) β‘Λβ¨ cong (_β§ _) (β§-idem p) β©
(p β§ p) β§ (q β§ qβ²) β‘β¨ β§-assoc p _ _ β©
p β§ (p β§ (q β§ qβ²)) β‘Λβ¨ cong (p β§_) (β§-assoc p _ _) β©
p β§ ((p β§ q) β§ qβ²) β‘β¨ cong (Ξ» q β p β§ (q β§ _)) (β§-comm p _) β©
p β§ ((q β§ p) β§ qβ²) β‘β¨ cong (p β§_) (β§-assoc q _ _) β©
p β§ (q β§ (p β§ qβ²)) β‘Λβ¨ β§-assoc p _ _ β©
(p β§ q) β§ (p β§ qβ²) β
β-distribΚ³-β§ : β r β (_β_β· r) DistributesOverΚ³ _β§_
β-distribΚ³-β§ = Ξ» where
π q p pβ² β
lemma _ p _
π q p pβ² β
(p β§ pβ²) + Ο Β· q β‘β¨ +-distribΚ³-β§ _ p _ β©
(p + Ο Β· q) β§ (pβ² + Ο Β· q) β
Ο q p pβ² β
Ο Β· ((p β§ pβ²) β§ q) β‘β¨ cong (_ Β·_) (lemma _ p _) β©
Ο Β· ((p β§ q) β§ (pβ² β§ q)) β‘β¨ Β·-distribΛ‘-β§ Ο (p β§ _) _ β©
Ο Β· (p β§ q) β§ Ο Β· (pβ² β§ q) β
where
open Tools.Reasoning.PropositionalEquality
lemma = Ξ» q p pβ² β
(p β§ pβ²) β§ q β‘β¨ β§-comm _ q β©
q β§ (p β§ pβ²) β‘β¨ β-distribΛ‘-β§ π q _ _ β©
(q β§ p) β§ (q β§ pβ²) β‘β¨ congβ _β§_ (β§-comm q _) (β§-comm q _) β©
(p β§ q) β§ (pβ² β§ q) β
Β¬-lower-bounded-greatest :
Β¬ ((has-star : Has-star zero-one-many-semiring-with-meet) β
β p q r β
Has-star._β_β·_ has-star p q r β€
Has-star._β_β·_ zero-one-many-lower-bounded-star p q r)
Β¬-lower-bounded-greatest hyp =
case hyp zero-one-many-greatest-star π π π of Ξ» ()
zero-one-many-greatest :
(variant : Modality-variant) β
let open Modality-variant variant in
(T πα΅-allowed β Β¬ β-available β T πβ€π) β
Modality
zero-one-many-greatest variant hyp = record
{ variant = variant
; semiring-with-meet = zero-one-many-semiring-with-meet
; π-well-behaved = Ξ» _ β zero-one-many-has-well-behaved-zero
; has-star = Ξ» _ β zero-one-many-greatest-star
; +-decreasingΛ‘ = Ξ» ok no-star β +-decreasingΛ‘ (hyp ok no-star)
}