--------------------------------------------------------------------------------
-- This is part of Agda Inference Systems 

{-# OPTIONS --guardedness #-}

open import Agda.Builtin.Equality
open import Data.Product
open import Data.Sum
open import Level
open import Relation.Unary using (_βŠ†_)

module is-lib.InfSys.FlexCoinduction {𝓁} where

  private
    variable
      U : Set 𝓁
  
  open import is-lib.InfSys.Base {𝓁}
  open import is-lib.InfSys.Induction {𝓁}
  open import is-lib.InfSys.Coinduction {𝓁}
  open MetaRule
  open IS

  {- Generalized inference systems -}

  FCoInd⟦_,_⟧ : βˆ€{𝓁c 𝓁p 𝓁n 𝓁n'} β†’ (I : IS {𝓁c} {𝓁p} {𝓁n} U) β†’ (C : IS {𝓁c} {𝓁p} {𝓁n'} U) β†’ U β†’ Set _
  FCoInd⟦ I , C ⟧ = CoInd⟦ I βŠ“ Ind⟦ I βˆͺ C ⟧ ⟧

  {- Bounded Coinduction Principle -}

  bdc-lem : βˆ€{𝓁c 𝓁p 𝓁n 𝓁' 𝓁''} 
      β†’ (I : IS {𝓁c} {𝓁p} {𝓁n} U)
      β†’ (S : U β†’ Set 𝓁') 
      β†’ (Q : U β†’ Set 𝓁'')
      β†’ S βŠ† Q
      β†’ S βŠ† ISF[ I ] S
      β†’ S βŠ† ISF[ I βŠ“ Q ] S
  bdc-lem _ _ _ bd cn Su with cn Su
  ... | rn , c , refl , pr = rn , (c , bd Su) , refl , pr

  bounded-coind[_,_] : βˆ€{𝓁c 𝓁p 𝓁n 𝓁n' 𝓁'} 
      β†’ (I : IS {𝓁c} {𝓁p} {𝓁n} U) 
      β†’ (C : IS {𝓁c} {𝓁p} {𝓁n'} U)
      β†’ (S : U β†’ Set 𝓁')                   
      β†’ S βŠ† Ind⟦ I βˆͺ C ⟧      -- S is bounded w.r.t. I βˆͺ C
      β†’ S βŠ† ISF[ I ] S        -- S is consistent w.r.t. I
      β†’ S βŠ† FCoInd⟦ I , C ⟧
  bounded-coind[ I , C ] S bd cn Su = coind[ I βŠ“ Ind⟦ I βˆͺ C ⟧ ] S (bdc-lem I S Ind⟦ I βˆͺ C ⟧ bd cn) Su

  {- Get Ind from FCoInd -}

  fcoind-to-ind : βˆ€{𝓁c 𝓁p 𝓁n 𝓁n'}
      {is : IS {𝓁c} {𝓁p} {𝓁n} U}{cois : IS {𝓁c} {𝓁p} {𝓁n'} U} 
      β†’ FCoInd⟦ is , cois ⟧ βŠ† Ind⟦ is βˆͺ cois ⟧
  fcoind-to-ind co with CoInd⟦_⟧.unfold co
  ... | _ , (_ , sd) , refl , _ = sd

  {- Apply Rule -}

  apply-fcoind : βˆ€{𝓁c 𝓁p 𝓁n 𝓁n'}
      {is : IS {𝓁c} {𝓁p} {𝓁n} U}{cois : IS {𝓁c} {𝓁p} {𝓁n'} U}
      β†’ (rn : is .Names) β†’ RClosed (is .rules rn) FCoInd⟦ is , cois ⟧
  apply-fcoind rn c pr = apply-coind rn (c , apply-ind (inj₁ rn) c Ξ» i β†’ fcoind-to-ind (pr i)) pr

  {- Postfix - Prefix -}
  
  fcoind-postfix : βˆ€{𝓁c 𝓁p 𝓁n 𝓁n'}
      {is : IS {𝓁c} {𝓁p} {𝓁n} U}{cois : IS {𝓁c} {𝓁p} {𝓁n'} U}
      β†’ FCoInd⟦ is , cois ⟧ βŠ† ISF[ is ] FCoInd⟦ is , cois ⟧
  fcoind-postfix FCoInd with FCoInd .CoInd⟦_⟧.unfold
  ... | rn , (c , _) , refl , pr = rn , c , refl , pr

  fcoind-prefix : βˆ€{𝓁c 𝓁p 𝓁n 𝓁n'}
      {is : IS {𝓁c} {𝓁p} {𝓁n} U}{cois : IS {𝓁c} {𝓁p} {𝓁n'} U}
      β†’ ISF[ is ] FCoInd⟦ is , cois ⟧ βŠ† FCoInd⟦ is , cois ⟧
  fcoind-prefix (rn , c , refl , pr) = apply-fcoind rn c pr