From 855bf3f56cb41932f34af09a95bda31efa6ab508 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sat, 20 Apr 2024 18:09:01 -0700
Subject: [PATCH] Add functions to reason about the 'monotonic state'
 operations

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 MonotonicState.agda | 36 ++++++++++++++++++++++++++++++++++--
 1 file changed, 34 insertions(+), 2 deletions(-)

diff --git a/MonotonicState.agda b/MonotonicState.agda
index 1f81abd..8f89e87 100644
--- a/MonotonicState.agda
+++ b/MonotonicState.agda
@@ -87,6 +87,10 @@ Both : {T₁ T₂ : S → Set s} → DependentPredicate T₁ → DependentPredic
        DependentPredicate (T₁ ⊗ T₂)
 Both P Q = (λ { s (t₁ , t₂) → (P s t₁ × Q s t₂) })
 
+And : {T : S → Set s} → DependentPredicate T → DependentPredicate T →
+      DependentPredicate T
+And P Q = (λ { s t → (P s t × Q s t) })
+
 -- Since monotnic functions keep adding on to the state, proofs of
 -- predicates over their outputs go stale fast (they describe old values of
 -- the state). To keep them relevant, we need them to still hold on 'bigger
@@ -103,14 +107,42 @@ record MonotonicPredicate {T : S → Set s} {{ r : Relaxable T }} (P : Dependent
 always : ∀ {T : S → Set s} → DependentPredicate T → MonotonicState T → Set s
 always P m = ∀ s₁ → let (s₂ , t , _) = m s₁ in P s₂ t
 
-⟨⊗⟩-reason : ∀ {T₁ T₂ : S → Set s} {{ _ : Relaxable T₁ }}
+infixr 4 _⟨⊗⟩-reason_
+_⟨⊗⟩-reason_ : ∀ {T₁ T₂ : S → Set s} {{ _ : Relaxable T₁ }}
              {P : DependentPredicate T₁} {Q : DependentPredicate T₂}
              {{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' =
     (MonotonicPredicate.relaxPredicate P-Mono _ _ _ s'≼s'' p , q)
+
+infixl 4 _update-reason_
+_update-reason_ : ∀ {T : S → Set s} {{ r : Relaxable T }} →
+                  {P : DependentPredicate T} {Q : DependentPredicate T}
+                  {{P-Mono : MonotonicPredicate P}}
+                  {m : MonotonicState T} {mod : ∀ (s : S) → T s → Σ S (λ s' → s ≼ s')} →
+                  always P m → (∀ (s : S) (t : T s) →
+                                let (s' , s≼s') = mod s t
+                                in P s t → Q s' (Relaxable.relax r s≼s' t)) →
+                  always (And P Q) (m update mod)
+_update-reason_ {{r = r}} {{P-Mono = P-Mono}} {m = m} {mod = mod} aP modQ s
+    with p ← aP s
+    with (s' , (t , s≼s')) ← m s
+    with q ← modQ s' t p
+    with (s'' , s'≼s'') ← mod s' t =
+    (MonotonicPredicate.relaxPredicate P-Mono _ _ _ s'≼s'' p , q)
+
+infixl 4 _map-reason_
+_map-reason_ : ∀ {T₁ T₂ : S → Set s}
+               {P : DependentPredicate T₁} {Q : DependentPredicate T₂}
+               {m : MonotonicState T₁}
+               {f : ∀ (s : S) → T₁ s → T₂ s} →
+               always P m → (∀ (s : S) (t₁ : T₁ s) (t₂ : T₂ s) → P s t₁ → Q s t₂) →
+               always Q (m map f)
+_map-reason_ {m = m} {f = f} aP P⇒Q s
+    with p ← aP s
+    with (s' , (t₁ , s≼s')) ← m s = P⇒Q s' t₁ (f s' t₁) p