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-09 15:49:15 +01:00
parent 9beebd009d
commit a6fd66ef29
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
1 changed files with 22 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -230,15 +230,30 @@ module Monad.Instance.Setoids.K' {ℓ : Level} where
-- Should follow by compositionality + fixpoint
eq₁ : [ ⟦ B ⟧ ][ (B Elgot-Algebra.#) helper' ⟨$⟩ z ≡ (B Elgot-Algebra.#) helper ⟨$⟩ liftF proj₁ z ]
eq₁ = {!!}
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 : ∀ {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))
-- ... | inj₁ r = {! !} -- <- contradiction!
-- ... | inj₂ r = {! !}
eq {now (x , suc n)} {now (y , suc m)} (now∼ (x≡y , n≡m)) = {! !}
-- TODO induction, by a recursive call to eq, we will get info about helper₁' (now (x , n))
eq {now (x , n)} {now (y , m)} (now∼ p∼q) = eq' {n} {m} {x} {y} (now∼ p∼q)
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)))
-- Should follow by uniformity