Use concatenation to represent adding new nodes

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

Language.agda

@@ -6,7 +6,7 @@ open import Data.Integer using (ℤ; +_) renaming (_+_ to _+ᶻ_; _-_ to _-ᶻ_)
 open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
 open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
 open import Data.Vec using (Vec; foldr; lookup; _∷_; []; _++_; cast)
-open import Data.Vec.Properties using (++-assoc; ++-identityʳ; lookup-++ˡ; lookup-cast₁)
+open import Data.Vec.Properties using (++-assoc; ++-identityʳ; lookup-++ˡ; lookup-cast₁; cast-sym)
 open import Data.Vec.Relation.Binary.Equality.Cast using (cast-is-id)
 open import Data.List using ([]; _∷_; List) renaming (foldr to foldrˡ; map to mapˡ; _++_ to _++ˡ_)
 open import Data.List.Properties using () renaming (++-assoc to ++ˡ-assoc; map-++ to mapˡ-++ˡ; ++-identityʳ to ++ˡ-identityʳ)
@@ -114,36 +114,27 @@ module Graphs where
         field
             n : ℕ
             sg₂≡sg₁+n : Graph.size g₂ ≡ Graph.size g₁ +ⁿ n
-            g₁[]≡g₂[] : ∀ (idx : Graph.Index g₁) →
+            newNodes : Vec (List BasicStmt) n
-                        lookup (Graph.nodes g₁) idx ≡
+            nsg₂≡nsg₁++newNodes : cast sg₂≡sg₁+n (Graph.nodes g₂) ≡ Graph.nodes g₁ ++ newNodes
-                        lookup (cast sg₂≡sg₁+n (Graph.nodes g₂)) (idx ↑ˡ n)
             e∈g₁⇒e∈g₂ : ∀ {e : Graph.Edge g₁} →
                         e ∈ˡ (Graph.edges g₁) →
                         (↑ˡ-Edge e n) ∈ˡ (subst (λ m → List (Fin m × Fin m)) sg₂≡sg₁+n (Graph.edges g₂))
 
     ⊆-trans : ∀ {g₁ g₂ g₃ : Graph} → g₁ ⊆ g₂ → g₂ ⊆ g₃ → g₁ ⊆ g₃
     ⊆-trans {MkGraph s₁ ns₁ es₁} {MkGraph s₂ ns₂ es₂} {MkGraph s₃ ns₃ es₃}
-            (Mk-⊆ n₁ p₁@refl g₁[]≡g₂[] e∈g₁⇒e∈g₂) (Mk-⊆ n₂ p₂@refl g₂[]≡g₃[] e∈g₂⇒e∈g₃) = record
+            (Mk-⊆ n₁ p₁@refl newNodes₁ nsg₂≡nsg₁++newNodes₁ e∈g₁⇒e∈g₂)
-        { n = n₁ +ⁿ n₂
+            (Mk-⊆ n₂ p₂@refl newNodes₂ nsg₃≡nsg₂++newNodes₂ e∈g₂⇒e∈g₃)
-        ; sg₂≡sg₁+n = +-assoc s₁ n₁ n₂
+        rewrite cast-is-id refl ns₂
-        ; g₁[]≡g₂[] = λ idx →
+        rewrite cast-is-id refl ns₃
-            begin
+        with refl ← nsg₂≡nsg₁++newNodes₁
-              lookup ns₁ idx
+        with refl ← nsg₃≡nsg₂++newNodes₂ =
-            ≡⟨ g₁[]≡g₂[] _ ⟩
+        record
-              lookup (cast p₁ ns₂) (idx ↑ˡ n₁)
+            { n = n₁ +ⁿ n₂
-            ≡⟨ lookup-cast₁ p₁ ns₂ _ ⟩
+            ; sg₂≡sg₁+n = +-assoc s₁ n₁ n₂
-              lookup ns₂ (castᶠ (sym p₁) (idx ↑ˡ n₁))
+            ; newNodes = newNodes₁ ++ newNodes₂
-            ≡⟨ g₂[]≡g₃[] _ ⟩
+            ; nsg₂≡nsg₁++newNodes = ++-assoc (+-assoc s₁ n₁ n₂) ns₁ newNodes₁ newNodes₂
-              lookup (cast p₂ ns₃) ((castᶠ (sym p₁) (idx ↑ˡ n₁)) ↑ˡ n₂)
+            ; e∈g₁⇒e∈g₂ = {!!}
-            ≡⟨ lookup-cast₁ p₂ _ _ ⟩
+            }
-              lookup ns₃ (castᶠ (sym p₂) (((castᶠ (sym p₁) (idx ↑ˡ n₁)) ↑ˡ n₂)))
-            ≡⟨ cong (lookup ns₃) (↑ˡ-assoc (sym p₂) (sym p₁) (sym (+-assoc s₁ n₁ n₂)) idx) ⟩
-              lookup ns₃ (castᶠ (sym (+-assoc s₁ n₁ n₂)) (idx ↑ˡ (n₁ +ⁿ n₂)))
-            ≡⟨ sym (lookup-cast₁ (+-assoc s₁ n₁ n₂) _ _) ⟩
-              lookup (cast (+-assoc s₁ n₁ n₂) ns₃) (idx ↑ˡ (n₁ +ⁿ n₂))
-            ∎
-        ; e∈g₁⇒e∈g₂ = {!!} -- λ e∈g₁ → e∈g₂⇒e∈g₃ (e∈g₁⇒e∈g₂ e∈g₁)
-        }
         where
             ↑ˡ-assoc : ∀ {s₁ s₂ s₃ n₁ n₂ : ℕ}
                             (p : s₂ +ⁿ n₂ ≡ s₃) (q : s₁ +ⁿ n₁ ≡ s₂)
@@ -160,7 +151,7 @@ module Graphs where
     instance
         IndexRelaxable : Relaxable Graph.Index
         IndexRelaxable = record
-            { relax = λ { (Mk-⊆ n refl _ _) idx → idx ↑ˡ n }
+            { relax = λ { (Mk-⊆ n refl _ _ _) idx → idx ↑ˡ n }
             }
 
         EdgeRelaxable : Relaxable Graph.Edge
@@ -185,9 +176,9 @@ module Graphs where
 
     relax-preserves-[]≡ : ∀ (g₁ g₂ : Graph) (g₁⊆g₂ : g₁ ⊆ g₂) (idx : Graph.Index g₁) →
                           g₁ [ idx ] ≡ g₂ [ relax g₁⊆g₂ idx ]
-    relax-preserves-[]≡ g₁ g₂ (Mk-⊆ n refl g₁[]≡g₂[] _) idx =
+    relax-preserves-[]≡ g₁ g₂ (Mk-⊆ n refl newNodes nsg₂≡nsg₁++newNodes _) idx
-        trans (g₁[]≡g₂[] idx) (cong (λ vec → lookup vec (idx ↑ˡ n))
+        rewrite cast-is-id refl (Graph.nodes g₂)
-                                    (cast-is-id refl (Graph.nodes g₂)))
+        with refl ← nsg₂≡nsg₁++newNodes = sym (lookup-++ˡ (Graph.nodes g₁) _ _)
 
     MonotonicGraphFunction : (Graph → Set) → Set
     MonotonicGraphFunction T = (g₁ : Graph) → Σ Graph (λ g₂ → T g₂ × g₁ ⊆ g₂)
@@ -228,8 +219,9 @@ module Graphs where
               , record
                   { n = 1
                   ; sg₂≡sg₁+n = refl
-                  ; g₁[]≡g₂[] = {!!} -- λ idx → trans (sym (lookup-++ˡ (Graph.nodes g) (bss ∷ []) idx)) (sym (cong (λ vec → lookup vec (idx ↑ˡ 1)) (cast-is-id refl (Graph.nodes g ++ (bss ∷ [])))))
+                  ; newNodes = (bss ∷ [])
-                  ; e∈g₁⇒e∈g₂ = λ e∈g₁ → x∈xs⇒fx∈fxs (λ e' → ↑ˡ-Edge e' 1) e∈g₁
+                  ; nsg₂≡nsg₁++newNodes = cast-is-id refl _
+                  ; e∈g₁⇒e∈g₂ = λ e∈g₁ → x∈xs⇒fx∈fxs (λ e → ↑ˡ-Edge e 1) e∈g₁
                   }
               )
             )
@@ -244,14 +236,8 @@ module Graphs where
             , record
                 { n = 0
                 ; sg₂≡sg₁+n = +-comm 0 s
-                ; g₁[]≡g₂[] = λ idx →
+                ; newNodes = []
-                    begin
+                ; nsg₂≡nsg₁++newNodes = cast-sym _ (++-identityʳ (+-comm s 0) ns)
-                        lookup ns idx
-                    ≡⟨ cong (lookup ns) (↑ˡ-identityʳ (sym (+-comm 0 s)) idx) ⟩
-                        lookup ns (castᶠ (sym (+-comm 0 s)) (idx ↑ˡ 0))
-                    ≡⟨ sym (lookup-cast₁ (+-comm 0 s) _ _) ⟩
-                        lookup (cast (+-comm 0 s) ns) (idx ↑ˡ 0)
-                    ∎
                 ; e∈g₁⇒e∈g₂ = {!!}
                 }
             )