------------------------------------------------------------------------
-- The Agda standard library
--
-- Infinite merge operation for coinductive lists
------------------------------------------------------------------------

module Data.Colist.Infinite-merge where

open import Coinduction
open import Data.Colist as Colist hiding (_⋎_)
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product as Prod
open import Data.Sum
open import Function
open import Function.Equality using (_⟨$⟩_)
open import Function.Inverse as Inv using (_↔_; module Inverse)
import Function.Related as Related
open import Function.Related.TypeIsomorphisms
open import Induction.Nat
import Induction.WellFounded as WF
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Binary.Sum

-- Some code that is used to work around Agda's syntactic guardedness
-- checker.

private

  infixr 5 _∷_ _⋎_

  data ColistP {a} (A : Set a) : Set a where
    []  : ColistP A
    _∷_ : A   (ColistP A)  ColistP A
    _⋎_ : ColistP A  ColistP A  ColistP A

  data ColistW {a} (A : Set a) : Set a where
    []  : ColistW A
    _∷_ : A  ColistP A  ColistW A

  program :  {a} {A : Set a}  Colist A  ColistP A
  program []       = []
  program (x  xs) = x   program ( xs)

  mutual

    _⋎W_ :  {a} {A : Set a}  ColistW A  ColistP A  ColistW A
    []       ⋎W ys = whnf ys
    (x  xs) ⋎W ys = x  (ys  xs)

    whnf :  {a} {A : Set a}  ColistP A  ColistW A
    whnf []        = []
    whnf (x  xs)  = x   xs
    whnf (xs  ys) = whnf xs ⋎W ys

  mutual

    ⟦_⟧P :  {a} {A : Set a}  ColistP A  Colist A
     xs ⟧P =  whnf xs ⟧W

    ⟦_⟧W :  {a} {A : Set a}  ColistW A  Colist A
     [] ⟧W     = []
     x  xs ⟧W = x    xs ⟧P

  mutual

    ⋎-homP :  {a} {A : Set a} (xs : ColistP A) {ys} 
              xs  ys ⟧P   xs ⟧P Colist.⋎  ys ⟧P
    ⋎-homP xs = ⋎-homW (whnf xs) _

    ⋎-homW :  {a} {A : Set a} (xs : ColistW A) ys 
              xs ⋎W ys ⟧W   xs ⟧W Colist.⋎  ys ⟧P
    ⋎-homW (x  xs) ys = x   ⋎-homP ys
    ⋎-homW []       ys = begin  ys ⟧P 
      where open ≈-Reasoning

  ⟦program⟧P :  {a} {A : Set a} (xs : Colist A) 
                program xs ⟧P  xs
  ⟦program⟧P []       = []
  ⟦program⟧P (x  xs) = x   ⟦program⟧P ( xs)

  Any-⋎P :  {a p} {A : Set a} {P : A  Set p} xs {ys} 
           Any P  program xs  ys ⟧P  (Any P xs  Any P  ys ⟧P)
  Any-⋎P {P = P} xs {ys} =
    Any P  program xs  ys ⟧P                ↔⟨ Any-cong Inv.id (⋎-homP (program xs)) 
    Any P ( program xs ⟧P Colist.⋎  ys ⟧P)  ↔⟨ Any-⋎ _ 
    (Any P  program xs ⟧P  Any P  ys ⟧P)   ↔⟨ Any-cong Inv.id (⟦program⟧P _) ⊎-cong (_ ) 
    (Any P xs  Any P  ys ⟧P)                
    where open Related.EquationalReasoning

  index-Any-⋎P :
     {a p} {A : Set a} {P : A  Set p} xs {ys}
    (p : Any P  program xs  ys ⟧P) 
    index p ≥′ [ index , index ]′ (Inverse.to (Any-⋎P xs) ⟨$⟩ p)
  index-Any-⋎P xs p
    with       Any-resp      id  (⋎-homW (whnf (program xs)) _) p
       | index-Any-resp {f = id} (⋎-homW (whnf (program xs)) _) p
  index-Any-⋎P xs p | q | q≡p
    with Inverse.to (Any-⋎  program xs ⟧P) ⟨$⟩ q
       |       index-Any-⋎  program xs ⟧P      q
  index-Any-⋎P xs p | q | q≡p | inj₂ r | r≤q rewrite q≡p = r≤q
  index-Any-⋎P xs p | q | q≡p | inj₁ r | r≤q
    with       Any-resp      id  (⟦program⟧P xs) r
       | index-Any-resp {f = id} (⟦program⟧P xs) r
  index-Any-⋎P xs p | q | q≡p | inj₁ r | r≤q | s | s≡r
    rewrite s≡r | q≡p = r≤q

-- Infinite variant of _⋎_.

private

  merge′ :  {a} {A : Set a}  Colist (A × Colist A)  ColistP A
  merge′ []               = []
  merge′ ((x , xs)  xss) = x   (program xs  merge′ ( xss))

merge :  {a} {A : Set a}  Colist (A × Colist A)  Colist A
merge xss =  merge′ xss ⟧P

-- Any lemma for merge.

Any-merge :
   {a p} {A : Set a} {P : A  Set p} xss 
  Any P (merge xss)  Any  { (x , xs)  P x  Any P xs }) xss
Any-merge {P = P} = λ xss  record
  { to         = P.→-to-⟶ (proj₁  to xss)
  ; from       = P.→-to-⟶ from
  ; inverse-of = record
    { left-inverse-of  = proj₂  to xss
    ; right-inverse-of = λ p  begin
        proj₁ (to xss (from p))  ≡⟨ from-injective _ _ (proj₂ (to xss (from p))) 
        p                        
    }
  }
  where
  open P.≡-Reasoning

  -- The from function.

  Q = λ { (x , xs)  P x  Any P xs }

  from :  {xss}  Any Q xss  Any P (merge xss)
  from (here (inj₁ p))        = here p
  from (here (inj₂ p))        = there (Inverse.from (Any-⋎P _)  ⟨$⟩ inj₁ p)
  from (there {x = _ , xs} p) = there (Inverse.from (Any-⋎P xs) ⟨$⟩ inj₂ (from p))

  -- Some lemmas.

  drop-there :
     {a p} {A : Set a} {P : A  Set p} {x xs} {p q : Any P _} 
    _≡_ {A = Any P (x  xs)} (there p) (there q)  p  q
  drop-there P.refl = P.refl

  drop-inj₁ :  {a b} {A : Set a} {B : Set b} {x y} 
              _≡_ {A = A  B} (inj₁ x) (inj₁ y)  x  y
  drop-inj₁ P.refl = P.refl

  drop-inj₂ :  {a b} {A : Set a} {B : Set b} {x y} 
              _≡_ {A = A  B} (inj₂ x) (inj₂ y)  x  y
  drop-inj₂ P.refl = P.refl

  -- The from function is injective.

  from-injective :  {xss} (p₁ p₂ : Any Q xss) 
                   from p₁  from p₂  p₁  p₂
  from-injective (here (inj₁ p))  (here (inj₁ .p)) P.refl = P.refl
  from-injective (here (inj₁ _))  (here (inj₂ _))  ()
  from-injective (here (inj₂ _))  (here (inj₁ _))  ()
  from-injective (here (inj₂ p₁)) (here (inj₂ p₂)) eq     =
    P.cong (here  inj₂) $
    drop-inj₁ $
    Inverse.injective (Inv.sym (Any-⋎P _)) {x = inj₁ p₁} {y = inj₁ p₂} $
    drop-there eq
  from-injective (here (inj₁ _))  (there _)  ()
  from-injective (here (inj₂ p₁)) (there p₂) eq
    with Inverse.injective (Inv.sym (Any-⋎P _))
                           {x = inj₁ p₁} {y = inj₂ (from p₂)}
                           (drop-there eq)
  ... | ()
  from-injective (there _)  (here (inj₁ _))  ()
  from-injective (there p₁) (here (inj₂ p₂)) eq
    with Inverse.injective (Inv.sym (Any-⋎P _))
                           {x = inj₂ (from p₁)} {y = inj₁ p₂}
                           (drop-there eq)
  ... | ()
  from-injective (there {x = _ , xs} p₁) (there p₂) eq =
    P.cong there $
    from-injective p₁ p₂ $
    drop-inj₂ $
    Inverse.injective (Inv.sym (Any-⋎P xs))
                      {x = inj₂ (from p₁)} {y = inj₂ (from p₂)} $
    drop-there eq

  -- The to function (defined as a right inverse of from).

  Input =  λ xss  Any P (merge xss)

  Pred : Input  Set _
  Pred (xss , p) =  λ (q : Any Q xss)  from q  p

  to :  xss p  Pred (xss , p)
  to = λ xss p 
    WF.All.wfRec (WF.Inverse-image.well-founded size <-well-founded) _
                 Pred step (xss , p)
    where
    size : Input  
    size (_ , p) = index p

    step :  p  WF.WfRec (_<′_ on size) Pred p  Pred p
    step ([]             , ())      rec
    step ((x , xs)  xss , here  p) rec = here (inj₁ p) , P.refl
    step ((x , xs)  xss , there p) rec
      with Inverse.to (Any-⋎P xs) ⟨$⟩ p
         | Inverse.left-inverse-of (Any-⋎P xs) p
         | index-Any-⋎P xs p
    step ((x , xs)  xss , there .(Inverse.from (Any-⋎P xs) ⟨$⟩ inj₁ q)) rec | inj₁ q | P.refl | _   = here (inj₂ q) , P.refl
    step ((x , xs)  xss , there .(Inverse.from (Any-⋎P xs) ⟨$⟩ inj₂ q)) rec | inj₂ q | P.refl | q≤p =
      Prod.map there
               (P.cong (there  _⟨$⟩_ (Inverse.from (Any-⋎P xs))  inj₂))
               (rec ( xss , q) (s≤′s q≤p))

-- Every member of xss is a member of merge xss, and vice versa (with
-- equal multiplicities).

∈-merge :  {a} {A : Set a} {y : A} xss 
          y  merge xss  ∃₂ λ x xs  (x , xs)  xss × (y  x  y  xs)
∈-merge {y = y} xss =
  y  merge xss                                           ↔⟨ Any-merge _ 
  Any  { (x , xs)  y  x  y  xs }) xss               ↔⟨ Any-∈ 
  ( λ { (x , xs)  (x , xs)  xss × (y  x  y  xs) })  ↔⟨ Σ-assoc 
  (∃₂ λ x xs  (x , xs)  xss × (y  x  y  xs))         
  where open Related.EquationalReasoning