------------------------------------------------------------------------
-- Coinductive definition of subtyping
------------------------------------------------------------------------

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  _∎

------------------------------------------------------------------------
-- Definition

-- The obvious definition of subtyping for trees.

data _≤∞_ {n} : Tree n  Tree n  Set where
     :  {τ}   ≤∞ τ
     :  {σ}  σ ≤∞ 
  var :  {x}  var x ≤∞ var x
  _⟶_ :  {σ₁ σ₂ τ₁ τ₂}
        (τ₁≤σ₁ :  ( τ₁ ≤∞  σ₁)) (σ₂≤τ₂ :  ( σ₂ ≤∞  τ₂)) 
        σ₁  σ₂ ≤∞ τ₁  τ₂

-- Subtyping for recursive types is defined in terms of subtyping for
-- trees.

_≤Coind_ :  {n}  Ty n  Ty n  Set
σ ≤Coind τ =  σ  ≤∞  τ 

------------------------------------------------------------------------
-- A trick used to ensure guardedness of expressions using
-- transitivity

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 τ₁  τ₂
  -- Reflexivity.
  _∎     :  τ  τ ≤∞Prog τ
  -- Transitivity.
  _≤⟨_⟩_ :  τ₁ {τ₂ τ₃}
           (τ₁≤τ₂ : τ₁ ≤∞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 ( σ₂≤τ₂)

------------------------------------------------------------------------
-- Some lemmas

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 (τ₁≤σ₁  σ₂≤τ₂) =  σ₂≤τ₂

------------------------------------------------------------------------
-- Double-negation does not affect _≤∞_

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 (¬≰  ()))