leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

Progress on proof that delay is preElgot

Browse source
This commit is contained in:
Leon Vatthauer 2023-12-14 14:40:38 +01:00
parent 17ecc55223
commit 7bd77a4f47
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 50 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

56
agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md
View file

@ -9,7 +9,7 @@ open import Data.Sum.Function.Setoid
open import Data.Sum.Relation.Binary.Pointwise open import Data.Sum.Relation.Binary.Pointwise
open import Function.Equality as SΠ renaming (id to idₛ) open import Function.Equality as SΠ renaming (id to idₛ)
open import Codata.Musical.Notation 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 import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_) renaming (sym to ≡-sym) 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 : A [ later (♯ iter {A} {Y} (g ._⟨$⟩_) (h ⟨$⟩ a)) ≈ later (♯ (iter {A} {Y} (g ._⟨$⟩_) c)) ]
help = later≈ (♯ iter-cong g (∼-sym Y helper)) 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 : Setoid ℓ ℓ} → Elgot-Algebra-on (delaySetoid A)
delay-algebras {A} = record 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 } { _# = λ {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} ; #-Fixpoint = λ {X} {f} → iter-fixpoint {A} {X} {f}
; #-Uniformity = λ {X} {Y} {f} {g} {h} → iter-uni {A} {X} {Y} {f} {g} {h} ; #-Uniformity = λ {X} {Y} {f} {g} {h} → iter-uni {A} {X} {Y} {f} {g} {h}
; #-Folding = {! !} ; #-Folding = λ {X} {Y} {f} {h} {x} {y} x∼y → iter-folding {A} {X} {Y} {f} {h} {x} {y} x∼y
; #-resp-≈ = {! !} ; #-resp-≈ = λ {X} {f} {g} → iter-resp-≈ {A} {X} f g
} }
where
iterr : ∀ {X : Setoid ℓ ℓ} → X ⟶ ((delaySetoid A) ⊎ₛ X) → X ⟶ (delaySetoid A) -- kleisli lifting (just for making the code cleaner)
iterr {X} f = record { _⟨$⟩_ = {! !} ; cong = {! !} } -- TODO
delayPreElgot : IsPreElgot delayMonad delayPreElgot : IsPreElgot delayMonad
delayPreElgot = record delayPreElgot = record