From f3e0d5f2e3ff0ac4b29339690612c9d9bf126b3f Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 20 Apr 2024 19:31:13 -0700 Subject: [PATCH] Use 'data' instead of aliases to prove reasoning properties Signed-off-by: Danila Fedorin --- MonotonicState.agda | 92 +++++++++++++++++++++++++++++++-------------- 1 file changed, 64 insertions(+), 28 deletions(-) diff --git a/MonotonicState.agda b/MonotonicState.agda index 8f89e87..b126a0f 100644 --- a/MonotonicState.agda +++ b/MonotonicState.agda @@ -83,13 +83,15 @@ _map_ f fn s = let (s' , (t₁ , s≼s')) = f s in (s' , (fn s' t₁ , s≼s')) DependentPredicate : (S → Set s) → Set (lsuc s) DependentPredicate T = ∀ (s₁ : S) → T s₁ → Set s -Both : {T₁ T₂ : S → Set s} → DependentPredicate T₁ → DependentPredicate T₂ → - DependentPredicate (T₁ ⊗ T₂) -Both P Q = (λ { s (t₁ , t₂) → (P s t₁ × Q s t₂) }) +data Both {T₁ T₂ : S → Set s} + (P : DependentPredicate T₁) + (Q : DependentPredicate T₂) : DependentPredicate (T₁ ⊗ T₂) where + MkBoth : ∀ {s : S} {t₁ : T₁ s} {t₂ : T₂ s} → P s t₁ → Q s t₂ → Both P Q s (t₁ , t₂) -And : {T : S → Set s} → DependentPredicate T → DependentPredicate T → - DependentPredicate T -And P Q = (λ { s t → (P s t × Q s t) }) +data And {T : S → Set s} + (P : DependentPredicate T) + (Q : DependentPredicate T) : DependentPredicate T where + MkAnd : ∀ {s : S} {t : T s} → P s t → Q s t → And P 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 @@ -101,48 +103,82 @@ record MonotonicPredicate {T : S → Set s} {{ r : Relaxable T }} (P : Dependent field relaxPredicate : ∀ (s₁ s₂ : S) (t₁ : T s₁) (s₁≼s₂ : s₁ ≼ s₂) → P s₁ t₁ → P s₂ (Relaxable.relax r s₁≼s₂ t₁) +instance + BothMonotonic : ∀ {T₁ : S → Set s} {T₂ : S → Set s} + {{ _ : Relaxable T₁ }} {{ _ : Relaxable T₂ }} + {P : DependentPredicate T₁} {Q : DependentPredicate T₂} + {{_ : MonotonicPredicate P}} {{_ : MonotonicPredicate Q}} → + MonotonicPredicate (Both P Q) + BothMonotonic {{_}} {{_}} {{P-Mono}} {{Q-Mono}} = record + { relaxPredicate = (λ { s₁ s₂ (t₁ , t₂) s₁≼s₂ (MkBoth p q) → + MkBoth (MonotonicPredicate.relaxPredicate P-Mono s₁ s₂ t₁ s₁≼s₂ p) + (MonotonicPredicate.relaxPredicate Q-Mono s₁ s₂ t₂ s₁≼s₂ q)}) + } + + AndMonotonic : ∀ {T : S → Set s} {{ _ : Relaxable T }} + {P : DependentPredicate T} {Q : DependentPredicate T} + {{_ : MonotonicPredicate P}} {{_ : MonotonicPredicate Q}} → + MonotonicPredicate (And P Q) + AndMonotonic {{_}} {{P-Mono}} {{Q-Mono}} = record + { relaxPredicate = (λ { s₁ s₂ t s₁≼s₂ (MkAnd p q) → + MkAnd (MonotonicPredicate.relaxPredicate P-Mono s₁ s₂ t s₁≼s₂ p) + (MonotonicPredicate.relaxPredicate Q-Mono s₁ s₂ t s₁≼s₂ q)}) + } + -- A MonotonicState "monad" m has a certain property if its ouputs satisfy that -- property for all inputs. -always : ∀ {T : S → Set s} → DependentPredicate T → MonotonicState T → Set s -always P m = ∀ s₁ → let (s₂ , t , _) = m s₁ in P s₂ t +data Always {T : S → Set s} (P : DependentPredicate T) (m : MonotonicState T) : Set s where + MkAlways : (∀ s₁ → let (s₂ , t , _) = m s₁ in P s₂ t) → Always P m 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 - 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) + Always P m₁ → Always Q m₂ → Always (Both P Q) (m₁ ⟨⊗⟩ m₂) +_⟨⊗⟩-reason_ {P = P} {Q = Q} {{P-Mono = P-Mono}} {m₁ = m₁} {m₂ = m₂} (MkAlways aP) (MkAlways aQ) = + MkAlways impl + where + impl : ∀ s₁ → let (s₂ , t , _) = (m₁ ⟨⊗⟩ m₂) s₁ in (Both P Q) s₂ t + impl s + with p ← aP s + with (s' , (t₁ , s≼s')) ← m₁ s + with q ← aQ s' + with (s'' , (t₂ , s'≼s'')) ← m₂ s' = + MkBoth (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) → + 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) + Always (And P Q) (m update mod) +_update-reason_ {{r = r}} {P = P} {Q = Q} {{P-Mono = P-Mono}} {m = m} {mod = mod} (MkAlways aP) modQ = + MkAlways impl + where + impl : ∀ s₁ → let (s₂ , t , _) = (m update mod) s₁ in (And P Q) s₂ t + impl 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 = + MkAnd (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 + Always P m → (∀ (s : S) (t₁ : T₁ s) (t₂ : T₂ s) → P s t₁ → Q s t₂) → + Always Q (m map f) +_map-reason_ {P = P} {Q = Q} {m = m} {f = f} (MkAlways aP) P⇒Q = + MkAlways impl + where + impl : ∀ s₁ → let (s₂ , t , _) = (m map f) s₁ in Q s₂ t + impl s + with p ← aP s + with (s' , (t₁ , s≼s')) ← m s = P⇒Q s' t₁ (f s' t₁) p