From 45d281fc5a7653df2585b34a7759d5bcd03a28b7 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Sun, 7 Jan 2024 15:55:54 +0100 Subject: [PATCH] fixed definition of iter --- agda/src/Monad/Instance/Setoids/K'.lagda.md | 68 ++++++--------------- 1 file changed, 20 insertions(+), 48 deletions(-) diff --git a/agda/src/Monad/Instance/Setoids/K'.lagda.md b/agda/src/Monad/Instance/Setoids/K'.lagda.md index 9c70809..e5c6376 100644 --- a/agda/src/Monad/Instance/Setoids/K'.lagda.md +++ b/agda/src/Monad/Instance/Setoids/K'.lagda.md @@ -38,7 +38,7 @@ module Monad.Instance.Setoids.K' {ℓ : Level} where force (iter′ {A} {X} f x) = iter {A} {X} f x iter {A} {X} f x with f x ... | inj₁ a = a - ... | inj₂ b = later (iter′ {A} {X} f x) + ... | inj₂ b = later (iter′ {A} {X} f b) conflict : ∀ {ℓ''} (X Y : Setoid ℓ ℓ) {Z : Set ℓ''} {x : ∣ X ∣} {y : ∣ Y ∣} → [ X ⊎ₛ Y ][ inj₁ x ≡ inj₂ y ] → Z @@ -69,17 +69,18 @@ module Monad.Instance.Setoids.K' {ℓ : Level} where ... | 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′ f x≡y) + ... | 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 { _⟨$⟩_ = iter {A} {X} (f ._⟨$⟩_) ; cong = iter-cong {A} {X} f } - iter-fixpoint : ∀ {A X : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ iter {A} {X} (f ._⟨$⟩_) x ≈ [ Function.id , iter {A} {X} (f ._⟨$⟩_) ] ((f ._⟨$⟩_) y) ] + iter-fixpoint : ∀ {A X : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ iter {A} {X} < f > x ≈ [ Function.id , iter {A} {X} < f > ] (f ⟨$⟩ y) ] iter-fixpoint {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 = ≈-trans A (≈-sym A later-self) (iter-cong f {! !}) + ... | inj₂ a | inj₂ b = ≈-trans A (≈-sym A later-self) (iter-cong f (inj₂-helper f x≡y eqx eqy)) + iter-resp-≈ : ∀ {A X : Setoid ℓ ℓ} (f g : X ⟶ (Delayₛ A ⊎ₛ X)) → f ≋ g → ∀ {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ iter {A} {X} (f ._⟨$⟩_) x ≈ iter {A} {X} (g ._⟨$⟩_) y ] iter-resp-≈′ : ∀ {A X : Setoid ℓ ℓ} (f g : X ⟶ (Delayₛ A ⊎ₛ X)) → f ≋ g → ∀ {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ iter {A} {X} (f ._⟨$⟩_) x ≈′ iter {A} {X} (g ._⟨$⟩_) y ] @@ -97,63 +98,35 @@ module Monad.Instance.Setoids.K' {ℓ : Level} where where helper : [ Delayₛ A ⊎ₛ X ][ inj₂ a ≡ inj₁ b ] helper rewrite (≣-sym eqy) | (≣-sym eqx) = f≋g x≡y - ... | inj₂ a | inj₂ b = later≈ (iter-resp-≈′ f g f≋g x≡y) + ... | inj₂ a | inj₂ b = later≈ (iter-resp-≈′ f g f≋g (drop-inj₂ helper)) + where + helper : [ Delayₛ A ⊎ₛ X ][ inj₂ a ≡ inj₂ b ] + helper rewrite (≣-sym eqy) | (≣-sym eqx) = f≋g x≡y - - iter-folding' : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {h : Y ⟶ X ⊎ₛ Y} {x y : ∣ 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 : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {h : Y ⟶ X ⊎ₛ Y} {x y : ∣ 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 : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {h : Y ⟶ X ⊎ₛ Y} {x y : ∣ 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 ] - force≈ (iter-folding′ {A} {X} {Y} {f} {h} {x} {y} x≡y) = iter-folding' {A} {X} {Y} {f} {h} x≡y - iter-folding' {A} {X} {Y} {f} {h} {inj₁ x} {inj₁ y} ix≡iy with f ⟨$⟩ x in eqx | f ⟨$⟩ y in eqy + force≈ (iter-folding′ {A} {X} {Y} {f} {h} {x} {y} x≡y) = iter-folding {A} {X} {Y} {f} {h} x≡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≈ helper + ... | inj₂ a | inj₂ b = later≈ (≈→≈′ A (≈-trans A (iter-cong f (inj₂-helper f (drop-inj₁ ix≡iy) eqx eqy)) (helper b))) where + helper : ∀ (b : ∣ X ∣) → [ A ][ iter < f > b ≈ iter [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ < f > , inj₂ ∘′ < h > ] (inj₁ b) ] helper' : ∀ (b : ∣ X ∣) → [ A ][ iter < f > b ≈′ iter [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ < f > , inj₂ ∘′ < h > ] (inj₁ b) ] - helper'' : ∀ (b : ∣ X ∣) → [ A ][ iter < f > b ≈ iter [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ < f > , inj₂ ∘′ < h > ] (inj₁ b) ] - helper'' b with f ⟨$⟩ b in eqb + helper b with f ⟨$⟩ b in eqb ... | inj₁ c = ≈-refl A - ... | inj₂ c = later≈ (helper' b) - force≈ (helper' b) with f ⟨$⟩ b in eqb - ... | inj₁ c = ≈-refl A - ... | inj₂ c = later≈ (helper' b) - helper : [ A ][ iter < f > x ≈′ iter [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ < f > , inj₂ ∘′ < h > ] (inj₁ y) ] - force≈ helper = ≈-trans A (iter-cong f (drop-inj₁ ix≡iy)) (helper'' y) + ... | inj₂ c = later≈ (helper' c) + force≈ (helper' b) = helper b - 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 !} + 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≈ {! !} - where - helper' : [ A ][ iter [ inj₁ ∘′ iter < f > , inj₂ ∘′ < h > ] (inj₂ x) ≈′ iter [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ < f > , inj₂ ∘′ < h > ] (inj₂ y) ] - force≈ helper' = later≈ {! iter-folding' {A} {X} {Y} {f} {h} {inj₂ a} {inj₂ b} ? !} - helper : [ X ⊎ₛ Y ][ inj₂ a ≡ inj₂ b ] - helper rewrite (≣-sym eqx) | (≣-sym eqy) = cong h (drop-inj₂ ix≡iy) - - - iter-folding : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {h : Y ⟶ X ⊎ₛ Y} {x y : ∣ 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≈ {! !} -- later≈ (♯ ≈-trans A (iter-cong f (inj₂-helper f (drop-inj₁ ix≡iy) eqx eqy)) (helper b)) - where - helper : ∀ (b : ∣ 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 (Delayₛ A) - ... | inj₂ c = later≈ {! !} -- 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) + ... | inj₂ a | inj₂ b = later≈ (iter-folding′ {A} {X} {Y} {f} {h} helper) where helper : [ X ⊎ₛ Y ][ inj₂ a ≡ inj₂ b ] helper rewrite (≣-sym eqx) | (≣-sym eqy) = cong h (drop-inj₂ ix≡iy) @@ -191,5 +164,4 @@ module Monad.Instance.Setoids.K' {ℓ : Level} where ; *-lift = {! !} ; *-uniq = {! !} } - ``` \ No newline at end of file