Prove that predecessors imply edges

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

Language.agda

@@ -86,6 +86,4 @@ record Program : Set where
 
     edge⇒incoming : ∀ {s₁ s₂ : State} → (s₁ , s₂) ListMem.∈ (Graph.edges graph) →
                     s₁ ListMem.∈ (incoming s₂)
-    edge⇒incoming {s₁} {s₂} s₁,s₂∈es =
-        ∈-filter⁺ (λ s' → (s' , s₂) ∈? (Graph.edges graph))
-                  (states-complete s₁) s₁,s₂∈es
+    edge⇒incoming = edge⇒predecessor graph

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 ()
+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)
@@ -161,3 +161,14 @@ module _ (g : Graph) where
 
     predecessors : (Graph.Index g) → List (Graph.Index g)
     predecessors idx = List.filter (λ idx' → (idx' , idx) ∈? (Graph.edges g)) indices
+
+    edge⇒predecessor : ∀ {idx₁ idx₂ : Graph.Index g} → (idx₁ , idx₂) ListMem.∈ (Graph.edges g) →
+                    idx₁ ListMem.∈ (predecessors idx₂)
+    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 )

Utils.agda

@@ -3,15 +3,16 @@ module Utils where
 open import Agda.Primitive using () renaming (_⊔_ to _⊔ℓ_)
 open import Data.Product as Prod using (_×_)
 open import Data.Nat using (ℕ; suc)
-open import Data.List using (List; cartesianProduct; []; _∷_; _++_; foldr) renaming (map to mapˡ)
+open import Data.List using (List; cartesianProduct; []; _∷_; _++_; foldr; filter) renaming (map to mapˡ)
 open import Data.List.Membership.Propositional using (_∈_)
 open import Data.List.Membership.Propositional.Properties as ListMemProp using ()
 open import Data.List.Relation.Unary.All using (All; []; _∷_; map)
 open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map
 open import Data.Sum using (_⊎_)
 open import Function.Definitions using (Injective)
-open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl)
-open import Relation.Nullary using (¬_)
+open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl; cong)
+open import Relation.Nullary using (¬_; yes; no)
+open import Relation.Unary using (Decidable)
 
 data Unique {c} {C : Set c} : List C → Set c where
     empty : Unique []
@@ -83,6 +84,14 @@ concat-∈ : ∀ {a} {A : Set a} {x : A} {l : List A} {ls : List (List A)} →
 concat-∈ x∈l (here refl) = ListMemProp.∈-++⁺ˡ x∈l
 concat-∈ {ls = l' ∷ ls'} x∈l (there l∈ls') = ListMemProp.∈-++⁺ʳ l' (concat-∈ x∈l l∈ls')
 
+filter-++ : ∀ {a p} {A : Set a} (l₁ l₂ : List A) {P : A → Set p} (P? : Decidable P) →
+            filter P? (l₁ ++ l₂) ≡ filter P? l₁ ++ filter P? l₂
+filter-++ [] l₂ P? = refl
+filter-++ (x ∷ xs) l₂ P?
+    with P? x
+...   | yes _ = cong (x ∷_) (filter-++ xs l₂ P?)
+...   | no _ = (filter-++ xs l₂ P?)
+
 _⇒_ : ∀ {a p₁ p₂} {A : Set a} (P : A → Set p₁) (Q : A → Set p₂) →
       Set (a ⊔ℓ p₁ ⊔ℓ p₂)
 _⇒_ P Q = ∀ a → P a → Q a