From 2f91ca113eb8082beaa00c2cde50b9932555567f Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 13 Apr 2024 20:56:56 -0700 Subject: [PATCH] Make 'MonotonicPredicate' into another typeclass Signed-off-by: Danila Fedorin --- MonotonicState.agda | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/MonotonicState.agda b/MonotonicState.agda index 4d4c3c8..1f81abd 100644 --- a/MonotonicState.agda +++ b/MonotonicState.agda @@ -93,9 +93,8 @@ Both P Q = (λ { s (t₁ , t₂) → (P s t₁ × Q s t₂) }) -- states'. We call such predicates monotonic as well, since they respect the -- ordering relation. -MonotonicPredicate : ∀ {T : S → Set s} {{ _ : Relaxable T }} → - DependentPredicate T → Set s -MonotonicPredicate {T} {{r}} P = ∀ (s₁ s₂ : S) (t₁ : T s₁) (s₁≼s₂ : s₁ ≼ s₂) → +record MonotonicPredicate {T : S → Set s} {{ r : Relaxable T }} (P : DependentPredicate T) : Set s where + field relaxPredicate : ∀ (s₁ s₂ : S) (t₁ : T s₁) (s₁≼s₂ : s₁ ≼ s₂) → P s₁ t₁ → P s₂ (Relaxable.relax r s₁≼s₂ t₁) -- A MonotonicState "monad" m has a certain property if its ouputs satisfy that @@ -106,11 +105,12 @@ always P m = ∀ s₁ → let (s₂ , t , _) = m s₁ in P s₂ t ⟨⊗⟩-reason : ∀ {T₁ T₂ : S → Set s} {{ _ : Relaxable T₁ }} {P : DependentPredicate T₁} {Q : DependentPredicate T₂} - {P-Mono : MonotonicPredicate P} + {{P-Mono : MonotonicPredicate P}} {m₁ : MonotonicState T₁} {m₂ : MonotonicState T₂} → always P m₁ → always Q m₂ → always (Both P Q) (m₁ ⟨⊗⟩ m₂) -⟨⊗⟩-reason {P-Mono = P-Mono} {m₁ = m₁} {m₂ = m₂} aP aQ s +⟨⊗⟩-reason {{P-Mono = P-Mono}} {m₁ = m₁} {m₂ = m₂} aP aQ s with p ← aP s with (s' , (t₁ , s≼s')) ← m₁ s with q ← aQ s' - with (s'' , (t₂ , s'≼s'')) ← m₂ s' = (P-Mono _ _ _ s'≼s'' p , q) + with (s'' , (t₂ , s'≼s'')) ← m₂ s' = + (MonotonicPredicate.relaxPredicate P-Mono _ _ _ s'≼s'' p , q)