open import Definition.Typed.Restrictions
open import Graded.Modality
open import Graded.Usage.Restrictions
module Graded.Derived.Identity
{a} {M : Set a}
{𝕄 : Modality M}
(UR : Usage-restrictions 𝕄)
where
open Modality 𝕄
open Usage-restrictions UR
open import Graded.Context 𝕄
open import Graded.Context.Properties 𝕄
open import Graded.Modality.Properties 𝕄
open import Graded.Mode 𝕄
open import Graded.Substitution.Properties 𝕄 UR
open import Graded.Usage 𝕄 UR
open import Graded.Usage.Erased-matches
open import Graded.Usage.Properties 𝕄 UR
open import Graded.Usage.Weakening 𝕄 UR
open import Definition.Untyped M
open import Definition.Untyped.Identity 𝕄
open import Tools.Bool
open import Tools.Function
open import Tools.Product
open import Tools.PropositionalEquality as PE using (_≡_)
import Tools.Reasoning.PartialOrder
open import Tools.Relation
private variable
A B t u v w : Term _
p : M
γ₁ γ₂ γ₃ γ₄ γ₅ γ₆ γ₇ : Conₘ _
m : Mode
sem : Some-erased-matches
opaque
unfolding subst
▸subst :
γ₁ ▸[ 𝟘ᵐ? ] A →
γ₂ ∙ ⌜ m ⌝ · p ▸[ m ] B →
γ₃ ▸[ m ] t →
γ₄ ▸[ m ] u →
γ₅ ▸[ m ] v →
γ₆ ▸[ m ] w →
ω ·ᶜ (γ₂ +ᶜ γ₃ +ᶜ γ₄ +ᶜ γ₅ +ᶜ γ₆) ▸[ m ] subst p A B t u v w
▸subst {γ₁} {γ₂} {m} {p} {γ₃} {γ₄} {γ₅} {γ₆} ▸A ▸B ▸t ▸u ▸v ▸w = sub
(Jₘ-generalised ▸A ▸t
(sub (wkUsage (step id) ▸B) $
let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
γ₂ ∙ ⌜ m ⌝ · p ∙ ⌜ m ⌝ · 𝟘 ≈⟨ ≈ᶜ-refl ∙ ·-zeroʳ _ ⟩
γ₂ ∙ ⌜ m ⌝ · p ∙ 𝟘 ∎)
▸w ▸u ▸v)
(let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
ω ·ᶜ (γ₂ +ᶜ γ₃ +ᶜ γ₄ +ᶜ γ₅ +ᶜ γ₆) ≈⟨ ·ᶜ-congˡ $
≈ᶜ-trans (≈ᶜ-sym $ +ᶜ-assoc _ _ _) $
≈ᶜ-trans (+ᶜ-congʳ $ +ᶜ-comm _ _) $
≈ᶜ-trans (+ᶜ-assoc _ _ _) $
+ᶜ-congˡ $ +ᶜ-congˡ $
≈ᶜ-trans (≈ᶜ-sym $ +ᶜ-assoc _ _ _) $
+ᶜ-comm _ _ ⟩
ω ·ᶜ (γ₃ +ᶜ γ₂ +ᶜ γ₆ +ᶜ γ₄ +ᶜ γ₅) ∎)
opaque
unfolding subst
▸subst-𝟘 :
erased-matches-for-J m ≡ not-none sem →
γ₁ ▸[ 𝟘ᵐ? ] A →
γ₂ ∙ 𝟘 ▸[ m ] B →
γ₃ ▸[ 𝟘ᵐ? ] t →
γ₄ ▸[ 𝟘ᵐ? ] u →
γ₅ ▸[ 𝟘ᵐ? ] v →
γ₆ ▸[ m ] w →
ω ·ᶜ (γ₂ +ᶜ γ₆) ▸[ m ] subst 𝟘 A B t u v w
▸subst-𝟘 ≡not-none ▸A ▸B ▸t ▸u ▸v ▸w =
J₀ₘ₁-generalised ≡not-none PE.refl PE.refl ▸A ▸t
(wkUsage (step id) ▸B) ▸w ▸u ▸v
opaque
unfolding cong
▸cong :
γ₁ ▸[ 𝟘ᵐ? ] A →
γ₂ ▸[ m ] t →
γ₃ ▸[ m ] u →
γ₄ ▸[ 𝟘ᵐ? ] B →
γ₅ ∙ ⌜ m ⌝ · p ▸[ m ] v →
γ₆ ▸[ m ] w →
(Id-erased →
γ₇ ∙ ⌜ m ⌝ · p ≤ᶜ 𝟘ᶜ) →
(¬ Id-erased →
γ₇ ≤ᶜ (⌜ m ⌝ · p) ·ᶜ γ₂ +ᶜ (𝟙 + 𝟙) ·ᶜ γ₅) →
ω ·ᶜ (γ₂ +ᶜ γ₃ +ᶜ γ₆ +ᶜ γ₇) ▸[ m ] cong p A t u B v w
▸cong
{γ₂} {m} {t} {γ₃} {γ₅} {p} {γ₆} {γ₇}
▸A ▸t ▸u ▸B ▸v ▸w hyp₁ hyp₂ =
case ▸→▸[ᵐ·] ▸t of λ
(γ₂′ , ▸t′ , pγ₂≈pγ₂′) →
sub
(▸subst ▸A
(Idₘ-generalised (wkUsage (step id) ▸B)
(wkUsage (step id) $ sgSubstₘ-lemma₁ ▸v ▸t′)
▸v
hyp₁
(λ not-erased → begin
γ₇ ∙ ⌜ m ⌝ · p ≤⟨ hyp₂ not-erased ∙ ≤-refl ⟩
((⌜ m ⌝ · p) ·ᶜ γ₂ +ᶜ (𝟙 + 𝟙) ·ᶜ γ₅) ∙ ⌜ m ⌝ · p ≈˘⟨ (≈ᶜ-trans (+ᶜ-congʳ $ +ᶜ-comm _ _) $
≈ᶜ-trans (+ᶜ-assoc _ _ _) $
≈ᶜ-sym $
+ᶜ-cong
(≈ᶜ-trans (·ᶜ-assoc _ _ _) $
≈ᶜ-trans (·ᶜ-congˡ pγ₂≈pγ₂′) $
≈ᶜ-sym $ ·ᶜ-assoc _ _ _)
(≈ᶜ-trans (·ᶜ-distribʳ-+ᶜ _ _ _) $
+ᶜ-cong (·ᶜ-identityˡ _) (·ᶜ-identityˡ _))) ∙
+-identityˡ _ ⟩
((γ₅ +ᶜ (⌜ m ⌝ · p) ·ᶜ γ₂′) +ᶜ γ₅) ∙ 𝟘 + ⌜ m ⌝ · p ∎))
▸t ▸u ▸w rflₘ)
(begin
ω ·ᶜ (γ₂ +ᶜ γ₃ +ᶜ γ₆ +ᶜ γ₇) ≈˘⟨ ·ᶜ-congˡ $
≈ᶜ-trans (≈ᶜ-sym $ +ᶜ-assoc _ _ _) $
≈ᶜ-trans (+ᶜ-congʳ $ +ᶜ-comm _ _) $
≈ᶜ-trans (+ᶜ-assoc _ _ _) $
+ᶜ-congˡ $
≈ᶜ-trans (≈ᶜ-sym $ +ᶜ-assoc _ _ _) $
≈ᶜ-trans (+ᶜ-congʳ $ +ᶜ-comm _ _) $
≈ᶜ-trans (+ᶜ-assoc _ _ _) $
+ᶜ-congˡ $
≈ᶜ-trans (≈ᶜ-sym $ +ᶜ-assoc _ _ _) $
≈ᶜ-trans (+ᶜ-congʳ $ +ᶜ-comm _ _) $
≈ᶜ-trans (+ᶜ-assoc _ _ _) $
+ᶜ-congˡ $
+ᶜ-identityʳ _ ⟩
ω ·ᶜ (γ₇ +ᶜ γ₂ +ᶜ γ₃ +ᶜ γ₆ +ᶜ 𝟘ᶜ) ∎)
where
open ≤ᶜ-reasoning