Start working on proving facts about graph construction

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

Language/Graphs.agda

@@ -12,8 +12,8 @@ open import Data.Nat as Nat using (ℕ; suc)
 open import Data.Nat.Properties using (+-assoc; +-comm)
 open import Data.Product using (_×_; Σ; _,_)
 open import Data.Vec using (Vec; []; _∷_; lookup; cast; _++_)
-open import Data.Vec.Properties using (cast-is-id; ++-assoc; lookup-++ˡ; cast-sym; ++-identityʳ)
+open import Data.Vec.Properties using (cast-is-id; ++-assoc; lookup-++ˡ; cast-sym; ++-identityʳ; lookup-++ʳ)
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; refl; subst)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; refl; subst; trans)
 
 open import Lattice
 open import Utils using (x∈xs⇒fx∈fxs; _⊗_; _,_)
@@ -134,6 +134,14 @@ relax-preserves-[]≡ g₁ g₂ (Mk-⊆ n refl newNodes nsg₂≡nsg₁++newNode
     rewrite cast-is-id refl (Graph.nodes g₂)
     with refl ← nsg₂≡nsg₁++newNodes = sym (lookup-++ˡ (Graph.nodes g₁) _ _)
 
+instance
+    NodeEqualsMonotonic : ∀ {bss : List BasicStmt} →
+                          MonotonicPredicate (λ g n → g [ n ] ≡ bss)
+    NodeEqualsMonotonic = record
+        { relaxPredicate = λ g₁ g₂ idx g₁⊆g₂ g₁[idx]≡bss →
+            trans (sym (relax-preserves-[]≡ g₁ g₂ g₁⊆g₂ idx)) g₁[idx]≡bss
+        }
+
 pushBasicBlock : List BasicStmt → MonotonicGraphFunction Graph.Index
 pushBasicBlock bss g =
     ( record
@@ -152,6 +160,9 @@ pushBasicBlock bss g =
       )
     )
 
+pushBasicBlock-works : ∀ (bss : List BasicStmt) → Always (λ g idx → g [ idx ] ≡ bss) (pushBasicBlock bss)
+pushBasicBlock-works bss = MkAlways (λ g → lookup-++ʳ (Graph.nodes g) (bss ∷ []) zero)
+
 addEdges : ∀ (g : Graph) → List (Graph.Edge g) → Σ Graph (λ g' → g ⊆ g')
 addEdges (MkGraph s ns es) es' =
     ( record