open import Tools.Level
open import Graded.Modality.Instances.Erasure
open import Graded.Modality.Variant lzero
module Graded.Modality.Instances.Erasure.Properties
(variant : Modality-variant)
where
open Modality-variant variant
open import Graded.Modality.Instances.Erasure.Modality
open import Graded.Context (ErasureModality variant)
open import Graded.Context.Properties (ErasureModality variant) public
hiding (+ᶜ-decreasingˡ)
open import Graded.FullReduction.Assumptions
open import Graded.Modality.Properties (ErasureModality variant) as P
public
open import Graded.Usage (ErasureModality variant)
open import Graded.Usage.Inversion (ErasureModality variant)
open import Graded.Mode (ErasureModality variant)
open import Definition.Typed.Restrictions Erasure
open import Definition.Untyped Erasure
open import Tools.Algebra Erasure
open import Tools.Bool hiding (_∧_)
open import Tools.Empty
open import Tools.Fin
open import Tools.Function
open import Tools.Nat using (Nat)
open import Tools.Nullary
open import Tools.Product
open import Tools.PropositionalEquality as PE using (_≡_; _≢_)
import Tools.Reasoning.PartialOrder
import Tools.Reasoning.PropositionalEquality
open import Tools.Sum
open import Tools.Unit
private
module EM = Modality (ErasureModality variant)
private
variable
m n : Nat
σ σ′ : Subst m n
γ δ : Conₘ n
t u a : Term n
x : Fin n
p : Erasure
mo : Mode
rs : Type-restrictions
+-decreasingʳ : (p q : Erasure) → (p + q) ≤ q
+-decreasingʳ 𝟘 𝟘 = PE.refl
+-decreasingʳ 𝟘 ω = PE.refl
+-decreasingʳ ω 𝟘 = PE.refl
+-decreasingʳ ω ω = PE.refl
+ᶜ-decreasingˡ : (γ δ : Conₘ n) → γ +ᶜ δ ≤ᶜ γ
+ᶜ-decreasingˡ ε ε = ≤ᶜ-refl
+ᶜ-decreasingˡ (γ ∙ p) (δ ∙ q) = (+ᶜ-decreasingˡ γ δ) ∙ (+-decreasingˡ p q)
+ᶜ-decreasingʳ : (γ δ : Conₘ n) → γ +ᶜ δ ≤ᶜ δ
+ᶜ-decreasingʳ ε ε = ≤ᶜ-refl
+ᶜ-decreasingʳ (γ ∙ p) (δ ∙ q) = (+ᶜ-decreasingʳ γ δ) ∙ (+-decreasingʳ p q)
+ᶜ-idem : (γ : Conₘ n) → γ +ᶜ γ PE.≡ γ
+ᶜ-idem ε = PE.refl
+ᶜ-idem (γ ∙ p) = PE.cong₂ _∙_ (+ᶜ-idem γ) (+-Idempotent p)
⊛-decreasingˡ : (p q r : Erasure) → p ⊛ q ▷ r ≤ p
⊛-decreasingˡ 𝟘 𝟘 r = PE.refl
⊛-decreasingˡ 𝟘 ω r = PE.refl
⊛-decreasingˡ ω 𝟘 r = PE.refl
⊛-decreasingˡ ω ω r = PE.refl
⊛-decreasingʳ : (p q r : Erasure) → p ⊛ q ▷ r ≤ q
⊛-decreasingʳ 𝟘 𝟘 r = PE.refl
⊛-decreasingʳ 𝟘 ω 𝟘 = PE.refl
⊛-decreasingʳ 𝟘 ω ω = PE.refl
⊛-decreasingʳ ω 𝟘 r = PE.refl
⊛-decreasingʳ ω ω r = PE.refl
⊛ᶜ-decreasingˡ : (γ δ : Conₘ n) (r : Erasure) → γ ⊛ᶜ δ ▷ r ≤ᶜ γ
⊛ᶜ-decreasingˡ ε ε r = ≤ᶜ-refl
⊛ᶜ-decreasingˡ (γ ∙ 𝟘) (δ ∙ 𝟘) r = (⊛ᶜ-decreasingˡ γ δ r) ∙ PE.refl
⊛ᶜ-decreasingˡ (γ ∙ 𝟘) (δ ∙ ω) r = (⊛ᶜ-decreasingˡ γ δ r) ∙ PE.refl
⊛ᶜ-decreasingˡ (γ ∙ ω) (δ ∙ 𝟘) r = (⊛ᶜ-decreasingˡ γ δ r) ∙ PE.refl
⊛ᶜ-decreasingˡ (γ ∙ ω) (δ ∙ ω) r = (⊛ᶜ-decreasingˡ γ δ r) ∙ PE.refl
⊛ᶜ-decreasingʳ : (γ δ : Conₘ n) (r : Erasure) → γ ⊛ᶜ δ ▷ r ≤ᶜ δ
⊛ᶜ-decreasingʳ ε ε r = ≤ᶜ-refl
⊛ᶜ-decreasingʳ (γ ∙ 𝟘) (δ ∙ 𝟘) r = ⊛ᶜ-decreasingʳ γ δ r ∙ PE.refl
⊛ᶜ-decreasingʳ (γ ∙ 𝟘) (δ ∙ ω) r = ⊛ᶜ-decreasingʳ γ δ r ∙ PE.refl
⊛ᶜ-decreasingʳ (γ ∙ ω) (δ ∙ 𝟘) r = ⊛ᶜ-decreasingʳ γ δ r ∙ PE.refl
⊛ᶜ-decreasingʳ (γ ∙ ω) (δ ∙ ω) r = ⊛ᶜ-decreasingʳ γ δ r ∙ PE.refl
greatest-elem : (p : Erasure) → p ≤ 𝟘
greatest-elem 𝟘 = PE.refl
greatest-elem ω = PE.refl
least-elem : (p : Erasure) → ω ≤ p
least-elem p = PE.refl
greatest-elem′ : (p : Erasure) → 𝟘 ≤ p → p PE.≡ 𝟘
greatest-elem′ p 𝟘≤p = ≤-antisym (greatest-elem p) 𝟘≤p
least-elem′ : (p : Erasure) → p ≤ ω → p PE.≡ ω
least-elem′ p p≤ω = ≤-antisym p≤ω (least-elem p)
greatest-elemᶜ : (γ : Conₘ n) → γ ≤ᶜ 𝟘ᶜ
greatest-elemᶜ ε = ε
greatest-elemᶜ (γ ∙ p) = (greatest-elemᶜ γ) ∙ (greatest-elem p)
least-elemᶜ : (γ : Conₘ n) → 𝟙ᶜ ≤ᶜ γ
least-elemᶜ ε = ε
least-elemᶜ (γ ∙ p) = (least-elemᶜ γ) ∙ (least-elem p)
∧ᶜ≈ᶜ+ᶜ : γ ∧ᶜ δ ≈ᶜ γ +ᶜ δ
∧ᶜ≈ᶜ+ᶜ {γ = ε} {δ = ε} = ≈ᶜ-refl
∧ᶜ≈ᶜ+ᶜ {γ = _ ∙ _} {δ = _ ∙ _} = ∧ᶜ≈ᶜ+ᶜ ∙ PE.refl
⌞ω⌟≡𝟙ᵐ : ⌞ ω ⌟ ≡ 𝟙ᵐ
⌞ω⌟≡𝟙ᵐ = 𝟙ᵐ′≡𝟙ᵐ
≢𝟘→≡ω : p ≢ 𝟘 → p ≡ ω
≢𝟘→≡ω {p = 𝟘} 𝟘≢𝟘 = ⊥-elim (𝟘≢𝟘 PE.refl)
≢𝟘→≡ω {p = ω} _ = PE.refl
/≡/ : ∀ p q → p P./ q ≡ (p / q)
/≡/ = λ where
𝟘 𝟘 → PE.refl , λ _ → λ _ → PE.refl
ω 𝟘 → PE.refl , λ _ → idᶠ
𝟘 ω → PE.refl , λ _ → idᶠ
ω ω → PE.refl , λ _ → idᶠ
Suitable-for-full-reduction :
Type-restrictions → Set
Suitable-for-full-reduction rs =
∀ p → Σₚ-allowed 𝟘 p → T 𝟘ᵐ-allowed
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 × T 𝟘ᵐ-allowed
}
, (λ _ → proj₂)
where
open Type-restrictions rs
full-reduction-assumptions :
Suitable-for-full-reduction rs →
Full-reduction-assumptions (ErasureModality variant) rs
full-reduction-assumptions {rs = rs} 𝟘→𝟘ᵐ = record
{ 𝟙≤𝟘 = λ _ → PE.refl
; ≡𝟙⊎𝟙≤𝟘 = λ where
{p = ω} _ → inj₁ PE.refl
{p = 𝟘} ok → inj₂ (PE.refl , 𝟘→𝟘ᵐ _ ok , PE.refl)
}
+-unique :
(_+_ : Op₂ Erasure) →
Identity 𝟘 _+_ →
_+_ DistributesOverˡ _∧_ →
∀ p q → (p + q) ≡ p ∧ q
+-unique _+_ (identityˡ , identityʳ) +-distrib-∧ˡ = λ where
𝟘 q →
let open Tools.Reasoning.PropositionalEquality in
𝟘 + q ≡⟨ identityˡ _ ⟩
q ≡⟨⟩
𝟘 ∧ q ∎
p 𝟘 →
let open Tools.Reasoning.PropositionalEquality in
p + 𝟘 ≡⟨ identityʳ _ ⟩
p ≡⟨ EM.∧-comm 𝟘 _ ⟩
p ∧ 𝟘 ∎
ω ω →
let open Tools.Reasoning.PartialOrder ≤-poset in
≤-antisym
(begin
ω + ω ≤⟨ +-distrib-∧ˡ ω ω 𝟘 ⟩
ω + 𝟘 ≡⟨ identityʳ _ ⟩
ω ∎)
(begin
ω ≤⟨ least-elem (ω + ω) ⟩
ω + ω ∎)
·-unique :
(_·′_ : Op₂ Erasure) →
Zero 𝟘 _·′_ →
LeftIdentity ω _·′_ →
∀ p q → (p ·′ q) ≡ p · q
·-unique _·′_ (zeroˡ , zeroʳ) identityˡ = λ where
𝟘 q →
𝟘 ·′ q ≡⟨ zeroˡ _ ⟩
𝟘 ≡⟨⟩
𝟘 · q ∎
p 𝟘 →
p ·′ 𝟘 ≡⟨ zeroʳ _ ⟩
𝟘 ≡˘⟨ EM.·-zeroʳ _ ⟩
p · 𝟘 ∎
ω ω →
ω ·′ ω ≡⟨ identityˡ _ ⟩
ω ≡⟨⟩
ω · ω ∎
where
open Tools.Reasoning.PropositionalEquality
⊛-unique :
(_⊛_▷_ : Op₃ Erasure) →
(∀ p q r → (p ⊛ q ▷ r) ≤ q + r · (p ⊛ q ▷ r)) →
(∀ p q r → (p ⊛ q ▷ r) ≤ p) →
(∀ r → _·_ SubDistributesOverʳ (_⊛_▷ r) by _≤_) →
∀ p q r → (p ⊛ q ▷ r) ≡ p ∧ q
⊛-unique _⊛_▷_ ⊛-ineq₁ ⊛-ineq₂ ·-sub-distribʳ-⊛ = λ where
ω q r → ≤-antisym
(begin
ω ⊛ q ▷ r ≤⟨ ⊛-ineq₂ ω q r ⟩
ω ∎)
(begin
ω ≤⟨ least-elem (ω ⊛ q ▷ r) ⟩
ω ⊛ q ▷ r ∎)
p ω r → ≤-antisym
(begin
p ⊛ ω ▷ r ≤⟨ ⊛-ineq₁ p ω r ⟩
ω ≡⟨ EM.∧-comm ω _ ⟩
p ∧ ω ∎)
(begin
p ∧ ω ≡⟨ EM.∧-comm p _ ⟩
ω ≤⟨ least-elem (p ⊛ ω ▷ r) ⟩
p ⊛ ω ▷ r ∎)
𝟘 𝟘 r → ≤-antisym
(begin
𝟘 ⊛ 𝟘 ▷ r ≤⟨ greatest-elem _ ⟩
𝟘 ∎)
(begin
𝟘 ≡˘⟨ EM.·-zeroʳ _ ⟩
(ω ⊛ 𝟘 ▷ r) · 𝟘 ≤⟨ ·-sub-distribʳ-⊛ r 𝟘 ω 𝟘 ⟩
𝟘 ⊛ 𝟘 ▷ r ∎)
where
open Tools.Reasoning.PartialOrder ≤-poset