------------------------------------------------------------------------ -- The Agda standard library -- -- Infinite merge operation for coinductive lists ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --guardedness #-} module Codata.Musical.Colist.Infinite-merge where open import Codata.Musical.Notation open import Codata.Musical.Colist as Colist hiding (_⋎_) open import Data.Nat.Base open import Data.Nat.Induction using (<′-wellFounded) open import Data.Nat.Properties open import Data.Product as Prod open import Data.Sum.Base open import Data.Sum.Properties open import Data.Sum.Function.Propositional using (_⊎-cong_) open import Function.Base open import Function.Equality using (_⟨$⟩_) open import Function.Inverse as Inv using (_↔_; Inverse; inverse) import Function.Related as Related open import Function.Related.TypeIsomorphisms import Induction.WellFounded as WF open import Relation.Binary.PropositionalEquality as P using (_≡_) import Relation.Binary.Construct.On as On ------------------------------------------------------------------------ -- 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. module _ {a p} {A : Set a} {P : A → Set p} where Any-merge : ∀ xss → Any P (merge xss) ↔ Any (λ { (x , xs) → P x ⊎ Any P xs }) xss Any-merge xss = inverse (proj₁ ∘ to xss) from (proj₂ ∘ to xss) to∘from 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)) -- 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₂ p₁)) (here (inj₂ p₂)) eq = P.cong (here ∘ inj₂) $ inj₁-injective $ Inverse.injective (Inv.sym (Any-⋎P _)) {x = inj₁ p₁} {y = inj₁ p₂} $ there-injective eq from-injective (here (inj₂ p₁)) (there p₂) eq with Inverse.injective (Inv.sym (Any-⋎P _)) {x = inj₁ p₁} {y = inj₂ (from p₂)} (there-injective eq) ... | () from-injective (there p₁) (here (inj₂ p₂)) eq with Inverse.injective (Inv.sym (Any-⋎P _)) {x = inj₂ (from p₁)} {y = inj₁ p₂} (there-injective eq) ... | () from-injective (there {x = _ , xs} p₁) (there p₂) eq = P.cong there $ from-injective p₁ p₂ $ inj₂-injective $ Inverse.injective (Inv.sym (Any-⋎P xs)) {x = inj₂ (from p₁)} {y = inj₂ (from p₂)} $ there-injective 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 (On.wellFounded size <′-wellFounded) _ 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 ... | inj₁ q | P.refl | _ = here (inj₂ q) , P.refl ... | 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)) to∘from = λ p → from-injective _ _ (proj₂ (to xss (from 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