import Graded.Modality
open import Graded.Usage.Restrictions
module Graded.Substitution.Properties
{a} {M : Set a}
(open Graded.Modality M)
(𝕄 : Modality)
(R : Usage-restrictions M)
where
open Modality 𝕄
open import Graded.Context 𝕄
open import Graded.Context.Properties 𝕄
open import Graded.Substitution 𝕄 R
open import Graded.Modality.Dedicated-star 𝕄
open import Graded.Modality.Natrec-star-instances
open import Graded.Modality.Properties 𝕄
open import Graded.Usage 𝕄 R
open import Graded.Usage.Properties 𝕄 R
open import Graded.Usage.Weakening 𝕄 R
open import Graded.Mode 𝕄
open import Definition.Untyped M renaming (_[_,_] to _[_,,_])
open import Tools.Bool using (T)
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
import Tools.Reasoning.Equivalence
import Tools.Reasoning.PartialOrder
import Tools.Reasoning.PropositionalEquality
import Tools.Relation
open import Tools.Sum using (_⊎_; inj₁; inj₂)
private
variable
ℓ m n : Nat
x y : Fin n
γ γ′ δ η θ χ : Conₘ n
t u u′ : Term n
σ : Subst m n
p q r : M
mo : Mode
mos mos₁ mos₂ : Mode-vector n
<*-distrib-+ᶜ : (Ψ : Substₘ m n) (γ δ : Conₘ n) → (γ +ᶜ δ) <* Ψ ≈ᶜ γ <* Ψ +ᶜ δ <* Ψ
<*-distrib-+ᶜ [] ε ε = ≈ᶜ-sym (+ᶜ-identityˡ 𝟘ᶜ)
<*-distrib-+ᶜ (Ψ ⊙ η) (γ ∙ p) (δ ∙ q) = begin
((γ ∙ p) +ᶜ (δ ∙ q)) <* (Ψ ⊙ η)
≈⟨ +ᶜ-cong (·ᶜ-distribʳ-+ᶜ p q η) (<*-distrib-+ᶜ Ψ γ δ) ⟩
(p ·ᶜ η +ᶜ q ·ᶜ η) +ᶜ γ <* Ψ +ᶜ δ <* Ψ
≈⟨ +ᶜ-congˡ (+ᶜ-comm (γ <* Ψ) (δ <* Ψ)) ⟩
(p ·ᶜ η +ᶜ q ·ᶜ η) +ᶜ δ <* Ψ +ᶜ γ <* Ψ
≈⟨ +ᶜ-assoc (p ·ᶜ η) (q ·ᶜ η) (δ <* Ψ +ᶜ γ <* Ψ) ⟩
p ·ᶜ η +ᶜ q ·ᶜ η +ᶜ δ <* Ψ +ᶜ γ <* Ψ
≈⟨ +ᶜ-comm (p ·ᶜ η) (q ·ᶜ η +ᶜ δ <* Ψ +ᶜ γ <* Ψ) ⟩
(q ·ᶜ η +ᶜ δ <* Ψ +ᶜ γ <* Ψ) +ᶜ p ·ᶜ η
≈⟨ +ᶜ-assoc _ _ _ ⟩
q ·ᶜ η +ᶜ (δ <* Ψ +ᶜ γ <* Ψ) +ᶜ p ·ᶜ η
≈⟨ +ᶜ-congˡ (+ᶜ-assoc (δ <* Ψ) (γ <* Ψ) (p ·ᶜ η)) ⟩
q ·ᶜ η +ᶜ δ <* Ψ +ᶜ γ <* Ψ +ᶜ p ·ᶜ η
≈˘⟨ +ᶜ-assoc _ _ _ ⟩
(q ·ᶜ η +ᶜ δ <* Ψ) +ᶜ γ <* Ψ +ᶜ p ·ᶜ η
≈⟨ +ᶜ-congˡ (+ᶜ-comm (γ <* Ψ) (p ·ᶜ η)) ⟩
(q ·ᶜ η +ᶜ δ <* Ψ) +ᶜ p ·ᶜ η +ᶜ γ <* Ψ
≈⟨ +ᶜ-comm _ _ ⟩
((p ·ᶜ η +ᶜ γ <* Ψ) +ᶜ q ·ᶜ η +ᶜ δ <* Ψ) ∎
where open Tools.Reasoning.Equivalence Conₘ-setoid
<*-distrib-·ᶜ : (Ψ : Substₘ m n) (p : M) (γ : Conₘ n)
→ (p ·ᶜ γ) <* Ψ ≈ᶜ p ·ᶜ (γ <* Ψ)
<*-distrib-·ᶜ [] p ε = ≈ᶜ-sym (·ᶜ-zeroʳ p)
<*-distrib-·ᶜ (Ψ ⊙ δ) p (γ ∙ q) = begin
(p · q) ·ᶜ δ +ᶜ (p ·ᶜ γ) <* Ψ ≈⟨ +ᶜ-cong (·ᶜ-assoc p q δ) (<*-distrib-·ᶜ Ψ p γ) ⟩
p ·ᶜ (q ·ᶜ δ) +ᶜ p ·ᶜ (γ <* Ψ) ≈˘⟨ ·ᶜ-distribˡ-+ᶜ p (q ·ᶜ δ) (γ <* Ψ) ⟩
p ·ᶜ (q ·ᶜ δ +ᶜ γ <* Ψ) ∎
where open Tools.Reasoning.Equivalence Conₘ-setoid
<*-linear : (Ψ : Substₘ m n) (p q : M) (γ δ : Conₘ n)
→ (p ·ᶜ γ +ᶜ q ·ᶜ δ) <* Ψ ≈ᶜ p ·ᶜ γ <* Ψ +ᶜ q ·ᶜ δ <* Ψ
<*-linear Ψ p q γ δ = begin
(p ·ᶜ γ +ᶜ q ·ᶜ δ) <* Ψ ≈⟨ <*-distrib-+ᶜ Ψ (p ·ᶜ γ) (q ·ᶜ δ) ⟩
(p ·ᶜ γ) <* Ψ +ᶜ (q ·ᶜ δ) <* Ψ ≈⟨ +ᶜ-cong (<*-distrib-·ᶜ Ψ p γ) (<*-distrib-·ᶜ Ψ q δ) ⟩
(p ·ᶜ γ <* Ψ +ᶜ q ·ᶜ δ <* Ψ) ∎
where open Tools.Reasoning.Equivalence Conₘ-setoid
<*-sub-distrib-∧ᶜ : (Ψ : Substₘ m n) (γ δ : Conₘ n) → (γ ∧ᶜ δ) <* Ψ ≤ᶜ γ <* Ψ ∧ᶜ δ <* Ψ
<*-sub-distrib-∧ᶜ [] ε ε = begin
𝟘ᶜ ≈˘⟨ ∧ᶜ-idem _ ⟩
𝟘ᶜ ∧ᶜ 𝟘ᶜ ∎
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
<*-sub-distrib-∧ᶜ (Ψ ⊙ η) (γ ∙ p) (δ ∙ q) = begin
(p ∧ q) ·ᶜ η +ᶜ (γ ∧ᶜ δ) <* Ψ ≤⟨ +ᶜ-monotone (≤ᶜ-reflexive (·ᶜ-distribʳ-∧ᶜ _ _ _))
(<*-sub-distrib-∧ᶜ Ψ γ δ) ⟩
(p ·ᶜ η ∧ᶜ q ·ᶜ η) +ᶜ (γ <* Ψ ∧ᶜ δ <* Ψ) ≤⟨ +ᶜ-sub-interchangeable-∧ᶜ _ _ _ _ ⟩
(p ·ᶜ η +ᶜ γ <* Ψ) ∧ᶜ q ·ᶜ η +ᶜ δ <* Ψ ∎
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
<*-sub-distrib-⊛ᶜ :
⦃ has-star : Has-star semiring-with-meet ⦄ →
(Ψ : Substₘ m n) (γ δ : Conₘ n) (r : M) →
(γ ⊛ᶜ δ ▷ r) <* Ψ ≤ᶜ (γ <* Ψ) ⊛ᶜ (δ <* Ψ) ▷ r
<*-sub-distrib-⊛ᶜ [] ε ε r = ≤ᶜ-reflexive (≈ᶜ-sym (⊛ᶜ-idem-𝟘ᶜ r))
<*-sub-distrib-⊛ᶜ (Ψ ⊙ η) (γ ∙ p) (δ ∙ q) r = begin
((γ ∙ p) ⊛ᶜ (δ ∙ q) ▷ r) <* (Ψ ⊙ η)
≡⟨⟩
(γ ⊛ᶜ δ ▷ r ∙ p ⊛ q ▷ r) <* (Ψ ⊙ η)
≡⟨⟩
p ⊛ q ▷ r ·ᶜ η +ᶜ (γ ⊛ᶜ δ ▷ r) <* Ψ
≤⟨ +ᶜ-monotone (·ᶜ-sub-distribʳ-⊛ p q r η) (<*-sub-distrib-⊛ᶜ Ψ γ δ r) ⟩
(p ·ᶜ η) ⊛ᶜ (q ·ᶜ η) ▷ r +ᶜ (γ <* Ψ) ⊛ᶜ (δ <* Ψ) ▷ r
≤⟨ +ᶜ-sub-interchangeable-⊛ᶜ r (p ·ᶜ η) (q ·ᶜ η) (γ <* Ψ) (δ <* Ψ) ⟩
(p ·ᶜ η +ᶜ γ <* Ψ) ⊛ᶜ (q ·ᶜ η +ᶜ δ <* Ψ) ▷ r
≡⟨⟩
((γ ∙ p) <* (Ψ ⊙ η)) ⊛ᶜ ((δ ∙ q) <* (Ψ ⊙ η)) ▷ r ∎
where open Tools.Reasoning.PartialOrder ≤ᶜ-poset
<*-zeroˡ : (Ψ : Substₘ m n) → 𝟘ᶜ <* Ψ ≈ᶜ 𝟘ᶜ
<*-zeroˡ [] = ≈ᶜ-refl
<*-zeroˡ (Ψ ⊙ γ) = begin
𝟘ᶜ <* (Ψ ⊙ γ) ≡⟨⟩
𝟘 ·ᶜ γ +ᶜ (𝟘ᶜ <* Ψ) ≈⟨ +ᶜ-cong (·ᶜ-zeroˡ γ) (<*-zeroˡ Ψ) ⟩
𝟘ᶜ +ᶜ 𝟘ᶜ ≈⟨ +ᶜ-identityˡ 𝟘ᶜ ⟩
𝟘ᶜ ∎
where open Tools.Reasoning.Equivalence Conₘ-setoid
<*-zeroʳ : (γ : Conₘ n) → γ <* εₘ ≈ᶜ ε
<*-zeroʳ ε = ε
<*-zeroʳ (γ ∙ p) = begin
ε +ᶜ γ <* εₘ ≈⟨ +ᶜ-congˡ (<*-zeroʳ γ) ⟩
ε +ᶜ ε ≈⟨ +ᶜ-identityˡ _ ⟩
ε ∎
where
open Tools.Reasoning.Equivalence Conₘ-setoid
<*-monotone : {γ δ : Conₘ n} (Ψ : Substₘ m n) → γ ≤ᶜ δ → γ <* Ψ ≤ᶜ δ <* Ψ
<*-monotone {γ = ε} {ε} [] γ≤δ = ≤ᶜ-refl
<*-monotone {γ = γ ∙ p} {δ ∙ q} (Ψ ⊙ η) (γ≤δ ∙ p≤q) =
+ᶜ-monotone (·ᶜ-monotoneˡ p≤q) (<*-monotone Ψ γ≤δ)
<*-cong : (Ψ : Substₘ m n) → γ ≈ᶜ δ → γ <* Ψ ≈ᶜ δ <* Ψ
<*-cong Ψ γ≈ᶜδ = ≤ᶜ-antisym
(<*-monotone Ψ (≤ᶜ-reflexive γ≈ᶜδ))
(<*-monotone Ψ (≤ᶜ-reflexive (≈ᶜ-sym γ≈ᶜδ)))
<*-<*>-assoc : {ℓ m n : Nat} (Ψ : Substₘ m n) (Φ : Substₘ n ℓ) (γ : Conₘ ℓ)
→ γ <* (Ψ <*> Φ) ≈ᶜ (γ <* Φ) <* Ψ
<*-<*>-assoc Ψ [] ε = ≈ᶜ-sym (<*-zeroˡ Ψ)
<*-<*>-assoc Ψ (Φ ⊙ δ) (γ ∙ p) = begin
p ·ᶜ (δ <* Ψ) +ᶜ γ <* (Ψ <*> Φ) ≈⟨ +ᶜ-cong (≈ᶜ-sym (<*-distrib-·ᶜ Ψ p δ)) (<*-<*>-assoc Ψ Φ γ) ⟩
(p ·ᶜ δ) <* Ψ +ᶜ (γ <* Φ) <* Ψ ≈˘⟨ <*-distrib-+ᶜ Ψ (p ·ᶜ δ) (γ <* Φ) ⟩
(p ·ᶜ δ +ᶜ γ <* Φ) <* Ψ ∎
where open Tools.Reasoning.Equivalence Conₘ-setoid
·ᶜ-<*-𝟘ᶜ,≔𝟙 :
(Ψ : Substₘ m n) →
p ·ᶜ (𝟘ᶜ , x ≔ 𝟙) <* Ψ ≈ᶜ (𝟘ᶜ , x ≔ p) <* Ψ
·ᶜ-<*-𝟘ᶜ,≔𝟙 {p = p} {x = x} Ψ = begin
p ·ᶜ (𝟘ᶜ , x ≔ 𝟙) <* Ψ ≈˘⟨ <*-distrib-·ᶜ Ψ _ (𝟘ᶜ , x ≔ 𝟙) ⟩
(p ·ᶜ (𝟘ᶜ , x ≔ 𝟙)) <* Ψ ≡˘⟨ cong (_<* Ψ) (update-distrib-·ᶜ 𝟘ᶜ p 𝟙 x) ⟩
(p ·ᶜ 𝟘ᶜ , x ≔ p · 𝟙) <* Ψ ≈⟨ <*-cong Ψ (update-cong (·ᶜ-zeroʳ _) (·-identityʳ _)) ⟩
(𝟘ᶜ , x ≔ p) <* Ψ ∎
where
open Tools.Reasoning.Equivalence Conₘ-setoid
wk1Substₘ-app : (Ψ : Substₘ m n) (γ : Conₘ n) → γ <* wk1Substₘ Ψ ≈ᶜ (γ <* Ψ) ∙ 𝟘
wk1Substₘ-app [] ε = ≈ᶜ-refl
wk1Substₘ-app (Ψ ⊙ δ) (γ ∙ p) = begin
(γ ∙ p) <* wk1Substₘ (Ψ ⊙ δ) ≡⟨⟩
((p ·ᶜ δ) ∙ (p · 𝟘)) +ᶜ γ <* wk1Substₘ Ψ
≈⟨ +ᶜ-cong (≈ᶜ-refl ∙ (·-zeroʳ p)) (wk1Substₘ-app Ψ γ) ⟩
((p ·ᶜ δ) ∙ 𝟘) +ᶜ ((γ <* Ψ) ∙ 𝟘)
≡⟨⟩
(p ·ᶜ δ) +ᶜ (γ <* Ψ) ∙ (𝟘 + 𝟘)
≈⟨ ≈ᶜ-refl ∙ (+-identityˡ 𝟘) ⟩
((γ ∙ p) <* (Ψ ⊙ δ)) ∙ 𝟘 ∎
where open Tools.Reasoning.Equivalence Conₘ-setoid
liftSubstₘ-app : (Ψ : Substₘ m n) (γ : Conₘ n) (p : M)
→ (γ ∙ p) <* liftSubstₘ Ψ ≈ᶜ (γ <* Ψ) ∙ p
liftSubstₘ-app [] ε p = begin
(ε ∙ p) <* liftSubstₘ [] ≡⟨⟩
(ε ∙ p) <* ([] ⊙ (𝟘ᶜ ∙ 𝟙)) ≡⟨⟩
p ·ᶜ (𝟘ᶜ ∙ 𝟙) +ᶜ 𝟘ᶜ ≡⟨⟩
((p ·ᶜ 𝟘ᶜ) ∙ (p · 𝟙)) +ᶜ 𝟘ᶜ ≈⟨ +ᶜ-identityʳ _ ⟩
(p ·ᶜ 𝟘ᶜ) ∙ (p · 𝟙) ≈⟨ (·ᶜ-zeroʳ p) ∙ (·-identityʳ p) ⟩
𝟘ᶜ ∙ p ≡⟨⟩
(ε <* []) ∙ p ∎
where open Tools.Reasoning.Equivalence Conₘ-setoid
liftSubstₘ-app (Ψ ⊙ η) γ p = begin
(γ ∙ p) <* liftSubstₘ (Ψ ⊙ η)
≡⟨⟩
(γ ∙ p) <* (wk1Substₘ (Ψ ⊙ η) ⊙ (𝟘ᶜ ∙ 𝟙))
≡⟨⟩
p ·ᶜ (𝟘ᶜ ∙ 𝟙) +ᶜ (γ <* wk1Substₘ (Ψ ⊙ η))
≈⟨ +ᶜ-cong ((·ᶜ-zeroʳ p) ∙ (·-identityʳ p)) (wk1Substₘ-app (Ψ ⊙ η) γ) ⟩
(𝟘ᶜ ∙ p) +ᶜ ((γ <* (Ψ ⊙ η)) ∙ 𝟘)
≈⟨ (+ᶜ-identityˡ (γ <* (Ψ ⊙ η))) ∙ (+-identityʳ p) ⟩
(γ <* (Ψ ⊙ η)) ∙ p ∎
where open Tools.Reasoning.Equivalence Conₘ-setoid
<*-identityˡ : (γ : Conₘ n) → γ <* idSubstₘ ≈ᶜ γ
<*-identityˡ ε = ≈ᶜ-refl
<*-identityˡ (γ ∙ p) = begin
(γ ∙ p) <* idSubstₘ ≡⟨⟩
((p ·ᶜ 𝟘ᶜ) ∙ (p · 𝟙)) +ᶜ (γ <* wk1Substₘ idSubstₘ)
≈⟨ +ᶜ-cong ((·ᶜ-zeroʳ p) ∙ (·-identityʳ p)) (wk1Substₘ-app idSubstₘ γ) ⟩
((𝟘ᶜ ∙ p) +ᶜ ((γ <* idSubstₘ) ∙ 𝟘))
≈⟨ (+ᶜ-identityˡ _) ∙ (+-identityʳ p) ⟩
(γ <* idSubstₘ) ∙ p
≈⟨ (<*-identityˡ γ) ∙ refl ⟩
γ ∙ p ∎
where open Tools.Reasoning.Equivalence Conₘ-setoid
wf-sgSubstₘ :
⌜ mo ⌝ ·ᶜ γ ▸[ mo ] u → sgSubstₘ γ ▶[ consᵐ mo mos ] sgSubst u
wf-sgSubstₘ {mo = mo} {γ = γ} γ▸u x0 = sub
γ▸u
(begin
⌜ mo ⌝ ·ᶜ γ +ᶜ 𝟘ᶜ <* idSubstₘ ≈⟨ +ᶜ-congˡ (<*-identityˡ 𝟘ᶜ) ⟩
⌜ mo ⌝ ·ᶜ γ +ᶜ 𝟘ᶜ ≈⟨ +ᶜ-identityʳ _ ⟩
⌜ mo ⌝ ·ᶜ γ ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
wf-sgSubstₘ {γ = γ} {mos = mos} _ (x +1) = sub
var
(begin
𝟘 ·ᶜ γ +ᶜ (𝟘ᶜ , x ≔ ⌜ mos x ⌝) <* idSubstₘ ≈⟨ +ᶜ-cong (·ᶜ-zeroˡ γ) (<*-identityˡ _) ⟩
𝟘ᶜ +ᶜ (𝟘ᶜ , x ≔ ⌜ mos x ⌝) ≈⟨ +ᶜ-identityˡ _ ⟩
𝟘ᶜ , x ≔ ⌜ mos x ⌝ ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
wf-wk1Substₘ : (Ψ : Substₘ m n) (σ : Subst m n)
→ Ψ ▶[ mos ] σ → wk1Substₘ Ψ ▶[ mos ] wk1Subst σ
wf-wk1Substₘ Ψ σ Ψ▶σ x =
sub (wkUsage (step id) (Ψ▶σ x)) (≤ᶜ-reflexive (wk1Substₘ-app Ψ (𝟘ᶜ , x ≔ _)))
wf-liftSubstₘ :
{Ψ : Substₘ m n} →
Ψ ▶[ mos ] σ → liftSubstₘ Ψ ▶[ consᵐ mo mos ] liftSubst σ
wf-liftSubstₘ {mo = mo} {Ψ = Ψ} _ x0 = sub
var
(begin
(⌜ mo ⌝ ·ᶜ 𝟘ᶜ ∙ ⌜ mo ⌝ · 𝟙) +ᶜ 𝟘ᶜ <* wk1Substₘ Ψ ≈⟨ +ᶜ-cong (·ᶜ-zeroʳ _ ∙ ·-identityʳ _) (<*-zeroˡ (wk1Substₘ Ψ)) ⟩
(𝟘ᶜ ∙ ⌜ mo ⌝) +ᶜ 𝟘ᶜ ≈⟨ +ᶜ-identityʳ _ ⟩
𝟘ᶜ ∙ ⌜ mo ⌝ ≡⟨⟩
𝟘ᶜ , x0 ≔ ⌜ mo ⌝ ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
wf-liftSubstₘ {mos = mos} {Ψ = Ψ} Ψ▶σ (x +1) = sub
(wf-wk1Substₘ Ψ _ Ψ▶σ x)
(begin
(𝟘 ·ᶜ 𝟘ᶜ ∙ 𝟘 · 𝟙) +ᶜ (𝟘ᶜ , x ≔ ⌜ mos x ⌝) <* wk1Substₘ Ψ ≈⟨ +ᶜ-congʳ (·ᶜ-zeroʳ _ ∙ ·-zeroˡ _) ⟩
𝟘ᶜ +ᶜ (𝟘ᶜ , x ≔ ⌜ mos x ⌝) <* wk1Substₘ Ψ ≈⟨ +ᶜ-identityˡ _ ⟩
(𝟘ᶜ , x ≔ ⌜ mos x ⌝) <* wk1Substₘ Ψ ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
wf-consSubstₘ :
{Ψ : Substₘ m n} {γ : Conₘ m} →
Ψ ▶[ mos ] σ → ⌜ mo ⌝ ·ᶜ γ ▸[ mo ] t →
Ψ ⊙ γ ▶[ consᵐ mo mos ] consSubst σ t
wf-consSubstₘ {mo = mo} {Ψ = Ψ} {γ = γ} Ψ▶σ γ▸t x0 = sub
γ▸t
(begin
⌜ mo ⌝ ·ᶜ γ +ᶜ 𝟘ᶜ <* Ψ ≈⟨ +ᶜ-congˡ (<*-zeroˡ Ψ) ⟩
⌜ mo ⌝ ·ᶜ γ +ᶜ 𝟘ᶜ ≈⟨ +ᶜ-identityʳ _ ⟩
⌜ mo ⌝ ·ᶜ γ ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
wf-consSubstₘ {mos = mos} {Ψ = Ψ} {γ = γ} Ψ▶σ γ▸t (x +1) = sub
(Ψ▶σ x)
(begin
𝟘 ·ᶜ γ +ᶜ (𝟘ᶜ , x ≔ ⌜ mos x ⌝) <* Ψ ≈⟨ +ᶜ-congʳ (·ᶜ-zeroˡ _) ⟩
𝟘ᶜ +ᶜ (𝟘ᶜ , x ≔ ⌜ mos x ⌝) <* Ψ ≈⟨ +ᶜ-identityˡ _ ⟩
(𝟘ᶜ , x ≔ ⌜ mos x ⌝) <* Ψ ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
wf-tailSubstₘ :
{Ψ : Substₘ m n} →
(Ψ ⊙ γ) ▶[ mos ] σ → Ψ ▶[ tailᵐ mos ] tail σ
wf-tailSubstₘ Ψ▶σ x =
sub (Ψ▶σ (x +1))
(≤ᶜ-reflexive (≈ᶜ-sym (≈ᶜ-trans (+ᶜ-congʳ (·ᶜ-zeroˡ _)) (+ᶜ-identityˡ _))))
▶-cong :
(Ψ : Substₘ m n) →
(∀ x → mos₁ x ≡ mos₂ x) → Ψ ▶[ mos₁ ] σ → Ψ ▶[ mos₂ ] σ
▶-cong Ψ mos₁≡mos₂ Ψ▶ x0 =
PE.subst (λ mo → (𝟘ᶜ ∙ ⌜ mo ⌝) <* Ψ ▸[ mo ] _) (mos₁≡mos₂ x0) (Ψ▶ x0)
▶-cong {mos₁ = mos₁} {mos₂ = mos₂} (Ψ ⊙ γ) mos₁≡mos₂ Ψ⊙▶ (x +1) = sub
(▶-cong Ψ (λ x → mos₁≡mos₂ (x +1))
(λ x → sub (Ψ⊙▶ (x +1)) (≤ᶜ-reflexive (≈ᶜ-sym (lemma mos₁ x))))
x)
(≤ᶜ-reflexive (lemma mos₂ x))
where
open Tools.Reasoning.Equivalence Conₘ-setoid
lemma = λ mos x → begin
𝟘 ·ᶜ γ +ᶜ (𝟘ᶜ , x ≔ ⌜ mos (x +1) ⌝) <* Ψ ≈⟨ +ᶜ-congʳ (·ᶜ-zeroˡ _) ⟩
𝟘ᶜ +ᶜ (𝟘ᶜ , x ≔ ⌜ mos (x +1) ⌝) <* Ψ ≈⟨ +ᶜ-identityˡ _ ⟩
(𝟘ᶜ , x ≔ ⌜ mos (x +1) ⌝) <* Ψ ∎
▶-≤ :
(Ψ : Substₘ m n) →
γ ≤ᶜ δ → Ψ ▶[ ⌞ γ ⌟ᶜ ] σ → Ψ ▶[ ⌞ δ ⌟ᶜ ] σ
▶-≤ Ψ γ≤δ Ψ▶ x = sub
(▸-≤ (lookup-monotone _ γ≤δ)
(sub (Ψ▶ x) (≤ᶜ-reflexive (·ᶜ-<*-𝟘ᶜ,≔𝟙 Ψ))))
(≤ᶜ-reflexive (≈ᶜ-sym (·ᶜ-<*-𝟘ᶜ,≔𝟙 Ψ)))
▶-without-𝟘ᵐ :
(Ψ : Substₘ m n) →
¬ T 𝟘ᵐ-allowed →
Ψ ▶[ mos₁ ] σ → Ψ ▶[ mos₂ ] σ
▶-without-𝟘ᵐ Ψ not-ok =
▶-cong Ψ (λ _ → Mode-propositional-without-𝟘ᵐ not-ok)
▶-⌞·⌟ :
(Ψ : Substₘ m n) (γ : Conₘ n) →
Ψ ▶[ ⌞ p ·ᶜ γ ⌟ᶜ ] σ →
(p ≡ 𝟘 × T 𝟘ᵐ-allowed) ⊎ (Ψ ▶[ ⌞ γ ⌟ᶜ ] σ)
▶-⌞·⌟ {p = p} {σ = σ} Ψ γ Ψ▶ = 𝟘ᵐ-allowed-elim
(λ ok → case is-𝟘? ok p of λ where
(yes p≡𝟘) → inj₁ (p≡𝟘 , ok)
(no p≢𝟘) → inj₂ λ x →
case ▸-⌞·⌟
(sub (▸-cong (cong ⌞_⌟ (lookup-distrib-·ᶜ γ _ _)) (Ψ▶ x))
(begin
⌜ ⌞ p · γ ⟨ x ⟩ ⌟ ⌝ ·ᶜ (𝟘ᶜ , x ≔ 𝟙) <* Ψ ≈⟨ ·ᶜ-<*-𝟘ᶜ,≔𝟙 Ψ ⟩
(𝟘ᶜ , x ≔ ⌜ ⌞ p · γ ⟨ x ⟩ ⌟ ⌝) <* Ψ ≡˘⟨ cong (λ p → (𝟘ᶜ , x ≔ ⌜ ⌞ p ⌟ ⌝) <* Ψ)
(lookup-distrib-·ᶜ γ _ _) ⟩
(𝟘ᶜ , x ≔ ⌜ ⌞ p ·ᶜ γ ⌟ᶜ x ⌝) <* Ψ ∎))
of λ where
(inj₂ ▸γx) → sub ▸γx (≤ᶜ-reflexive (≈ᶜ-sym (·ᶜ-<*-𝟘ᶜ,≔𝟙 Ψ)))
(inj₁ ▸p) → lemma _ _ _ (≢𝟘→⌞⌟≡𝟙ᵐ p≢𝟘) ▸p)
(λ not-ok → inj₂ (▶-without-𝟘ᵐ Ψ not-ok Ψ▶))
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
lemma :
∀ mo₁ mo₂ x →
mo₁ ≡ 𝟙ᵐ →
⌜ mo₁ ⌝ ·ᶜ (𝟘ᶜ , x ≔ 𝟙) <* Ψ ▸[ mo₁ ] t →
(𝟘ᶜ , x ≔ ⌜ mo₂ ⌝) <* Ψ ▸[ mo₂ ] t
lemma 𝟙ᵐ 𝟘ᵐ x _ ▸t = sub (▸-𝟘 ▸t)
(begin
(𝟘ᶜ , x ≔ 𝟘) <* Ψ ≡⟨ cong (_<* Ψ) 𝟘ᶜ,≔𝟘 ⟩
𝟘ᶜ <* Ψ ≈⟨ <*-zeroˡ Ψ ⟩
𝟘ᶜ ∎)
lemma 𝟙ᵐ 𝟙ᵐ x _ ▸t = sub ▸t
(begin
(𝟘ᶜ , x ≔ 𝟙) <* Ψ ≈˘⟨ ·ᶜ-identityˡ _ ⟩
𝟙 ·ᶜ (𝟘ᶜ , x ≔ 𝟙) <* Ψ ∎)
▶-⌞+ᶜ⌟ˡ :
(Ψ : Substₘ m n) (γ : Conₘ n) →
Ψ ▶[ ⌞ γ +ᶜ δ ⌟ᶜ ] σ → Ψ ▶[ ⌞ γ ⌟ᶜ ] σ
▶-⌞+ᶜ⌟ˡ {δ = δ} Ψ γ Ψ▶ x = sub
(▸-⌞+⌟ˡ
(sub (▸-cong (cong ⌞_⌟ (lookup-distrib-+ᶜ γ _ _)) (Ψ▶ x)) (begin
⌜ ⌞ γ ⟨ x ⟩ + δ ⟨ x ⟩ ⌟ ⌝ ·ᶜ (𝟘ᶜ , x ≔ 𝟙) <* Ψ ≈⟨ ·ᶜ-<*-𝟘ᶜ,≔𝟙 Ψ ⟩
(𝟘ᶜ , x ≔ ⌜ ⌞ γ ⟨ x ⟩ + δ ⟨ x ⟩ ⌟ ⌝) <* Ψ ≡˘⟨ cong (λ p → (𝟘ᶜ , x ≔ ⌜ ⌞ p ⌟ ⌝) <* Ψ)
(lookup-distrib-+ᶜ γ _ _) ⟩
(𝟘ᶜ , x ≔ ⌜ ⌞ γ +ᶜ δ ⌟ᶜ x ⌝) <* Ψ ∎)))
(≤ᶜ-reflexive (≈ᶜ-sym (·ᶜ-<*-𝟘ᶜ,≔𝟙 Ψ)))
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
▶-⌞+ᶜ⌟ʳ :
(Ψ : Substₘ m n) (γ : Conₘ n) →
Ψ ▶[ ⌞ γ +ᶜ δ ⌟ᶜ ] σ → Ψ ▶[ ⌞ δ ⌟ᶜ ] σ
▶-⌞+ᶜ⌟ʳ {δ = δ} Ψ γ Ψ▶ =
▶-⌞+ᶜ⌟ˡ Ψ δ (▶-cong Ψ (⌞⌟ᶜ-cong (+ᶜ-comm γ _)) Ψ▶)
▸-⌞<*⌟ :
(Ψ : Substₘ m n) →
⌜ ⌞ γ <* Ψ ⌟ᶜ y ⌝ ·ᶜ δ ▸[ ⌞ γ <* Ψ ⌟ᶜ y ] t →
⌜ ⌞ (𝟘ᶜ , x ≔ γ ⟨ x ⟩) <* Ψ ⌟ᶜ y ⌝ ·ᶜ δ
▸[ ⌞ (𝟘ᶜ , x ≔ γ ⟨ x ⟩) <* Ψ ⌟ᶜ y ] t
▸-⌞<*⌟ {γ = γ ∙ p} {y = y} {δ = δ} {t = t} {x = x0} (Ψ ⊙ η) ▸₁ = ▸₄
where
▸₂ :
⌜ ⌞ (p ·ᶜ η) ⟨ y ⟩ + (γ <* Ψ) ⟨ y ⟩ ⌟ ⌝ ·ᶜ δ
▸[ ⌞ (p ·ᶜ η) ⟨ y ⟩ + (γ <* Ψ) ⟨ y ⟩ ⌟ ] t
▸₂ = PE.subst
(λ γ → ⌜ ⌞ γ ⌟ ⌝ ·ᶜ _ ▸[ ⌞ γ ⌟ ] _)
(lookup-distrib-+ᶜ (_ ·ᶜ η) _ _)
▸₁
▸₃ : ⌜ ⌞ p ·ᶜ η ⌟ᶜ y ⌝ ·ᶜ δ ▸[ ⌞ p ·ᶜ η ⌟ᶜ y ] t
▸₃ = ▸-⌞+⌟ˡ ▸₂
▸₄ :
⌜ ⌞ p ·ᶜ η +ᶜ (𝟘ᶜ <* Ψ) ⌟ᶜ y ⌝ ·ᶜ δ
▸[ ⌞ p ·ᶜ η +ᶜ (𝟘ᶜ <* Ψ) ⌟ᶜ y ] t
▸₄ = PE.subst
(λ m → ⌜ m ⌝ ·ᶜ δ ▸[ m ] t)
(⌞⌟-cong (lookup-cong (begin
p ·ᶜ η ≈˘⟨ +ᶜ-identityʳ _ ⟩
p ·ᶜ η +ᶜ 𝟘ᶜ ≈˘⟨ +ᶜ-congˡ (<*-zeroˡ Ψ) ⟩
p ·ᶜ η +ᶜ (𝟘ᶜ <* Ψ) ∎)))
▸₃
where
open Tools.Reasoning.Equivalence Conₘ-setoid
▸-⌞<*⌟ {γ = γ ∙ p} {y = y} {δ = δ} {t = t} {x = x +1} (Ψ ⊙ η) ▸₁ = ▸₅
where
▸₂ :
⌜ ⌞ (p ·ᶜ η) ⟨ y ⟩ + (γ <* Ψ) ⟨ y ⟩ ⌟ ⌝ ·ᶜ δ
▸[ ⌞ (p ·ᶜ η) ⟨ y ⟩ + (γ <* Ψ) ⟨ y ⟩ ⌟ ] t
▸₂ = PE.subst
(λ γ → ⌜ ⌞ γ ⌟ ⌝ ·ᶜ _ ▸[ ⌞ γ ⌟ ] _)
(lookup-distrib-+ᶜ (_ ·ᶜ η) _ _)
▸₁
▸₃ : ⌜ ⌞ γ <* Ψ ⌟ᶜ y ⌝ ·ᶜ δ ▸[ ⌞ γ <* Ψ ⌟ᶜ y ] t
▸₃ = ▸-⌞+⌟ʳ ▸₂
▸₄ : ⌜ ⌞ (𝟘ᶜ , x ≔ γ ⟨ x ⟩) <* Ψ ⌟ᶜ y ⌝ ·ᶜ δ
▸[ ⌞ (𝟘ᶜ , x ≔ γ ⟨ x ⟩) <* Ψ ⌟ᶜ y ] t
▸₄ = ▸-⌞<*⌟ {γ = γ} Ψ ▸₃
▸₅ :
⌜ ⌞ 𝟘 ·ᶜ η +ᶜ ((𝟘ᶜ , x ≔ γ ⟨ x ⟩) <* Ψ) ⌟ᶜ y ⌝ ·ᶜ δ
▸[ ⌞ 𝟘 ·ᶜ η +ᶜ ((𝟘ᶜ , x ≔ γ ⟨ x ⟩) <* Ψ) ⌟ᶜ y ] t
▸₅ = PE.subst
(λ m → ⌜ m ⌝ ·ᶜ δ ▸[ m ] t)
(⌞⌟-cong (lookup-cong (begin
(𝟘ᶜ , x ≔ γ ⟨ x ⟩) <* Ψ ≈˘⟨ +ᶜ-identityˡ ((𝟘ᶜ , _ ≔ _) <* Ψ) ⟩
𝟘ᶜ +ᶜ (𝟘ᶜ , x ≔ γ ⟨ x ⟩) <* Ψ ≈˘⟨ +ᶜ-congʳ (·ᶜ-zeroˡ η) ⟩
𝟘 ·ᶜ η +ᶜ (𝟘ᶜ , x ≔ γ ⟨ x ⟩) <* Ψ ∎)))
▸₄
where
open Tools.Reasoning.Equivalence Conₘ-setoid
▶-⌞<*⌟ :
(Ψ : Substₘ ℓ m) {Φ : Substₘ m n} →
Ψ ▶[ ⌞ γ <* Φ ⌟ᶜ ] σ →
Ψ ▶[ ⌞ (𝟘ᶜ , x ≔ γ ⟨ x ⟩) <* Φ ⌟ᶜ ] σ
▶-⌞<*⌟ {γ = γ} {x = x} Ψ {Φ = Φ} Ψ▶ y = sub
(▸-⌞<*⌟ {γ = γ} Φ (sub (Ψ▶ y) (≤ᶜ-reflexive (·ᶜ-<*-𝟘ᶜ,≔𝟙 Ψ))))
(≤ᶜ-reflexive (≈ᶜ-sym (·ᶜ-<*-𝟘ᶜ,≔𝟙 Ψ)))
▶-⌞∧ᶜ⌟ˡ :
(Ψ : Substₘ m n) (γ : Conₘ n) →
Ψ ▶[ ⌞ γ ∧ᶜ δ ⌟ᶜ ] σ → Ψ ▶[ ⌞ γ ⌟ᶜ ] σ
▶-⌞∧ᶜ⌟ˡ {δ = δ} Ψ γ Ψ▶ x = sub
(▸-⌞∧⌟ˡ
(sub (▸-cong (cong ⌞_⌟ (lookup-distrib-∧ᶜ γ _ _)) (Ψ▶ x)) (begin
⌜ ⌞ γ ⟨ x ⟩ ∧ δ ⟨ x ⟩ ⌟ ⌝ ·ᶜ (𝟘ᶜ , x ≔ 𝟙) <* Ψ ≈⟨ ·ᶜ-<*-𝟘ᶜ,≔𝟙 Ψ ⟩
(𝟘ᶜ , x ≔ ⌜ ⌞ γ ⟨ x ⟩ ∧ δ ⟨ x ⟩ ⌟ ⌝) <* Ψ ≡˘⟨ cong (λ p → (𝟘ᶜ , x ≔ ⌜ ⌞ p ⌟ ⌝) <* Ψ)
(lookup-distrib-∧ᶜ γ _ _) ⟩
(𝟘ᶜ , x ≔ ⌜ ⌞ γ ∧ᶜ δ ⌟ᶜ x ⌝) <* Ψ ∎)))
(≤ᶜ-reflexive (≈ᶜ-sym (·ᶜ-<*-𝟘ᶜ,≔𝟙 Ψ)))
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
▶-⌞∧ᶜ⌟ʳ :
(Ψ : Substₘ m n) (γ : Conₘ n) →
Ψ ▶[ ⌞ γ ∧ᶜ δ ⌟ᶜ ] σ → Ψ ▶[ ⌞ δ ⌟ᶜ ] σ
▶-⌞∧ᶜ⌟ʳ {δ = δ} Ψ γ Ψ▶ =
▶-⌞∧ᶜ⌟ˡ Ψ δ (▶-cong Ψ (⌞⌟ᶜ-cong (∧ᶜ-comm γ _)) Ψ▶)
▶-⌞⊛ᶜ⌟ˡ :
⦃ has-star : Has-star semiring-with-meet ⦄ →
(Ψ : Substₘ m n) (γ : Conₘ n) →
Ψ ▶[ ⌞ γ ⊛ᶜ δ ▷ r ⌟ᶜ ] σ → Ψ ▶[ ⌞ γ ⌟ᶜ ] σ
▶-⌞⊛ᶜ⌟ˡ {δ = δ} {r = r} Ψ γ Ψ▶ x = sub
(▸-⌞⊛⌟ˡ
(sub (▸-cong (cong ⌞_⌟ (lookup-distrib-⊛ᶜ γ _ _ _)) (Ψ▶ x)) (begin
⌜ ⌞ γ ⟨ x ⟩ ⊛ δ ⟨ x ⟩ ▷ r ⌟ ⌝ ·ᶜ (𝟘ᶜ , x ≔ 𝟙) <* Ψ ≡˘⟨ cong (λ p → ⌜ ⌞ p ⌟ ⌝ ·ᶜ _)
(lookup-distrib-⊛ᶜ γ _ _ _) ⟩
⌜ ⌞ γ ⊛ᶜ δ ▷ r ⌟ᶜ x ⌝ ·ᶜ (𝟘ᶜ , x ≔ 𝟙) <* Ψ ≈⟨ ·ᶜ-<*-𝟘ᶜ,≔𝟙 Ψ ⟩
(𝟘ᶜ , x ≔ ⌜ ⌞ γ ⊛ᶜ δ ▷ r ⌟ᶜ x ⌝) <* Ψ ∎)))
(≤ᶜ-reflexive (≈ᶜ-sym (·ᶜ-<*-𝟘ᶜ,≔𝟙 Ψ)))
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
▶-⌞⊛ᶜ⌟ʳ :
⦃ has-star : Has-star semiring-with-meet ⦄ →
(Ψ : Substₘ m n) (γ : Conₘ n) →
Ψ ▶[ ⌞ γ ⊛ᶜ δ ▷ r ⌟ᶜ ] σ → Ψ ▶[ ⌞ δ ⌟ᶜ ] σ
▶-⌞⊛ᶜ⌟ʳ {δ = δ} {r = r} Ψ γ Ψ▶ x = sub
(▸-⌞⊛⌟ʳ
(sub (▸-cong (cong ⌞_⌟ (lookup-distrib-⊛ᶜ γ _ _ _)) (Ψ▶ x)) (begin
⌜ ⌞ γ ⟨ x ⟩ ⊛ δ ⟨ x ⟩ ▷ r ⌟ ⌝ ·ᶜ (𝟘ᶜ , x ≔ 𝟙) <* Ψ ≡˘⟨ cong (λ p → ⌜ ⌞ p ⌟ ⌝ ·ᶜ _)
(lookup-distrib-⊛ᶜ γ _ _ _) ⟩
⌜ ⌞ γ ⊛ᶜ δ ▷ r ⌟ᶜ x ⌝ ·ᶜ (𝟘ᶜ , x ≔ 𝟙) <* Ψ ≈⟨ ·ᶜ-<*-𝟘ᶜ,≔𝟙 Ψ ⟩
(𝟘ᶜ , x ≔ ⌜ ⌞ γ ⊛ᶜ δ ▷ r ⌟ᶜ x ⌝) <* Ψ ∎)))
(≤ᶜ-reflexive (≈ᶜ-sym (·ᶜ-<*-𝟘ᶜ,≔𝟙 Ψ)))
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
substₘ-lemma₀ :
∀ ⦃ ok ⦄ (Ψ : Substₘ m n) →
Ψ ▶[ mos ] σ → γ ▸[ mo ] t → 𝟘ᶜ ▸[ 𝟘ᵐ[ ok ] ] t [ σ ]
substₘ-lemma₀ _ _ Uₘ =
Uₘ
substₘ-lemma₀ _ _ ℕₘ =
ℕₘ
substₘ-lemma₀ _ _ Emptyₘ =
Emptyₘ
substₘ-lemma₀ _ _ Unitₘ =
Unitₘ
substₘ-lemma₀ Ψ Ψ▶σ (ΠΣₘ {p = p} γ▸F δ▸G) = sub
(ΠΣₘ (substₘ-lemma₀ Ψ Ψ▶σ γ▸F)
(sub (substₘ-lemma₀ (liftSubstₘ Ψ) (wf-liftSubstₘ {mo = 𝟘ᵐ} Ψ▶σ)
δ▸G)
(≤ᶜ-reflexive (≈ᶜ-refl ∙ ·-zeroˡ _))))
(≤ᶜ-reflexive (≈ᶜ-sym (+ᶜ-identityˡ _)))
substₘ-lemma₀ Ψ Ψ▶σ (var {x = x}) = ▸-𝟘 (Ψ▶σ x)
substₘ-lemma₀ Ψ Ψ▶σ (lamₘ γ▸t) = lamₘ
(sub (substₘ-lemma₀ (liftSubstₘ Ψ) (wf-liftSubstₘ {mo = 𝟘ᵐ} Ψ▶σ) γ▸t)
(≤ᶜ-reflexive (≈ᶜ-refl ∙ ·-zeroˡ _)))
substₘ-lemma₀ Ψ Ψ▶σ (_∘ₘ_ {p = p} γ▸t δ▸u) = sub
(substₘ-lemma₀ Ψ Ψ▶σ γ▸t ∘ₘ
substₘ-lemma₀ Ψ Ψ▶σ δ▸u)
(begin
𝟘ᶜ ≈˘⟨ +ᶜ-identityˡ _ ⟩
𝟘ᶜ +ᶜ 𝟘ᶜ ≈˘⟨ +ᶜ-congˡ (·ᶜ-zeroʳ _) ⟩
𝟘ᶜ +ᶜ p ·ᶜ 𝟘ᶜ ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
substₘ-lemma₀ Ψ Ψ▶σ (prodᵣₘ {p = p} γ▸t δ▸u) = sub
(prodᵣₘ (substₘ-lemma₀ Ψ Ψ▶σ γ▸t) (substₘ-lemma₀ Ψ Ψ▶σ δ▸u))
(begin
𝟘ᶜ ≈˘⟨ ·ᶜ-zeroʳ _ ⟩
p ·ᶜ 𝟘ᶜ ≈˘⟨ +ᶜ-identityʳ _ ⟩
p ·ᶜ 𝟘ᶜ +ᶜ 𝟘ᶜ ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
substₘ-lemma₀ Ψ Ψ▶σ (prodₚₘ {p = p} γ▸t γ▸u) = sub
(prodₚₘ (substₘ-lemma₀ Ψ Ψ▶σ γ▸t) (substₘ-lemma₀ Ψ Ψ▶σ γ▸u))
(begin
𝟘ᶜ ≈˘⟨ ∧ᶜ-idem _ ⟩
𝟘ᶜ ∧ᶜ 𝟘ᶜ ≈˘⟨ ∧ᶜ-congʳ (·ᶜ-zeroʳ _) ⟩
p ·ᶜ 𝟘ᶜ ∧ᶜ 𝟘ᶜ ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
substₘ-lemma₀ Ψ Ψ▶σ (fstₘ m γ▸t PE.refl ok) =
fstₘ 𝟘ᵐ (substₘ-lemma₀ Ψ Ψ▶σ γ▸t) PE.refl λ ()
substₘ-lemma₀ Ψ Ψ▶σ (sndₘ γ▸t) =
sndₘ (substₘ-lemma₀ Ψ Ψ▶σ γ▸t)
substₘ-lemma₀ ⦃ ok = ok ⦄ Ψ Ψ▶σ (prodrecₘ {r = r} {q = q} γ▸t δ▸u η▸A P) = sub
(prodrecₘ (substₘ-lemma₀ Ψ Ψ▶σ γ▸t)
(sub (substₘ-lemma₀ (liftSubstₘ (liftSubstₘ Ψ))
(wf-liftSubstₘ {mo = 𝟘ᵐ} (wf-liftSubstₘ {mo = 𝟘ᵐ} Ψ▶σ))
δ▸u)
(≤ᶜ-reflexive (≈ᶜ-refl ∙ ·-zeroˡ _ ∙ ·-zeroˡ _)))
(sub (▸-cong (PE.sym 𝟘ᵐ?≡𝟘ᵐ)
(substₘ-lemma₀ (liftSubstₘ Ψ)
(wf-liftSubstₘ {mo = 𝟘ᵐ} Ψ▶σ) η▸A))
(let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
𝟘ᶜ ∙ ⌜ 𝟘ᵐ? ⌝ · q ≈⟨ ≈ᶜ-refl ∙ ·-congʳ (⌜𝟘ᵐ?⌝≡𝟘 ok) ⟩
𝟘ᶜ ∙ 𝟘 · q ≈⟨ ≈ᶜ-refl ∙ ·-zeroˡ _ ⟩
𝟘ᶜ ∎))
P)
(let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
𝟘ᶜ ≈˘⟨ +ᶜ-identityˡ _ ⟩
𝟘ᶜ +ᶜ 𝟘ᶜ ≈˘⟨ +ᶜ-congʳ (·ᶜ-zeroʳ _) ⟩
r ·ᶜ 𝟘ᶜ +ᶜ 𝟘ᶜ ∎)
substₘ-lemma₀ _ _ zeroₘ =
zeroₘ
substₘ-lemma₀ Ψ Ψ▶σ (sucₘ γ▸t) =
sucₘ (substₘ-lemma₀ Ψ Ψ▶σ γ▸t)
substₘ-lemma₀ ⦃ ok = ok ⦄ Ψ Ψ▶σ
(natrecₘ {p = p} {r = r} {q = q} γ▸z δ▸s η▸n θ▸A) = sub
(natrecₘ (substₘ-lemma₀ Ψ Ψ▶σ γ▸z)
(sub (substₘ-lemma₀ (liftSubstₘ (liftSubstₘ Ψ))
(wf-liftSubstₘ {mo = 𝟘ᵐ} (wf-liftSubstₘ {mo = 𝟘ᵐ} Ψ▶σ))
δ▸s)
(≤ᶜ-reflexive (≈ᶜ-refl ∙ ·-zeroˡ _ ∙ ·-zeroˡ _)))
(substₘ-lemma₀ Ψ Ψ▶σ η▸n)
(sub (▸-cong (PE.sym 𝟘ᵐ?≡𝟘ᵐ)
(substₘ-lemma₀ (liftSubstₘ Ψ)
(wf-liftSubstₘ {mo = 𝟘ᵐ} Ψ▶σ) θ▸A))
(let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
𝟘ᶜ ∙ ⌜ 𝟘ᵐ? ⌝ · q ≈⟨ ≈ᶜ-refl ∙ ·-congʳ (⌜𝟘ᵐ?⌝≡𝟘 ok) ⟩
𝟘ᶜ ∙ 𝟘 · q ≈⟨ ≈ᶜ-refl ∙ ·-zeroˡ _ ⟩
𝟘ᶜ ∎)))
(let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
𝟘ᶜ ≈˘⟨ ⊛ᶜ-idem-𝟘ᶜ _ ⟩
𝟘ᶜ ⊛ᶜ 𝟘ᶜ ▷ r ≈˘⟨ ⊛ᵣᶜ-congˡ (·ᶜ-zeroʳ _) ⟩
𝟘ᶜ ⊛ᶜ p ·ᶜ 𝟘ᶜ ▷ r ≈˘⟨ ⊛ᵣᶜ-cong (∧ᶜ-idem _) (+ᶜ-identityˡ _) ⟩
(𝟘ᶜ ∧ᶜ 𝟘ᶜ) ⊛ᶜ 𝟘ᶜ +ᶜ p ·ᶜ 𝟘ᶜ ▷ r ∎)
where
open import Graded.Modality.Dedicated-star.Instance
substₘ-lemma₀ ⦃ ok = ok ⦄ Ψ Ψ▶σ
(natrec-no-starₘ {p = p} {r = r} {q = q} γ▸z δ▸s η▸n θ▸A fix) =
natrec-no-starₘ (substₘ-lemma₀ Ψ Ψ▶σ γ▸z)
(sub (substₘ-lemma₀ (liftSubstₘ (liftSubstₘ Ψ))
(wf-liftSubstₘ {mo = 𝟘ᵐ} (wf-liftSubstₘ {mo = 𝟘ᵐ} Ψ▶σ))
δ▸s)
(≤ᶜ-reflexive (≈ᶜ-refl ∙ ·-zeroˡ _ ∙ ·-zeroˡ _)))
(substₘ-lemma₀ Ψ Ψ▶σ η▸n)
(sub (▸-cong (PE.sym 𝟘ᵐ?≡𝟘ᵐ)
(substₘ-lemma₀ (liftSubstₘ Ψ)
(wf-liftSubstₘ {mo = 𝟘ᵐ} Ψ▶σ) θ▸A))
(let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
𝟘ᶜ ∙ ⌜ 𝟘ᵐ? ⌝ · q ≈⟨ ≈ᶜ-refl ∙ ·-congʳ (⌜𝟘ᵐ?⌝≡𝟘 ok) ⟩
𝟘ᶜ ∙ 𝟘 · q ≈⟨ ≈ᶜ-refl ∙ ·-zeroˡ _ ⟩
𝟘ᶜ ∎))
(let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
𝟘ᶜ ≈˘⟨ ∧ᶜ-idem _ ⟩
𝟘ᶜ ∧ᶜ 𝟘ᶜ ≈˘⟨ ∧ᶜ-congˡ $ ∧ᶜ-idem _ ⟩
𝟘ᶜ ∧ᶜ 𝟘ᶜ ∧ᶜ 𝟘ᶜ ≈˘⟨ ∧ᶜ-congˡ $ ∧ᶜ-congˡ $ +ᶜ-identityˡ _ ⟩
𝟘ᶜ ∧ᶜ 𝟘ᶜ ∧ᶜ (𝟘ᶜ +ᶜ 𝟘ᶜ) ≈˘⟨ ∧ᶜ-congˡ $ ∧ᶜ-congˡ $ +ᶜ-cong (·ᶜ-zeroʳ _) (·ᶜ-zeroʳ _) ⟩
𝟘ᶜ ∧ᶜ 𝟘ᶜ ∧ᶜ (p ·ᶜ 𝟘ᶜ +ᶜ r ·ᶜ 𝟘ᶜ) ≈˘⟨ ∧ᶜ-congˡ $ ∧ᶜ-congˡ $ +ᶜ-identityˡ _ ⟩
𝟘ᶜ ∧ᶜ 𝟘ᶜ ∧ᶜ (𝟘ᶜ +ᶜ p ·ᶜ 𝟘ᶜ +ᶜ r ·ᶜ 𝟘ᶜ) ∎)
substₘ-lemma₀ Ψ Ψ▶σ (emptyrecₘ γ▸t δ▸A) =
sub (emptyrecₘ (substₘ-lemma₀ Ψ Ψ▶σ γ▸t)
(▸-cong (PE.sym 𝟘ᵐ?≡𝟘ᵐ) (substₘ-lemma₀ Ψ Ψ▶σ δ▸A)))
(≤ᶜ-reflexive (≈ᶜ-sym (·ᶜ-zeroʳ _)))
substₘ-lemma₀ _ _ starₘ =
starₘ
substₘ-lemma₀ Ψ Ψ▶σ (sub γ▸t _) =
substₘ-lemma₀ Ψ Ψ▶σ γ▸t
private
*>∙∙≤liftSubst-listSubst*>∙∙ :
(Ψ : Substₘ m n) →
(δ <* Ψ) ∙ p ∙ q ≤ᶜ (δ ∙ p ∙ q) <* liftSubstₘ (liftSubstₘ Ψ)
*>∙∙≤liftSubst-listSubst*>∙∙ {δ = δ} {p = p} {q = q} Ψ = begin
(δ <* Ψ) ∙ p ∙ q ≈˘⟨ +ᶜ-identityˡ _ ∙ +-identityʳ _ ∙ refl ⟩
(𝟘ᶜ +ᶜ δ <* Ψ) ∙ (p + 𝟘) ∙ q ≈˘⟨ (+ᶜ-cong (·ᶜ-zeroʳ _ ∙ ·-identityʳ _) (wk1Substₘ-app Ψ δ)) ∙ refl ⟩
(p ·ᶜ 𝟘ᶜ ∙ p · 𝟙) +ᶜ δ <* wk1Substₘ Ψ ∙ q ≈˘⟨ liftSubstₘ-app (liftSubstₘ Ψ) (δ ∙ _) _ ⟩
(δ ∙ p ∙ q) <* liftSubstₘ (liftSubstₘ Ψ) ∎
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
∧∧+·+·<*≤ :
∀ (Ψ : Substₘ m n) γ →
(γ ∧ᶜ η ∧ᶜ (δ +ᶜ p ·ᶜ η +ᶜ r ·ᶜ χ)) <* Ψ ≤ᶜ
γ <* Ψ ∧ᶜ η <* Ψ ∧ᶜ (δ <* Ψ +ᶜ p ·ᶜ η <* Ψ +ᶜ r ·ᶜ χ <* Ψ)
∧∧+·+·<*≤ {η = η} {δ = δ} {χ = χ} Ψ γ =
≤ᶜ-trans (<*-sub-distrib-∧ᶜ Ψ γ _) $
∧ᶜ-monotoneʳ $
≤ᶜ-trans (<*-sub-distrib-∧ᶜ Ψ η _) $
≤ᶜ-reflexive $
∧ᶜ-congˡ $
≈ᶜ-trans (<*-distrib-+ᶜ Ψ δ _) $
+ᶜ-congˡ $
≈ᶜ-trans (<*-distrib-+ᶜ Ψ (_ ·ᶜ η) _) $
+ᶜ-cong (<*-distrib-·ᶜ Ψ _ η) (<*-distrib-·ᶜ Ψ _ χ)
substₘ-lemma₁ :
¬ T 𝟘ᵐ-allowed →
(Ψ : Substₘ m n) →
Ψ ▶[ mos ] σ → γ ▸[ mo ] t → substₘ Ψ γ ▸[ 𝟙ᵐ ] t [ σ ]
substₘ-lemma₁ {mo = 𝟘ᵐ[ ok ]} not-ok = ⊥-elim (not-ok ok)
substₘ-lemma₁ _ Ψ _ Uₘ =
sub Uₘ (≤ᶜ-reflexive (<*-zeroˡ Ψ))
substₘ-lemma₁ _ Ψ _ ℕₘ =
sub ℕₘ (≤ᶜ-reflexive (<*-zeroˡ Ψ))
substₘ-lemma₁ _ Ψ _ Emptyₘ =
sub Emptyₘ (≤ᶜ-reflexive (<*-zeroˡ Ψ))
substₘ-lemma₁ _ Ψ _ Unitₘ =
sub Unitₘ (≤ᶜ-reflexive (<*-zeroˡ Ψ))
substₘ-lemma₁ {mo = 𝟙ᵐ} not-ok Ψ Ψ▶σ (ΠΣₘ {γ = γ} {δ = δ} γ▸F δ▸G) = sub
(ΠΣₘ (▸-without-𝟘ᵐ not-ok
(substₘ-lemma₁ not-ok Ψ Ψ▶σ γ▸F))
(sub (substₘ-lemma₁ not-ok (liftSubstₘ Ψ)
(wf-liftSubstₘ {mo = 𝟙ᵐ} Ψ▶σ)
δ▸G)
(≤ᶜ-reflexive (≈ᶜ-sym (liftSubstₘ-app Ψ δ _)))))
(≤ᶜ-reflexive (<*-distrib-+ᶜ Ψ γ δ))
substₘ-lemma₁ {mos = mos} {mo = 𝟙ᵐ} not-ok Ψ Ψ▶σ (var {x = x}) = sub
(▸-without-𝟘ᵐ not-ok (Ψ▶σ x))
(begin
(𝟘ᶜ , x ≔ 𝟙) <* Ψ ≡˘⟨ cong (λ m → (𝟘ᶜ , x ≔ ⌜ m ⌝) <* Ψ)
(only-𝟙ᵐ-without-𝟘ᵐ {m = mos x} not-ok) ⟩
(𝟘ᶜ , x ≔ ⌜ mos x ⌝) <* Ψ ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
substₘ-lemma₁ {mo = 𝟙ᵐ} not-ok Ψ Ψ▶σ (lamₘ {γ = γ} {p = p} γ▸t) = lamₘ
(sub (substₘ-lemma₁ not-ok (liftSubstₘ Ψ)
(wf-liftSubstₘ {mo = 𝟙ᵐ} Ψ▶σ)
γ▸t)
(≤ᶜ-reflexive (≈ᶜ-sym (liftSubstₘ-app Ψ γ _))))
substₘ-lemma₁ not-ok Ψ Ψ▶σ (_∘ₘ_ {γ = γ} {δ = δ} {p = p} γ▸t δ▸u) = sub
(substₘ-lemma₁ not-ok Ψ Ψ▶σ γ▸t ∘ₘ
▸-without-𝟘ᵐ not-ok (substₘ-lemma₁ not-ok Ψ Ψ▶σ δ▸u))
(begin
(γ +ᶜ p ·ᶜ δ) <* Ψ ≈⟨ <*-distrib-+ᶜ Ψ γ (p ·ᶜ δ) ⟩
γ <* Ψ +ᶜ (p ·ᶜ δ) <* Ψ ≈⟨ +ᶜ-congˡ (<*-distrib-·ᶜ Ψ _ δ) ⟩
γ <* Ψ +ᶜ p ·ᶜ δ <* Ψ ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
substₘ-lemma₁
not-ok Ψ Ψ▶σ (prodᵣₘ {γ = γ} {p = p} {δ = δ} γ▸t δ▸u) = sub
(prodᵣₘ (▸-without-𝟘ᵐ not-ok (substₘ-lemma₁ not-ok Ψ Ψ▶σ γ▸t))
(substₘ-lemma₁ not-ok Ψ Ψ▶σ δ▸u))
(begin
(p ·ᶜ γ +ᶜ δ) <* Ψ ≈⟨ <*-distrib-+ᶜ Ψ (p ·ᶜ γ) δ ⟩
(p ·ᶜ γ) <* Ψ +ᶜ δ <* Ψ ≈⟨ +ᶜ-congʳ (<*-distrib-·ᶜ Ψ _ γ) ⟩
p ·ᶜ γ <* Ψ +ᶜ δ <* Ψ ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
substₘ-lemma₁
not-ok Ψ Ψ▶σ (prodₚₘ {γ = γ} {p = p} {δ = δ} γ▸t δ▸u) = sub
(prodₚₘ (▸-without-𝟘ᵐ not-ok (substₘ-lemma₁ not-ok Ψ Ψ▶σ γ▸t))
(substₘ-lemma₁ not-ok Ψ Ψ▶σ δ▸u))
(begin
(p ·ᶜ γ ∧ᶜ δ) <* Ψ ≤⟨ <*-sub-distrib-∧ᶜ Ψ (p ·ᶜ γ) δ ⟩
(p ·ᶜ γ) <* Ψ ∧ᶜ δ <* Ψ ≈⟨ ∧ᶜ-congʳ (<*-distrib-·ᶜ Ψ _ γ) ⟩
p ·ᶜ γ <* Ψ ∧ᶜ δ <* Ψ ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
substₘ-lemma₁ {mo = 𝟙ᵐ} not-ok Ψ Ψ▶σ (fstₘ m γ▸t _ ok) =
fstₘ m (▸-without-𝟘ᵐ not-ok (substₘ-lemma₁ not-ok Ψ Ψ▶σ γ▸t))
(only-𝟙ᵐ-without-𝟘ᵐ not-ok) ok
substₘ-lemma₁ not-ok Ψ Ψ▶σ (sndₘ γ▸t) =
sndₘ (substₘ-lemma₁ not-ok Ψ Ψ▶σ γ▸t)
substₘ-lemma₁
{mo = 𝟙ᵐ} not-ok Ψ Ψ▶σ
(prodrecₘ {γ = γ} {r = r} {δ = δ} {η = η} {q = q}
γ▸t δ▸u η▸A P) = sub
(prodrecₘ (▸-without-𝟘ᵐ not-ok (substₘ-lemma₁ not-ok Ψ Ψ▶σ γ▸t))
(sub (substₘ-lemma₁ not-ok (liftSubstₘ (liftSubstₘ Ψ))
(wf-liftSubstₘ {mo = 𝟙ᵐ} (wf-liftSubstₘ {mo = 𝟙ᵐ} Ψ▶σ))
δ▸u)
(*>∙∙≤liftSubst-listSubst*>∙∙ {δ = δ} Ψ))
(sub (▸-cong (PE.sym (only-𝟙ᵐ-without-𝟘ᵐ not-ok))
(substₘ-lemma₁ not-ok (liftSubstₘ Ψ)
(wf-liftSubstₘ {mo = 𝟙ᵐ} Ψ▶σ)
η▸A))
(let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
η <* Ψ ∙ ⌜ 𝟘ᵐ? ⌝ · q ≈˘⟨ liftSubstₘ-app Ψ η _ ⟩
(η ∙ ⌜ 𝟘ᵐ? ⌝ · q) <* liftSubstₘ Ψ ∎))
P)
(let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
(r ·ᶜ γ +ᶜ δ) <* Ψ ≈⟨ <*-distrib-+ᶜ Ψ (r ·ᶜ γ) δ ⟩
(r ·ᶜ γ) <* Ψ +ᶜ δ <* Ψ ≈⟨ +ᶜ-congʳ (<*-distrib-·ᶜ Ψ _ γ) ⟩
r ·ᶜ γ <* Ψ +ᶜ δ <* Ψ ∎)
substₘ-lemma₁ _ Ψ _ zeroₘ =
sub zeroₘ (≤ᶜ-reflexive (<*-zeroˡ Ψ))
substₘ-lemma₁ not-ok Ψ Ψ▶σ (sucₘ γ▸t) =
sucₘ (substₘ-lemma₁ not-ok Ψ Ψ▶σ γ▸t)
substₘ-lemma₁
{mo = 𝟙ᵐ} not-ok Ψ Ψ▶σ
(natrecₘ {γ = γ} {δ = δ} {p = p} {r = r} {η = η} {θ = θ} {q = q}
γ▸z δ▸s η▸n θ▸A) = sub
(natrecₘ
(substₘ-lemma₁ not-ok Ψ Ψ▶σ γ▸z)
(sub
(substₘ-lemma₁ not-ok (liftSubstₘ (liftSubstₘ Ψ))
(wf-liftSubstₘ {mo = 𝟙ᵐ} (wf-liftSubstₘ {mo = 𝟙ᵐ} Ψ▶σ)) δ▸s)
(*>∙∙≤liftSubst-listSubst*>∙∙ {δ = δ} Ψ))
(substₘ-lemma₁ not-ok Ψ Ψ▶σ η▸n)
(sub (▸-cong (PE.sym (only-𝟙ᵐ-without-𝟘ᵐ not-ok))
(substₘ-lemma₁ not-ok (liftSubstₘ Ψ)
(wf-liftSubstₘ {mo = 𝟙ᵐ} Ψ▶σ) θ▸A))
(let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
θ <* Ψ ∙ ⌜ 𝟘ᵐ? ⌝ · q ≈˘⟨ liftSubstₘ-app Ψ θ _ ⟩
(θ ∙ ⌜ 𝟘ᵐ? ⌝ · q) <* liftSubstₘ Ψ ∎)))
(let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
((γ ∧ᶜ η) ⊛ᶜ (δ +ᶜ p ·ᶜ η) ▷ r) <* Ψ ≤⟨ <*-sub-distrib-⊛ᶜ Ψ (γ ∧ᶜ η) (δ +ᶜ p ·ᶜ η) _ ⟩
((γ ∧ᶜ η) <* Ψ) ⊛ᶜ ((δ +ᶜ p ·ᶜ η) <* Ψ) ▷ r ≈⟨ ⊛ᵣᶜ-congˡ (<*-distrib-+ᶜ Ψ δ (p ·ᶜ η)) ⟩
((γ ∧ᶜ η) <* Ψ) ⊛ᶜ (δ <* Ψ +ᶜ (p ·ᶜ η) <* Ψ) ▷ r ≤⟨ ⊛ᶜ-monotoneʳ (<*-sub-distrib-∧ᶜ Ψ γ η) ⟩
(γ <* Ψ ∧ᶜ η <* Ψ) ⊛ᶜ (δ <* Ψ +ᶜ (p ·ᶜ η) <* Ψ) ▷ r ≈⟨ ⊛ᵣᶜ-congˡ (+ᶜ-congˡ (<*-distrib-·ᶜ Ψ _ η)) ⟩
(γ <* Ψ ∧ᶜ η <* Ψ) ⊛ᶜ (δ <* Ψ +ᶜ p ·ᶜ η <* Ψ) ▷ r ∎)
where
open import Graded.Modality.Dedicated-star.Instance
substₘ-lemma₁
{mo = 𝟙ᵐ} not-ok Ψ Ψ▶σ
(natrec-no-starₘ
{γ = γ} {δ = δ} {p = p} {r = r} {η = η} {θ = θ} {q = q} {χ = χ}
γ▸z δ▸s η▸n θ▸A fix) =
natrec-no-starₘ
(substₘ-lemma₁ not-ok Ψ Ψ▶σ γ▸z)
(sub
(substₘ-lemma₁ not-ok (liftSubstₘ (liftSubstₘ Ψ))
(wf-liftSubstₘ {mo = 𝟙ᵐ} (wf-liftSubstₘ {mo = 𝟙ᵐ} Ψ▶σ)) δ▸s)
(*>∙∙≤liftSubst-listSubst*>∙∙ {δ = δ} Ψ))
(substₘ-lemma₁ not-ok Ψ Ψ▶σ η▸n)
(sub (▸-cong (PE.sym (only-𝟙ᵐ-without-𝟘ᵐ not-ok))
(substₘ-lemma₁ not-ok (liftSubstₘ Ψ)
(wf-liftSubstₘ {mo = 𝟙ᵐ} Ψ▶σ) θ▸A))
(let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
θ <* Ψ ∙ ⌜ 𝟘ᵐ? ⌝ · q ≈˘⟨ liftSubstₘ-app Ψ θ _ ⟩
(θ ∙ ⌜ 𝟘ᵐ? ⌝ · q) <* liftSubstₘ Ψ ∎))
(let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
χ <* Ψ ≤⟨ <*-monotone Ψ fix ⟩
(γ ∧ᶜ η ∧ᶜ (δ +ᶜ p ·ᶜ η +ᶜ r ·ᶜ χ)) <* Ψ ≤⟨ ∧∧+·+·<*≤ Ψ γ ⟩
γ <* Ψ ∧ᶜ η <* Ψ ∧ᶜ (δ <* Ψ +ᶜ p ·ᶜ η <* Ψ +ᶜ r ·ᶜ χ <* Ψ) ∎)
substₘ-lemma₁
{mo = 𝟙ᵐ} not-ok Ψ Ψ▶σ
(emptyrecₘ {γ = γ} {p = p} γ▸t δ▸A) = sub
(emptyrecₘ (▸-without-𝟘ᵐ not-ok (substₘ-lemma₁ not-ok Ψ Ψ▶σ γ▸t))
(▸-cong (PE.sym (only-𝟙ᵐ-without-𝟘ᵐ not-ok))
(substₘ-lemma₁ not-ok Ψ Ψ▶σ δ▸A)))
(≤ᶜ-reflexive (<*-distrib-·ᶜ Ψ _ γ))
substₘ-lemma₁ _ Ψ _ starₘ = sub
starₘ
(≤ᶜ-reflexive (<*-zeroˡ Ψ))
substₘ-lemma₁ not-ok Ψ Ψ▶σ (sub γ▸t γ≤δ) = sub
(substₘ-lemma₁ not-ok Ψ Ψ▶σ γ▸t)
(<*-monotone Ψ γ≤δ)
private
substₘ-lemma-𝟘ᵐ? :
(Ψ : Substₘ m n) →
Ψ ▶[ mos ] σ → γ ▸[ mo ] t →
∃ λ δ → δ ▸[ 𝟘ᵐ? ] t [ σ ]
substₘ-lemma-𝟘ᵐ? Ψ Ψ▶ γ▸ = 𝟘ᵐ-allowed-elim
(λ ok →
_
, ▸-cong
(PE.sym 𝟘ᵐ?≡𝟘ᵐ)
(substₘ-lemma₀ ⦃ ok = ok ⦄ Ψ Ψ▶ γ▸))
(λ not-ok →
_
, ▸-cong
(PE.sym (only-𝟙ᵐ-without-𝟘ᵐ not-ok))
(substₘ-lemma₁ not-ok Ψ Ψ▶ γ▸))
substₘ-lemma-∙⌜𝟘ᵐ?⌝·▸[𝟘ᵐ?] :
(Ψ : Substₘ m n) →
Ψ ▶[ mos ] σ → γ ∙ ⌜ 𝟘ᵐ? ⌝ · p ▸[ mo ] t →
∃ λ δ → δ ∙ ⌜ 𝟘ᵐ? ⌝ · p ▸[ 𝟘ᵐ? ] t [ liftSubst σ ]
substₘ-lemma-∙⌜𝟘ᵐ?⌝·▸[𝟘ᵐ?] {γ = γ} {p = p} Ψ Ψ▶ γ▸ = 𝟘ᵐ-allowed-elim
(λ ok →
_
, ▸-cong
(PE.sym 𝟘ᵐ?≡𝟘ᵐ)
(sub (substₘ-lemma₀ ⦃ ok = ok ⦄ (liftSubstₘ Ψ)
(wf-liftSubstₘ {mo = 𝟙ᵐ} Ψ▶) γ▸)
(let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in
begin
𝟘ᶜ ∙ ⌜ 𝟘ᵐ? ⌝ · p ≈⟨ ≈ᶜ-refl ∙ ·-congʳ (⌜𝟘ᵐ?⌝≡𝟘 ok) ⟩
𝟘ᶜ ∙ 𝟘 · p ≈⟨ ≈ᶜ-refl ∙ ·-zeroˡ _ ⟩
𝟘ᶜ ∎)))
(λ not-ok →
_
, ▸-cong
(PE.sym (only-𝟙ᵐ-without-𝟘ᵐ not-ok))
(sub (substₘ-lemma₁ not-ok (liftSubstₘ Ψ)
(wf-liftSubstₘ {mo = 𝟙ᵐ} Ψ▶) γ▸)
(let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in
begin
γ <* Ψ ∙ ⌜ 𝟘ᵐ? ⌝ · p ≈˘⟨ liftSubstₘ-app Ψ γ _ ⟩
(γ ∙ ⌜ 𝟘ᵐ? ⌝ · p) <* liftSubstₘ Ψ ∎)))
≡𝟘→𝟘ᵐ≡ᵐ· : ∀ ⦃ ok ⦄ mo → p ≡ 𝟘 → 𝟘ᵐ[ ok ] ≡ mo ᵐ· p
≡𝟘→𝟘ᵐ≡ᵐ· {p = p} mo p≡𝟘 =
𝟘ᵐ ≡˘⟨ 𝟘ᵐ?≡𝟘ᵐ ⟩
𝟘ᵐ? ≡˘⟨ ᵐ·-zeroʳ mo ⟩
mo ᵐ· 𝟘 ≡˘⟨ ᵐ·-cong mo p≡𝟘 ⟩
mo ᵐ· p ∎
where
open Tools.Reasoning.PropositionalEquality
≡𝟘→·<*≈ᶜ·𝟘 : (Ψ : Substₘ m n) → p ≡ 𝟘 → p ·ᶜ δ <* Ψ ≈ᶜ p ·ᶜ 𝟘ᶜ
≡𝟘→·<*≈ᶜ·𝟘 {p = p} {δ = δ} Ψ p≡𝟘 = begin
p ·ᶜ δ <* Ψ ≈⟨ ·ᶜ-congʳ p≡𝟘 ⟩
𝟘 ·ᶜ δ <* Ψ ≈⟨ ·ᶜ-zeroˡ _ ⟩
𝟘ᶜ ≈˘⟨ ·ᶜ-zeroʳ _ ⟩
p ·ᶜ 𝟘ᶜ ∎
where
open Tools.Reasoning.Equivalence Conₘ-setoid
substₘ-lemma :
(Ψ : Substₘ m n) →
Ψ ▶[ ⌞ γ ⌟ᶜ ] σ → γ ▸[ mo ] t → substₘ Ψ γ ▸[ mo ] t [ σ ]
substₘ-lemma Ψ _ Uₘ =
sub Uₘ (≤ᶜ-reflexive (<*-zeroˡ Ψ))
substₘ-lemma Ψ _ ℕₘ =
sub ℕₘ (≤ᶜ-reflexive (<*-zeroˡ Ψ))
substₘ-lemma Ψ _ Emptyₘ =
sub Emptyₘ (≤ᶜ-reflexive (<*-zeroˡ Ψ))
substₘ-lemma Ψ _ Unitₘ =
sub Unitₘ (≤ᶜ-reflexive (<*-zeroˡ Ψ))
substₘ-lemma Ψ Ψ▶σ (ΠΣₘ {γ = γ} {δ = δ} γ▸F δ▸G) = sub
(ΠΣₘ (substₘ-lemma Ψ (▶-⌞+ᶜ⌟ˡ Ψ γ Ψ▶σ) γ▸F)
(sub (substₘ-lemma (liftSubstₘ Ψ)
(▶-cong (liftSubstₘ Ψ)
(λ where
(_ +1) → PE.refl
x0 → PE.refl)
(wf-liftSubstₘ (▶-⌞+ᶜ⌟ʳ Ψ γ Ψ▶σ)))
δ▸G)
(≤ᶜ-reflexive (≈ᶜ-sym (liftSubstₘ-app Ψ δ _)))))
(≤ᶜ-reflexive (<*-distrib-+ᶜ Ψ γ δ))
substₘ-lemma {σ = σ} {mo = mo} Ψ Ψ▶σ (var {x = x}) = sub
(▸-cong (let open Tools.Reasoning.PropositionalEquality in
⌞ (𝟘ᶜ , x ≔ ⌜ mo ⌝) ⟨ x ⟩ ⌟ ≡⟨ cong ⌞_⌟ (update-lookup 𝟘ᶜ x) ⟩
⌞ ⌜ mo ⌝ ⌟ ≡⟨ ⌞⌜⌝⌟ _ ⟩
mo ∎)
(Ψ▶σ x))
(let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
(𝟘ᶜ , x ≔ ⌜ mo ⌝) <* Ψ ≈˘⟨ <*-cong Ψ (update-congʳ {γ = 𝟘ᶜ} {x = x} (cong ⌜_⌝ (⌞⌜⌝⌟ mo))) ⟩
(𝟘ᶜ , x ≔ ⌜ ⌞ ⌜ mo ⌝ ⌟ ⌝) <* Ψ ≡˘⟨ cong (λ p → (𝟘ᶜ , x ≔ ⌜ ⌞ p ⌟ ⌝) <* Ψ) (update-lookup 𝟘ᶜ x) ⟩
(𝟘ᶜ , x ≔ ⌜ ⌞ (𝟘ᶜ , x ≔ ⌜ mo ⌝) ⟨ x ⟩ ⌟ ⌝) <* Ψ ∎)
substₘ-lemma {mo = mo} Ψ Ψ▶σ (lamₘ {γ = γ} {p = p} γ▸t) = lamₘ
(sub (substₘ-lemma (liftSubstₘ Ψ)
(▶-cong (liftSubstₘ Ψ)
(λ where
(_ +1) → PE.refl
x0 →
mo ᵐ· p ≡˘⟨ ⌞⌜⌝·⌟ mo ⟩
⌞ ⌜ mo ⌝ · p ⌟ ∎)
(wf-liftSubstₘ Ψ▶σ))
γ▸t)
(≤ᶜ-reflexive (≈ᶜ-sym (liftSubstₘ-app Ψ γ _))))
where
open Tools.Reasoning.PropositionalEquality
substₘ-lemma
{σ = σ} {mo = mo} Ψ Ψ▶σ
(_∘ₘ_ {γ = γ} {t = t} {δ = δ} {p = p} {u = u} γ▸t δ▸u) =
case ▶-⌞·⌟ Ψ δ (▶-⌞+ᶜ⌟ʳ Ψ γ Ψ▶σ) of λ where
(inj₂ Ψ▶σ) → lemma (substₘ-lemma Ψ Ψ▶σ δ▸u) ≈ᶜ-refl
(inj₁ (p≡𝟘 , ok)) → lemma
(▸-cong (≡𝟘→𝟘ᵐ≡ᵐ· ⦃ ok = ok ⦄ mo p≡𝟘)
(substₘ-lemma₀ ⦃ ok = ok ⦄ Ψ Ψ▶σ δ▸u))
(≡𝟘→·<*≈ᶜ·𝟘 {δ = δ} Ψ p≡𝟘)
where
lemma :
η ▸[ mo ᵐ· p ] u [ σ ] →
p ·ᶜ δ <* Ψ ≈ᶜ p ·ᶜ η →
(γ +ᶜ p ·ᶜ δ) <* Ψ ▸[ mo ] (t ∘⟨ p ⟩ u) [ σ ]
lemma {η = η} hyp₁ hyp₂ = sub
(substₘ-lemma Ψ (▶-⌞+ᶜ⌟ˡ Ψ γ Ψ▶σ) γ▸t ∘ₘ hyp₁)
(begin
(γ +ᶜ p ·ᶜ δ) <* Ψ ≈⟨ <*-distrib-+ᶜ Ψ γ (p ·ᶜ δ) ⟩
γ <* Ψ +ᶜ (p ·ᶜ δ) <* Ψ ≈⟨ +ᶜ-congˡ (<*-distrib-·ᶜ Ψ _ δ) ⟩
γ <* Ψ +ᶜ p ·ᶜ δ <* Ψ ≈⟨ +ᶜ-congˡ hyp₂ ⟩
γ <* Ψ +ᶜ p ·ᶜ η ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
substₘ-lemma
{σ = σ} {mo = mo} Ψ Ψ▶σ
(prodᵣₘ {γ = γ} {p = p} {t = t} {δ = δ} {u = u} γ▸t δ▸u) =
case ▶-⌞·⌟ Ψ γ (▶-⌞+ᶜ⌟ˡ Ψ (_ ·ᶜ γ) Ψ▶σ) of λ where
(inj₂ Ψ▶σ) → lemma (substₘ-lemma Ψ Ψ▶σ γ▸t) ≈ᶜ-refl
(inj₁ (p≡𝟘 , ok)) → lemma
(▸-cong (≡𝟘→𝟘ᵐ≡ᵐ· ⦃ ok = ok ⦄ mo p≡𝟘)
(substₘ-lemma₀ ⦃ ok = ok ⦄ Ψ Ψ▶σ γ▸t))
(≡𝟘→·<*≈ᶜ·𝟘 {δ = γ} Ψ p≡𝟘)
where
lemma :
η ▸[ mo ᵐ· p ] t [ σ ] →
p ·ᶜ γ <* Ψ ≈ᶜ p ·ᶜ η →
(p ·ᶜ γ +ᶜ δ) <* Ψ ▸[ mo ] prodᵣ p t u [ σ ]
lemma {η = η} hyp₁ hyp₂ = sub
(prodᵣₘ hyp₁ (substₘ-lemma Ψ (▶-⌞+ᶜ⌟ʳ Ψ (_ ·ᶜ γ) Ψ▶σ) δ▸u))
(begin
(p ·ᶜ γ +ᶜ δ) <* Ψ ≈⟨ <*-distrib-+ᶜ Ψ (p ·ᶜ γ) δ ⟩
(p ·ᶜ γ) <* Ψ +ᶜ δ <* Ψ ≈⟨ +ᶜ-congʳ (<*-distrib-·ᶜ Ψ _ γ) ⟩
p ·ᶜ γ <* Ψ +ᶜ δ <* Ψ ≈⟨ +ᶜ-congʳ hyp₂ ⟩
p ·ᶜ η +ᶜ δ <* Ψ ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
substₘ-lemma
{σ = σ} {mo = mo} Ψ Ψ▶σ
(prodₚₘ {γ = γ} {p = p} {t = t} {δ = δ} {u = u} γ▸t δ▸u) =
case ▶-⌞·⌟ Ψ γ (▶-⌞∧ᶜ⌟ˡ Ψ (_ ·ᶜ γ) Ψ▶σ) of λ where
(inj₂ Ψ▶σ) → lemma (substₘ-lemma Ψ Ψ▶σ γ▸t) ≈ᶜ-refl
(inj₁ (p≡𝟘 , ok)) → lemma
(▸-cong (≡𝟘→𝟘ᵐ≡ᵐ· ⦃ ok = ok ⦄ mo p≡𝟘)
(substₘ-lemma₀ ⦃ ok = ok ⦄ Ψ Ψ▶σ γ▸t))
(≡𝟘→·<*≈ᶜ·𝟘 {δ = γ} Ψ p≡𝟘)
where
lemma :
η ▸[ mo ᵐ· p ] t [ σ ] →
p ·ᶜ γ <* Ψ ≈ᶜ p ·ᶜ η →
(p ·ᶜ γ ∧ᶜ δ) <* Ψ ▸[ mo ] prodₚ p t u [ σ ]
lemma {η = η} hyp₁ hyp₂ = sub
(prodₚₘ hyp₁ (substₘ-lemma Ψ (▶-⌞∧ᶜ⌟ʳ Ψ (_ ·ᶜ γ) Ψ▶σ) δ▸u))
(begin
(p ·ᶜ γ ∧ᶜ δ) <* Ψ ≤⟨ <*-sub-distrib-∧ᶜ Ψ (p ·ᶜ γ) δ ⟩
(p ·ᶜ γ) <* Ψ ∧ᶜ δ <* Ψ ≈⟨ ∧ᶜ-congʳ (<*-distrib-·ᶜ Ψ _ γ) ⟩
p ·ᶜ γ <* Ψ ∧ᶜ δ <* Ψ ≈⟨ ∧ᶜ-congʳ hyp₂ ⟩
p ·ᶜ η ∧ᶜ δ <* Ψ ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
substₘ-lemma Ψ Ψ▶σ (fstₘ m γ▸t PE.refl ok) =
fstₘ m (substₘ-lemma Ψ Ψ▶σ γ▸t) PE.refl ok
substₘ-lemma Ψ Ψ▶σ (sndₘ γ▸t) =
sndₘ (substₘ-lemma Ψ Ψ▶σ γ▸t)
substₘ-lemma
{σ = σ} {mo = mo} Ψ Ψ▶σ
(prodrecₘ
{γ = γ} {r = r} {t = t} {δ = δ} {p = p} {u = u} {η = η} {q = q}
{A = A} γ▸t δ▸u η▸A P) =
case ▶-⌞·⌟ Ψ γ (▶-⌞+ᶜ⌟ˡ Ψ (_ ·ᶜ γ) Ψ▶σ) of λ where
(inj₂ Ψ▶σ) → lemma (substₘ-lemma Ψ Ψ▶σ γ▸t) ≈ᶜ-refl
(inj₁ (p≡𝟘 , ok)) → lemma
(▸-cong (≡𝟘→𝟘ᵐ≡ᵐ· ⦃ ok = ok ⦄ mo p≡𝟘)
(substₘ-lemma₀ ⦃ ok = ok ⦄ Ψ Ψ▶σ γ▸t))
(≡𝟘→·<*≈ᶜ·𝟘 {δ = γ} Ψ p≡𝟘)
where
lemma :
θ ▸[ mo ᵐ· r ] t [ σ ] →
r ·ᶜ γ <* Ψ ≈ᶜ r ·ᶜ θ →
(r ·ᶜ γ +ᶜ δ) <* Ψ ▸[ mo ] prodrec r p q A t u [ σ ]
lemma {θ = θ} hyp₁ hyp₂ = sub
(prodrecₘ hyp₁
(sub (substₘ-lemma (liftSubstₘ (liftSubstₘ Ψ))
(▶-cong (liftSubstₘ (liftSubstₘ Ψ))
(λ where
x0 → PE.refl
(x0 +1) → PE.refl
((_ +1) +1) → PE.refl)
(wf-liftSubstₘ
(wf-liftSubstₘ (▶-⌞+ᶜ⌟ʳ Ψ (_ ·ᶜ γ) Ψ▶σ))))
δ▸u)
(*>∙∙≤liftSubst-listSubst*>∙∙ {δ = δ} Ψ))
(substₘ-lemma-∙⌜𝟘ᵐ?⌝·▸[𝟘ᵐ?] Ψ Ψ▶σ η▸A .proj₂)
P)
(let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
(r ·ᶜ γ +ᶜ δ) <* Ψ ≈⟨ <*-distrib-+ᶜ Ψ (r ·ᶜ γ) δ ⟩
(r ·ᶜ γ) <* Ψ +ᶜ δ <* Ψ ≈⟨ +ᶜ-congʳ (<*-distrib-·ᶜ Ψ _ γ) ⟩
r ·ᶜ γ <* Ψ +ᶜ δ <* Ψ ≈⟨ +ᶜ-congʳ hyp₂ ⟩
r ·ᶜ θ +ᶜ δ <* Ψ ∎)
substₘ-lemma Ψ _ zeroₘ =
sub zeroₘ (≤ᶜ-reflexive (<*-zeroˡ Ψ))
substₘ-lemma Ψ Ψ▶σ (sucₘ γ▸t) =
sucₘ (substₘ-lemma Ψ Ψ▶σ γ▸t)
substₘ-lemma
Ψ Ψ▶σ
(natrecₘ {γ = γ} {δ = δ} {p = p} {r = r} {η = η} {θ = θ} {q = q}
γ▸z δ▸s η▸n θ▸A) = sub
(natrecₘ
(substₘ-lemma Ψ (▶-⌞∧ᶜ⌟ˡ Ψ γ (▶-⌞⊛ᶜ⌟ˡ Ψ (γ ∧ᶜ _) Ψ▶σ)) γ▸z)
(sub
(substₘ-lemma (liftSubstₘ (liftSubstₘ Ψ))
(▶-cong (liftSubstₘ (liftSubstₘ Ψ))
(λ where
x0 → PE.refl
(x0 +1) → PE.refl
((_ +1) +1) → PE.refl)
(wf-liftSubstₘ
(wf-liftSubstₘ (▶-⌞+ᶜ⌟ˡ Ψ δ (▶-⌞⊛ᶜ⌟ʳ Ψ (γ ∧ᶜ _) Ψ▶σ)))))
δ▸s)
(*>∙∙≤liftSubst-listSubst*>∙∙ {δ = δ} Ψ))
(substₘ-lemma Ψ (▶-⌞∧ᶜ⌟ʳ Ψ γ (▶-⌞⊛ᶜ⌟ˡ Ψ (γ ∧ᶜ _) Ψ▶σ)) η▸n)
(substₘ-lemma-∙⌜𝟘ᵐ?⌝·▸[𝟘ᵐ?] Ψ Ψ▶σ θ▸A .proj₂))
(let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
((γ ∧ᶜ η) ⊛ᶜ (δ +ᶜ p ·ᶜ η) ▷ r) <* Ψ ≤⟨ <*-sub-distrib-⊛ᶜ Ψ (γ ∧ᶜ η) (δ +ᶜ p ·ᶜ η) _ ⟩
((γ ∧ᶜ η) <* Ψ) ⊛ᶜ ((δ +ᶜ p ·ᶜ η) <* Ψ) ▷ r ≈⟨ ⊛ᵣᶜ-congˡ (<*-distrib-+ᶜ Ψ δ (p ·ᶜ η)) ⟩
((γ ∧ᶜ η) <* Ψ) ⊛ᶜ (δ <* Ψ +ᶜ (p ·ᶜ η) <* Ψ) ▷ r ≤⟨ ⊛ᶜ-monotoneʳ (<*-sub-distrib-∧ᶜ Ψ γ η) ⟩
(γ <* Ψ ∧ᶜ η <* Ψ) ⊛ᶜ (δ <* Ψ +ᶜ (p ·ᶜ η) <* Ψ) ▷ r ≈⟨ ⊛ᵣᶜ-congˡ (+ᶜ-congˡ (<*-distrib-·ᶜ Ψ _ η)) ⟩
(γ <* Ψ ∧ᶜ η <* Ψ) ⊛ᶜ (δ <* Ψ +ᶜ p ·ᶜ η <* Ψ) ▷ r ∎)
where
open import Graded.Modality.Dedicated-star.Instance
substₘ-lemma
Ψ Ψ▶σ
▸natrec@(natrec-no-starₘ
{γ = γ} {δ = δ} {p = p} {r = r} {η = η} {χ = χ}
⦃ no-star = no-star ⦄ γ▸z δ▸s η▸n θ▸A fix) =
𝟘ᵐ-allowed-elim
(λ ok →
natrec-no-starₘ
(substₘ-lemma Ψ
(flip (▶-≤ Ψ) Ψ▶σ $
let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
χ ≤⟨ fix ⟩
γ ∧ᶜ η ∧ᶜ (δ +ᶜ p ·ᶜ η +ᶜ r ·ᶜ χ) ≤⟨ ∧ᶜ-decreasingˡ _ _ ⟩
γ ∎)
γ▸z)
(sub
(substₘ-lemma (liftSubstₘ (liftSubstₘ Ψ))
(▶-cong (liftSubstₘ (liftSubstₘ Ψ))
(λ where
x0 → PE.refl
(x0 +1) → PE.refl
(_ +1 +1) → PE.refl)
(wf-liftSubstₘ $ wf-liftSubstₘ $
flip (▶-≤ Ψ) Ψ▶σ $
let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in
begin
χ ≤⟨ fix ⟩
γ ∧ᶜ η ∧ᶜ (δ +ᶜ p ·ᶜ η +ᶜ r ·ᶜ χ) ≤⟨ ∧ᶜ-decreasingʳ _ _ ⟩
η ∧ᶜ (δ +ᶜ p ·ᶜ η +ᶜ r ·ᶜ χ) ≤⟨ ∧ᶜ-decreasingʳ _ _ ⟩
δ +ᶜ p ·ᶜ η +ᶜ r ·ᶜ χ ≤⟨ +ᶜ-decreasingˡ ok (no-star .No-dedicated-star.no-star) ⟩
δ ∎))
δ▸s)
(*>∙∙≤liftSubst-listSubst*>∙∙ {δ = δ} Ψ))
(substₘ-lemma Ψ
(flip (▶-≤ Ψ) Ψ▶σ $
let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
χ ≤⟨ fix ⟩
γ ∧ᶜ η ∧ᶜ (δ +ᶜ p ·ᶜ η +ᶜ r ·ᶜ χ) ≤⟨ ∧ᶜ-decreasingʳ _ _ ⟩
η ∧ᶜ (δ +ᶜ p ·ᶜ η +ᶜ r ·ᶜ χ) ≤⟨ ∧ᶜ-decreasingˡ _ _ ⟩
η ∎)
η▸n)
(substₘ-lemma-∙⌜𝟘ᵐ?⌝·▸[𝟘ᵐ?] Ψ Ψ▶σ θ▸A .proj₂)
(let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
χ <* Ψ ≤⟨ <*-monotone Ψ fix ⟩
(γ ∧ᶜ η ∧ᶜ (δ +ᶜ p ·ᶜ η +ᶜ r ·ᶜ χ)) <* Ψ ≤⟨ ∧∧+·+·<*≤ Ψ γ ⟩
γ <* Ψ ∧ᶜ η <* Ψ ∧ᶜ (δ <* Ψ +ᶜ p ·ᶜ η <* Ψ +ᶜ r ·ᶜ χ <* Ψ) ∎))
(λ not-ok →
▸-without-𝟘ᵐ not-ok (substₘ-lemma₁ not-ok Ψ Ψ▶σ ▸natrec))
substₘ-lemma {mo = mo} Ψ Ψ▶σ (emptyrecₘ {γ = γ} {p = p} γ▸t δ▸A) =
case ▶-⌞·⌟ Ψ γ Ψ▶σ of λ where
(inj₂ Ψ▶σ) → sub
(emptyrecₘ (substₘ-lemma Ψ Ψ▶σ γ▸t)
(substₘ-lemma-𝟘ᵐ? Ψ Ψ▶σ δ▸A .proj₂))
(≤ᶜ-reflexive (<*-distrib-·ᶜ Ψ _ γ))
(inj₁ (p≡𝟘 , ok)) → sub
(emptyrecₘ (▸-cong (≡𝟘→𝟘ᵐ≡ᵐ· ⦃ ok = ok ⦄ mo p≡𝟘)
(substₘ-lemma₀ ⦃ ok = ok ⦄ Ψ Ψ▶σ γ▸t))
(▸-cong
(PE.sym 𝟘ᵐ?≡𝟘ᵐ)
(substₘ-lemma₀ ⦃ ok = ok ⦄ Ψ Ψ▶σ δ▸A)))
(let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
(p ·ᶜ γ) <* Ψ ≈⟨ <*-distrib-·ᶜ Ψ _ γ ⟩
p ·ᶜ γ <* Ψ ≈⟨ ≡𝟘→·<*≈ᶜ·𝟘 {δ = γ} Ψ p≡𝟘 ⟩
p ·ᶜ 𝟘ᶜ ∎)
substₘ-lemma Ψ Ψ▶σ starₘ = sub
starₘ
(≤ᶜ-reflexive (<*-zeroˡ Ψ))
substₘ-lemma Ψ Ψ▶σ (sub γ▸t γ≤δ) = sub
(substₘ-lemma Ψ (▶-≤ Ψ γ≤δ Ψ▶σ) γ▸t)
(<*-monotone Ψ γ≤δ)
sgSubstₘ-lemma₁ :
γ ∙ ⌜ mo ⌝ · p ▸[ mo ] t → δ ▸[ mo ᵐ· p ] u →
γ +ᶜ (⌜ mo ⌝ · p) ·ᶜ δ ▸[ mo ] t [ u ]₀
sgSubstₘ-lemma₁ {γ = γ} {mo = mo} {p = p} {δ = δ} γ▸t δ▸u = sub
(substₘ-lemma (sgSubstₘ δ)
(▶-cong (sgSubstₘ δ)
(λ where
(_ +1) → PE.refl
x0 → PE.sym (⌞⌜⌝·⌟ mo))
(wf-sgSubstₘ (▸-·′ δ▸u)))
γ▸t)
(begin
γ +ᶜ (⌜ mo ⌝ · p) ·ᶜ δ ≈⟨ +ᶜ-comm _ _ ⟩
(⌜ mo ⌝ · p) ·ᶜ δ +ᶜ γ ≈˘⟨ +ᶜ-congˡ (<*-identityˡ _) ⟩
(⌜ mo ⌝ · p) ·ᶜ δ +ᶜ γ <* idSubstₘ ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
sgSubstₘ-lemma₂ :
γ ∙ ⌜ mo ⌝ · p ▸[ mo ] t → δ ▸[ mo ᵐ· p ] u →
γ +ᶜ p ·ᶜ δ ▸[ mo ] t [ u ]₀
sgSubstₘ-lemma₂ {γ = γ} {mo = 𝟙ᵐ} {p = p} {δ = δ} γ▸t δ▸u = sub
(sgSubstₘ-lemma₁ γ▸t δ▸u)
(begin
γ +ᶜ p ·ᶜ δ ≈˘⟨ +ᶜ-congˡ (·ᶜ-congʳ (·-identityˡ _)) ⟩
γ +ᶜ (𝟙 · p) ·ᶜ δ ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
sgSubstₘ-lemma₂ {γ = γ} {mo = 𝟘ᵐ} {p = p} {δ = δ} γ▸t δ▸u = sub
(sgSubstₘ-lemma₁ γ▸t δ▸u)
(begin
γ +ᶜ p ·ᶜ δ ≤⟨ +ᶜ-monotoneʳ (·ᶜ-monotoneʳ (▸-𝟘ᵐ δ▸u)) ⟩
γ +ᶜ p ·ᶜ 𝟘ᶜ ≈⟨ +ᶜ-congˡ (·ᶜ-zeroʳ _) ⟩
γ +ᶜ 𝟘ᶜ ≈˘⟨ +ᶜ-congˡ (·ᶜ-zeroˡ _) ⟩
γ +ᶜ 𝟘 ·ᶜ δ ≈˘⟨ +ᶜ-congˡ (·ᶜ-congʳ (·-zeroˡ _)) ⟩
γ +ᶜ (𝟘 · p) ·ᶜ δ ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
sgSubstₘ-lemma₃ :
γ ∙ ⌜ mo ⌝ · p ▸[ mo ] t → δ ▸[ mo ] u →
γ +ᶜ p ·ᶜ δ ▸[ mo ] t [ u ]₀
sgSubstₘ-lemma₃ {mo = 𝟘ᵐ} =
sgSubstₘ-lemma₂
sgSubstₘ-lemma₃ {mo = 𝟙ᵐ} ▸t ▸u =
case ▸[𝟙ᵐ]→▸[⌞⌟] ▸u of λ where
(_ , ▸u , eq) → sub
(sgSubstₘ-lemma₂ ▸t ▸u)
(≤ᶜ-reflexive (+ᶜ-congˡ eq))
doubleSubstₘ-lemma₁ :
γ ∙ ⌜ mo ⌝ · q ∙ ⌜ mo ⌝ · p ▸[ mo ] t →
δ ▸[ mo ᵐ· p ] u → η ▸[ mo ᵐ· q ] u′ →
γ +ᶜ (⌜ mo ⌝ · p) ·ᶜ δ +ᶜ (⌜ mo ⌝ · q) ·ᶜ η ▸[ mo ] t [ u′ ,, u ]
doubleSubstₘ-lemma₁
{γ = γ} {mo = mo} {q = q} {p = p} {δ = δ} {η = η} γ▸t δ▸u η▸u′ = sub
(substₘ-lemma (consSubstₘ (sgSubstₘ _) _)
(▶-cong (consSubstₘ (sgSubstₘ _) _)
(λ where
x0 → PE.sym (⌞⌜⌝·⌟ mo)
(x0 +1) → PE.sym (⌞⌜⌝·⌟ mo)
((_ +1) +1) → PE.refl)
(wf-consSubstₘ (wf-sgSubstₘ (▸-·′ η▸u′)) (▸-·′ δ▸u)))
γ▸t)
(begin
γ +ᶜ (⌜ mo ⌝ · p) ·ᶜ δ +ᶜ (⌜ mo ⌝ · q) ·ᶜ η ≈⟨ +ᶜ-comm _ _ ⟩
((⌜ mo ⌝ · p) ·ᶜ δ +ᶜ (⌜ mo ⌝ · q) ·ᶜ η) +ᶜ γ ≈⟨ +ᶜ-assoc _ _ _ ⟩
(⌜ mo ⌝ · p) ·ᶜ δ +ᶜ (⌜ mo ⌝ · q) ·ᶜ η +ᶜ γ ≈˘⟨ +ᶜ-congˡ (+ᶜ-congˡ (<*-identityˡ _)) ⟩
(⌜ mo ⌝ · p) ·ᶜ δ +ᶜ (⌜ mo ⌝ · q) ·ᶜ η +ᶜ γ <* idSubstₘ ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
doubleSubstₘ-lemma₂ :
γ ∙ ⌜ mo ⌝ · q ∙ ⌜ mo ⌝ · p ▸[ mo ] t →
δ ▸[ mo ᵐ· p ] u → η ▸[ mo ᵐ· q ] u′ →
γ +ᶜ p ·ᶜ δ +ᶜ q ·ᶜ η ▸[ mo ] t [ u′ ,, u ]
doubleSubstₘ-lemma₂
{γ = γ} {mo = 𝟙ᵐ} {q = q} {p = p} {δ = δ} {η = η} γ▸t δ▸u η▸u′ = sub
(doubleSubstₘ-lemma₁ γ▸t δ▸u η▸u′)
(begin
γ +ᶜ p ·ᶜ δ +ᶜ q ·ᶜ η ≈˘⟨ +ᶜ-congˡ (+ᶜ-cong (·ᶜ-congʳ (·-identityˡ _)) (·ᶜ-congʳ (·-identityˡ _))) ⟩
γ +ᶜ (𝟙 · p) ·ᶜ δ +ᶜ (𝟙 · q) ·ᶜ η ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
doubleSubstₘ-lemma₂
{γ = γ} {mo = 𝟘ᵐ} {q = q} {p = p} {δ = δ} {η = η} γ▸t δ▸u η▸u′ = sub
(doubleSubstₘ-lemma₁ γ▸t δ▸u η▸u′)
(begin
γ +ᶜ p ·ᶜ δ +ᶜ q ·ᶜ η ≤⟨ +ᶜ-monotoneʳ (+ᶜ-monotone (·ᶜ-monotoneʳ (▸-𝟘ᵐ δ▸u)) (·ᶜ-monotoneʳ (▸-𝟘ᵐ η▸u′))) ⟩
γ +ᶜ p ·ᶜ 𝟘ᶜ +ᶜ q ·ᶜ 𝟘ᶜ ≈⟨ +ᶜ-congˡ (+ᶜ-cong (·ᶜ-zeroʳ _) (·ᶜ-zeroʳ _)) ⟩
γ +ᶜ 𝟘ᶜ +ᶜ 𝟘ᶜ ≈˘⟨ +ᶜ-congˡ (+ᶜ-cong (·ᶜ-zeroˡ _) (·ᶜ-zeroˡ _)) ⟩
γ +ᶜ 𝟘 ·ᶜ δ +ᶜ 𝟘 ·ᶜ η ≈˘⟨ +ᶜ-congˡ (+ᶜ-cong (·ᶜ-congʳ (·-zeroˡ _)) (·ᶜ-congʳ (·-zeroˡ _))) ⟩
γ +ᶜ (𝟘 · p) ·ᶜ δ +ᶜ (𝟘 · q) ·ᶜ η ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
doubleSubstₘ-lemma₃ :
γ ∙ ⌜ mo ⌝ · q ∙ ⌜ mo ⌝ · p ▸[ mo ] t →
δ ▸[ mo ] u → η ▸[ mo ] u′ →
γ +ᶜ p ·ᶜ δ +ᶜ q ·ᶜ η ▸[ mo ] t [ u′ ,, u ]
doubleSubstₘ-lemma₃ {mo = 𝟘ᵐ} =
doubleSubstₘ-lemma₂
doubleSubstₘ-lemma₃ {mo = 𝟙ᵐ} ▸t ▸u ▸u′ =
case ▸[𝟙ᵐ]→▸[⌞⌟] ▸u of λ where
(_ , ▸u , eq) → case ▸[𝟙ᵐ]→▸[⌞⌟] ▸u′ of λ where
(_ , ▸u′ , eq′) → sub
(doubleSubstₘ-lemma₂ ▸t ▸u ▸u′)
(≤ᶜ-reflexive (+ᶜ-congˡ (+ᶜ-cong eq eq′)))
substₘ-calc-row :
⦃ has-star : Has-star semiring-with-meet ⦄ →
(σ : Subst m n) (x : Fin n) →
(𝟘ᶜ , x ≔ 𝟙) <* ∥ σ ∥ mos ≈ᶜ ⌈ σ x ⌉ (mos x)
substₘ-calc-row {mos = mos} σ x0 = begin
(𝟘ᶜ , x0 ≔ 𝟙) <* ∥ σ ∥ mos ≡⟨⟩
(𝟘ᶜ ∙ 𝟙) <* ∥ σ ∥ mos ≡⟨⟩
𝟙 ·ᶜ ⌈ σ x0 ⌉ (headᵐ mos) +ᶜ 𝟘ᶜ <* ∥ tail σ ∥ (tailᵐ mos) ≈⟨ +ᶜ-cong (·ᶜ-identityˡ _) (<*-zeroˡ (∥ tail σ ∥ _)) ⟩
⌈ σ x0 ⌉ (headᵐ mos) +ᶜ 𝟘ᶜ ≈⟨ +ᶜ-identityʳ _ ⟩
⌈ σ x0 ⌉ (headᵐ mos) ∎
where open Tools.Reasoning.Equivalence Conₘ-setoid
substₘ-calc-row {mos = mos} σ (x +1) = begin
(𝟘ᶜ , x +1 ≔ 𝟙) <* ∥ σ ∥ mos ≡⟨⟩
((𝟘ᶜ , x ≔ 𝟙) ∙ 𝟘) <* ∥ σ ∥ mos ≡⟨⟩
𝟘 ·ᶜ ⌈ σ x0 ⌉ (headᵐ mos) +ᶜ (𝟘ᶜ , x ≔ 𝟙) <* ∥ tail σ ∥ (tailᵐ mos) ≈⟨ +ᶜ-cong (·ᶜ-zeroˡ _) (substₘ-calc-row (tail σ) x) ⟩
𝟘ᶜ +ᶜ ⌈ tail σ x ⌉ (tailᵐ mos x) ≈⟨ +ᶜ-identityˡ _ ⟩
⌈ σ (x +1) ⌉ (tailᵐ mos x) ∎
where open Tools.Reasoning.Equivalence Conₘ-setoid
∥∥-*>-𝟘ᶜ,≔𝟙 :
⦃ has-star : Has-star semiring-with-meet ⦄ →
(σ : Subst m n) →
(𝟘ᶜ , x ≔ 𝟙) <* ∥ σ ∥ mos ≈ᶜ (𝟘ᶜ , x ≔ ⌜ mos x ⌝) <* ∥ σ ∥ mos
∥∥-*>-𝟘ᶜ,≔𝟙 {x = x} {mos = mos} σ = begin
(𝟘ᶜ , x ≔ 𝟙) <* ∥ σ ∥ mos ≈⟨ substₘ-calc-row σ _ ⟩
⌈ σ x ⌉ (mos x) ≈˘⟨ ·-⌈⌉ (σ x) ⟩
⌜ mos x ⌝ ·ᶜ ⌈ σ x ⌉ (mos x) ≈˘⟨ ·ᶜ-congˡ (substₘ-calc-row σ _) ⟩
⌜ mos x ⌝ ·ᶜ (𝟘ᶜ , x ≔ 𝟙) <* ∥ σ ∥ mos ≈⟨ ·ᶜ-<*-𝟘ᶜ,≔𝟙 (∥ σ ∥ _) ⟩
(𝟘ᶜ , x ≔ ⌜ mos x ⌝) <* ∥ σ ∥ mos ∎
where
open Tools.Reasoning.Equivalence Conₘ-setoid
open import Graded.Modality.Dedicated-star.Instance
substₘ-calc-correct :
⦃ has-star : Dedicated-star ⦄ →
(σ : Subst m n) →
(∀ x → ∃ λ γ → γ ▸[ mos x ] σ x) → ∥ σ ∥ mos ▶[ mos ] σ
substₘ-calc-correct {mos = mos} σ prop x with prop x
... | γ , γ▸σx = sub
(usage-inf γ▸σx)
(begin
(𝟘ᶜ , x ≔ ⌜ mos x ⌝) <* ∥ σ ∥ mos ≈˘⟨ ·ᶜ-<*-𝟘ᶜ,≔𝟙 (∥ σ ∥ _) ⟩
⌜ mos x ⌝ ·ᶜ (𝟘ᶜ , x ≔ 𝟙) <* ∥ σ ∥ mos ≈⟨ ·ᶜ-congˡ (substₘ-calc-row σ _) ⟩
⌜ mos x ⌝ ·ᶜ ⌈ σ x ⌉ (mos x) ≈⟨ ·-⌈⌉ {m = mos x} (σ x) ⟩
⌈ σ x ⌉ (mos x) ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
subst-calc-correct′ :
⦃ has-star : Dedicated-star ⦄ →
(Ψ : Substₘ m n) →
Ψ ▶[ mos ] σ → ∥ σ ∥ mos ▶[ mos ] σ
subst-calc-correct′ {mos = mos} {σ = σ} (Ψ ⊙ γ) Ψ▶σ x0 = sub
(usage-inf (Ψ▶σ x0))
(begin
⌜ headᵐ mos ⌝ ·ᶜ ⌈ head σ ⌉ (headᵐ mos) +ᶜ
𝟘ᶜ <* ∥ tail σ ∥ (tailᵐ mos) ≈⟨ +ᶜ-congˡ (<*-zeroˡ (∥ tail σ ∥ _)) ⟩
⌜ headᵐ mos ⌝ ·ᶜ ⌈ head σ ⌉ (headᵐ mos) +ᶜ 𝟘ᶜ ≈⟨ +ᶜ-identityʳ _ ⟩
⌜ headᵐ mos ⌝ ·ᶜ ⌈ head σ ⌉ (headᵐ mos) ≈⟨ ·-⌈⌉ (head σ) ⟩
⌈ head σ ⌉ (headᵐ mos) ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset
subst-calc-correct′ (Ψ ⊙ γ) Ψ▶σ (x +1) =
sub (subst-calc-correct′ Ψ (wf-tailSubstₘ Ψ▶σ) x)
(≤ᶜ-reflexive (≈ᶜ-trans (+ᶜ-congʳ (·ᶜ-zeroˡ _)) (+ᶜ-identityˡ _)))
substₘ-calc-upper-bound :
⦃ has-star : Dedicated-star ⦄ →
{γ : Conₘ m} (σ : Subst m n) (x : Fin n) →
γ ▸[ mos x ] σ x → γ ≤ᶜ (𝟘ᶜ , x ≔ 𝟙) <* ∥ σ ∥ mos
substₘ-calc-upper-bound σ x γ▸σx =
≤ᶜ-trans (usage-upper-bound γ▸σx)
(≤ᶜ-reflexive (≈ᶜ-sym (substₘ-calc-row σ x)))
wf-compSubst :
(Ψ : Substₘ m ℓ) {Φ : Substₘ ℓ n} {σ : Subst m ℓ} {σ′ : Subst ℓ n} →
Ψ ▶[ ⌞ ⌜ mos ⌝ᶜ <* Φ ⌟ᶜ ] σ → Φ ▶[ mos ] σ′ →
(Ψ <*> Φ) ▶[ mos ] (σ ₛ•ₛ σ′)
wf-compSubst {mos = mos} Ψ {Φ = Φ} {σ = σ} {σ′ = σ′} Ψ▶σ Φ▶σ′ x = sub
(substₘ-lemma Ψ
(▶-cong Ψ
(λ y → cong (λ p → ⌞ (𝟘ᶜ , x ≔ p) <* Φ ⌟ᶜ y) (⌜⌝ᶜ⟨⟩ {ms = mos} x))
(▶-⌞<*⌟ {γ = ⌜ mos ⌝ᶜ} Ψ {Φ = Φ} Ψ▶σ))
(Φ▶σ′ x))
(begin
(𝟘ᶜ , x ≔ ⌜ mos x ⌝) <* (Ψ <*> Φ) ≈˘⟨ ·ᶜ-<*-𝟘ᶜ,≔𝟙 (Ψ <*> Φ) ⟩
⌜ mos x ⌝ ·ᶜ (𝟘ᶜ , x ≔ 𝟙) <* (Ψ <*> Φ) ≈⟨ ·ᶜ-congˡ (<*-<*>-assoc Ψ Φ (𝟘ᶜ , x ≔ 𝟙)) ⟩
⌜ mos x ⌝ ·ᶜ ((𝟘ᶜ , x ≔ 𝟙) <* Φ) <* Ψ ≈˘⟨ <*-distrib-·ᶜ Ψ _ ((𝟘ᶜ , x ≔ 𝟙) <* Φ) ⟩
(⌜ mos x ⌝ ·ᶜ (𝟘ᶜ , x ≔ 𝟙) <* Φ) <* Ψ ≈⟨ <*-cong Ψ (·ᶜ-<*-𝟘ᶜ,≔𝟙 Φ) ⟩
((𝟘ᶜ , x ≔ ⌜ mos x ⌝) <* Φ) <* Ψ ∎)
where
open Tools.Reasoning.PartialOrder ≤ᶜ-poset