open import Tools.Bool
open import Tools.Level
open import Graded.Modality.Instances.Zero-one-many true as ππΟ
open import Graded.Modality.Variant lzero
module Graded.Modality.Instances.Affine
(variant : Modality-variant)
where
open Modality-variant variant
open ππΟ renaming (Zero-one-many to Affine) public
open import Graded.Modality Affine
import Graded.Modality.Properties
open import Graded.FullReduction.Assumptions
import Graded.Usage.Restrictions
import Definition.Typed.Restrictions
open import Definition.Untyped
open import Tools.Empty
open import Tools.Function
open import Tools.Nat using (Sequence)
open import Tools.Product
open import Tools.PropositionalEquality
open import Tools.Relation
open import Tools.Sum
private variable
p : Affine
pα΅’ : Sequence Affine
affineModality : Modality
affineModality = zero-one-many-modality variant
open Definition.Typed.Restrictions affineModality
open Graded.Modality.Properties affineModality
open Graded.Usage.Restrictions affineModality
private variable
rs : Type-restrictions
us : Usage-restrictions
alternative-greater :
let nrβ = zero-one-many-has-nr .Has-nr.nr
nrβ = zero-one-many-greatest-star-nr .Has-nr.nr
in
(ββ
Ξ» p r z s n β Β¬ nrβ p r z s n β‘ nrβ p r z s n) Γ
(β p r z s n β nrβ p r z s n β€ nrβ p r z s n)
alternative-greater =
(π , π , π , π , π , (Ξ» ()))
, Ξ» 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
π Ο π π π β 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
π π Ο π Ο β 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
Ο π π π π β 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
instance
affine-has-well-behaved-zero :
Has-well-behaved-zero (Modality.semiring-with-meet affineModality)
affine-has-well-behaved-zero = zero-one-many-has-well-behaved-zero
β€π : p β€ π
β€π {p = π} = refl
β€π {p = π} = refl
β€π {p = Ο} = refl
Suitable-for-full-reduction :
Type-restrictions β Set
Suitable-for-full-reduction rs =
(β p β Ξ£Λ’-allowed π p β T πα΅-allowed) Γ
(β 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
{ Ξ Ξ£-allowed = Ξ» b p q β
Ξ Ξ£-allowed b p q Γ
(b β‘ BMΞ£ π€ Γ p β‘ π β T πα΅-allowed) Γ
Β¬ (b β‘ BMΞ£ π€ Γ p β‘ Ο)
; []-cong-allowed = Ξ» s β
[]-cong-allowed s Γ T πα΅-allowed
; []-congβErased = Ξ» (okβ , okβ) β
[]-congβErased okβ .projβ , []-congβErased okβ .projβ
, (Ξ» _ β okβ) , Ξ» ()
; []-congβΒ¬Trivial =
πα΅.non-trivial ββ projβ
}
, (Ξ» _ β (_$ (refl , refl)) ββ projβ ββ projβ)
, (Ξ» _ β (_$ (refl , refl)) ββ projβ ββ projβ)
where
open Type-restrictions rs
full-reduction-assumptions :
Suitable-for-full-reduction rs β
Full-reduction-assumptions rs us
full-reduction-assumptions (πβπα΅ , Β¬Ο) = record
{ sinkβπβ€π = Ξ» _ _ β injβ refl
; β‘πβπβ€π = Ξ» where
{p = Ο} ok β β₯-elim (Β¬Ο _ ok)
{p = π} _ β injβ refl
{p = π} ok β injβ (refl , πβπα΅ _ ok , refl)
}
full-reduction-assumptions-suitable :
Full-reduction-assumptions rs us β Suitable-for-full-reduction rs
full-reduction-assumptions-suitable as =
(Ξ» p Ξ£-ok β case β‘πβπβ€π Ξ£-ok of Ξ» where
(injβ ())
(injβ (_ , πα΅-ok , _)) β πα΅-ok)
, Ξ» p Ξ£-ok β case β‘πβπβ€π Ξ£-ok of Ξ» where
(injβ ())
(injβ (() , _))
where
open Full-reduction-assumptions as
opaque
π-GLB-inv :
Semiring-with-meet.Greatest-lower-bound zero-one-many-semiring-with-meet π pα΅’ β
β i β pα΅’ i β‘ π β pα΅’ i β‘ π
π-GLB-inv π-glb i = lemma _ (π-glb .projβ i)
where
lemma : β p β π β€ p β p β‘ π β p β‘ π
lemma π _ = injβ refl
lemma π _ = injβ refl
lemma Ο ()
opaque
nrα΅’-GLB-π-inv :
let π = zero-one-many-semiring-with-meet in
β r z s β
Semiring-with-meet.Greatest-lower-bound π π (Semiring-with-meet.nrα΅’ π r z s) β
z β‘ π Γ s β‘ π
nrα΅’-GLB-π-inv r π π (πβ€ , _) = refl , refl
nrα΅’-GLB-π-inv π π π (πβ€ , _) = case πβ€ 1 of Ξ» ()
nrα΅’-GLB-π-inv π π π (πβ€ , _) = case πβ€ 1 of Ξ» ()
nrα΅’-GLB-π-inv Ο π π (πβ€ , _) = case πβ€ 1 of Ξ» ()
nrα΅’-GLB-π-inv r π Ο (πβ€ , _) = case πβ€ 1 of Ξ» ()
nrα΅’-GLB-π-inv r π s (πβ€ , _) = case πβ€ 0 of Ξ» ()
nrα΅’-GLB-π-inv r Ο s (πβ€ , _) = case πβ€ 0 of Ξ» ()
opaque
nrα΅’-GLB-π-inv :
let π = zero-one-many-semiring-with-meet in
β r z s β
Semiring-with-meet.Greatest-lower-bound π π (Semiring-with-meet.nrα΅’ π r z s) β
r β‘ π Γ z β‘ π Γ s β‘ π β r β‘ π Γ z β‘ π Γ s β‘ π β
r β‘ π Γ z β‘ π Γ s β‘ π β r β‘ π Γ z β‘ π Γ s β‘ π
nrα΅’-GLB-π-inv π π π (πβ€ , glb) = case glb π (Ξ» i β β€-reflexive (sym (nrα΅’-π i))) of Ξ» ()
nrα΅’-GLB-π-inv π π π (πβ€ , glb) = case glb π (Ξ» i β β€-reflexive (sym (nrα΅’-π i))) of Ξ» ()
nrα΅’-GLB-π-inv Ο π π (πβ€ , glb) = case glb π (Ξ» i β β€-reflexive (sym (nrα΅’-π i))) of Ξ» ()
nrα΅’-GLB-π-inv π π π (πβ€ , _) = injβ (injβ (injβ (refl , refl , refl)))
nrα΅’-GLB-π-inv π π π (πβ€ , _) = case πβ€ 2 of Ξ» ()
nrα΅’-GLB-π-inv Ο π π (πβ€ , _) = case πβ€ 2 of Ξ» ()
nrα΅’-GLB-π-inv r π Ο (πβ€ , _) = case πβ€ 1 of Ξ» ()
nrα΅’-GLB-π-inv π π π (πβ€ , _) = injβ (injβ (injβ (refl , refl , refl)))
nrα΅’-GLB-π-inv π π π (πβ€ , _) = injβ (refl , refl , refl)
nrα΅’-GLB-π-inv Ο π π (πβ€ , _) = case πβ€ 1 of Ξ» ()
nrα΅’-GLB-π-inv π π π (πβ€ , _) = injβ (injβ (refl , refl , refl))
nrα΅’-GLB-π-inv π π π (πβ€ , _) = case πβ€ 1 of Ξ» ()
nrα΅’-GLB-π-inv Ο π π (πβ€ , _) = case πβ€ 1 of Ξ» ()
nrα΅’-GLB-π-inv r π Ο (πβ€ , _) = case πβ€ 1 of Ξ» ()
nrα΅’-GLB-π-inv r Ο s (πβ€ , _) = case πβ€ 0 of Ξ» ()
opaque
nrα΅’-rπp-GLB-π-inv :
let π = zero-one-many-semiring-with-meet in
β p r β
Semiring-with-meet.Greatest-lower-bound π π (Semiring-with-meet.nrα΅’ π r π p) β
p β‘ π Γ r β‘ π β p β‘ π Γ r β‘ π β p β‘ π Γ r β‘ π
nrα΅’-rπp-GLB-π-inv p r glb =
case nrα΅’-GLB-π-inv r π p glb of Ξ» where
(injβ (rβ‘π , _ , pβ‘π)) β injβ (pβ‘π , rβ‘π)
(injβ (injβ (rβ‘π , _ , pβ‘π))) β injβ (injβ (pβ‘π , rβ‘π))
(injβ (injβ (injβ (_ , () , _))))
(injβ (injβ (injβ (rβ‘π , _ , pβ‘π)))) β injβ (injβ (pβ‘π , rβ‘π))