Add proof of node preservation for adding edges.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-04-08 22:43:07 -07:00
parent 85fdf544b9
commit 78252b6c9e

View File

@ -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 []