Start formalizing monotonic function predicates

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

Language.agda

@@ -209,9 +209,16 @@ module Graphs where
         rewrite cast-is-id refl (Graph.nodes g₂)
         with refl ← nsg₂≡nsg₁++newNodes = sym (lookup-++ˡ (Graph.nodes g₁) _ _)
 
+    -- Tools for graph construction. The most important is a 'monotonic function':
+    -- one that takes a graph, and produces another graph, such that the
+    -- new graph includes all the information from the old one.
+
     MonotonicGraphFunction : (Graph → Set) → Set
     MonotonicGraphFunction T = (g₁ : Graph) → Σ Graph (λ g₂ → T g₂ × g₁ ⊆ g₂)
 
+    -- Now, define some operations on monotonic functions; these are useful
+    -- to save the work of threading intermediate graphs in and out of operations.
+
     infixr 2 _⟨⊗⟩_
     _⟨⊗⟩_ : ∀ {T₁ T₂ : Graph → Set} {{ T₁Relaxable : Relaxable T₁ }} →
           MonotonicGraphFunction T₁ → MonotonicGraphFunction T₂ →
@@ -236,6 +243,43 @@ module Graphs where
           MonotonicGraphFunction T₂
     _map_ f fn g = let (g' , (t₁ , g⊆g')) = f g in (g' , (fn g' t₁ , g⊆g'))
 
+
+    -- To reason about monotonic functions and what we do, we need a way
+    -- to describe values they produce. A 'graph-value predicate' is
+    -- just a predicate for some (dependent) value.
+
+    GraphValuePredicate : (Graph → Set) → Set₁
+    GraphValuePredicate T = ∀ (g : Graph) → T g → Set
+
+    Both : {T₁ T₂ : Graph → Set} → GraphValuePredicate T₁ → GraphValuePredicate T₂ →
+           GraphValuePredicate (T₁ ⊗ T₂)
+    Both P Q = (λ { g (t₁ , t₂) → (P g t₁ × Q g t₂) })
+
+    -- Since monotnic functions keep adding on to a function, proofs of
+    -- graph-value predicates go stale fast (they describe old values of
+    -- the graph). To keep propagating them through, we need them to still
+    -- on 'bigger graphs'. We call such predicates monotonic as well, since
+    -- they respect the ordering of graphs.
+
+    MonotonicPredicate : ∀ {T : Graph → Set} {{ TRelaxable : Relaxable T }} →
+                         GraphValuePredicate T → Set
+    MonotonicPredicate {T} P = ∀ (g₁ g₂ : Graph) (t₁ : T g₁) (g₁⊆g₂ : g₁ ⊆ g₂) →
+                               P g₁ t₁ → P g₂ (relax g₁⊆g₂ t₁)
+
+
+    -- A 'map' has a certain property if its ouputs satisfy that property
+    -- for all inputs.
+
+    always : ∀ {T : Graph → Set} → GraphValuePredicate T → MonotonicGraphFunction T → Set
+    always P m = ∀ g₁ → let (g₂ , t , _) = m g₁ in P g₂ t
+
+    ⟨⊗⟩-reason : ∀ {T₁ T₂ : Graph → Set} {{ T₁Relaxable : Relaxable T₁ }}
+                 {P : GraphValuePredicate T₁} {Q : GraphValuePredicate T₂}
+                 {P-Mono : MonotonicPredicate P}
+                 {m₁ : MonotonicGraphFunction T₁} {m₂ : MonotonicGraphFunction T₂} →
+                 always P m₁ → always Q m₂ → always (Both P Q) (m₁ ⟨⊗⟩ m₂)
+    ⟨⊗⟩-reason = {!!}
+
     module Construction where
         pushBasicBlock : List BasicStmt → MonotonicGraphFunction Graph.Index
         pushBasicBlock bss g =