From 78252b6c9e2ab1904e9b5d30183da3bafded0f18 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Mon, 8 Apr 2024 22:43:07 -0700
Subject: [PATCH] Add proof of node preservation for adding edges.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Language.agda | 42 +++++++++++++++++++++++++++---------------
 1 file changed, 27 insertions(+), 15 deletions(-)

diff --git a/Language.agda b/Language.agda
index 202acf5..e769597 100644
--- a/Language.agda
+++ b/Language.agda
@@ -117,7 +117,7 @@ module Graphs where
             g₁[]≡g₂[] : ∀ (idx : Graph.Index g₁) →
                         lookup (Graph.nodes g₁) idx ≡
                         lookup (cast sg₂≡sg₁+n (Graph.nodes g₂)) (idx ↑ˡ n)
-            e∈g₁⇒e∈g₂ : ∀ (e : Graph.Edge g₁) →
+            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₂))
 
@@ -137,23 +137,22 @@ module Graphs where
               lookup (cast p₂ ns₃) ((castᶠ (sym p₁) (idx ↑ˡ n₁)) ↑ˡ n₂)
             ≡⟨ lookup-cast₁ p₂ _ _ ⟩
               lookup ns₃ (castᶠ (sym p₂) (((castᶠ (sym p₁) (idx ↑ˡ n₁)) ↑ˡ n₂)))
-            ≡⟨ cong (lookup ns₃) (flatten-casts (sym p₂) (sym p₁) (sym (+-assoc s₁ n₁ n₂)) idx) ⟩
+            ≡⟨ 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₁⇒e∈g₂ e∈g₁)
         }
         where
-            flatten-casts : ∀ {s₁ s₂ s₃ n₁ n₂ : ℕ}
+            ↑ˡ-assoc : ∀ {s₁ s₂ s₃ n₁ n₂ : ℕ}
                             (p : s₂ +ⁿ n₂ ≡ s₃) (q : s₁ +ⁿ n₁ ≡ s₂)
                             (r : s₁ +ⁿ (n₁ +ⁿ n₂) ≡ s₃)
                             (idx : Fin s₁) →
                             castᶠ p ((castᶠ q (idx ↑ˡ n₁)) ↑ˡ n₂) ≡ castᶠ r (idx ↑ˡ (n₁ +ⁿ n₂))
-            flatten-casts refl refl r zero = refl
-            flatten-casts {(suc s₁)} {s₂} {s₃} {n₁} {n₂} refl refl r (suc idx')
-                rewrite flatten-casts refl refl (sym (+-assoc s₁ n₁ n₂)) idx' = refl
-
+            ↑ˡ-assoc refl refl r zero = refl
+            ↑ˡ-assoc {(suc s₁)} {s₂} {s₃} {n₁} {n₂} refl refl r (suc idx')
+                rewrite ↑ˡ-assoc refl refl (sym (+-assoc s₁ n₁ n₂)) idx' = refl
 
     record Relaxable (T : Graph → Set) : Set where
         field relax : ∀ {g₁ g₂ : Graph} → g₁ ⊆ g₂ → T g₁ → T g₂
@@ -230,25 +229,38 @@ module Graphs where
                   { 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 ∷ [])))))
-                  ; e∈g₁⇒e∈g₂ = λ e e∈g₁ → x∈xs⇒fx∈fxs (λ e' → ↑ˡ-Edge e' 1) e∈g₁
+                  ; e∈g₁⇒e∈g₂ = λ e∈g₁ → x∈xs⇒fx∈fxs (λ e' → ↑ˡ-Edge e' 1) e∈g₁
                   }
               )
             )
 
         addEdges : ∀ (g : Graph) → List (Graph.Edge g) → Σ Graph (λ g' → g ⊆ g')
-        addEdges g es =
+        addEdges (MkGraph s ns es) es' =
             ( record
-                { size = Graph.size g
-                ; nodes = Graph.nodes g
-                ; edges = es ++ˡ Graph.edges g
+                { size = s
+                ; nodes = ns
+                ; edges = es' ++ˡ es
                 }
             , record
                 { n = 0
-                ; sg₂≡sg₁+n = +-comm 0 (Graph.size g)
-                ; g₁[]≡g₂[] = {!!}
+                ; sg₂≡sg₁+n = +-comm 0 s
+                ; g₁[]≡g₂[] = λ idx →
+                    begin
+                        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₂ = {!!}
                 }
             )
+            where
+                ↑ˡ-identityʳ : ∀ {s} (p : s +ⁿ 0 ≡ s) (idx : Fin s) →
+                           idx ≡ castᶠ p (idx ↑ˡ 0)
+                ↑ˡ-identityʳ p zero = refl
+                ↑ˡ-identityʳ {suc s'} p (suc f')
+                    rewrite sym (↑ˡ-identityʳ (+-comm s' 0) f') = refl
 
         pushEmptyBlock : MonotonicGraphFunction Graph.Index
         pushEmptyBlock = pushBasicBlock []