1
------------------------------------------------------------------------
2
-- The Agda standard library
4
-- An All predicate for the partiality monad
5
------------------------------------------------------------------------
7
module Category.Monad.Partiality.All where
9
open import Category.Monad
10
open import Category.Monad.Partiality as Partiality using (_⊥; ⇒≈)
11
open import Coinduction
14
open import Relation.Binary using (_Respects_; IsEquivalence)
15
open import Relation.Binary.PropositionalEquality as P using (_≡_)
18
open Partiality.Equality using (Rel)
19
open Partiality.Equality.Rel
21
open module E {a} {A : Set a} = Partiality.Equality (_≡_ {A = A})
23
open module M {f} = RawMonad (Partiality.monad {f = f})
26
------------------------------------------------------------------------
27
-- All, along with some lemmas
29
-- All P x means that if x terminates with the value v, then P v
32
data All {a p} {A : Set a} (P : A → Set p) : A ⊥ → Set (a ⊔ p) where
33
now : ∀ {v} (p : P v) → All P (now v)
34
later : ∀ {x} (p : ∞ (All P (♭ x))) → All P (later x)
36
-- Bind preserves All in the following way:
38
_>>=-cong_ : ∀ {ℓ p q} {A B : Set ℓ} {P : A → Set p} {Q : B → Set q}
39
{x : A ⊥} {f : A → B ⊥} →
40
All P x → (∀ {x} → P x → All Q (f x)) →
42
now p >>=-cong f = f p
43
later p >>=-cong f = later (♯ (♭ p >>=-cong f))
45
-- All respects all the relations, given that the predicate respects
46
-- the underlying relation.
49
∀ {k a p ℓ} {A : Set a} {P : A → Set p} {_∼_ : A → A → Set ℓ} →
50
P Respects _∼_ → All P Respects Rel _∼_ k
51
respects resp (now x∼y) (now p) = now (resp x∼y p)
52
respects resp (later x∼y) (later p) = later (♯ respects resp (♭ x∼y) (♭ p))
53
respects resp (laterˡ x∼y) (later p) = respects resp x∼y (♭ p)
54
respects resp (laterʳ x≈y) p = later (♯ respects resp x≈y p)
57
∀ {k a p ℓ} {A : Set a} {P : A → Set p} {_∼_ : A → A → Set ℓ} →
58
P Respects flip _∼_ → All P Respects flip (Rel _∼_ k)
59
respects-flip resp (now x∼y) (now p) = now (resp x∼y p)
60
respects-flip resp (later x∼y) (later p) = later (♯ respects-flip resp (♭ x∼y) (♭ p))
61
respects-flip resp (laterˡ x∼y) p = later (♯ respects-flip resp x∼y p)
62
respects-flip resp (laterʳ x≈y) (later p) = respects-flip resp x≈y (♭ p)
64
-- "Equational" reasoning.
66
module Reasoning {a p ℓ}
67
{A : Set a} {P : A → Set p}
69
(resp : P Respects flip _∼_) where
72
infixr 2 _≡⟨_⟩_ _∼⟨_⟩_
74
_≡⟨_⟩_ : ∀ x {y} → x ≡ y → All P y → All P x
77
_∼⟨_⟩_ : ∀ {k} x {y} → Rel _∼_ k x y → All P y → All P x
78
_ ∼⟨ x∼y ⟩ p = respects-flip resp (⇒≈ x∼y) p
80
-- A cosmetic combinator.
82
finally : (x : A ⊥) → All P x → All P x
85
syntax finally x p = x ⟨ p ⟩
87
-- "Equational" reasoning with _∼_ instantiated to propositional
90
module Reasoning-≡ {a p} {A : Set a} {P : A → Set p}
91
= Reasoning {P = P} {_∼_ = _≡_} (P.subst P ∘ P.sym)
93
------------------------------------------------------------------------
94
-- An alternative, but equivalent, formulation of All
96
module Alternative {a p : Level} where
98
infixr 2 _≅⟨_⟩P_ _≳⟨_⟩P_
103
data AllP {A : Set a} (P : A → Set p) : A ⊥ → Set (suc (a ⊔ p)) where
104
now : ∀ {x} (p : P x) → AllP P (now x)
105
later : ∀ {x} (p : ∞ (AllP P (♭ x))) → AllP P (later x)
106
_>>=-congP_ : ∀ {B : Set a} {Q : B → Set p} {x f}
107
(p-x : AllP Q x) (p-f : ∀ {v} → Q v → AllP P (f v)) →
109
_≅⟨_⟩P_ : ∀ x {y} (x≅y : x ≅ y) (p : AllP P y) → AllP P x
110
_≳⟨_⟩P_ : ∀ x {y} (x≳y : x ≳ y) (p : AllP P y) → AllP P x
111
_⟨_⟩P : ∀ x (p : AllP P x) → AllP P x
117
data AllW {A} (P : A → Set p) : A ⊥ → Set (suc (a ⊔ p)) where
118
now : ∀ {x} (p : P x) → AllW P (now x)
119
later : ∀ {x} (p : AllP P (♭ x)) → AllW P (later x)
121
-- A function which turns WHNFs into programs.
123
program : ∀ {A} {P : A → Set p} {x} → AllW P x → AllP P x
124
program (now p) = now p
125
program (later p) = later (♯ p)
127
-- Functions which turn programs into WHNFs.
129
trans-≅ : ∀ {A} {P : A → Set p} {x y : A ⊥} →
130
x ≅ y → AllW P y → AllW P x
131
trans-≅ (now P.refl) (now p) = now p
132
trans-≅ (later x≅y) (later p) = later (_ ≅⟨ ♭ x≅y ⟩P p)
134
trans-≳ : ∀ {A} {P : A → Set p} {x y : A ⊥} →
135
x ≳ y → AllW P y → AllW P x
136
trans-≳ (now P.refl) (now p) = now p
137
trans-≳ (later x≳y) (later p) = later (_ ≳⟨ ♭ x≳y ⟩P p)
138
trans-≳ (laterˡ x≳y) p = later (_ ≳⟨ x≳y ⟩P program p)
142
_>>=-congW_ : ∀ {A B} {P : A → Set p} {Q : B → Set p} {x f} →
143
AllW P x → (∀ {v} → P v → AllP Q (f v)) →
145
now p >>=-congW p-f = whnf (p-f p)
146
later p >>=-congW p-f = later (p >>=-congP p-f)
148
whnf : ∀ {A} {P : A → Set p} {x} → AllP P x → AllW P x
150
whnf (later p) = later (♭ p)
151
whnf (p-x >>=-congP p-f) = whnf p-x >>=-congW p-f
152
whnf (_ ≅⟨ x≅y ⟩P p) = trans-≅ x≅y (whnf p)
153
whnf (_ ≳⟨ x≳y ⟩P p) = trans-≳ x≳y (whnf p)
154
whnf (_ ⟨ p ⟩P) = whnf p
156
-- AllP P is sound and complete with respect to All P.
158
sound : ∀ {A} {P : A → Set p} {x} → AllP P x → All P x
159
sound = λ p → soundW (whnf p)
161
soundW : ∀ {A} {P : A → Set p} {x} → AllW P x → All P x
162
soundW (now p) = now p
163
soundW (later p) = later (♯ sound p)
165
complete : ∀ {A} {P : A → Set p} {x} → All P x → AllP P x
166
complete (now p) = now p
167
complete (later p) = later (♯ complete (♭ p))
added
removed
src/Category/Monad/Partiality/All.agda
