-- An implementation of "A Unifying Approach to Recursive and
-- Co-recursive Definitions" by Pietro Di Gianantonio and Marino
-- Miculan

-- See the paper for more explanations.

module Contractive where

open import Relation.Unary
open import Relation.Binary
import Relation.Binary.EqReasoning as EqR
import Induction.WellFounded as WF
open import Data.Function

-- Well-founded orders.

record IsWellFoundedOrder {A} (_<_ : Rel A) : Set where
    trans         : Transitive _<_
    isWellFounded :  a  WF.Acc _<_ a

-- Ordered families of equivalences.

record OFE : Set1 where
    carrier            : Set
    domain             : Set
    _<_                : Rel carrier
    isWellFoundedOrder : IsWellFoundedOrder _<_
    Eq                 : carrier  Rel domain
    isEquivalence      :  a  IsEquivalence (Eq a)

  open IsWellFoundedOrder isWellFoundedOrder public
  open WF _<_ public using (WfRec)
  open WF.All _<_ isWellFounded public

  setoid : carrier  Setoid
  setoid a = record { carrier       = domain
                    ; _≈_           = Eq a
                    ; isEquivalence = isEquivalence a

  module EqReasoning {a : carrier} where
    open EqR    (setoid a) public
    open Setoid (setoid a) public using (refl; sym)

  -- The set of predecessors of a.

   : carrier  Pred carrier
   a = λ a'  a' < a

  -- The intersection of all the equivalences.

  _≅_ : Rel domain
  x  y =  a  Eq a x y

  Family : Pred carrier  Set
  Family I =  x  x  I  domain

  lift :  {I}  (carrier  domain)  Family I
  lift P = λ x _  P x

  IsCoherent :  {I}  Family I  Set
  IsCoherent {I} fam =  {a' a}
    (a'∈I : a'  I) (a∈I : a  I)  a' < a 
    Eq a' (fam a' a'∈I) (fam a a∈I)

  IsLimit :  {I}  Family I  domain  Set
  IsLimit {I} fam y =  {a'}
    (a'∈I : a'  I)  Eq a' (fam a' a'∈I) y

  IsContractive : (domain  domain)  Set
  IsContractive F =  {x y a} 
    (∀ {a'}  a' < a  Eq a' x y)  Eq a (F x) (F y)

-- Complete ordered families of equivalences.

record COFE : Set1 where
    ofe : OFE

  open OFE ofe

    limU     : (carrier  domain)  domain
    isLimitU :  {fam} 
               IsCoherent {U} (lift fam) 
               IsLimit {U} (lift fam) (limU fam)

    lim↓     :  a  Family ( a)  domain
    isLimit↓ :  a {fam : Family ( a)} 
               IsCoherent fam  IsLimit fam (lim↓ a fam)

  open OFE ofe public

-- Contractive functions over complete ordered families have
-- fixpoints.

record ContractiveFun (cofe : COFE) : Set where
  open COFE cofe
    F             : domain  domain
    isContractive : IsContractive F

  open EqReasoning

  -- The fixpoint is the limit of the following family.

  fam : carrier  domain
  fam = wfRec (const₁ domain)  a rec  F (lim↓ a rec))

  fixpoint : domain
  fixpoint = limU fam

  -- I am not sure if this lemma can be proved without assuming some
  -- kind of proof irrelevance and/or extensionality. It is not
  -- central to the ideas developed here, though, so I leave it as a
  -- postulate.

  postulate unfold :  a  fam a  F (lim↓ a (lift fam))

  -- The family is coherent in several ways.

  fam-isCoherent-↓ :  a  IsCoherent { a} (lift fam)
  fam-isCoherent-↓ = wfRec P step
    P : Pred carrier
    P a = IsCoherent { a} (lift fam)

    step :  a  WfRec P a  P a
    step a rec {c} {b} c<a b<a c<b = begin
      fam c                  ≈⟨ unfold c c 
      F (lim↓ c (lift fam))  ≈⟨ isContractive  {d} d<c  begin
         lim↓ c (lift fam)      ≈⟨ sym $ isLimit↓ c (rec c c<a) d<c 
         lift { a} fam d
              (trans d<c c<a)   ≈⟨ isLimit↓ b (rec b b<a) (trans d<c c<b) 
         lim↓ b (lift fam)      ) 
      F (lim↓ b (lift fam))  ≈⟨ sym $ unfold b c 
      fam b                  

  fam-isCoherent-U : IsCoherent {U} (lift fam)
  fam-isCoherent-U {a'} {a} _ _ = wfRec P step a a'
    P : Pred carrier
    P a =  a'  a' < a  Eq a' (fam a') (fam a)

    step :  a  WfRec P a  P a
    step a rec a' a'<a = begin
      fam a'                  ≈⟨ unfold a' a' 
      F (lim↓ a' (lift fam))  ≈⟨ isContractive  {b} b<a'  begin
         lim↓ a' (lift fam)      ≈⟨ sym $ isLimit↓ a' (fam-isCoherent-↓ a') b<a' 
         fam b                   ≈⟨ isLimit↓ a (fam-isCoherent-↓ a) (trans b<a' a'<a) 
         lim↓ a  (lift fam)      ) 
      F (lim↓ a  (lift fam))  ≈⟨ sym $ unfold a a' 
      fam a                   

  -- The fixpoint is a fixpoint.

  isFixpoint : fixpoint  F fixpoint
  isFixpoint a = begin
    fixpoint               ≈⟨ sym $ isLimitU fam-isCoherent-U _ 
    fam a                  ≈⟨ unfold a a 
    F (lim↓ a (lift fam))  ≈⟨ isContractive  {a'} a'<a  begin
       lim↓ a (lift fam)      ≈⟨ sym $ isLimit↓ a (fam-isCoherent-↓ a) a'<a 
       fam a'                 ≈⟨ isLimitU fam-isCoherent-U _ 
       limU fam               ) 
    F (limU fam)           ≈⟨ refl 
    F fixpoint             

  -- And it is unique.

  unique :  x  x  F x  x  fixpoint
  unique x isFix = wfRec P step
    P = λ a  Eq a x fixpoint

    step :  a  WfRec P a  P a
    step a rec = begin
      x           ≈⟨ isFix a 
      F x         ≈⟨ isContractive  {a'} a'<a  rec a' a'<a) 
      F fixpoint  ≈⟨ sym $ isFixpoint a