From e0248397b778e07e446951770a1e9e0949050bfe Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 9 May 2024 23:18:51 -0700 Subject: [PATCH] Prove that predecessors imply edges Signed-off-by: Danila Fedorin --- Language/Graphs.agda | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/Language/Graphs.agda b/Language/Graphs.agda index fdf826c..e294eea 100644 --- a/Language/Graphs.agda +++ b/Language/Graphs.agda @@ -6,7 +6,7 @@ open import Data.Fin as Fin using (Fin; suc; zero) open import Data.Fin.Properties as FinProp using (suc-injective) open import Data.List as List using (List; []; _∷_) open import Data.List.Membership.Propositional as ListMem using () -open import Data.List.Membership.Propositional.Properties as ListMemProp using (∈-filter⁺) +open import Data.List.Membership.Propositional.Properties as ListMemProp using (∈-filter⁺; ∈-filter⁻) open import Data.List.Relation.Unary.All using (All; []; _∷_) open import Data.List.Relation.Unary.Any as RelAny using () open import Data.Nat as Nat using (ℕ; suc) @@ -167,3 +167,8 @@ module _ (g : Graph) where edge⇒predecessor {idx₁} {idx₂} idx₁,idx₂∈es = ∈-filter⁺ (λ idx' → (idx' , idx₂) ∈? (Graph.edges g)) (indices-complete idx₁) idx₁,idx₂∈es + + predecessor⇒edge : ∀ {idx₁ idx₂ : Graph.Index g} → idx₁ ListMem.∈ (predecessors idx₂) → + (idx₁ , idx₂) ListMem.∈ (Graph.edges g) + predecessor⇒edge {idx₁} {idx₂} idx₁∈pred = + proj₂ (∈-filter⁻ (λ idx' → (idx' , idx₂) ∈? (Graph.edges g)) {v = idx₁} {xs = indices} idx₁∈pred )