Finish subproof

agda/src/Monad/Instance/K/Instance/D.lagda.md

@@ -246,6 +246,13 @@ module DelayMonad where
       ∼-cong {.(now _)} {.(now _)} (now∼ x≡y) = now-cong∼ (cong f x≡y)
       ∼-cong {.(later _)} {.(later _)} (later∼ x∼y) = later∼ (∼-cong′ x∼y)
 
+  lift-comp∼ : ∀ {A B C : Setoid c (c ⊔ ℓ)} {f : A ⟶ B} {g : B ⟶ C} {x y : Delay ∣ A ∣} → [ A ][ x ∼ y ] → [ C ][ liftFₛ (g ∘ f) ⟨$⟩ x ∼ (liftFₛ g ∘ liftFₛ f) ⟨$⟩ y ]
+  lift-comp∼′ : ∀ {A B C : Setoid c (c ⊔ ℓ)} {f : A ⟶ B} {g : B ⟶ C} {x y : Delay ∣ A ∣} → [ A ][ x ∼′ y ] → [ C ][ liftFₛ (g ∘ f) ⟨$⟩ x ∼′ (liftFₛ g ∘ liftFₛ f) ⟨$⟩ y ]
+  lift-comp∼ {A} {B} {C} {f} {g} {.(now _)} {.(now _)} (now∼ x≡y) = now-cong∼ (cong g (cong f (x≡y)))
+  lift-comp∼ {A} {B} {C} {f} {g} {.(later _)} {.(later _)} (later∼ x∼y) = later∼ (lift-comp∼′ {A} {B} {C} {f} {g} x∼y)
+  force∼ (lift-comp∼′ {A} {B} {C} {f} {g} {x} {y} x∼y) = lift-comp∼ {A} {B} {C} {f} {g} {x} {y} (force∼ x∼y)
+
+
   -- this needs polymorphic universe levels
   _≋_ : ∀ {c' ℓ'} {A B : Setoid c' ℓ'} → A ⟶ B → A ⟶ B → Set (c' ⊔ ℓ')
   _≋_ {c'} {ℓ'} {A} {B} f g = Setoid._≈_ (A ⇨ B) f g
@@ -360,6 +367,12 @@ module DelayMonad where
   identityˡ↓ {A} {now x} {y} x↓y = x↓y
   identityˡ↓ {A} {later x} {y} (later↓ x↓y) = later↓ (identityˡ↓ x↓y)
 
+  identityˡ∼ : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Delay ∣ A ∣} → [ A ][ x ∼ y ] → [ A ][ (μₛ A ∘ liftFₛ (ηₛ A)) ⟨$⟩ x ∼ y ]
+  identityˡ∼′ : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Delay ∣ A ∣} → [ A ][ x ∼′ y ] → [ A ][ (μₛ A ∘ liftFₛ (ηₛ A)) ⟨$⟩ x ∼′ y ]
+  identityˡ∼ {A} {.(now _)} {.(now _)} (now∼ x≡y) = now-cong∼ x≡y
+  identityˡ∼ {A} {.(later _)} {.(later _)} (later∼ x∼y) = later∼ (identityˡ∼′ {A} x∼y)
+  force∼ (identityˡ∼′ {A} {x} {y} x∼y) = identityˡ∼ (force∼ x∼y)
+
   identityˡ : ∀ {A : Setoid c (c ⊔ ℓ)} → (μₛ A ∘ liftFₛ (ηₛ A)) ≋ idₛ
   identityˡ′ : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Delay ∣ A ∣} → [ A ][ x ≈′ y ] → [ A ][ (μₛ A ∘ liftFₛ (ηₛ A)) ⟨$⟩ x ≈′ y ]
   force≈ (identityˡ′ {A} {x} {y} x≈y) = identityˡ (force≈ x≈y)

agda/src/Monad/Instance/Setoids/K'.lagda.md

@@ -1,7 +1,7 @@
 <!--
 ```agda
 {-# OPTIONS --allow-unsolved-metas --guardedness #-}
-open import Level
+open import Level renaming (zero to ℓ-zero; suc to ℓ-suc) 
 open import Relation.Binary
 open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′)
 open import Data.Sum.Function.Setoid
@@ -211,50 +211,39 @@ module Monad.Instance.Setoids.K' {ℓ : Level} where
 
     helper#≈-cong' {z} = ≡-trans ⟦ B ⟧ (≡-sym ⟦ B ⟧ eq₁) eq₂
       where     
-        helper₁' : Delay (∣ A ∣ × ℕ {ℓ}) → ∣ ⟦ B ⟧ ∣ ⊎ Delay (∣ A ∣ × ℕ)
+        outer : A ⟶ A ×ₛ ℕ-setoid {ℓ}
+        outer = record { _⟨$⟩_ = λ z → z , zero ; cong = λ {x} {y} x≡y → x≡y , ≣-refl }
+
+        zero-helper : Delayₛ' A ⟶ Delayₛ' (A ×ₛ ℕ-setoid {ℓ})
+        zero-helper = liftFₛ∼ outer
+
+        ι-cancel : ∀ {x} → [ A ][ (ι ∘′ (λ z → z , zero)) x ∼ now x ]
+        ι-cancel = ∼-refl A
+        helper₁' : Delay (∣ A ∣ × ℕ {ℓ}) → ∣ ⟦ B ⟧ ∣ ⊎ Delay (∣ A ∣ × ℕ {ℓ})
         helper₁' (now (x , zero))  = inj₁ (< f > x)
-        helper₁' (now (x , suc n)) with helper₁' (now (x , n))
-        ... | inj₁ r = inj₁ r
-        ... | inj₂ y = inj₂ (later (record { force = y }))
+        helper₁' (now (x , suc n)) = inj₂ (< zero-helper > (ι {A} (x , n)))
         helper₁' (later y)         = inj₂ (force y)
 
         helper₁-cong' : {x y : Delay (∣ A ∣ × ℕ {ℓ})} → (x∼y : [ A ×ₛ ℕ-setoid ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ Delayₛ' (A ×ₛ ℕ-setoid) ][ helper₁' x ≡ helper₁' y ]
         helper₁-cong' {now (x , zero)}  (now∼ (x≡y , ≣-refl)) = inj₁ (cong f x≡y)
-        helper₁-cong' {now (x , suc n)} {now (y , suc _)} (now∼ (x≡y , ≣-refl)) with helper₁' (now (x , n)) | helper₁' (now (y , n)) | helper₁-cong' {now (x , n)} (now∼ (x≡y , ≣-refl))
-        ... | inj₁ r  | inj₁ s  | inj₁ r≡s = inj₁ r≡s
-        ... | inj₂ x' | inj₂ y' | inj₂ x'∼y' = inj₂ (later∼ (record { force∼ = x'∼y' }))
-        helper₁-cong' (later∼ x≡y) = inj₂ (force∼ x≡y)
+        helper₁-cong' {now (x , suc n)} {now (y , suc _)} (now∼ (x≡y , ≣-refl)) = inj₂ (cong zero-helper (cong ιₛ' (x≡y , ≣-refl)))
+        helper₁-cong' (later∼ x∼y) = inj₂ (force∼ x∼y)
 
         helper' : Delayₛ' (A ×ₛ ℕ-setoid) ⟶ ⟦ B ⟧ ⊎ₛ Delayₛ' (A ×ₛ ℕ-setoid)
         helper' = record { _⟨$⟩_ = helper₁' ; cong = helper₁-cong'}
 
         -- Should follow by compositionality + fixpoint
-        eq₁ :  [ ⟦ B ⟧ ][ (B Elgot-Algebra.#) helper' ⟨$⟩ z ≡ (B Elgot-Algebra.#) helper ⟨$⟩ liftF proj₁ z ]
-        eq₁ = {!  !}
-
-
-        -- eq : ∀ {x y} → [ A ×ₛ ℕ-setoid ][ x ∼ y ] → [ ⟦ B ⟧ ⊎ₛ Delayₛ' A ][ [ inj₁ , inj₂ ∘′ μ ∘′ (liftF ι) ] (helper₁' x) ≡ (helper₁ ∘′ μ ∘′ (liftF ι)) y ]
-        -- eq {now (x , zero)} {now (y , zero)} (now∼ (x≡y , _)) = cong (inj₁ₛ {_} {_} {_} {_} {⟦ B ⟧} {Delayₛ' A}) (cong f x≡y)
-        -- eq {now (x , suc n)} {now (y , suc m)} (now∼ (x≡y , n≡m)) with helper₁' (now (x , n)) in eqr
-        -- ...                                                       | inj₁ r = {! eq {now (x , n)} {now (y , m)}  !} -- problem: recursive call to eq does not pass termination checker
-        --   where
-        --     help : [ ⟦ B ⟧ ⊎ₛ Delayₛ' A ][ [ inj₁ , inj₂ ∘′ μ ∘′ (liftF ι) ] (helper₁' (now (x , n))) ≡ inj₁ r ]
-        --     help = cong [ inj₁ₛ , (inj₂ₛ ∘ μₛ∼ A ∘ liftFₛ∼ ιₛ') ]ₛ (≡→≡ eqr)
-        -- ...                                                       | inj₂ r = {!   !}
-        -- eq {.(later _)} {.(later _)} (later∼ x≡y) = cong (inj₂ₛ {_} {_} {_} {_} {⟦ B ⟧} {Delayₛ' A}) (cong (μₛ∼ A) (cong (liftFₛ∼ ιₛ') (force∼ x≡y)))
+        eq₁ :  ∀ {z} → [ ⟦ B ⟧ ][ (B Elgot-Algebra.#) helper' ⟨$⟩ z ≡ (B Elgot-Algebra.#) helper ⟨$⟩ liftF proj₁ z ]
+        eq₁ {now (x , n)} = {!   !}
+        eq₁ {later p} = {!   !}
 
         eq : ∀ {x y} → [ A ×ₛ ℕ-setoid ][ x ∼ y ] → [ ⟦ B ⟧ ⊎ₛ Delayₛ' A ][ [ inj₁ , inj₂ ∘′ μ ∘′ (liftF ι) ] (helper₁' x) ≡ (helper₁ ∘′ μ ∘′ (liftF ι)) y ]
-        eq {now (x , n)} {now (y , m)} (now∼ p∼q) = eq' {n} {m} {x} {y} (now∼ p∼q)
+        eq {now (x , n)} {now (y , .n)} (now∼ (x∼y , ≣-refl)) = eq'
           where
-            eq' : ∀ {n m x y} → [ A ×ₛ ℕ-setoid ][ now (x , n) ∼ now (y , m) ] → [ ⟦ B ⟧ ⊎ₛ Delayₛ' A ][ [ inj₁ , inj₂ ∘′ μ ∘′ (liftF ι) ] (helper₁' (now (x , n))) ≡ (helper₁ ∘′ μ ∘′ (liftF ι)) (now (y , m)) ]
-            eq' {zero} {zero} {x} {y} (now∼ (x≡y , _)) = cong (inj₁ₛ {_} {_} {_} {_} {⟦ B ⟧} {Delayₛ' A}) (cong f x≡y)
-            eq' {suc n} {suc m} {x} {y} (now∼ (x≡y , sn≡sm)) with helper₁' (now (x , n)) in eqr 
-            ...                     | inj₁ r = ≡-trans (⟦ B ⟧ ⊎ₛ Delayₛ' A) (≡-sym (⟦ B ⟧ ⊎ₛ Delayₛ' A) help) (≡-trans (⟦ B ⟧ ⊎ₛ Delayₛ' A) (eq' {n} {m} {x} {y} (now∼ (x≡y , suc-inj sn≡sm))) {! -should this be provable?-  !})
-              where
-                help : [ ⟦ B ⟧ ⊎ₛ Delayₛ' A ][ [ inj₁ , inj₂ ∘′ μ ∘′ (liftF ι) ] (helper₁' (now (x , n))) ≡ inj₁ r ]
-                help = cong [ inj₁ₛ , (inj₂ₛ ∘ μₛ∼ A ∘ liftFₛ∼ ιₛ') ]ₛ (≡→≡ eqr)
-            ...                     | inj₂ r = {!   !}
-        eq {.(later _)} {.(later _)} (later∼ x≡y) = cong (inj₂ₛ {_} {_} {_} {_} {⟦ B ⟧} {Delayₛ' A}) (cong (μₛ∼ A) (cong (liftFₛ∼ ιₛ') (force∼ x≡y)))
+            eq' : ∀ {n} → [ ⟦ B ⟧ ⊎ₛ Delayₛ' A ][ [ inj₁ , inj₂ ∘′ μ ∘′ liftF ι ] (helper₁' (now (x , n))) ≡ (helper₁ ∘′ μ {A} ∘′ liftF ι) (now (y , n)) ]
+            eq' {zero}  = inj₁ (cong f x∼y)
+            eq' {suc n} = inj₂ (∼-trans A (cong (μₛ∼ A) (∼-sym (Delayₛ' A) (lift-comp∼ {f = outer} {g = ιₛ'} {ι (x , n)} (∼-refl A)))) (identityˡ∼ (cong ιₛ' (x∼y , ≣-refl))))
+        eq (later∼ x∼y) = inj₂ (cong (μₛ∼ A) (cong (liftFₛ∼ ιₛ') (force∼ x∼y)))
 
         -- Should follow by uniformity
         eq₂ : [ ⟦ B ⟧ ][ (B Elgot-Algebra.#) helper' ⟨$⟩ z ≡ (B Elgot-Algebra.#) helper ⟨$⟩ μ {A} (liftF (ι {A}) z)]