module RecursiveTypes.Subtyping.Axiomatic.Coinductive where
open import Data.Nat using (ℕ; zero; suc)
open import Coinduction
open import RecursiveTypes.Syntax
open import RecursiveTypes.Substitution
open import RecursiveTypes.Semantics
open import RecursiveTypes.Subtyping.Semantic.Coinductive as Sem
using (_≤∞Prog_; _≤Coind_; ⟦_⟧≤∞; ⊥; ⊤; var; _⟶_; _∎; _≤⟨_⟩_)
infixr 10 _⟶_
infix 4 _≤_
infixr 2 _≤⟨_⟩_
infix 2 _∎
data _≤_ {n} : Ty n → Ty n → Set where
⊥ : ∀ {τ} → ⊥ ≤ τ
⊤ : ∀ {σ} → σ ≤ ⊤
_⟶_ : ∀ {σ₁ σ₂ τ₁ τ₂} (τ₁≤σ₁ : ∞ (τ₁ ≤ σ₁)) (σ₂≤τ₂ : ∞ (σ₂ ≤ τ₂)) →
σ₁ ⟶ σ₂ ≤ τ₁ ⟶ τ₂
unfold : ∀ {τ₁ τ₂} → μ τ₁ ⟶ τ₂ ≤ unfold[μ τ₁ ⟶ τ₂ ]
fold : ∀ {τ₁ τ₂} → unfold[μ τ₁ ⟶ τ₂ ] ≤ μ τ₁ ⟶ τ₂
_∎ : ∀ τ → τ ≤ τ
_≤⟨_⟩_ : ∀ τ₁ {τ₂ τ₃} (τ₁≤τ₂ : τ₁ ≤ τ₂) (τ₂≤τ₃ : τ₂ ≤ τ₃) → τ₁ ≤ τ₃
sound′ : ∀ {n} {σ τ : Ty n} → σ ≤ τ → ⟦ σ ⟧ ≤∞Prog ⟦ τ ⟧
sound′ ⊥ = ⊥
sound′ ⊤ = ⊤
sound′ (τ₁≤σ₁ ⟶ σ₂≤τ₂) = ♯ sound′ (♭ τ₁≤σ₁) ⟶ ♯ sound′ (♭ σ₂≤τ₂)
sound′ unfold = Sem.prog Sem.unfold
sound′ fold = Sem.prog Sem.fold
sound′ (τ ∎) = _ ∎
sound′ (τ₁ ≤⟨ τ₁≤τ₂ ⟩ τ₂≤τ₃) = _ ≤⟨ sound′ τ₁≤τ₂ ⟩ sound′ τ₂≤τ₃
sound : ∀ {n} {σ τ : Ty n} → σ ≤ τ → σ ≤Coind τ
sound σ≤τ = ⟦ sound′ σ≤τ ⟧≤∞
complete : ∀ {n} (σ τ : Ty n) → σ ≤Coind τ → σ ≤ τ
complete ⊥ _ _ = ⊥
complete _ ⊤ _ = ⊤
complete ⊤ ⊥ ()
complete ⊤ (var x) ()
complete ⊤ (σ ⟶ τ) ()
complete ⊤ (μ σ ⟶ τ) ()
complete (var x) ⊥ ()
complete (var x) (var .x) var = var x ∎
complete (var x) (σ ⟶ τ) ()
complete (var x) (μ σ ⟶ τ) ()
complete (σ₁ ⟶ σ₂) ⊥ ()
complete (σ₁ ⟶ σ₂) (var x) ()
complete (σ₁ ⟶ σ₂) (τ₁ ⟶ τ₂) (τ₁≤σ₁ ⟶ σ₂≤τ₂) =
♯ complete τ₁ σ₁ (♭ τ₁≤σ₁) ⟶ ♯ complete σ₂ τ₂ (♭ σ₂≤τ₂)
complete (σ₁ ⟶ σ₂) (μ τ₁ ⟶ τ₂) (τ₁≤σ₁ ⟶ σ₂≤τ₂) =
σ₁ ⟶ σ₂ ≤⟨ ♯ complete _ _ (♭ τ₁≤σ₁) ⟶
♯ complete _ _ (♭ σ₂≤τ₂) ⟩
unfold[μ τ₁ ⟶ τ₂ ] ≤⟨ fold ⟩
μ τ₁ ⟶ τ₂ ∎
complete (μ σ₁ ⟶ σ₂) ⊥ ()
complete (μ σ₁ ⟶ σ₂) (var x) ()
complete (μ σ₁ ⟶ σ₂) (τ₁ ⟶ τ₂) (τ₁≤σ₁ ⟶ σ₂≤τ₂) =
μ σ₁ ⟶ σ₂ ≤⟨ unfold ⟩
unfold[μ σ₁ ⟶ σ₂ ] ≤⟨ ♯ complete _ _ (♭ τ₁≤σ₁) ⟶
♯ complete _ _ (♭ σ₂≤τ₂) ⟩
(τ₁ ⟶ τ₂) ∎
complete (μ σ₁ ⟶ σ₂) (μ τ₁ ⟶ τ₂) (τ₁≤σ₁ ⟶ σ₂≤τ₂) =
μ σ₁ ⟶ σ₂ ≤⟨ unfold ⟩
unfold[μ σ₁ ⟶ σ₂ ] ≤⟨ ♯ complete _ _ (♭ τ₁≤σ₁) ⟶
♯ complete _ _ (♭ σ₂≤τ₂) ⟩
unfold[μ τ₁ ⟶ τ₂ ] ≤⟨ fold ⟩
μ τ₁ ⟶ τ₂ ∎