From 7bd77a4f477f348868d837cacc605dfbf35d6327 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Thu, 14 Dec 2023 14:40:38 +0100 Subject: [PATCH] Progress on proof that delay is preElgot --- .../Instance/Setoids/Delay/PreElgot.lagda.md | 56 +++++++++++++++++-- 1 file changed, 50 insertions(+), 6 deletions(-) diff --git a/agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md b/agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md index 963d347..e73b753 100644 --- a/agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md +++ b/agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md @@ -9,7 +9,7 @@ open import Data.Sum.Function.Setoid open import Data.Sum.Relation.Binary.Pointwise open import Function.Equality as SΠ renaming (id to idₛ) open import Codata.Musical.Notation -open import Function using () renaming (_∘_ to _∘f_) +open import Function using (_∘′_) renaming (_∘_ to _∘f_) import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_) renaming (sym to ≡-sym) ``` @@ -105,17 +105,61 @@ module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where help : A [ later (♯ iter {A} {Y} (g ._⟨$⟩_) (h ⟨$⟩ a)) ≈ later (♯ (iter {A} {Y} (g ._⟨$⟩_) c)) ] help = later≈ (♯ iter-cong g (∼-sym Y helper)) + + -- TODO maybe I can improve inj₁-helper etc. to handle this case as well + iter-resp-≈ : ∀ {A X : Setoid ℓ ℓ} (f g : X ⟶ (delaySetoid A ⊎ₛ X)) → f ≋ g → ∀ {x y : Setoid.Carrier X} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ iter {A} {X} (g ._⟨$⟩_) y ] + iter-resp-≈ {A} {X} f g f≋g {x} {y} x∼y with (f ._⟨$⟩_) x in eqx | (g ._⟨$⟩_) y in eqy + ... | inj₁ a | inj₁ b = drop-inj₁ helper + where + helper : (delaySetoid A ⊎ₛ X) [ inj₁ a ∼ inj₁ b ] + helper rewrite (≡-sym eqy) | (≡-sym eqx) = f≋g x∼y + ... | inj₁ a | inj₂ b = conflict (delaySetoid A) X helper + where + helper : (delaySetoid A ⊎ₛ X) [ inj₁ a ∼ inj₂ b ] + helper rewrite (≡-sym eqy) | (≡-sym eqx) = f≋g x∼y + ... | inj₂ a | inj₁ b = conflict (delaySetoid A) X (∼-sym (delaySetoid A ⊎ₛ X) helper) + where + helper : (delaySetoid A ⊎ₛ X) [ inj₂ a ∼ inj₁ b ] + helper rewrite (≡-sym eqy) | (≡-sym eqx) = f≋g x∼y + ... | inj₂ a | inj₂ b = later≈ (♯ iter-resp-≈ {A} {X} f g f≋g (drop-inj₂ helper)) + where + helper : (delaySetoid A ⊎ₛ X) [ inj₂ a ∼ inj₂ b ] + helper rewrite (≡-sym eqy) | (≡-sym eqx) = f≋g x∼y + + iter-folding : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (delaySetoid A ⊎ₛ X)} {h : Y ⟶ X ⊎ₛ Y} {x y : Setoid.Carrier (X ⊎ₛ Y)} → (X ⊎ₛ Y) [ x ∼ y ] → A [ iter {A} {X ⊎ₛ Y} [ inj₁ ∘f iter {A} {X} (f ._⟨$⟩_) , inj₂ ∘f (h ._⟨$⟩_) ] x ≈ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘f (f ._⟨$⟩_) , (inj₂ ∘f (h ._⟨$⟩_)) ] y ] + iter-folding {A} {X} {Y} {f} {h} {inj₁ x} {inj₁ y} ix∼iy with f ⟨$⟩ x in eqx | f ⟨$⟩ y in eqy + ... | inj₁ a | inj₁ b = inj₁-helper f (drop-inj₁ ix∼iy) eqx eqy + ... | inj₁ a | inj₂ b = absurd-helper f (drop-inj₁ ix∼iy) eqx eqy + ... | inj₂ a | inj₁ b = absurd-helper f (∼-sym X (drop-inj₁ ix∼iy)) eqy eqx + ... | inj₂ a | inj₂ b = later≈ (♯ ≈-trans (iter-cong f (inj₂-helper f (drop-inj₁ ix∼iy) eqx eqy)) (helper b)) + where + helper : ∀ (b : Setoid.Carrier X) → A [ iter {A} {X} (f ._⟨$⟩_) b ≈ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ (f ._⟨$⟩_) , inj₂ ∘′ (h ._⟨$⟩_) ] (inj₁ b) ] + helper b with f ⟨$⟩ b in eqb + ... | inj₁ c = ∼-refl (delaySetoid A) + ... | inj₂ c = later≈ (♯ helper c) + iter-folding {A} {X} {Y} {f} {h} {inj₂ x} {inj₂ y} ix∼iy with h ⟨$⟩ x in eqx | h ⟨$⟩ y in eqy + ... | inj₁ a | inj₁ b = later≈ (♯ iter-folding {A} {X} {Y} {f} {h} {inj₁ a} {inj₁ b} helper) + where + helper : (X ⊎ₛ Y) [ inj₁ a ∼ inj₁ b ] + helper rewrite (≡-sym eqx) | (≡-sym eqy) = cong h (drop-inj₂ ix∼iy) + ... | inj₁ a | inj₂ b = absurd-helper h (drop-inj₂ ix∼iy) eqx eqy + ... | inj₂ a | inj₁ b = absurd-helper h (∼-sym Y (drop-inj₂ ix∼iy)) eqy eqx + ... | inj₂ a | inj₂ b = later≈ (♯ iter-folding {A} {X} {Y} {f} {h} {inj₂ a} {inj₂ b} helper) + where + helper : (X ⊎ₛ Y) [ inj₂ a ∼ inj₂ b ] + helper rewrite (≡-sym eqx) | (≡-sym eqy) = cong h (drop-inj₂ ix∼iy) + delay-algebras : ∀ {A : Setoid ℓ ℓ} → Elgot-Algebra-on (delaySetoid A) delay-algebras {A} = record { _# = λ {X} f → record { _⟨$⟩_ = iter {A} {X} (f ._⟨$⟩_) ; cong = λ {x} {y} x∼y → iter-cong {A} {X} f {x} {y} x∼y } ; #-Fixpoint = λ {X} {f} → iter-fixpoint {A} {X} {f} ; #-Uniformity = λ {X} {Y} {f} {g} {h} → iter-uni {A} {X} {Y} {f} {g} {h} - ; #-Folding = {! !} - ; #-resp-≈ = {! !} + ; #-Folding = λ {X} {Y} {f} {h} {x} {y} x∼y → iter-folding {A} {X} {Y} {f} {h} {x} {y} x∼y + ; #-resp-≈ = λ {X} {f} {g} → iter-resp-≈ {A} {X} f g } - where - iterr : ∀ {X : Setoid ℓ ℓ} → X ⟶ ((delaySetoid A) ⊎ₛ X) → X ⟶ (delaySetoid A) - iterr {X} f = record { _⟨$⟩_ = {! !} ; cong = {! !} } + + -- kleisli lifting (just for making the code cleaner) + -- TODO delayPreElgot : IsPreElgot delayMonad delayPreElgot = record