module Graded.Modality.Instances.Linear-or-affine where
import Tools.Algebra
open import Tools.Bool using (T)
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
open import Tools.Unit
import Graded.Modality
open import Graded.FullReduction.Assumptions
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
import Graded.Restrictions
import Definition.Typed.Restrictions
data Linear-or-affine : Set where
π π β€π β€Ο : Linear-or-affine
open Graded.Modality Linear-or-affine
open Definition.Typed.Restrictions Linear-or-affine
open Tools.Algebra Linear-or-affine
private variable
p q r : Linear-or-affine
variant : Modality-variant
trs : Type-restrictions
infixr 40 _β§_
_β§_ : Linear-or-affine β Linear-or-affine β Linear-or-affine
π β§ π = π
π β§ π = π
β€Ο β§ _ = β€Ο
_ β§ β€Ο = β€Ο
_ β§ _ = β€π
infixr 40 _+_
_+_ : Linear-or-affine β Linear-or-affine β Linear-or-affine
π + q = q
p + π = p
_ + _ = β€Ο
infixr 45 _Β·_
_Β·_ : Linear-or-affine β Linear-or-affine β Linear-or-affine
π Β· _ = π
_ Β· π = π
π Β· q = q
p Β· π = p
β€π Β· β€π = β€π
_ Β· _ = β€Ο
infix 10 _β€_
_β€_ : Linear-or-affine β Linear-or-affine β Set
p β€ q = p β‘ p β§ q
β€Οβ€ : β p β β€Ο β€ p
β€Οβ€ _ = refl
π-maximal : π β€ p β p β‘ π
π-maximal {p = π} refl = refl
π-maximal : π β€ p β p β‘ π
π-maximal {p = π} refl = refl
+-zeroΛ‘ : LeftZero β€Ο _+_
+-zeroΛ‘ π = refl
+-zeroΛ‘ π = refl
+-zeroΛ‘ β€π = refl
+-zeroΛ‘ β€Ο = refl
+-zeroΚ³ : RightZero β€Ο _+_
+-zeroΚ³ π = refl
+-zeroΚ³ π = refl
+-zeroΚ³ β€π = refl
+-zeroΚ³ β€Ο = refl
+-zero : Zero β€Ο _+_
+-zero = +-zeroΛ‘ , +-zeroΚ³
β’π+β’π : p β’ π β q β’ π β p + q β‘ β€Ο
β’π+β’π {p = π} πβ’π _ = β₯-elim (πβ’π refl)
β’π+β’π {p = π} {q = π} _ πβ’π = β₯-elim (πβ’π refl)
β’π+β’π {p = π} {q = π} _ _ = refl
β’π+β’π {p = π} {q = β€π} _ _ = refl
β’π+β’π {p = π} {q = β€Ο} _ _ = refl
β’π+β’π {p = β€π} {q = π} _ πβ’π = β₯-elim (πβ’π refl)
β’π+β’π {p = β€π} {q = π} _ _ = refl
β’π+β’π {p = β€π} {q = β€π} _ _ = refl
β’π+β’π {p = β€π} {q = β€Ο} _ _ = refl
β’π+β’π {p = β€Ο} {q = π} _ πβ’π = β₯-elim (πβ’π refl)
β’π+β’π {p = β€Ο} {q = π} _ _ = refl
β’π+β’π {p = β€Ο} {q = β€π} _ _ = refl
β’π+β’π {p = β€Ο} {q = β€Ο} _ _ = refl
Β·-idempotent : Idempotent _Β·_
Β·-idempotent π = refl
Β·-idempotent π = refl
Β·-idempotent β€π = refl
Β·-idempotent β€Ο = refl
Β·-comm : Commutative _Β·_
Β·-comm = Ξ» where
π π β refl
π π β refl
π β€π β refl
π β€Ο β refl
π π β refl
π π β refl
π β€π β refl
π β€Ο β refl
β€π π β refl
β€π π β refl
β€π β€π β refl
β€π β€Ο β refl
β€Ο π β refl
β€Ο π β refl
β€Ο β€π β refl
β€Ο β€Ο β refl
β€ΟΒ·β’π : p β’ π β β€Ο Β· p β‘ β€Ο
β€ΟΒ·β’π {p = π} πβ’π = β₯-elim (πβ’π refl)
β€ΟΒ·β’π {p = π} _ = refl
β€ΟΒ·β’π {p = β€π} _ = refl
β€ΟΒ·β’π {p = β€Ο} _ = refl
πΒ·β’π : p β’ π β π Β· p β’ π
πΒ·β’π {p = π} πβ’π = πβ’π
β€πΒ·β’π : p β’ π β β€π Β· p β’ π
β€πΒ·β’π {p = π} πβ’π = πβ’π
linear-or-affine-semiring-with-meet : Semiring-with-meet
linear-or-affine-semiring-with-meet = record
{ _+_ = _+_
; _Β·_ = _Β·_
; _β§_ = _β§_
; π = π
; π = π
; +-Β·-Semiring = record
{ isSemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = record
{ isMonoid = record
{ isSemigroup = record
{ isMagma = record
{ isEquivalence = PE.isEquivalence
; β-cong = congβ _+_
}
; assoc = +-assoc
}
; identity =
(Ξ» _ β refl)
, comm+idΛ‘βidΚ³ +-comm (Ξ» _ β refl)
}
; comm = +-comm
}
; *-isMonoid = record
{ isSemigroup = record
{ isMagma = record
{ isEquivalence = PE.isEquivalence
; β-cong = congβ _Β·_
}
; assoc = Β·-assoc
}
; 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 = β§-assoc
}
; idem = Ξ» where
π β refl
π β refl
β€π β refl
β€Ο β refl
}
; comm = β§-comm
}
; Β·-distrib-β§ =
Β·-distribΛ‘-β§
, comm+distrΛ‘βdistrΚ³ Β·-comm Β·-distribΛ‘-β§
; +-distrib-β§ =
+-distribΛ‘-β§
, comm+distrΛ‘βdistrΚ³ +-comm +-distribΛ‘-β§
}
where
+-assoc : Associative _+_
+-assoc = Ξ» where
π _ _ β refl
π π _ β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
β€π π _ β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π β€π π β refl
β€π β€π π β refl
β€π β€π β€π β refl
β€π β€π β€Ο β refl
β€π β€Ο π β refl
β€π β€Ο π β refl
β€π β€Ο β€π β refl
β€π β€Ο β€Ο β refl
β€Ο π _ β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο β€π π β refl
β€Ο β€π π β refl
β€Ο β€π β€π β refl
β€Ο β€π β€Ο β refl
β€Ο β€Ο π β refl
β€Ο β€Ο π β refl
β€Ο β€Ο β€π β refl
β€Ο β€Ο β€Ο β refl
+-comm : Commutative _+_
+-comm = Ξ» where
π π β refl
π π β refl
π β€π β refl
π β€Ο β refl
π π β refl
π π β refl
π β€π β refl
π β€Ο β refl
β€π π β refl
β€π π β refl
β€π β€π β refl
β€π β€Ο β refl
β€Ο π β refl
β€Ο π β refl
β€Ο β€π β refl
β€Ο β€Ο β refl
Β·-assoc : Associative _Β·_
Β·-assoc = Ξ» where
π _ _ β refl
π π _ β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
β€π π _ β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π β€π π β refl
β€π β€π π β refl
β€π β€π β€π β refl
β€π β€π β€Ο β refl
β€π β€Ο π β refl
β€π β€Ο π β refl
β€π β€Ο β€π β refl
β€π β€Ο β€Ο β refl
β€Ο π _ β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο β€π π β refl
β€Ο β€π π β refl
β€Ο β€π β€π β refl
β€Ο β€π β€Ο β refl
β€Ο β€Ο π β refl
β€Ο β€Ο π β refl
β€Ο β€Ο β€π β refl
β€Ο β€Ο β€Ο β refl
Β·-identityΛ‘ : LeftIdentity π _Β·_
Β·-identityΛ‘ = Ξ» where
π β refl
π β refl
β€π β refl
β€Ο β refl
Β·-distribΛ‘-+ : _Β·_ DistributesOverΛ‘ _+_
Β·-distribΛ‘-+ = Ξ» where
π _ _ β refl
π π _ β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
β€π π _ β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π β€π π β refl
β€π β€π π β refl
β€π β€π β€π β refl
β€π β€π β€Ο β refl
β€π β€Ο π β refl
β€π β€Ο π β refl
β€π β€Ο β€π β refl
β€π β€Ο β€Ο β refl
β€Ο π _ β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο β€π π β refl
β€Ο β€π π β refl
β€Ο β€π β€π β refl
β€Ο β€π β€Ο β refl
β€Ο β€Ο π β refl
β€Ο β€Ο π β refl
β€Ο β€Ο β€π β refl
β€Ο β€Ο β€Ο β refl
β§-assoc : Associative _β§_
β§-assoc = Ξ» where
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π β€π π β refl
β€π β€π π β refl
β€π β€π β€π β refl
β€π β€π β€Ο β refl
β€π β€Ο π β refl
β€π β€Ο π β refl
β€π β€Ο β€π β refl
β€π β€Ο β€Ο β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο β€π π β refl
β€Ο β€π π β refl
β€Ο β€π β€π β refl
β€Ο β€π β€Ο β refl
β€Ο β€Ο π β refl
β€Ο β€Ο π β refl
β€Ο β€Ο β€π β refl
β€Ο β€Ο β€Ο β refl
β§-comm : Commutative _β§_
β§-comm = Ξ» where
π π β refl
π π β refl
π β€π β refl
π β€Ο β refl
π π β refl
π π β refl
π β€π β refl
π β€Ο β refl
β€π π β refl
β€π π β refl
β€π β€π β refl
β€π β€Ο β refl
β€Ο π β refl
β€Ο π β refl
β€Ο β€π β refl
β€Ο β€Ο β refl
Β·-distribΛ‘-β§ : _Β·_ DistributesOverΛ‘ _β§_
Β·-distribΛ‘-β§ = Ξ» where
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π β€π π β refl
β€π β€π π β refl
β€π β€π β€π β refl
β€π β€π β€Ο β refl
β€π β€Ο π β refl
β€π β€Ο π β refl
β€π β€Ο β€π β refl
β€π β€Ο β€Ο β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο β€π π β refl
β€Ο β€π π β refl
β€Ο β€π β€π β refl
β€Ο β€π β€Ο β refl
β€Ο β€Ο π β refl
β€Ο β€Ο π β refl
β€Ο β€Ο β€π β refl
β€Ο β€Ο β€Ο β refl
+-distribΛ‘-β§ : _+_ DistributesOverΛ‘ _β§_
+-distribΛ‘-β§ = Ξ» where
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π β€π π β refl
β€π β€π π β refl
β€π β€π β€π β refl
β€π β€π β€Ο β refl
β€π β€Ο π β refl
β€π β€Ο π β refl
β€π β€Ο β€π β refl
β€π β€Ο β€Ο β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο β€π π β refl
β€Ο β€π π β refl
β€Ο β€π β€π β refl
β€Ο β€π β€Ο β refl
β€Ο β€Ο π β refl
β€Ο β€Ο π β refl
β€Ο β€Ο β€π β refl
β€Ο β€Ο β€Ο β refl
linear-or-affine-has-well-behaved-zero : Has-well-behaved-zero linear-or-affine-semiring-with-meet
linear-or-affine-has-well-behaved-zero = record
{ πβ’π = Ξ» ()
; is-π? = Ξ» where
π β yes refl
π β no (Ξ» ())
β€π β no (Ξ» ())
β€Ο β no (Ξ» ())
; zero-product = Ξ» where
{p = π} _ β injβ refl
{q = π} _ β injβ refl
; +-positiveΛ‘ = Ξ» where
{p = π} {q = π} _ β refl
{p = π} {q = π} _ β refl
{p = π} {q = β€π} ()
{p = π} {q = β€Ο} ()
; β§-positiveΛ‘ = Ξ» where
{p = π} {q = π} _ β refl
{p = π} {q = π} _ β refl
{p = π} {q = β€π} ()
{p = π} {q = β€Ο} ()
}
Star-requirements :
(Linear-or-affine β Linear-or-affine β Linear-or-affine β
Linear-or-affine) β
Set
Star-requirements _β_β·_ =
(β {q r} β (β€Ο β q β· r) β‘ β€Ο) Γ
(β {p r} β (p β β€Ο β· r) β‘ β€Ο) Γ
(β {p q} β Β¬ (p β‘ π Γ q β‘ π) β (p β q β· β€Ο) β‘ β€Ο) Γ
(β {r} β (π β π β· r) β‘ π) Γ
(β {p} β (p β π β· π) β‘ β€Ο) Γ
(β {p} β (p β π β· β€π) β‘ β€Ο) Γ
(β {p} β (p β β€π β· π) β‘ β€Ο) Γ
(β {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 β‘ _β§_ β
(_β_β·_ :
Linear-or-affine β Linear-or-affine β Linear-or-affine β
Linear-or-affine) β
(β 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Κ³-β =
(Ξ» {_ _} β Οββ·)
, (Ξ» {_ _} β βΟβ·)
, (Ξ» {_ _} β ββ·Ο _ _)
, (Ξ» {r = r} β β€-antisym
(begin
π β π β· r β€β¨ β-ineqβ _ _ _ β©
π β)
(begin
π β‘Λβ¨ Β·-zeroΚ³ (π β π β· r) β©
π β π β· r Β· π β€β¨ Β·-sub-distribΚ³-β _ _ _ _ β©
π β π β· r β))
, (Ξ» {p = p} β β€-antisym
(begin
p β π β· π β€β¨ β-ineqβ _ _ _ β©
π + π Β· p β π β· π ββ¨ β’π+β’π {p = π} (Ξ» ()) (πΒ·β’π βπβ·) β©
β€Ο β)
(β€Οβ€ (p β π β· π)))
, (Ξ» {p = p} β β€-antisym
(begin
p β π β· β€π β€β¨ β-ineqβ _ _ _ β©
π + β€π Β· p β π β· β€π ββ¨ β’π+β’π {p = π} (Ξ» ()) (β€πΒ·β’π βπβ·) β©
β€Ο β)
(β€Οβ€ (p β π β· β€π)))
, (Ξ» {p = p} β β€-antisym
(begin
p β β€π β· π β€β¨ β-ineqβ _ _ _ β©
β€π + π Β· p β β€π β· π ββ¨ β’π+β’π {p = β€π} (Ξ» ()) (πΒ·β’π ββ€πβ·) β©
β€Ο β)
(β€Οβ€ (p β β€π β· π)))
, (Ξ» {p = p} β β€-antisym
(begin
p β β€π β· β€π β€β¨ β-ineqβ _ _ _ β©
β€π + β€π Β· p β β€π β· β€π ββ¨ β’π+β’π {p = β€π} (Ξ» ()) (β€πΒ·β’π ββ€πβ·) β©
β€Ο β)
(β€Οβ€ (p β β€π β· β€π)))
, β§-greatest-lower-bound
(β-ineqβ _ _ _)
(begin
π β π β· π β€β¨ β-ineqβ _ _ _ β©
π + π Β· π β π β· π β‘β¨β©
π β)
, (begin
π β β€π β· π β€β¨ β-ineqβ _ _ _ β©
β€π + π Β· π β β€π β· π β‘β¨β©
β€π β)
, β§-greatest-lower-bound
(begin
π β π β· π β€β¨ β-ineqβ _ _ _ β©
π + π Β· π β π β· π β‘β¨β©
π β)
(β-ineqβ _ _ _)
, β-ineqβ _ _ _
, β-ineqβ _ _ _
, (begin
π β π β· β€π β€β¨ β-ineqβ _ _ _ β©
β€π Β· π β π β· β€π β€β¨ Β·-monotoneΚ³ {r = β€π} (β-ineqβ _ _ _) β©
β€π Β· π β‘β¨β©
β€π β)
, β-ineqβ _ _ _
, β-ineqβ _ _ _
, β-ineqβ _ _ _
, (begin
π β β€π β· π β€β¨ β-ineqβ _ _ _ β©
β€π + π Β· π β β€π β· π β‘β¨β©
β€π β)
, β-ineqβ _ _ _
, β-ineqβ _ _ _
where
open Semiring-with-meet M using (Β·-zeroΚ³)
open PartialOrder M
open Meet M
open Multiplication M
open Tools.Reasoning.PartialOrder β€-poset
infix 50 _β_β·_
_β_β·_ :
Linear-or-affine β Linear-or-affine β Linear-or-affine β
Linear-or-affine
_β_β·_ = 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 β‘β¨ +-zeroΛ‘ (r Β· _) β©
β€Ο β)
(β€Οβ€ (p β β€Ο β· r))
πββ· : π β q β· r β’ π
πββ· {q = q} {r = r} πββ·β‘π =
case begin
π β‘β¨β©
π Β· β€Ο β‘Λβ¨ cong (_Β· _) πββ·β‘π β©
π β q β· r Β· β€Ο β€β¨ Β·-sub-distribΚ³-β _ _ _ _ β©
β€Ο β q Β· β€Ο β· r β‘β¨ Οββ· β©
β€Ο β
of Ξ» ()
β€πββ· : β€π β 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 β β€π β· 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 β π β· β€Ο))
ββ·Ο p β€π _ = β€-antisym
(begin
p β β€π β· β€Ο β€β¨ β-ineqβ _ _ _ β©
β€π + β€Ο Β· p β β€π β· β€Ο β‘β¨ cong (β€π +_) (β€ΟΒ·β’π ββ€πβ·) β©
β€π + β€Ο β‘β¨β©
β€Ο β)
(β€Οβ€ (p β π β· β€Ο))
ββ·Ο π π _ = β€-antisym
(begin
π β π β· β€Ο β€β¨ β-ineqβ _ _ _ β©
β€Ο Β· π β π β· β€Ο ββ¨ β€ΟΒ·β’π πββ· β©
β€Ο β)
(β€Οβ€ (π β π β· β€Ο))
ββ·Ο β€π π _ = β€-antisym
(begin
β€π β π β· β€Ο β€β¨ β-ineqβ _ _ _ β©
β€Ο Β· β€π β π β· β€Ο ββ¨ β€ΟΒ·β’π β€πββ· β©
β€Ο β)
(β€Οβ€ (β€π β π β· β€Ο))
Star-requirements-required :
(has-star : Has-star linear-or-affine-semiring-with-meet) β
Star-requirements (Has-star._β_β·_ has-star)
Star-requirements-required has-star =
Star-requirements-requiredβ²
linear-or-affine-semiring-with-meet refl refl refl refl refl
_β_β·_ β-ineqβ β-ineqβ Β·-sub-distribΚ³-β
where
open Has-star has-star
infix 50 _β_β·_
_β_β·_ :
Linear-or-affine β Linear-or-affine β Linear-or-affine β
Linear-or-affine
p β q β· π = p β§ q
p β q β· π = p + β€Ο Β· q
p β q β· β€π = p β§ β€Ο Β· q
p β q β· β€Ο = β€Ο Β· (p β§ q)
β€Οββ· : β r β β€Ο β q β· r β‘ β€Ο
β€Οββ· π = refl
β€Οββ· {q = π} π = refl
β€Οββ· {q = π} π = refl
β€Οββ· {q = β€π} π = refl
β€Οββ· {q = β€Ο} π = refl
β€Οββ· {q = π} β€π = refl
β€Οββ· {q = π} β€π = refl
β€Οββ· {q = β€π} β€π = refl
β€Οββ· {q = β€Ο} β€π = refl
β€Οββ· β€Ο = refl
ββ€Οβ· : β r β p β β€Ο β· r β‘ β€Ο
ββ€Οβ· {p = π} π = refl
ββ€Οβ· {p = π} π = refl
ββ€Οβ· {p = β€π} π = refl
ββ€Οβ· {p = β€Ο} π = refl
ββ€Οβ· {p = π} π = refl
ββ€Οβ· {p = π} π = refl
ββ€Οβ· {p = β€π} π = refl
ββ€Οβ· {p = β€Ο} π = refl
ββ€Οβ· {p = π} β€π = refl
ββ€Οβ· {p = π} β€π = refl
ββ€Οβ· {p = β€π} β€π = refl
ββ€Οβ· {p = β€Ο} β€π = refl
ββ€Οβ· {p = π} β€Ο = refl
ββ€Οβ· {p = π} β€Ο = refl
ββ€Οβ· {p = β€π} β€Ο = refl
ββ€Οβ· {p = β€Ο} β€Ο = refl
πβπβ· : β r β π β π β· r β‘ π
πβπβ· π = refl
πβπβ· π = refl
πβπβ· β€π = refl
πβπβ· β€Ο = refl
ββ·β€Ο : β p q β Β¬ (p β‘ π Γ q β‘ π) β (p β q β· β€Ο) β‘ β€Ο
ββ·β€Ο = Ξ» where
π π Β¬β‘πΓβ‘π β β₯-elim (Β¬β‘πΓβ‘π (refl , refl))
π π _ β refl
β€π π _ β refl
β€Ο π _ β refl
π π _ β refl
π π _ β refl
β€π π _ β refl
β€Ο π _ β refl
π β€π _ β refl
π β€π _ β refl
β€π β€π _ β refl
β€Ο β€π _ β refl
p β€Ο _ β ββ€Οβ· {p = p} β€Ο
βπβ·π : β p β p β π β· π β‘ β€Ο
βπβ·π π = refl
βπβ·π π = refl
βπβ·π β€π = refl
βπβ·π β€Ο = refl
βπβ·β€π : β p β p β π β· β€π β‘ β€Ο
βπβ·β€π π = refl
βπβ·β€π π = refl
βπβ·β€π β€π = refl
βπβ·β€π β€Ο = refl
ββ€πβ·π : β p β p β β€π β· π β‘ β€Ο
ββ€πβ·π π = refl
ββ€πβ·π π = refl
ββ€πβ·π β€π = refl
ββ€πβ·π β€Ο = refl
ββ€πβ·β€π : β p β p β β€π β· β€π β‘ β€Ο
ββ€πβ·β€π π = refl
ββ€πβ·β€π π = refl
ββ€πβ·β€π β€π = refl
ββ€πβ·β€π β€Ο = refl
β-greatest :
(has-star : Has-star linear-or-affine-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
β€Ο q r β begin
β€Ο β q β·β² r ββ¨ β€Οββ·β² β©
β€Ο βΛβ¨ β€Οββ· r β©
β€Ο β q β· r β
p β€Ο r β begin
p β β€Ο β·β² r ββ¨ ββ€Οβ·β² β©
β€Ο βΛβ¨ ββ€Οβ· r β©
p β β€Ο β· r β
π π r β begin
π β π β·β² r ββ¨ πβπβ·β² β©
π βΛβ¨ πβπβ· r β©
π β π β· r β
π π β€Ο β begin
π β π β·β² β€Ο ββ¨ ββ·β²β€Ο (Ξ» { (_ , ()) }) β©
β€Ο βΛβ¨ ββ·β€Ο π π (Ξ» { (_ , ()) }) β©
π β π β· β€Ο β
π β€π β€Ο β begin
π β β€π β·β² β€Ο ββ¨ ββ·β²β€Ο (Ξ» { (_ , ()) }) β©
β€Ο βΛβ¨ ββ·β€Ο π π (Ξ» { (_ , ()) }) β©
π β β€π β· β€Ο β
π q β€Ο β begin
π β q β·β² β€Ο ββ¨ ββ·β²β€Ο (Ξ» { (() , _) }) β©
β€Ο βΛβ¨ ββ·β€Ο π q (Ξ» { (() , _) }) β©
π β q β· β€Ο β
β€π q β€Ο β begin
β€π β q β·β² β€Ο ββ¨ ββ·β²β€Ο (Ξ» { (() , _) }) β©
β€Ο βΛβ¨ ββ·β€Ο β€π q (Ξ» { (() , _) }) β©
β€π β q β· β€Ο β
p π π β begin
p β π β·β² π ββ¨ βπβ·β²π β©
β€Ο βΛβ¨ βπβ·π p β©
p β π β· π β
p β€π π β begin
p β β€π β·β² π ββ¨ ββ€πβ·β²π β©
β€Ο βΛβ¨ ββ€πβ·π p β©
p β β€π β· π β
p π β€π β begin
p β π β·β² β€π ββ¨ βπβ·β²β€π β©
β€Ο βΛβ¨ βπβ·β€π p β©
p β π β· β€π β
p β€π β€π β begin
p β β€π β·β² β€π ββ¨ ββ€πβ·β²β€π β©
β€Ο βΛβ¨ ββ€πβ·β€π p β©
p β β€π β· β€π β
π π π β begin
π β π β·β² π β€β¨ πβπβ·β²π β©
β€π β
π β€π π β begin
π β β€π β·β² π β€β¨ πββ€πβ·β²π β©
β€π β
π π π β begin
π β π β·β² π β€β¨ πβπβ·β²π β©
β€π β
β€π π π β begin
β€π β π β·β² π β€β¨ β€πβπβ·β²π β©
β€π β
π π π β begin
π β π β·β² π β€β¨ πβπβ·β²π β©
π β
π π β€π β begin
π β π β·β² β€π β€β¨ πβπβ·β²β€π β©
β€π β
β€π π π β begin
β€π β π β·β² π β€β¨ β€πβπβ·β²π β©
β€π β
β€π π β€π β begin
β€π β π β·β² β€π β€β¨ β€πβπβ·β²β€π β©
β€π β
π π π β begin
π β π β·β² π β€β¨ πβπβ·β²π β©
π β
π β€π π β begin
π β β€π β·β² π β€β¨ πββ€πβ·β²π β©
β€π β
β€π π π β begin
β€π β π β·β² π β€β¨ β€πβπβ·β²π β©
β€π β
β€π β€π π β begin
β€π β β€π β·β² π β€β¨ β€πββ€πβ·β²π β©
β€π β
where
open Has-star has-star renaming (_β_β·_ to _β_β·β²_)
open PartialOrder linear-or-affine-semiring-with-meet
open Tools.Reasoning.PartialOrder β€-poset
linear-or-affine-has-star :
Has-star linear-or-affine-semiring-with-meet
linear-or-affine-has-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 = linear-or-affine-semiring-with-meet
open Semiring-with-meet semiring-with-meet
hiding (π; π; _+_; _Β·_; _β§_; _β€_)
open PartialOrder semiring-with-meet
open Addition semiring-with-meet
open Multiplication semiring-with-meet
β-ineqβ : β p q r β p β q β· r β€ q + r Β· p β q β· r
β-ineqβ = Ξ» where
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π β€π π β refl
β€π β€π π β refl
β€π β€π β€π β refl
β€π β€π β€Ο β refl
β€π β€Ο π β refl
β€π β€Ο π β refl
β€π β€Ο β€π β refl
β€π β€Ο β€Ο β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο β€π π β refl
β€Ο β€π π β refl
β€Ο β€π β€π β refl
β€Ο β€π β€Ο β refl
β€Ο β€Ο π β refl
β€Ο β€Ο π β refl
β€Ο β€Ο β€π β refl
β€Ο β€Ο β€Ο β refl
β-ineqβ : β p q r β (p β q β· r) β€ p
β-ineqβ = Ξ» where
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π β€π π β refl
β€π β€π π β refl
β€π β€π β€π β refl
β€π β€π β€Ο β refl
β€π β€Ο π β refl
β€π β€Ο π β refl
β€π β€Ο β€π β refl
β€π β€Ο β€Ο β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο β€π π β refl
β€Ο β€π π β refl
β€Ο β€π β€π β refl
β€Ο β€π β€Ο β refl
β€Ο β€Ο π β refl
β€Ο β€Ο π β refl
β€Ο β€Ο β€π β refl
β€Ο β€Ο β€Ο β refl
+-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 ((p + _) +_) (Β·-distribΛ‘-+ β€Ο q _) β©
(p + pβ²) + β€Ο Β· (q + qβ²) β
β€π p q pβ² qβ² β begin
(p β§ β€Ο Β· q) + (pβ² β§ β€Ο Β· qβ²) β€β¨ +-sub-interchangeable-β§ p _ _ _ β©
(p + pβ²) β§ (β€Ο Β· q + β€Ο Β· qβ²) βΛβ¨ β§-congΛ‘ (Β·-distribΛ‘-+ β€Ο q _) β©
(p + pβ²) β§ β€Ο Β· (q + qβ²) β
β€Ο p q pβ² qβ² β begin
β€Ο Β· (p β§ q) + β€Ο Β· (pβ² β§ qβ²) βΛβ¨ Β·-distribΛ‘-+ β€Ο (p β§ _) _ β©
β€Ο Β· ((p β§ q) + (pβ² β§ qβ²)) β€β¨ Β·-monotoneΚ³ {r = β€Ο} (+-sub-interchangeable-β§ p _ _ _) β©
β€Ο Β· ((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 (p Β· _ +_) (Β·-assoc β€Ο 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 β§ 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 (p +_) (Β·-distribΛ‘-β§ β€Ο q _) β©
p + (β€Ο Β· q β§ β€Ο Β· qβ²) β‘β¨ +-distribΛ‘-β§ p _ _ β©
(p + β€Ο Β· q) β§ (p + β€Ο Β· qβ²) β
β€π p q qβ² β
p β§ β€Ο Β· (q β§ qβ²) β‘β¨ β§-congΛ‘ (Β·-distribΛ‘-β§ β€Ο q _) β©
p β§ (β€Ο Β· q β§ β€Ο Β· qβ²) β‘β¨ lemma 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
π _ p _ β lemma _ p _
π q p pβ² β
(p β§ pβ²) + β€Ο Β· q β‘β¨ +-distribΚ³-β§ _ p _ β©
(p + β€Ο Β· q) β§ (pβ² + β€Ο Β· q) β
β€π q p pβ² β
(p β§ pβ²) β§ β€Ο Β· q β‘β¨ lemma _ _ _ β©
(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) β
linear-or-affine :
(variant : Modality-variant) β
let open Modality-variant variant in
(Β¬ β-available β Β¬ T πα΅-allowed) β
Modality
linear-or-affine variant ok = record
{ variant = variant
; semiring-with-meet = linear-or-affine-semiring-with-meet
; π-well-behaved = Ξ» _ β linear-or-affine-has-well-behaved-zero
; has-star = Ξ» _ β linear-or-affine-has-star
; +-decreasingΛ‘ = Ξ» πα΅-ok no-star β β₯-elim (ok no-star πα΅-ok)
}
Suitable-for-full-reduction :
Type-restrictions β Set
Suitable-for-full-reduction rs =
Β¬ Unit-allowed Γ
(β p β Β¬ Ξ£β-allowed π p) Γ
(β p β Β¬ Ξ£β-allowed β€π p) Γ
(β p β Β¬ Ξ£β-allowed β€Ο p)
where
open Type-restrictions rs
suitable-for-full-reduction :
Type-restrictions β β Suitable-for-full-reduction
suitable-for-full-reduction rs =
record rs
{ Unit-allowed = β₯
; Ξ Ξ£-allowed = Ξ» b p q β
Ξ Ξ£-allowed b p q Γ p β’ π Γ p β’ β€π Γ p β’ β€Ο
}
, idαΆ
, (Ξ» _ β (_$ refl) ββ projβ ββ projβ)
, (Ξ» _ β (_$ refl) ββ projβ ββ projβ ββ projβ)
, (Ξ» _ β (_$ refl) ββ projβ ββ projβ ββ projβ)
where
open Type-restrictions rs
full-reduction-assumptions :
let open Modality-variant variant in
{variant-ok : Β¬ β-available β Β¬ T πα΅-allowed} β
Suitable-for-full-reduction trs β
Full-reduction-assumptions (linear-or-affine variant variant-ok) trs
full-reduction-assumptions (Β¬Unit , Β¬π , Β¬β€π , Β¬β€Ο) = record
{ πβ€π = β₯-elim ββ Β¬Unit
; β‘πβπβ€π = Ξ» where
{p = π} ok β β₯-elim (Β¬π _ ok)
{p = β€π} ok β β₯-elim (Β¬β€π _ ok)
{p = β€Ο} ok β β₯-elim (Β¬β€Ο _ ok)
{p = π} _ β injβ refl
}