------------------------------------------------------------------------
-- Some derived properties of the semantics
------------------------------------------------------------------------

module SimplyTyped.Semantics.Lemmas where

open import SimplyTyped.TypeSystem
open import SimplyTyped.Semantics
open import Data.Star hiding (_▻_)
open import Data.Star.Properties

-- Preorder reasoning for ⇛⋆.

private
  module Dummy {Γ : Ctxt} {σ : Ty} where
    open StarReasoning {I = Γ ⊢ σ} _⇛_ public
      renaming (_⟶⟨_⟩_ to _⇛⟨_⟩_; _⟶⋆⟨_⟩_ to _⇛⋆⟨_⟩_)

open Dummy public

-- Some congruences.

ƛ-cong : ∀ {Γ σ τ} {t₁ t₂ : Γ ▻ σ ⊢ τ} →
         t₁ ⇛⋆ t₂ → ƛ t₁ ⇛⋆ ƛ t₂
ƛ-cong = gmap _ ƛ-cong'
  where
  ƛ-cong' : ∀ {Γ σ τ} {t₁ t₂ : Γ ▻ σ ⊢ τ} →
            t₁ ⇛ t₂ → ƛ t₁ ⇛ ƛ t₂
  ƛ-cong' (red C t₁⟶t₂) = red (ƛ• C) t₁⟶t₂

_·-cong_ : ∀ {Γ σ τ} {t₁ t₂ : Γ ⊢ σ ⟶ τ} {u₁ u₂ : Γ ⊢ σ} →
           t₁ ⇛⋆ t₂ → u₁ ⇛⋆ u₂ → t₁ · u₁ ⇛⋆ t₂ · u₂
_·-cong_ {t₁ = t₁} {t₂} {u₁} {u₂} t₁⇛⋆t₂ u₁⇛⋆u₂ = begin
  t₁ · u₁
    ⇛⋆⟨ gmap _ (·-cong₂ t₁) u₁⇛⋆u₂ ⟩
  t₁ · u₂
    ⇛⋆⟨ gmap _ (·-cong₁ u₂) t₁⇛⋆t₂ ⟩
  t₂ · u₂
    ∎
  where
  ·-cong₁ : ∀ {Γ σ τ} {t₁ t₂ : Γ ⊢ σ ⟶ τ} u →
            t₁ ⇛ t₂ → t₁ · u ⇛ t₂ · u
  ·-cong₁ u (red C t₁⇛t₂) = red (C •· u) t₁⇛t₂

  ·-cong₂ : ∀ {Γ σ τ} {u₁ u₂} (t : Γ ⊢ σ ⟶ τ) →
            u₁ ⇛ u₂ → t · u₁ ⇛ t · u₂
  ·-cong₂ t (red C u₁⇛u₂) = red (t ·• C) u₁⇛u₂