143
150
------------------------------------------------------------------------
144
151
-- Lemmas relating the three relations
147
module Dummy {a ℓ} {A : Set a} {_∼_ : A → A → Set ℓ} where
153
module _ {a ℓ} {A : Set a} {_∼_ : A → A → Set ℓ} where
149
155
open Equality _∼_ using (Rel; _≅_; _≳_; _≲_; _≈_; _⇓[_]_; _⇑[_])
150
156
open Equality.Rel
324
330
module S {k eq} = Setoid (setoid isEquivalence k {eq})
327
infixr 2 _≅⟨_⟩_ _≳⟨_⟩_ _≈⟨_⟩_
333
infixr 2 _≡⟨_⟩_ _≅⟨_⟩_ _≳⟨_⟩_ _≈⟨_⟩_
335
_≡⟨_⟩_ : ∀ {k} x {y z : A ⊥} → x ≡ y → Rel k y z → Rel k x z
336
_ ≡⟨ P.refl ⟩ y∼z = y∼z
329
338
_≅⟨_⟩_ : ∀ {k} x {y z : A ⊥} → x ≅ y → Rel k y z → Rel k x z
330
339
_ ≅⟨ x≅y ⟩ y∼z = Pre.trans (≅⇒ x≅y) y∼z
432
441
(x >>= λ _ → never) ≅ never
433
442
right-zero (later x) = later (♯ right-zero (♭ x))
434
443
right-zero (now x) = never≅never
435
where never≅never = later (♯ never≅never)
444
where never≅never : never ≅ never
445
never≅never = later (♯ never≅never)
437
447
-- Now is a left and right identity of bind (for a reflexive
438
448
-- underlying relation).
458
468
associative refl-∼ (later x) f g =
459
469
later (♯ associative refl-∼ (♭ x) f g)
464
module Dummy₂ {s ℓ} {A B : Set s}
465
{_∼A_ : A → A → Set ℓ}
466
{_∼B_ : B → B → Set ℓ} where
471
module _ {s ℓ} {A B : Set s}
472
{_∼A_ : A → A → Set ℓ}
473
{_∼B_ : B → B → Set ℓ} where
683
685
_∎ : ∀ {k} x → RelP S k x x
684
686
sym : ∀ {k x y} {eq : Equality k} (x∼y : RelP S k x y) → RelP S k y x
687
_≡⟨_⟩_ : ∀ {k} x {y z} (x≡y : x ≡ y) (y∼z : RelP S k y z) → RelP S k x z
685
688
_≅⟨_⟩_ : ∀ {k} x {y z} (x≅y : S ∣ x ≅P y) (y∼z : RelP S k y z) → RelP S k x z
686
689
_≳⟨_⟩_ : let open Equality (Eq S) in
687
690
∀ x {y z} (x≳y : x ≳ y) (y≳z : S ∣ y ≳P z) → S ∣ x ≳P z
772
775
-- Strong equality programs can be turned into WHNFs.
774
777
whnf≅ : ∀ {S x y} → S ∣ x ≅P y → RelW S strong x y
775
whnf≅ (now xRy) = now xRy
776
whnf≅ (later x≅y) = later (♭ x≅y)
777
whnf≅ (x₁≅x₂ >>= f₁≅f₂) = whnf≅ x₁≅x₂ >>=W λ xRy → whnf≅ (f₁≅f₂ xRy)
778
whnf≅ (x ∎) = reflW x
779
whnf≅ (sym x≅y) = symW _ (whnf≅ x≅y)
780
whnf≅ (x ≅⟨ x≅y ⟩ y≅z) = trans≅W (whnf≅ x≅y) (whnf≅ y≅z)
778
whnf≅ (now xRy) = now xRy
779
whnf≅ (later x≅y) = later (♭ x≅y)
780
whnf≅ (x₁≅x₂ >>= f₁≅f₂) = whnf≅ x₁≅x₂ >>=W λ xRy → whnf≅ (f₁≅f₂ xRy)
781
whnf≅ (x ∎) = reflW x
782
whnf≅ (sym x≅y) = symW _ (whnf≅ x≅y)
783
whnf≅ (x ≡⟨ P.refl ⟩ y≅z) = whnf≅ y≅z
784
whnf≅ (x ≅⟨ x≅y ⟩ y≅z) = trans≅W (whnf≅ x≅y) (whnf≅ y≅z)
782
786
-- More transitivity lemmas.
804
808
-- Order programs can be turned into WHNFs.
806
810
whnf≳ : ∀ {S x y} → S ∣ x ≳P y → RelW S (other geq) x y
807
whnf≳ (now xRy) = now xRy
808
whnf≳ (later x∼y) = later (♭ x∼y)
809
whnf≳ (laterˡ x≲y) = laterˡ (whnf≳ x≲y)
810
whnf≳ (x₁∼x₂ >>= f₁∼f₂) = whnf≳ x₁∼x₂ >>=W λ xRy → whnf≳ (f₁∼f₂ xRy)
811
whnf≳ (x ∎) = reflW x
811
whnf≳ (now xRy) = now xRy
812
whnf≳ (later x∼y) = later (♭ x∼y)
813
whnf≳ (laterˡ x≲y) = laterˡ (whnf≳ x≲y)
814
whnf≳ (x₁∼x₂ >>= f₁∼f₂) = whnf≳ x₁∼x₂ >>=W λ xRy → whnf≳ (f₁∼f₂ xRy)
815
whnf≳ (x ∎) = reflW x
812
816
whnf≳ (sym {eq = ()} x≅y)
813
whnf≳ (x ≅⟨ x≅y ⟩ y≳z) = trans≅∼W (whnf≅ x≅y) (whnf≳ y≳z)
814
whnf≳ (x ≳⟨ x≳y ⟩ y≳z) = trans≳-W x≳y (whnf≳ y≳z)
815
whnf≳ (x ≳⟨ x≳y ⟩≅ y≅z) = trans∼≅W (whnf≳ x≳y) (whnf≅ y≅z)
817
whnf≳ (x ≡⟨ P.refl ⟩ y≳z) = whnf≳ y≳z
818
whnf≳ (x ≅⟨ x≅y ⟩ y≳z) = trans≅∼W (whnf≅ x≅y) (whnf≳ y≳z)
819
whnf≳ (x ≳⟨ x≳y ⟩ y≳z) = trans≳-W x≳y (whnf≳ y≳z)
820
whnf≳ (x ≳⟨ x≳y ⟩≅ y≅z) = trans∼≅W (whnf≳ x≳y) (whnf≅ y≅z)
817
822
-- Another transitivity lemma.
828
833
-- All programs can be turned into WHNFs.
830
835
whnf : ∀ {S k x y} → RelP S k x y → RelW S k x y
831
whnf (now xRy) = now xRy
832
whnf (later x∼y) = later (♭ x∼y)
833
whnf (laterʳ x≈y) = laterʳ (whnf x≈y)
834
whnf (laterˡ x∼y) = laterˡ (whnf x∼y)
835
whnf (x₁∼x₂ >>= f₁∼f₂) = whnf x₁∼x₂ >>=W λ xRy → whnf (f₁∼f₂ xRy)
837
whnf (sym {eq = eq} x≈y) = symW eq (whnf x≈y)
838
whnf (x ≅⟨ x≅y ⟩ y∼z) = trans≅∼W (whnf x≅y) (whnf y∼z)
839
whnf (x ≳⟨ x≳y ⟩ y≳z) = trans≳-W x≳y (whnf y≳z)
840
whnf (x ≳⟨ x≳y ⟩≅ y≅z) = trans∼≅W (whnf x≳y) (whnf y≅z)
841
whnf (x ≳⟨ x≳y ⟩≈ y≈z) = trans≳≈W (whnf x≳y) (whnf y≈z)
842
whnf (x ≈⟨ x≈y ⟩≅ y≅z) = trans∼≅W (whnf x≈y) (whnf y≅z)
843
whnf (x ≈⟨ x≈y ⟩≲ y≲z) = symW _ (trans≳≈W (whnf y≲z) (symW _ (whnf x≈y)))
836
whnf (now xRy) = now xRy
837
whnf (later x∼y) = later (♭ x∼y)
838
whnf (laterʳ x≈y) = laterʳ (whnf x≈y)
839
whnf (laterˡ x∼y) = laterˡ (whnf x∼y)
840
whnf (x₁∼x₂ >>= f₁∼f₂) = whnf x₁∼x₂ >>=W λ xRy → whnf (f₁∼f₂ xRy)
842
whnf (sym {eq = eq} x≈y) = symW eq (whnf x≈y)
843
whnf (x ≡⟨ P.refl ⟩ y∼z) = whnf y∼z
844
whnf (x ≅⟨ x≅y ⟩ y∼z) = trans≅∼W (whnf x≅y) (whnf y∼z)
845
whnf (x ≳⟨ x≳y ⟩ y≳z) = trans≳-W x≳y (whnf y≳z)
846
whnf (x ≳⟨ x≳y ⟩≅ y≅z) = trans∼≅W (whnf x≳y) (whnf y≅z)
847
whnf (x ≳⟨ x≳y ⟩≈ y≈z) = trans≳≈W (whnf x≳y) (whnf y≈z)
848
whnf (x ≈⟨ x≈y ⟩≅ y≅z) = trans∼≅W (whnf x≈y) (whnf y≅z)
849
whnf (x ≈⟨ x≈y ⟩≲ y≲z) = symW _ (trans≳≈W (whnf y≲z) (symW _ (whnf x≈y)))
864
870
correct = equivalence sound complete
866
872
------------------------------------------------------------------------
875
-- Bind is "idempotent".
878
∀ {ℓ} {A : Set ℓ} (B : Setoid ℓ ℓ) →
879
let open M; open Setoid B using (_≈_; Carrier); open Equality _≈_ in
880
(x : A ⊥) (f : A → A → Carrier ⊥) →
881
(x >>= λ y′ → x >>= λ y″ → f y′ y″) ≳ (x >>= λ y′ → f y′ y′)
882
idempotent {A = A} B x f = sound (idem x)
884
open AlternativeEquality hiding (_>>=_)
886
open Equality.Rel using (laterˡ)
887
open Equivalence using (refl)
890
B ∣ (x >>= λ y′ → x >>= λ y″ → f y′ y″) ≳P
891
(x >>= λ y′ → f y′ y′)
892
idem (now x) = f x x ∎
893
idem (later x) = later (♯ (
894
(♭ x >>= λ y′ → later x >>= λ y″ → f y′ y″) ≳⟨ (refl P.refl {x = ♭ x} ≡->>=-cong λ _ →
895
laterˡ (refl (Setoid.refl B))) ⟩
896
(♭ x >>= λ y′ → ♭ x >>= λ y″ → f y′ y″) ≳⟨ idem (♭ x) ⟩≅
897
(♭ x >>= λ y′ → f y′ y′) ∎))
899
------------------------------------------------------------------------
added
removed
src/Category/Monad/Partiality.agda
