import Graded.Modality
module Graded.Context.Properties.Lookup
{a} {M : Set a}
(open Graded.Modality M)
(𝕄 : Modality)
where
open Modality 𝕄
open import Graded.Context 𝕄
open import Graded.Context.Properties.Equivalence 𝕄
open import Graded.Context.Properties.PartialOrder 𝕄
open import Graded.Modality.Nr-instances
open import Graded.Modality.Properties.PartialOrder semiring-with-meet
open import Tools.Fin
open import Tools.Function
open import Tools.Nat using (Nat)
open import Tools.Product
open import Tools.PropositionalEquality as PE
private
variable
n : Nat
x : Fin n
p r : M
γ δ : Conₘ n
𝟘ᶜ-lookup : (x : Fin n) → 𝟘ᶜ ⟨ x ⟩ ≡ 𝟘
𝟘ᶜ-lookup x0 = PE.refl
𝟘ᶜ-lookup (x +1) = 𝟘ᶜ-lookup x
𝟙ᶜ-lookup : (x : Fin n) → 𝟙ᶜ ⟨ x ⟩ ≡ 𝟙
𝟙ᶜ-lookup x0 = PE.refl
𝟙ᶜ-lookup (x +1) = 𝟙ᶜ-lookup x
lookup-monotone : (x : Fin n) → γ ≤ᶜ δ → (γ ⟨ x ⟩) ≤ (δ ⟨ x ⟩)
lookup-monotone {γ = γ ∙ p} {δ ∙ q} x0 (γ≤δ ∙ p≤q) = p≤q
lookup-monotone {γ = γ ∙ p} {δ ∙ q} (x +1) (γ≤δ ∙ p≤q) = lookup-monotone x γ≤δ
lookup-cong : γ ≈ᶜ δ → γ ⟨ x ⟩ ≡ δ ⟨ x ⟩
lookup-cong γ≈ᶜδ = ≤-antisym
(lookup-monotone _ (≤ᶜ-reflexive γ≈ᶜδ))
(lookup-monotone _ (≤ᶜ-reflexive (≈ᶜ-sym γ≈ᶜδ)))
lookup-distrib-+ᶜ : (γ δ : Conₘ n) (x : Fin n) → (γ +ᶜ δ) ⟨ x ⟩ ≡ γ ⟨ x ⟩ + δ ⟨ x ⟩
lookup-distrib-+ᶜ (γ ∙ p) (δ ∙ q) x0 = PE.refl
lookup-distrib-+ᶜ (γ ∙ p) (δ ∙ q) (x +1) = lookup-distrib-+ᶜ γ δ x
lookup-distrib-·ᶜ : (γ : Conₘ n) (p : M) (x : Fin n) → (p ·ᶜ γ) ⟨ x ⟩ ≡ p · γ ⟨ x ⟩
lookup-distrib-·ᶜ (γ ∙ q) p x0 = PE.refl
lookup-distrib-·ᶜ (γ ∙ q) p (x +1) = lookup-distrib-·ᶜ γ p x
lookup-distrib-∧ᶜ : (γ δ : Conₘ n) (x : Fin n)
→ (γ ∧ᶜ δ) ⟨ x ⟩ ≡ (γ ⟨ x ⟩) ∧ (δ ⟨ x ⟩)
lookup-distrib-∧ᶜ (γ ∙ p) (δ ∙ q) x0 = PE.refl
lookup-distrib-∧ᶜ (γ ∙ p) (δ ∙ q) (x +1) = lookup-distrib-∧ᶜ γ δ x
lookup-distrib-⊛ᶜ :
⦃ has-star : Has-star semiring-with-meet ⦄ →
(γ δ : Conₘ n) (r : M) (x : Fin n) →
(γ ⊛ᶜ δ ▷ r) ⟨ x ⟩ ≡ (γ ⟨ x ⟩) ⊛ (δ ⟨ x ⟩) ▷ r
lookup-distrib-⊛ᶜ (γ ∙ p) (δ ∙ q) r x0 = PE.refl
lookup-distrib-⊛ᶜ (γ ∙ p) (δ ∙ q) r (x +1) = lookup-distrib-⊛ᶜ γ δ r x
update-lookup : (γ : Conₘ n) (x : Fin n) → (γ , x ≔ p) ⟨ x ⟩ ≡ p
update-lookup (_ ∙ _) x0 = PE.refl
update-lookup (γ ∙ _) (x +1) = update-lookup γ x
opaque
≈ᶜ𝟘ᶜ⇔⟨⟩≡𝟘 : γ ≈ᶜ 𝟘ᶜ ⇔ (∀ x → γ ⟨ x ⟩ ≡ 𝟘)
≈ᶜ𝟘ᶜ⇔⟨⟩≡𝟘 = to , from
where
to : γ ≈ᶜ 𝟘ᶜ → ∀ x → γ ⟨ x ⟩ ≡ 𝟘
to {γ = ε} ε ()
to {γ = _ ∙ _} (_ ∙ ≡𝟘) x0 = ≡𝟘
to {γ = _ ∙ _} (≈𝟘 ∙ _) (x +1) = to ≈𝟘 x
from : (∀ x → γ ⟨ x ⟩ ≡ 𝟘) → γ ≈ᶜ 𝟘ᶜ
from {γ = ε} _ = ε
from {γ = _ ∙ _} hyp = from (hyp ∘→ _+1) ∙ hyp x0