module Graded.Modality.Instances.Nat-plus-infinity where
import Tools.Algebra
open import Tools.Bool using (T)
open import Tools.Function
open import Tools.Level
open import Tools.Nat as N using (Nat; 1+)
open import Tools.Nullary
open import Tools.Product as Σ
open import Tools.PropositionalEquality as PE
import Tools.Reasoning.PartialOrder
import Tools.Reasoning.PropositionalEquality
open import Tools.Relation
open import Tools.Sum as ⊎ using (_⊎_; inj₁; inj₂)
open import Graded.FullReduction.Assumptions
import Graded.Modality
import Graded.Modality.Instances.BoundedStar as BoundedStar
import Graded.Modality.Instances.LowerBounded as LowerBounded
import Graded.Modality.Instances.Recursive.Sequences
import Graded.Modality.Properties.Division
import Graded.Modality.Properties.Meet
import Graded.Modality.Properties.PartialOrder
open import Graded.Modality.Variant lzero
import Definition.Typed.Restrictions
data ℕ⊎∞ : Set where
⌞_⌟ : Nat → ℕ⊎∞
∞ : ℕ⊎∞
open Definition.Typed.Restrictions ℕ⊎∞
open Graded.Modality ℕ⊎∞
open Tools.Algebra ℕ⊎∞
private variable
m n o : ℕ⊎∞
TRs : Type-restrictions
variant : Modality-variant
infixr 40 _∧_
_∧_ : ℕ⊎∞ → ℕ⊎∞ → ℕ⊎∞
∞ ∧ _ = ∞
⌞ _ ⌟ ∧ ∞ = ∞
⌞ m ⌟ ∧ ⌞ n ⌟ = ⌞ m N.⊔ n ⌟
infixr 40 _+_
_+_ : ℕ⊎∞ → ℕ⊎∞ → ℕ⊎∞
∞ + _ = ∞
⌞ _ ⌟ + ∞ = ∞
⌞ m ⌟ + ⌞ n ⌟ = ⌞ m N.+ n ⌟
infixr 45 _·_
_·_ : ℕ⊎∞ → ℕ⊎∞ → ℕ⊎∞
⌞ 0 ⌟ · _ = ⌞ 0 ⌟
_ · ⌞ 0 ⌟ = ⌞ 0 ⌟
∞ · _ = ∞
⌞ _ ⌟ · ∞ = ∞
⌞ m ⌟ · ⌞ n ⌟ = ⌞ m N.* n ⌟
infixl 45 _/_
_/_ : ℕ⊎∞ → ℕ⊎∞ → ℕ⊎∞
_ / ⌞ 0 ⌟ = ∞
⌞ m ⌟ / ⌞ 1+ n ⌟ = ⌞ m N./ 1+ n ⌟
∞ / ⌞ 1+ _ ⌟ = ∞
∞ / ∞ = ∞
⌞ _ ⌟ / ∞ = ⌞ 0 ⌟
infix 50 _*
_* : ℕ⊎∞ → ℕ⊎∞
⌞ 0 ⌟ * = ⌞ 1 ⌟
_ * = ∞
infix 10 _≤_
_≤_ : ℕ⊎∞ → ℕ⊎∞ → Set
m ≤ n = m ≡ m ∧ n
∞≤ : ∀ n → ∞ ≤ n
∞≤ _ = refl
≤0 : n ≤ ⌞ 0 ⌟
≤0 {n = ∞} = refl
≤0 {n = ⌞ n ⌟} = cong ⌞_⌟ (
n ≡˘⟨ N.⊔-identityʳ _ ⟩
n N.⊔ 0 ∎)
where
open Tools.Reasoning.PropositionalEquality
·-comm : Commutative _·_
·-comm = λ where
⌞ 0 ⌟ ⌞ 0 ⌟ → refl
⌞ 1+ _ ⌟ ⌞ 0 ⌟ → refl
⌞ 0 ⌟ ⌞ 1+ _ ⌟ → refl
⌞ 1+ m ⌟ ⌞ 1+ _ ⌟ → cong ⌞_⌟ (N.*-comm (1+ m) _)
⌞ 0 ⌟ ∞ → refl
⌞ 1+ _ ⌟ ∞ → refl
∞ ⌞ 0 ⌟ → refl
∞ ⌞ 1+ _ ⌟ → refl
∞ ∞ → refl
⌞⌟-injective : ∀ {m n} → ⌞ m ⌟ ≡ ⌞ n ⌟ → m ≡ n
⌞⌟-injective refl = refl
⌞⌟-antitone : ∀ {m n} → m N.≤ n → ⌞ n ⌟ ≤ ⌞ m ⌟
⌞⌟-antitone {m = m} {n = n} m≤n =
⌞ n ⌟ ≡˘⟨ cong ⌞_⌟ (N.m≥n⇒m⊔n≡m m≤n) ⟩
⌞ n N.⊔ m ⌟ ∎
where
open Tools.Reasoning.PropositionalEquality
⌞⌟-antitone⁻¹ : ∀ {m n} → ⌞ n ⌟ ≤ ⌞ m ⌟ → m N.≤ n
⌞⌟-antitone⁻¹ {m = m} {n = n} =
⌞ n ⌟ ≤ ⌞ m ⌟ →⟨ ⌞⌟-injective ⟩
n ≡ n N.⊔ m →⟨ N.m⊔n≡m⇒n≤m ∘→ sym ⟩
m N.≤ n □
⌞⌟·⌞⌟≡⌞*⌟ : ∀ {m n} → ⌞ m ⌟ · ⌞ n ⌟ ≡ ⌞ m N.* n ⌟
⌞⌟·⌞⌟≡⌞*⌟ {m = 0} = refl
⌞⌟·⌞⌟≡⌞*⌟ {m = 1+ _} {n = 1+ _} = refl
⌞⌟·⌞⌟≡⌞*⌟ {m = 1+ m} {n = 0} = cong ⌞_⌟ (sym (N.*-zeroʳ m))
+-decreasingˡ : m + n ≤ m
+-decreasingˡ {m = ∞} = refl
+-decreasingˡ {m = ⌞ _ ⌟} {n = ∞} = refl
+-decreasingˡ {m = ⌞ _ ⌟} {n = ⌞ n ⌟} = ⌞⌟-antitone (N.m≤m+n _ n)
*≡+·* : n * ≡ ⌞ 1 ⌟ + n · n *
*≡+·* {n = ∞} = refl
*≡+·* {n = ⌞ 0 ⌟} = refl
*≡+·* {n = ⌞ 1+ _ ⌟} = refl
*≡+*· : n * ≡ ⌞ 1 ⌟ + n * · n
*≡+*· {n = ∞} = refl
*≡+*· {n = ⌞ 0 ⌟} = refl
*≡+*· {n = ⌞ 1+ _ ⌟} = refl
_≟_ : Decidable (_≡_ {A = ℕ⊎∞})
_≟_ = λ where
∞ ∞ → yes refl
⌞ _ ⌟ ∞ → no (λ ())
∞ ⌞ _ ⌟ → no (λ ())
⌞ m ⌟ ⌞ n ⌟ → case m N.≟ n of λ where
(yes refl) → yes refl
(no m≢n) → no (λ { refl → m≢n refl })
ℕ⊎∞-semiring-with-meet : Semiring-with-meet
ℕ⊎∞-semiring-with-meet = record
{ _+_ = _+_
; _·_ = _·_
; _∧_ = _∧_
; 𝟘 = ⌞ 0 ⌟
; 𝟙 = ⌞ 1 ⌟
; +-·-Semiring = record
{ isSemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = record
{ isMonoid = record
{ isSemigroup = record
{ isMagma = record
{ isEquivalence = PE.isEquivalence
; ∙-cong = cong₂ _+_
}
; assoc = +-assoc
}
; identity =
(λ where
⌞ _ ⌟ → refl
∞ → refl)
, (λ where
⌞ _ ⌟ → cong ⌞_⌟ (N.+-identityʳ _)
∞ → refl)
}
; comm = +-comm
}
; *-isMonoid = record
{ isSemigroup = record
{ isMagma = record
{ isEquivalence = PE.isEquivalence
; ∙-cong = cong₂ _·_
}
; assoc = ·-assoc
}
; identity =
(λ where
⌞ 0 ⌟ → refl
⌞ 1+ _ ⌟ → cong ⌞_⌟ (N.+-identityʳ _)
∞ → refl)
, (λ where
⌞ 0 ⌟ → refl
⌞ 1+ _ ⌟ → cong (⌞_⌟ ∘→ 1+) (N.*-identityʳ _)
∞ → refl)
}
; distrib = ·-distrib-+
}
; zero =
(λ _ → refl)
, (λ where
⌞ 0 ⌟ → refl
⌞ 1+ _ ⌟ → refl
∞ → refl)
}
; ∧-Semilattice = record
{ isBand = record
{ isSemigroup = record
{ isMagma = record
{ isEquivalence = PE.isEquivalence
; ∙-cong = cong₂ _∧_
}
; assoc = ∧-assoc
}
; idem = λ where
⌞ _ ⌟ → cong ⌞_⌟ (N.⊔-idem _)
∞ → refl
}
; comm = ∧-comm
}
; ·-distrib-∧ = ·-distrib-∧
; +-distrib-∧ = +-distrib-∧
}
where
open Tools.Reasoning.PropositionalEquality
+-assoc : Associative _+_
+-assoc = λ where
⌞ m ⌟ ⌞ _ ⌟ ⌞ _ ⌟ → cong ⌞_⌟ (N.+-assoc m _ _)
⌞ _ ⌟ ⌞ _ ⌟ ∞ → refl
⌞ _ ⌟ ∞ _ → refl
∞ _ _ → refl
+-comm : Commutative _+_
+-comm = λ where
⌞ 0 ⌟ ⌞ 0 ⌟ → refl
⌞ 1+ _ ⌟ ⌞ 0 ⌟ → cong ⌞_⌟ (N.+-identityʳ _)
⌞ 0 ⌟ ⌞ 1+ _ ⌟ → cong ⌞_⌟ (sym (N.+-identityʳ _))
⌞ 1+ m ⌟ ⌞ 1+ _ ⌟ → cong ⌞_⌟ (N.+-comm (1+ m) _)
⌞ 0 ⌟ ∞ → refl
⌞ 1+ _ ⌟ ∞ → refl
∞ ⌞ 0 ⌟ → refl
∞ ⌞ 1+ _ ⌟ → refl
∞ ∞ → refl
·-assoc : Associative _·_
·-assoc = λ where
⌞ 0 ⌟ _ _ → refl
⌞ 1+ _ ⌟ ⌞ 0 ⌟ _ → refl
⌞ 1+ _ ⌟ ⌞ 1+ _ ⌟ ⌞ 0 ⌟ → refl
⌞ 1+ m ⌟ ⌞ 1+ n ⌟ ⌞ 1+ _ ⌟ → cong ⌞_⌟ $
N.*-assoc (1+ m) (1+ n) (1+ _)
⌞ 1+ _ ⌟ ⌞ 1+ _ ⌟ ∞ → refl
⌞ 1+ _ ⌟ ∞ ⌞ 0 ⌟ → refl
⌞ 1+ _ ⌟ ∞ ⌞ 1+ _ ⌟ → refl
⌞ 1+ _ ⌟ ∞ ∞ → refl
∞ ⌞ 0 ⌟ _ → refl
∞ ⌞ 1+ _ ⌟ ⌞ 0 ⌟ → refl
∞ ⌞ 1+ _ ⌟ ⌞ 1+ _ ⌟ → refl
∞ ⌞ 1+ _ ⌟ ∞ → refl
∞ ∞ ⌞ 0 ⌟ → refl
∞ ∞ ⌞ 1+ _ ⌟ → refl
∞ ∞ ∞ → refl
·-distribˡ-+ : _·_ DistributesOverˡ _+_
·-distribˡ-+ = λ where
⌞ 0 ⌟ _ _ → refl
⌞ 1+ _ ⌟ ⌞ 0 ⌟ ⌞ 0 ⌟ → refl
⌞ 1+ _ ⌟ ⌞ 0 ⌟ ⌞ 1+ _ ⌟ → refl
⌞ 1+ _ ⌟ ⌞ 0 ⌟ ∞ → refl
⌞ 1+ m ⌟ ⌞ 1+ n ⌟ ⌞ 0 ⌟ →
⌞ 1+ m ⌟ · (⌞ 1+ n ⌟ + ⌞ 0 ⌟) ≡⟨⟩
⌞ 1+ m N.* (1+ n N.+ 0) ⌟ ≡⟨ cong ⌞_⌟ (N.*-distribˡ-+ (1+ m) (1+ _) 0) ⟩
⌞ 1+ m N.* 1+ n N.+ 1+ m N.* 0 ⌟ ≡⟨ cong (λ o → ⌞ 1+ m N.* 1+ n N.+ o ⌟) (N.*-zeroʳ (1+ m)) ⟩
⌞ 1+ m N.* 1+ n N.+ 0 ⌟ ≡⟨⟩
⌞ 1+ m ⌟ · ⌞ 1+ n ⌟ + ⌞ 1+ m ⌟ · ⌞ 0 ⌟ ∎
⌞ 1+ m ⌟ ⌞ 1+ _ ⌟ ⌞ 1+ _ ⌟ → cong ⌞_⌟ $
N.*-distribˡ-+ (1+ m) (1+ _) (1+ _)
⌞ 1+ _ ⌟ ⌞ 1+ _ ⌟ ∞ → refl
⌞ 1+ _ ⌟ ∞ ⌞ 0 ⌟ → refl
⌞ 1+ _ ⌟ ∞ ⌞ 1+ _ ⌟ → refl
⌞ 1+ _ ⌟ ∞ ∞ → refl
∞ ⌞ 0 ⌟ ⌞ 0 ⌟ → refl
∞ ⌞ 0 ⌟ ⌞ 1+ _ ⌟ → refl
∞ ⌞ 0 ⌟ ∞ → refl
∞ ⌞ 1+ _ ⌟ ⌞ 0 ⌟ → refl
∞ ⌞ 1+ _ ⌟ ⌞ 1+ _ ⌟ → refl
∞ ⌞ 1+ _ ⌟ ∞ → refl
∞ ∞ ⌞ 0 ⌟ → refl
∞ ∞ ⌞ 1+ _ ⌟ → refl
∞ ∞ ∞ → refl
·-distrib-+ : _·_ DistributesOver _+_
·-distrib-+ =
·-distribˡ-+ , comm+distrˡ⇒distrʳ ·-comm ·-distribˡ-+
∧-assoc : Associative _∧_
∧-assoc = λ where
⌞ m ⌟ ⌞ _ ⌟ ⌞ _ ⌟ → cong ⌞_⌟ (N.⊔-assoc m _ _)
⌞ _ ⌟ ⌞ _ ⌟ ∞ → refl
⌞ _ ⌟ ∞ _ → refl
∞ _ _ → refl
∧-comm : Commutative _∧_
∧-comm = λ where
⌞ 0 ⌟ ⌞ 0 ⌟ → refl
⌞ 1+ _ ⌟ ⌞ 0 ⌟ → refl
⌞ 0 ⌟ ⌞ 1+ _ ⌟ → refl
⌞ 1+ m ⌟ ⌞ 1+ _ ⌟ → cong ⌞_⌟ (N.⊔-comm (1+ m) (1+ _))
⌞ 0 ⌟ ∞ → refl
⌞ 1+ _ ⌟ ∞ → refl
∞ ⌞ 0 ⌟ → refl
∞ ⌞ 1+ _ ⌟ → refl
∞ ∞ → refl
·-distribˡ-∧ : _·_ DistributesOverˡ _∧_
·-distribˡ-∧ = λ where
⌞ 0 ⌟ _ _ → refl
⌞ 1+ _ ⌟ ⌞ 0 ⌟ ⌞ 0 ⌟ → refl
⌞ 1+ _ ⌟ ⌞ 0 ⌟ ⌞ 1+ _ ⌟ → refl
⌞ 1+ _ ⌟ ⌞ 0 ⌟ ∞ → refl
⌞ 1+ _ ⌟ ⌞ 1+ _ ⌟ ⌞ 0 ⌟ → refl
⌞ 1+ m ⌟ ⌞ 1+ n ⌟ ⌞ 1+ _ ⌟ → cong ⌞_⌟ $
N.*-distribˡ-⊔ (1+ m) (1+ n) (1+ _)
⌞ 1+ _ ⌟ ⌞ 1+ _ ⌟ ∞ → refl
⌞ 1+ _ ⌟ ∞ ⌞ 0 ⌟ → refl
⌞ 1+ _ ⌟ ∞ ⌞ 1+ _ ⌟ → refl
⌞ 1+ _ ⌟ ∞ ∞ → refl
∞ ⌞ 0 ⌟ ⌞ 0 ⌟ → refl
∞ ⌞ 0 ⌟ ⌞ 1+ _ ⌟ → refl
∞ ⌞ 0 ⌟ ∞ → refl
∞ ⌞ 1+ _ ⌟ ⌞ 0 ⌟ → refl
∞ ⌞ 1+ _ ⌟ ⌞ 1+ _ ⌟ → refl
∞ ⌞ 1+ _ ⌟ ∞ → refl
∞ ∞ ⌞ 0 ⌟ → refl
∞ ∞ ⌞ 1+ _ ⌟ → refl
∞ ∞ ∞ → refl
·-distrib-∧ : _·_ DistributesOver _∧_
·-distrib-∧ =
·-distribˡ-∧ , comm+distrˡ⇒distrʳ ·-comm ·-distribˡ-∧
+-distribˡ-∧ : _+_ DistributesOverˡ _∧_
+-distribˡ-∧ = λ where
⌞ m ⌟ ⌞ _ ⌟ ⌞ _ ⌟ → cong ⌞_⌟ (N.+-distribˡ-⊔ m _ _)
⌞ _ ⌟ ⌞ _ ⌟ ∞ → refl
⌞ _ ⌟ ∞ _ → refl
∞ _ _ → refl
+-distrib-∧ : _+_ DistributesOver _∧_
+-distrib-∧ =
+-distribˡ-∧ , comm+distrˡ⇒distrʳ +-comm +-distribˡ-∧
ℕ⊎∞-has-well-behaved-zero :
Has-well-behaved-zero ℕ⊎∞-semiring-with-meet
ℕ⊎∞-has-well-behaved-zero = record
{ 𝟙≢𝟘 = λ ()
; is-𝟘? = _≟ ⌞ 0 ⌟
; zero-product = λ where
{p = ⌞ 0 ⌟} {q = ⌞ _ ⌟} _ → inj₁ refl
{p = ⌞ 0 ⌟} {q = ∞} _ → inj₁ refl
{p = ⌞ _ ⌟} {q = ⌞ 0 ⌟} _ → inj₂ refl
{p = ∞} {q = ⌞ 0 ⌟} _ → inj₂ refl
; +-positiveˡ = λ where
{p = ⌞ 0 ⌟} {q = ⌞ _ ⌟} _ → refl
; ∧-positiveˡ = λ where
{p = ⌞ 0 ⌟} {q = ⌞ _ ⌟} _ → refl
{p = ⌞ 1+ _ ⌟} {q = ⌞ 0 ⌟} ()
}
private
module BS =
BoundedStar
ℕ⊎∞-semiring-with-meet _* (λ _ → *≡+·*) (λ _ → inj₁ ≤0)
ℕ⊎∞-has-star-bounded-star : Has-star ℕ⊎∞-semiring-with-meet
ℕ⊎∞-has-star-bounded-star = BS.has-star
ℕ⊎∞-has-star-lower-bounded : Has-star ℕ⊎∞-semiring-with-meet
ℕ⊎∞-has-star-lower-bounded =
LowerBounded.has-star ℕ⊎∞-semiring-with-meet ∞ ∞≤
≢𝟘→⊛▷≡⊛▷ :
let module HS₁ = Has-star ℕ⊎∞-has-star-bounded-star
module HS₂ = Has-star ℕ⊎∞-has-star-lower-bounded
in
o ≢ ⌞ 0 ⌟ →
m HS₁.⊛ n ▷ o ≡ m HS₂.⊛ n ▷ o
≢𝟘→⊛▷≡⊛▷ {o = ∞} _ = refl
≢𝟘→⊛▷≡⊛▷ {o = ⌞ 1+ _ ⌟} _ = refl
≢𝟘→⊛▷≡⊛▷ {o = ⌞ 0 ⌟} 0≢0 = ⊥-elim (0≢0 refl)
⊛▷<⊛▷ :
let module HS₁ = Has-star ℕ⊎∞-has-star-bounded-star
module HS₂ = Has-star ℕ⊎∞-has-star-lower-bounded
in
(∀ m n o → m HS₂.⊛ n ▷ o ≤ m HS₁.⊛ n ▷ o) ×
(∃₃ λ m n o → m HS₂.⊛ n ▷ o ≢ m HS₁.⊛ n ▷ o)
⊛▷<⊛▷ =
BS.LowerBounded.⊛′≤⊛ ∞ (λ _ → refl)
, ⌞ 1 ⌟ , ⌞ 1 ⌟ , ⌞ 0 ⌟ , (λ ())
ℕ⊎∞-modality : Modality-variant → Modality
ℕ⊎∞-modality variant =
BS.isModality
variant
(λ _ → ℕ⊎∞-has-well-behaved-zero)
(λ _ _ _ _ → +-decreasingˡ)
private
module D = Graded.Modality.Properties.Division ℕ⊎∞-semiring-with-meet
/≡/ : m D./ n ≡ m / n
/≡/ {m = ∞} {n = ∞} = refl , λ _ _ → refl
/≡/ {m = ⌞ _ ⌟} {n = ∞} = ≤0 , λ { ⌞ 0 ⌟ _ → refl }
/≡/ {n = ⌞ 0 ⌟} = ≤0 , λ _ _ → refl
/≡/ {m = ∞} {n = ⌞ 1+ _ ⌟} = refl , λ _ _ → refl
/≡/ {m = ⌞ m ⌟} {n = ⌞ 1+ n ⌟} =
(begin
⌞ m ⌟ ≤⟨ ⌞⌟-antitone (N.m/n*n≤m _ (1+ _)) ⟩
⌞ (m N./ 1+ n) N.* 1+ n ⌟ ≡⟨ cong ⌞_⌟ (N.*-comm _ (1+ n)) ⟩
⌞ 1+ n N.* (m N./ 1+ n) ⌟ ≡˘⟨ ⌞⌟·⌞⌟≡⌞*⌟ ⟩
⌞ 1+ n ⌟ · ⌞ m N./ 1+ n ⌟ ∎)
, λ where
⌞ o ⌟ →
⌞ m ⌟ ≤ ⌞ 1+ n ⌟ · ⌞ o ⌟ ≡⟨ cong (_ ≤_) ⌞⌟·⌞⌟≡⌞*⌟ ⟩→
⌞ m ⌟ ≤ ⌞ 1+ n N.* o ⌟ →⟨ ⌞⌟-antitone⁻¹ ⟩
1+ n N.* o N.≤ m →⟨ N.*≤→≤/ ⟩
o N.≤ m N./ 1+ n →⟨ ⌞⌟-antitone ⟩
⌞ m N./ 1+ n ⌟ ≤ ⌞ o ⌟ □
where
open Graded.Modality.Properties.PartialOrder ℕ⊎∞-semiring-with-meet
open Tools.Reasoning.PartialOrder ≤-poset
open Graded.Modality.Instances.Recursive.Sequences
ℕ⊎∞-semiring-with-meet
¬-Has-fixpoints-nr : ¬ Has-fixpoints-nr
¬-Has-fixpoints-nr =
(∀ r → ∃ λ n → ∀ p q → nr (1+ n) p q r ≡ nr n p q r) →⟨ (λ hyp → Σ.map idᶠ (λ f → f p q) (hyp r)) ⟩
(∃ λ n → nr (1+ n) p q r ≡ nr n p q r) →⟨ Σ.map idᶠ (λ {x = n} → trans (sym (increasing n))) ⟩
(∃ λ n → ⌞ 1 ⌟ + nr n p q r ≡ nr n p q r) →⟨ (λ (n , hyp) →
_
, subst (λ n → ⌞ 1 ⌟ + n ≡ n) (always-⌞⌟ n .proj₂) hyp) ⟩
(∃ λ n → ⌞ 1+ n ⌟ ≡ ⌞ n ⌟) →⟨ (λ { (_ , ()) }) ⟩
⊥ □
where
open module S = Semiring-with-meet ℕ⊎∞-semiring-with-meet using (𝟘; 𝟙)
open Graded.Modality.Properties.Meet ℕ⊎∞-semiring-with-meet
open Tools.Reasoning.PropositionalEquality
r = 𝟙
p = 𝟘
q = 𝟙
increasing : ∀ n → nr (1+ n) p q r ≡ 𝟙 + nr n p q r
increasing 0 = refl
increasing (1+ n) =
p ∧ (q + r · nr (1+ n) p q r) ≡⟨ largest→∧≡ʳ (λ _ → ≤0) ⟩
q + r · nr (1+ n) p q r ≡⟨ cong (λ n → q + r · n) (increasing n) ⟩
q + r · (𝟙 + nr n p q r) ≡⟨ cong (q +_) (S.·-identityˡ _) ⟩
q + (𝟙 + nr n p q r) ≡˘⟨ S.+-assoc _ _ _ ⟩
(q + 𝟙) + nr n p q r ≡⟨ cong (_+ nr n p q r) (S.+-comm q _) ⟩
(𝟙 + q) + nr n p q r ≡⟨ S.+-assoc _ _ _ ⟩
𝟙 + (q + nr n p q r) ≡˘⟨ cong ((𝟙 +_) ∘→ (q +_)) (S.·-identityˡ _) ⟩
𝟙 + (q + r · nr n p q r) ≡˘⟨ cong (𝟙 +_) (largest→∧≡ʳ (λ _ → ≤0)) ⟩
𝟙 + (p ∧ (q + r · nr n p q r)) ∎
always-⌞⌟ : ∀ m → ∃ λ n → nr m p q r ≡ ⌞ n ⌟
always-⌞⌟ 0 = _ , refl
always-⌞⌟ (1+ m) =
case always-⌞⌟ m of λ {
(n , eq) →
1+ n
, (nr (1+ m) p q r ≡⟨ increasing m ⟩
𝟙 + nr m p q r ≡⟨ cong (𝟙 +_) eq ⟩
⌞ 1+ n ⌟ ∎) }
Suitable-for-full-reduction :
Modality-variant → Type-restrictions → Set
Suitable-for-full-reduction variant TRs =
∀ m n → Σₚ-allowed m n → m ≡ ⌞ 1 ⌟ ⊎ m ≡ ⌞ 0 ⌟ × T 𝟘ᵐ-allowed
where
open Modality-variant variant
open Type-restrictions TRs
suitable-for-full-reduction :
(variant : Modality-variant) → Type-restrictions →
∃ (Suitable-for-full-reduction variant)
suitable-for-full-reduction variant TRs =
record TRs
{ ΠΣ-allowed = λ b m n →
ΠΣ-allowed b m n ×
(m ≡ ⌞ 1 ⌟ ⊎ m ≡ ⌞ 0 ⌟ × T 𝟘ᵐ-allowed)
}
, (λ _ _ (_ , ok) → ok)
where
open Modality-variant variant
open Type-restrictions TRs
full-reduction-assumptions :
Suitable-for-full-reduction variant TRs →
Full-reduction-assumptions (ℕ⊎∞-modality variant) TRs
full-reduction-assumptions ok = record
{ 𝟙≤𝟘 = λ _ → refl
; ≡𝟙⊎𝟙≤𝟘 = ⊎.map idᶠ (λ (p≡⌞0⌟ , ok) → p≡⌞0⌟ , ok , refl) ∘→ ok _ _
}