module RecursiveTypes.Subtyping.Semantic.Coinductive where
open import Coinduction
open import Data.Nat using (ℕ; zero; suc)
open import Data.Fin using (Fin)
open import Data.Function
open import Data.Empty using (⊥-elim)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import RecursiveTypes.Syntax
open import RecursiveTypes.Substitution
open import RecursiveTypes.Semantics
infixr 10 _⟶_
infix 4 _≤∞_ _≤Coind_
infixr 2 _≤⟨_⟩_
infix 2 _∎
data _≤∞_ {n} : Tree n → Tree n → Set where
⊥ : ∀ {τ} → ⊥ ≤∞ τ
⊤ : ∀ {σ} → σ ≤∞ ⊤
var : ∀ {x} → var x ≤∞ var x
_⟶_ : ∀ {σ₁ σ₂ τ₁ τ₂}
(τ₁≤σ₁ : ∞ (♭ τ₁ ≤∞ ♭ σ₁)) (σ₂≤τ₂ : ∞ (♭ σ₂ ≤∞ ♭ τ₂)) →
σ₁ ⟶ σ₂ ≤∞ τ₁ ⟶ τ₂
_≤Coind_ : ∀ {n} → Ty n → Ty n → Set
σ ≤Coind τ = ⟦ σ ⟧ ≤∞ ⟦ τ ⟧
infix 4 _≤∞Prog_ _≤∞WHNF_
data _≤∞Prog_ {n} : Tree n → Tree n → Set where
⊥ : ∀ {τ} → ⊥ ≤∞Prog τ
⊤ : ∀ {σ} → σ ≤∞Prog ⊤
var : ∀ {x} → var x ≤∞Prog var x
_⟶_ : ∀ {σ₁ σ₂ τ₁ τ₂}
(τ₁≤σ₁ : ∞ (♭ τ₁ ≤∞Prog ♭ σ₁)) (σ₂≤τ₂ : ∞ (♭ σ₂ ≤∞Prog ♭ τ₂)) →
σ₁ ⟶ σ₂ ≤∞Prog τ₁ ⟶ τ₂
_∎ : ∀ τ → τ ≤∞Prog τ
_≤⟨_⟩_ : ∀ τ₁ {τ₂ τ₃}
(τ₁≤τ₂ : τ₁ ≤∞Prog τ₂) (τ₂≤τ₃ : τ₂ ≤∞Prog τ₃) → τ₁ ≤∞Prog τ₃
data _≤∞WHNF_ {n} : Tree n → Tree n → Set where
⊥ : ∀ {τ} → ⊥ ≤∞WHNF τ
⊤ : ∀ {σ} → σ ≤∞WHNF ⊤
var : ∀ {x} → var x ≤∞WHNF var x
_⟶_ : ∀ {σ₁ σ₂ τ₁ τ₂}
(τ₁≤σ₁ : ♭ τ₁ ≤∞Prog ♭ σ₁) (σ₂≤τ₂ : ♭ σ₂ ≤∞Prog ♭ τ₂) →
σ₁ ⟶ σ₂ ≤∞WHNF τ₁ ⟶ τ₂
whnf : ∀ {n} {σ τ : Tree n} → σ ≤∞Prog τ → σ ≤∞WHNF τ
whnf ⊥ = ⊥
whnf ⊤ = ⊤
whnf var = var
whnf (τ₁≤σ₁ ⟶ σ₂≤τ₂) = ♭ τ₁≤σ₁ ⟶ ♭ σ₂≤τ₂
whnf (⊥ ∎) = ⊥
whnf (⊤ ∎) = ⊤
whnf (var x ∎) = var
whnf (σ ⟶ τ ∎) = (♭ σ ∎) ⟶ (♭ τ ∎)
whnf (σ ≤⟨ τ₁≤τ₂ ⟩ τ₂≤τ₃) with whnf τ₁≤τ₂ | whnf τ₂≤τ₃
whnf (._ ≤⟨ τ₁≤τ₂ ⟩ τ₂≤τ₃) | ⊥ | _ = ⊥
whnf (_ ≤⟨ τ₁≤τ₂ ⟩ τ₂≤τ₃) | _ | ⊤ = ⊤
whnf (._ ≤⟨ τ₁≤τ₂ ⟩ τ₂≤τ₃) | var | var = var
whnf (._ ≤⟨ τ₁≤τ₂ ⟩ τ₂≤τ₃) | τ₁≤σ₁ ⟶ σ₂≤τ₂ | χ₁≤τ₁ ⟶ τ₂≤χ₂ =
(_ ≤⟨ χ₁≤τ₁ ⟩ τ₁≤σ₁) ⟶ (_ ≤⟨ σ₂≤τ₂ ⟩ τ₂≤χ₂)
mutual
value : ∀ {n} {σ τ : Tree n} → σ ≤∞WHNF τ → σ ≤∞ τ
value ⊥ = ⊥
value ⊤ = ⊤
value var = var
value (τ₁≤σ₁ ⟶ σ₂≤τ₂) = ♯ ⟦ τ₁≤σ₁ ⟧≤∞ ⟶ ♯ ⟦ σ₂≤τ₂ ⟧≤∞
⟦_⟧≤∞ : ∀ {n} {σ τ : Tree n} → σ ≤∞Prog τ → σ ≤∞ τ
⟦ σ≤τ ⟧≤∞ = value (whnf σ≤τ)
prog : ∀ {n} {σ τ : Tree n} → σ ≤∞ τ → σ ≤∞Prog τ
prog ⊥ = ⊥
prog ⊤ = ⊤
prog var = var
prog (τ₁≤σ₁ ⟶ σ₂≤τ₂) = ♯ prog (♭ τ₁≤σ₁) ⟶ ♯ prog (♭ σ₂≤τ₂)
trans : ∀ {n} {τ₁ τ₂ τ₃ : Tree n} →
τ₁ ≤∞ τ₂ → τ₂ ≤∞ τ₃ → τ₁ ≤∞ τ₃
trans {τ₁ = τ₁} {τ₂} {τ₃} τ₁≤τ₂ τ₂≤τ₃ =
⟦ τ₁ ≤⟨ prog τ₁≤τ₂ ⟩
τ₂ ≤⟨ prog τ₂≤τ₃ ⟩
τ₃ ∎ ⟧≤∞
unfold : ∀ {n} {τ₁ τ₂ : Ty (suc n)} →
μ τ₁ ⟶ τ₂ ≤Coind unfold[μ τ₁ ⟶ τ₂ ]
unfold = ♯ ⟦ _ ∎ ⟧≤∞ ⟶ ♯ ⟦ _ ∎ ⟧≤∞
fold : ∀ {n} {τ₁ τ₂ : Ty (suc n)} →
unfold[μ τ₁ ⟶ τ₂ ] ≤Coind μ τ₁ ⟶ τ₂
fold = ♯ ⟦ _ ∎ ⟧≤∞ ⟶ ♯ ⟦ _ ∎ ⟧≤∞
var:≤∞⟶≡ : ∀ {n} {x y : Fin n} →
var x ≤∞ var y → var x ≡ var y
var:≤∞⟶≡ var = refl
left-proj : ∀ {n} {σ₁ σ₂ τ₁ τ₂ : ∞ (Tree n)} →
σ₁ ⟶ σ₂ ≤∞ τ₁ ⟶ τ₂ → ♭ τ₁ ≤∞ ♭ σ₁
left-proj (τ₁≤σ₁ ⟶ σ₂≤τ₂) = ♭ τ₁≤σ₁
right-proj : ∀ {n} {σ₁ σ₂ τ₁ τ₂ : ∞ (Tree n)} →
σ₁ ⟶ σ₂ ≤∞ τ₁ ⟶ τ₂ → ♭ σ₂ ≤∞ ♭ τ₂
right-proj (τ₁≤σ₁ ⟶ σ₂≤τ₂) = ♭ σ₂≤τ₂
drop-¬¬ : ∀ {n} (σ τ : Tree n) → ¬ ¬ σ ≤∞ τ → σ ≤∞ τ
drop-¬¬ ⊥ τ ¬≰ = ⊥
drop-¬¬ σ ⊤ ¬≰ = ⊤
drop-¬¬ (var x) (var y) ¬≰ with var x ≡? var y
drop-¬¬ (var x) (var .x) ¬≰ | yes refl = var
drop-¬¬ (var x) (var y) ¬≰ | no x≠y = ⊥-elim (¬≰ (x≠y ∘ var:≤∞⟶≡))
drop-¬¬ (σ₁ ⟶ σ₂) (τ₁ ⟶ τ₂) ¬≰ =
♯ drop-¬¬ (♭ τ₁) (♭ σ₁) (λ ≰ → ¬≰ (≰ ∘ left-proj)) ⟶
♯ drop-¬¬ (♭ σ₂) (♭ τ₂) (λ ≰ → ¬≰ (≰ ∘ right-proj))
drop-¬¬ ⊤ ⊥ ¬≰ = ⊥-elim (¬≰ (λ ()))
drop-¬¬ ⊤ (var x) ¬≰ = ⊥-elim (¬≰ (λ ()))
drop-¬¬ ⊤ (τ₁ ⟶ τ₂) ¬≰ = ⊥-elim (¬≰ (λ ()))
drop-¬¬ (var x) ⊥ ¬≰ = ⊥-elim (¬≰ (λ ()))
drop-¬¬ (var x) (τ₁ ⟶ τ₂) ¬≰ = ⊥-elim (¬≰ (λ ()))
drop-¬¬ (σ₁ ⟶ σ₂) ⊥ ¬≰ = ⊥-elim (¬≰ (λ ()))
drop-¬¬ (σ₁ ⟶ σ₂) (var x) ¬≰ = ⊥-elim (¬≰ (λ ()))