DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Reorder some definitions

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-04-12 23:27:17 -07:00
parent 57606636a7
commit 71cb97ad8c
1 changed files with 17 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
Language.agda
View File

@ -104,12 +104,26 @@ module Graphs where
nodes : Vec (List BasicStmt) size nodes : Vec (List BasicStmt) size
edges : List Edge edges : List Edge
castᵉ : ∀ {n m : ℕ} .(p : n ≡ m) → (Fin n × Fin n) → (Fin m × Fin m)
castᵉ p (idx₁ , idx₂) = (castᶠ p idx₁ , castᶠ p idx₂)
↑ˡ-Edge : ∀ {n} → (Fin n × Fin n) → ∀ m → (Fin (n +ⁿ m) × Fin (n +ⁿ m)) ↑ˡ-Edge : ∀ {n} → (Fin n × Fin n) → ∀ m → (Fin (n +ⁿ m) × Fin (n +ⁿ m))
↑ˡ-Edge (idx₁ , idx₂) m = (idx₁ ↑ˡ m , idx₂ ↑ˡ m) ↑ˡ-Edge (idx₁ , idx₂) m = (idx₁ ↑ˡ m , idx₂ ↑ˡ m)
_[_] : ∀ (g : Graph) → Graph.Index g → List BasicStmt
_[_] g idx = lookup (Graph.nodes g) idx
record _⊆_ (g₁ g₂ : Graph) : Set where
constructor Mk-⊆
field
n : ℕ
sg₂≡sg₁+n : Graph.size g₂ ≡ Graph.size g₁ +ⁿ n
newNodes : Vec (List BasicStmt) n
nsg₂≡nsg₁++newNodes : cast sg₂≡sg₁+n (Graph.nodes g₂) ≡ Graph.nodes g₁ ++ newNodes
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₂))
castᵉ : ∀ {n m : ℕ} .(p : n ≡ m) → (Fin n × Fin n) → (Fin m × Fin m)
castᵉ p (idx₁ , idx₂) = (castᶠ p idx₁ , castᶠ p idx₂)
↑ˡ-assoc : ∀ {s n₁ n₂} (f : Fin s) (p : s +ⁿ (n₁ +ⁿ n₂) ≡ s +ⁿ n₁ +ⁿ n₂) → ↑ˡ-assoc : ∀ {s n₁ n₂} (f : Fin s) (p : s +ⁿ (n₁ +ⁿ n₂) ≡ s +ⁿ n₁ +ⁿ n₂) →
f ↑ˡ n₁ ↑ˡ n₂ ≡ castᶠ p (f ↑ˡ (n₁ +ⁿ n₂)) f ↑ˡ n₁ ↑ˡ n₂ ≡ castᶠ p (f ↑ˡ (n₁ +ⁿ n₂))
↑ˡ-assoc zero p = refl ↑ˡ-assoc zero p = refl
@ -140,20 +154,6 @@ module Graphs where
rewrite castᶠ-is-id refl idx₁ rewrite castᶠ-is-id refl idx₁
rewrite castᶠ-is-id refl idx₂ = e∈es rewrite castᶠ-is-id refl idx₂ = e∈es
_[_] : ∀ (g : Graph) → Graph.Index g → List BasicStmt
_[_] g idx = lookup (Graph.nodes g) idx
record _⊆_ (g₁ g₂ : Graph) : Set where
constructor Mk-⊆
field
n : ℕ
sg₂≡sg₁+n : Graph.size g₂ ≡ Graph.size g₁ +ⁿ n
newNodes : Vec (List BasicStmt) n
nsg₂≡nsg₁++newNodes : cast sg₂≡sg₁+n (Graph.nodes g₂) ≡ Graph.nodes g₁ ++ newNodes
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 : ∀ {g₁ g₂ g₃ : Graph} → g₁ ⊆ g₂ → g₂ ⊆ g₃ → g₁ ⊆ g₃
⊆-trans {MkGraph s₁ ns₁ es₁} {MkGraph s₂ ns₂ es₂} {MkGraph s₃ ns₃ es₃} ⊆-trans {MkGraph s₁ ns₁ es₁} {MkGraph s₂ ns₂ es₂} {MkGraph s₃ ns₃ es₃}
(Mk-⊆ n₁ p₁@refl newNodes₁ nsg₂≡nsg₁++newNodes₁ e∈g₁⇒e∈g₂) (Mk-⊆ n₁ p₁@refl newNodes₁ nsg₂≡nsg₁++newNodes₁ e∈g₁⇒e∈g₂)