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