Add functions to reason about the 'monotonic state' operations

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-04-20 18:09:01 -07:00
parent 2f91ca113e
commit 855bf3f56c

View File

@ -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