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

Work on example

Browse source
This commit is contained in:
Leon Vatthauer 2023-12-14 19:11:20 +01:00
parent ce13e19d1a
commit 5f1ab060bb
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 12 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1,7 +1,6 @@
<!-- <!--
```agda ```agda
{-# OPTIONS --allow-unsolved-metas --guardedness #-} {-# OPTIONS --allow-unsolved-metas --guardedness #-}
open import Level open import Level
open import Relation.Binary open import Relation.Binary
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]) open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_])
@ -66,7 +65,7 @@ module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where
... | inj₁ a | inj₂ b = absurd-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 = absurd-helper f (∼-sym X x∼y) eqy eqx
... | inj₂ a | inj₂ b = ≈-sym (later-eq (later≈ (♯ iter-cong f (∼-sym X (inj₂-helper f x∼y eqx eqy))))) ... | inj₂ a | inj₂ b = ≈-sym (later-eq (later≈ (♯ iter-cong f (∼-sym X (inj₂-helper f x∼y eqx eqy)))))
{-# TERMINATING #-}
iter-uni : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (delaySetoid A ⊎ₛ X)} {g : Y ⟶ (delaySetoid A ⊎ₛ Y)} {h : X ⟶ Y} → ([ inj₁ₛ ∘ idₛ , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h) → ∀ {x y : Setoid.Carrier X} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ y) ] iter-uni : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (delaySetoid A ⊎ₛ X)} {g : Y ⟶ (delaySetoid A ⊎ₛ Y)} {h : X ⟶ Y} → ([ inj₁ₛ ∘ idₛ , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h) → ∀ {x y : Setoid.Carrier X} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ y) ]
iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y with (f ._⟨$⟩_) x in eqx | (f ._⟨$⟩_) y in eqy iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y with (f ._⟨$⟩_) x in eqx | (f ._⟨$⟩_) y in eqy
... | inj₁ a | inj₁ b with g ⟨$⟩ (h ⟨$⟩ y) in eqc ... | inj₁ a | inj₁ b with g ⟨$⟩ (h ⟨$⟩ y) in eqc
@ -88,9 +87,16 @@ module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where
helper rewrite (≡-sym eqc) = helper' helper rewrite (≡-sym eqc) = helper'
iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y | inj₁ a | inj₂ b = absurd-helper f x∼y eqx eqy iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y | inj₁ a | inj₂ b = absurd-helper f x∼y eqx eqy
iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y | inj₂ a | inj₁ b = absurd-helper f (∼-sym X x∼y) eqy eqx iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y | inj₂ a | inj₁ b = absurd-helper f (∼-sym X x∼y) eqy eqx
iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y | inj₂ a | inj₂ b with g ⟨$⟩ (h ⟨$⟩ y) in eqc -- = ≈-sym (later-eq (later≈ (♯ {! !}))) -- (iter-uni {A} {X} {Y} {f} {{! !}} {h} hf≈gh ((inj₂-helper f x∼y eqx eqy))) iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y | inj₂ a | inj₂ b with g ⟨$⟩ (h ⟨$⟩ y) in eqc
... | inj₁ c = {! !} -- absurd, probably... ... | inj₁ c = conflict (delaySetoid A) Y (∼-sym (delaySetoid A ⊎ₛ Y) helper)
... | inj₂ c = later≈ (♯ {! !}) where
helper' : (delaySetoid A ⊎ₛ Y) [ ([ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x)) ∼ g ⟨$⟩ (h ⟨$⟩ y) ]
helper' = hf≈gh {x} {y} x∼y
helper'' : (delaySetoid A ⊎ₛ Y) [ inj₂ (h ⟨$⟩ a) ∼ ([ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x)) ]
helper'' rewrite eqx = ∼-refl (delaySetoid A ⊎ₛ Y)
helper : (delaySetoid A ⊎ₛ Y) [ inj₂ (h ⟨$⟩ a) ∼ inj₁ c ]
helper rewrite (≡-sym eqc) = ∼-trans (delaySetoid A ⊎ₛ Y) helper'' helper'
... | inj₂ c = ≈-trans (later≈ {A} {_} {♯ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ a)} (♯ (iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh (∼-refl X)))) (later≈ (♯ iter-cong g (∼-sym Y helper)))
-- why does this not terminate?? -- why does this not terminate??
-- | inj₂ c = ≈-trans (later≈ {A} {_} {♯ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ a)} (♯ (iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh (∼-refl X)))) (later≈ (♯ iter-cong g (∼-sym Y helper))) -- | inj₂ c = ≈-trans (later≈ {A} {_} {♯ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ a)} (♯ (iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh (∼-refl X)))) (later≈ (♯ iter-cong g (∼-sym Y helper)))
where where
@ -102,9 +108,6 @@ module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where
helper' rewrite eqx = ∼-refl (delaySetoid A ⊎ₛ Y) helper' rewrite eqx = ∼-refl (delaySetoid A ⊎ₛ Y)
helper : Y [ c ∼ h ⟨$⟩ a ] helper : Y [ c ∼ h ⟨$⟩ a ]
helper = drop-inj₂ {x = c} {y = h ⟨$⟩ a} (∼-trans (delaySetoid A ⊎ₛ Y) helper''' (∼-trans (delaySetoid A ⊎ₛ Y) helper'' helper')) helper = drop-inj₂ {x = c} {y = h ⟨$⟩ a} (∼-trans (delaySetoid A ⊎ₛ Y) helper''' (∼-trans (delaySetoid A ⊎ₛ Y) helper'' helper'))
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 -- 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 : 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 ]
@ -160,6 +163,7 @@ module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where
-- kleisli lifting (just for making the code cleaner) -- kleisli lifting (just for making the code cleaner)
-- TODO -- TODO
-- TODO, freealgebras approach is probably easier
delayPreElgot : IsPreElgot delayMonad delayPreElgot : IsPreElgot delayMonad
delayPreElgot = record delayPreElgot = record