{-# OPTIONS --without-K --safe #-}

-- Properties of domain-level operations that do not rely on functional extensionality
module Mints.Semantics.Properties.NoFunExt.Domain where

open import Data.Nat.Properties as Nₚ

open import Lib
open import Mints.Statics.Syntax
open import Mints.Semantics.Domain

O-add-ρ : ∀ n m (ρ : Envs) → O ρ (n + m) ≡ O ρ n + O (ρ ∥ n) m
O-add-ρ zero m ρ    = refl
O-add-ρ (suc n) m ρ = trans (cong (proj₁ (ρ ) +_) (O-add-ρ n m (ρ ∥ )))
                            (sym (+-assoc (proj₁ (ρ )) (O (ρ ∥ ) n) (O (ρ ∥ suc n) m)))

O-vone : ∀ n → O vone n ≡ n
O-vone zero    = refl
O-vone (suc n) = cong suc (O-vone n)

O-+ : ∀ (κ : UMoT) n m → O κ (n + m) ≡ O κ n + O (κ ∥ n) m
O-+ κ zero m              = refl
O-+ κ (suc n) m
  rewrite O-+ (κ ∥ ) n m = sym (+-assoc (κ ) (O (κ ∥ ) n) (O (κ ∥ suc n) m))

O-ø : ∀ κ κ′ n → O (κ ø κ′) n ≡ O κ′ (O κ n)
O-ø κ κ′ zero                        = refl
O-ø κ κ′ (suc n)
  rewrite O-ø (κ ∥ ) (κ′ ∥ κ ) n
        | O-+ κ′ (κ ) (O (κ ∥ ) n) = refl


O-drop : ∀ n ρ → O (drop ρ) n ≡ O ρ n
O-drop zero ρ    = refl
O-drop (suc n) ρ = refl

O-↦ : ∀ n ρ a → O (ρ ↦ a) n ≡ O ρ n
O-↦ zero ρ a    = refl
O-↦ (suc n) ρ a = refl

O-ρ-+ : ∀ (ρ : Envs) n m → O ρ (n + m) ≡ O ρ n + O (ρ ∥ n) m
O-ρ-+ ρ zero m = refl
O-ρ-+ ρ (suc n) m = trans (cong (proj₁ (ρ ) +_) (O-ρ-+ (ρ ∥ ) n m))
                          (sym (+-assoc (proj₁ (ρ )) (O (ρ ∥ ) n) (O (ρ ∥ suc n) m)))