Use 'data' instead of aliases to prove reasoning properties

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

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₂ →
+data Both {T₁ T₂ : S → Set s}
-       DependentPredicate (T₁ ⊗ T₂)
+          (P : DependentPredicate T₁)
-Both P Q = (λ { s (t₁ , t₂) → (P s t₁ × Q s 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 →
+data And {T : S → Set s}
-      DependentPredicate T
+         (P : DependentPredicate T)
-And P Q = (λ { s t → (P s t × Q s 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
+data Always {T : S → Set s} (P : DependentPredicate T) (m : MonotonicState T) : Set s where
-always P m = ∀ s₁ → let (s₂ , t , _) = m s₁ in P s₂ t
+    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₂)
+             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 = 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' =
-    (MonotonicPredicate.relaxPredicate P-Mono _ _ _ s'≼s'' p , q)
+            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)
+                  Always (And P Q) (m update mod)
-_update-reason_ {{r = r}} {{P-Mono = P-Mono}} {m = m} {mod = mod} aP modQ s
+_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 =
-    (MonotonicPredicate.relaxPredicate P-Mono _ _ _ s'≼s'' p , q)
+            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 P m → (∀ (s : S) (t₁ : T₁ s) (t₂ : T₂ s) → P s t₁ → Q s t₂) →
-               always Q (m map f)
+               Always Q (m map f)
-_map-reason_ {m = m} {f = f} aP P⇒Q s
+_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