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

sync

Browse source
This commit is contained in:
Leon Vatthauer 2024-01-29 15:38:50 +01:00
parent f0923f1007
commit 2dc6420a35
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 36 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

42
agda/src/Monad/Instance/Setoids/K.lagda.md
View file

@ -72,6 +72,26 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
helper : [ Y ⊎ₛ X ][ inj₁ a ≡ inj₂ b ] helper : [ Y ⊎ₛ X ][ inj₁ a ≡ inj₂ b ]
helper rewrite (≣-sym fi₁) | (≣-sym fi₂) = cong f x≡y helper rewrite (≣-sym fi₁) | (≣-sym fi₂) = cong f x≡y
-- TODO remove the following two later
iter-cong∼' : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delayₛ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ∼ (iter {A} {X} < f > y) ]
iter-cong∼′' : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delayₛ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ∼′ (iter {A} {X} < f > y) ]
force∼ (iter-cong∼′' {A} {X} f {x} {y} x≡y) = iter-cong∼' f x≡y
iter-cong∼' {A} {X} f {x} {y} x≡y with < f > x in eqx | < f > y in eqy
... | inj₁ a | inj₁ b = {! inj₁-helper f x≡y eqx eqy !} -- inj₁-helper f x≡y eqx eqy
... | inj₁ a | inj₂ b = absurd-helper f x≡y eqx eqy
... | inj₂ a | inj₁ b = absurd-helper f (≡-sym X x≡y) eqy eqx
... | inj₂ a | inj₂ b = {! !} -- later∼ (iter-cong∼′' {A} {X} f (inj₂-helper f x≡y eqx eqy))
iter-cong∼ : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delayₛ∼ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ∼ (iter {A} {X} < f > y) ]
iter-cong∼′ : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delayₛ∼ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ∼′ (iter {A} {X} < f > y) ]
force∼ (iter-cong∼′ {A} {X} f {x} {y} x≡y) = iter-cong∼ f x≡y
iter-cong∼ {A} {X} f {x} {y} x≡y with < f > x in eqx | < f > y in eqy
... | inj₁ a | inj₁ b = inj₁-helper f x≡y eqx eqy
... | inj₁ a | inj₂ b = absurd-helper f x≡y eqx eqy
... | inj₂ a | inj₁ b = absurd-helper f (≡-sym X x≡y) eqy eqx
... | inj₂ a | inj₂ b = later∼ (iter-cong∼′ {A} {X} f (inj₂-helper f x≡y eqx eqy))
iter-cong : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delayₛ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ≈ (iter {A} {X} < f > y) ] iter-cong : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delayₛ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ≈ (iter {A} {X} < f > y) ]
iter-cong′ : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delayₛ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ≈′ (iter {A} {X} < f > y) ] iter-cong′ : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delayₛ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ≈′ (iter {A} {X} < f > y) ]
force≈ (iter-cong′ {A} {X} f {x} {y} x≡y) = iter-cong f x≡y force≈ (iter-cong′ {A} {X} f {x} {y} x≡y) = iter-cong f x≡y
@ -81,6 +101,9 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
... | inj₂ a | inj₁ b = absurd-helper f (≡-sym X x≡y) eqy eqx ... | inj₂ a | inj₁ b = absurd-helper f (≡-sym X x≡y) eqy eqx
... | inj₂ a | inj₂ b = later≈ (iter-cong′ {A} {X} f (inj₂-helper f x≡y eqx eqy)) ... | inj₂ a | inj₂ b = later≈ (iter-cong′ {A} {X} f (inj₂-helper f x≡y eqx eqy))
iterₛ∼ : ∀ {A X : Setoid ℓ ℓ} → (X ⟶ (Delayₛ∼ A ⊎ₛ X)) → X ⟶ Delayₛ∼ A
iterₛ∼ {A} {X} f = record { to = iter {A} {X} < f > ; cong = iter-cong∼ {A} {X} f }
iterₛ : ∀ {A X : Setoid ℓ ℓ} → (X ⟶ (Delayₛ A ⊎ₛ X)) → X ⟶ Delayₛ A iterₛ : ∀ {A X : Setoid ℓ ℓ} → (X ⟶ (Delayₛ A ⊎ₛ X)) → X ⟶ Delayₛ A
iterₛ {A} {X} f = record { to = iter {A} {X} < f > ; cong = iter-cong {A} {X} f } iterₛ {A} {X} f = record { to = iter {A} {X} < f > ; cong = iter-cong {A} {X} f }
@ -159,7 +182,7 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
delay-lift : ∀ {A : Setoid ℓ ℓ} {B : Elgot-Algebra} → A ⟶ ⟦ B ⟧ → Elgot-Algebra-Morphism (delay-algebras A) B delay-lift : ∀ {A : Setoid ℓ ℓ} {B : Elgot-Algebra} → A ⟶ ⟦ B ⟧ → Elgot-Algebra-Morphism (delay-algebras A) B
delay-lift {A} {B} f = record { h = delay-lift' ; preserves = λ {X} {g} {x} → {! !} } delay-lift {A} {B} f = record { h = delay-lift' ; preserves = λ {X} {g} {x} → ≡-trans ⟦ B ⟧ (preserves' {X} {g} {x}) (#-resp-≈ B (≡-refl (⟦ B ⟧ ⊎ₛ X))) }
where where
open Elgot-Algebra B using (_#) open Elgot-Algebra B using (_#)
-- (f + id) ∘ out -- (f + id) ∘ out
@ -179,7 +202,6 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
helper#∼-cong {x} {y} x∼y = cong (helper #) x∼y helper#∼-cong {x} {y} x∼y = cong (helper #) x∼y
helper#≈-cong : {x y : Delay ∣ A ∣} → (x≈y : [ A ][ x ≈ y ]) → [ ⟦ B ⟧ ][ helper # ⟨$⟩ x ≡ helper # ⟨$⟩ y ] helper#≈-cong : {x y : Delay ∣ A ∣} → (x≈y : [ A ][ x ≈ y ]) → [ ⟦ B ⟧ ][ helper # ⟨$⟩ x ≡ helper # ⟨$⟩ y ]
-- key special case -- key special case
helper#≈-cong' : {z : Delay (∣ A ∣ × ℕ)} → [ ⟦ B ⟧ ][ helper # ⟨$⟩ liftF proj₁ z ≡ helper # ⟨$⟩ μ {A} (liftF (ι {A}) z) ] helper#≈-cong' : {z : Delay (∣ A ∣ × ℕ)} → [ ⟦ B ⟧ ][ helper # ⟨$⟩ liftF proj₁ z ≡ helper # ⟨$⟩ μ {A} (liftF (ι {A}) z) ]
@ -288,11 +310,18 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
delay-lift' = record { to = < helper # > ; cong = helper#≈-cong } delay-lift' = record { to = < helper # > ; cong = helper#≈-cong }
preserves' : ∀ {X : Setoid ℓ ℓ} {g : X ⟶ (Delayₛ A ⊎ₛ X)} → ∀ {x} → [ ⟦ B ⟧ ][ (< helper # > (iter {A} {X} < g > x)) ≡ < ([ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g) # > x ] preserves' : ∀ {X : Setoid ℓ ℓ} {g : X ⟶ (Delayₛ A ⊎ₛ X)} → ∀ {x} → [ ⟦ B ⟧ ][ (delay-lift' ∘ (iterₛ {A} {X} g)) ⟨$⟩ x ≡ ([ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g) # ⟨$⟩ x ]
preserves' {X} {g} {x} = ≡-sym ⟦ B ⟧ (#-Uniformity B {! λ {x} → by-uni {x} !}) -- #-Uniformity B {! !} -- h would need iter-cong∼', which is not doable i think
preserves' {X} {g} {x} = ≡-sym ⟦ B ⟧ (#-Uniformity B {f = [ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g} {g = helper} {h = {! !}} {! !})--(≡-trans (⟦ B ⟧ ⊎ₛ Delayₛ A) by-uni trivial))
where where
by-uni : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ < [ inj₁ₛ ∘ delay-lift' , inj₂ₛ ∘ iterₛ {A} {X} g ]ₛ ∘ g > x ≡ (helper₁ ∘′ iter {A} {X} < g >) x ] by-uni : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ < [ inj₁ₛ , inj₂ₛ ∘ iterₛ {A} {X} g ]ₛ ∘ ([ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g) > x ≡ (< helper > ∘′ (iter {A} {X} < g >)) x ]
by-uni = {! !} by-uni {x} with g ⟨$⟩ x in eqa
... | inj₁ a = {! !}
-- ... | inj₁ (now a) = {! !} -- easy
-- ... | inj₁ (later a) = {! !} -- impossible?
... | inj₂ a = inj₂ (∼-refl A)
trivial : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ (< helper > ∘′ iter < g >) x ≡ helper₁ (iter < g > x) ]
trivial {x} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ A)
<<_>> = Elgot-Algebra-Morphism.h <<_>> = Elgot-Algebra-Morphism.h
@ -308,6 +337,7 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
*-uniq' : ∀ {B : Elgot-Algebra} (f : A ⟶ ⟦ B ⟧) (g : Elgot-Algebra-Morphism (delay-algebras A) B) (eq : (<< g >> ∘ (ηₛ A)) ≋ f) {x : Delay ∣ A ∣} → [_][_≡_] (⟦ B ⟧) ((<< g >>) ⟨$⟩ x) ((<< delay-lift {A} {B} f >>) ⟨$⟩ x) *-uniq' : ∀ {B : Elgot-Algebra} (f : A ⟶ ⟦ B ⟧) (g : Elgot-Algebra-Morphism (delay-algebras A) B) (eq : (<< g >> ∘ (ηₛ A)) ≋ f) {x : Delay ∣ A ∣} → [_][_≡_] (⟦ B ⟧) ((<< g >>) ⟨$⟩ x) ((<< delay-lift {A} {B} f >>) ⟨$⟩ x)
*-uniq' {B} f g eq {now x} = ≡-trans ⟦ B ⟧ (eq {x}) (≡-sym ⟦ B ⟧ (#-Fixpoint B)) *-uniq' {B} f g eq {now x} = ≡-trans ⟦ B ⟧ (eq {x}) (≡-sym ⟦ B ⟧ (#-Fixpoint B))
*-uniq' {B} f g eq {later x} = ≡-trans ⟦ B ⟧ {! !} (≡-sym ⟦ B ⟧ (#-Fixpoint B)) *-uniq' {B} f g eq {later x} = ≡-trans ⟦ B ⟧ {! !} (≡-sym ⟦ B ⟧ (#-Fixpoint B))
-- *-uniq' {B} f g eq {later x} = ≡-trans ⟦ B ⟧ {! *-uniq' {B} f g eq {force x} !} (≡-sym ⟦ B ⟧ (#-Fixpoint B))