Prove that the inputs to wrap are empty

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

Language/Properties.agda

@@ -6,23 +6,84 @@ open import Language.Graphs
 open import Language.Traces
 
 open import Data.Fin as Fin using (suc; zero)
+open import Data.Fin.Properties as FinProp using (suc-injective)
 open import Data.List as List using (List; _∷_; [])
+open import Data.List.Properties using (filter-none)
 open import Data.List.Relation.Unary.Any using (here; there)
+open import Data.List.Relation.Unary.All using (All; []; _∷_; map; tabulate)
 open import Data.List.Membership.Propositional as ListMem using ()
 open import Data.List.Membership.Propositional.Properties as ListMemProp using ()
-open import Data.Product using (Σ; _,_; _×_)
+open import Data.Nat as Nat using ()
+open import Data.Product using (Σ; _,_; _×_; proj₂)
+open import Data.Product.Properties as ProdProp using ()
+open import Data.Sum using (inj₁; inj₂)
 open import Data.Vec as Vec using (_∷_)
 open import Data.Vec.Properties using (lookup-++ˡ; ++-identityʳ; lookup-++ʳ)
 open import Function using (_∘_)
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; cong)
+open import Relation.Nullary using (¬_)
 
 open import Utils using (x∈xs⇒fx∈fxs; ∈-cartesianProduct; concat-∈)
 
-wrap-input : ∀ (g : Graph) → Σ (Graph.Index (wrap g)) (λ idx → Graph.inputs (wrap g) ≡ idx ∷ [])
-wrap-input g = (_ , refl)
+-- All of the below helpers are to reason about what edges aren't included
+-- when combinings graphs. The currenty most important use for this is proving
+-- that the entry node has no incoming edges.
+--
+-- -------------- Begin ugly code to make this work ----------------
+↑-≢ : ∀ {n m} (f₁ : Fin.Fin n) (f₂ : Fin.Fin m) → ¬ (f₁ Fin.↑ˡ m) ≡ (n Fin.↑ʳ f₂)
+↑-≢ zero f₂ ()
+↑-≢ (suc f₁') f₂ f₁≡f₂ = ↑-≢ f₁' f₂ (suc-injective f₁≡f₂)
 
-wrap-output : ∀ (g : Graph) → Σ (Graph.Index (wrap g)) (λ idx → Graph.outputs (wrap g) ≡ idx ∷ [])
-wrap-output g = (_ , refl)
+idx→f∉↑ʳᵉ : ∀ {n m} (idx : Fin.Fin (n Nat.+ m)) (f : Fin.Fin n) (es₂ : List (Fin.Fin m × Fin.Fin m)) → ¬ (idx , f Fin.↑ˡ m) ListMem.∈ (n ↑ʳᵉ es₂)
+idx→f∉↑ʳᵉ idx f ((idx₁ , idx₂) ∷ es') (here idx,f≡idx₁,idx₂) = ↑-≢ f idx₂ (cong proj₂ idx,f≡idx₁,idx₂)
+idx→f∉↑ʳᵉ idx f (_ ∷ es₂') (there idx→f∈es₂') = idx→f∉↑ʳᵉ idx f es₂' idx→f∈es₂'
+
+idx→f∉pair : ∀ {n m} (idx idx' : Fin.Fin (n Nat.+ m)) (f : Fin.Fin n) (inputs₂ : List (Fin.Fin m)) → ¬ (idx , f Fin.↑ˡ m) ListMem.∈ (List.map (idx' ,_) (n ↑ʳⁱ inputs₂))
+idx→f∉pair idx idx' f [] ()
+idx→f∉pair idx idx' f (input ∷ inputs') (here idx,f≡idx',input) = ↑-≢ f input (cong proj₂ idx,f≡idx',input)
+idx→f∉pair idx idx' f (_ ∷ inputs₂') (there idx,f∈inputs₂') = idx→f∉pair idx idx' f inputs₂' idx,f∈inputs₂'
+
+idx→f∉cart : ∀ {n m} (idx : Fin.Fin (n Nat.+ m)) (f : Fin.Fin n) (outputs₁ : List (Fin.Fin n)) (inputs₂ : List (Fin.Fin m)) → ¬ (idx , f Fin.↑ˡ m) ListMem.∈ (List.cartesianProduct (outputs₁ ↑ˡⁱ m) (n ↑ʳⁱ inputs₂))
+idx→f∉cart idx f [] inputs₂ ()
+idx→f∉cart {n} {m} idx f (output ∷ outputs₁') inputs₂ idx,f∈pair++cart
+    with ListMemProp.∈-++⁻ (List.map (output Fin.↑ˡ m ,_) (n ↑ʳⁱ inputs₂)) idx,f∈pair++cart
+...   | inj₁ idx,f∈pair = idx→f∉pair idx (output Fin.↑ˡ m) f inputs₂ idx,f∈pair
+...   | inj₂ idx,f∈cart = idx→f∉cart idx f outputs₁' inputs₂ idx,f∈cart
+
+help : let g₁ = singleton [] in
+       ∀ (g₂ : Graph) (idx₁ : Graph.Index g₁) (idx : Graph.Index (g₁ ↦ g₂)) →
+       ¬ (idx , idx₁ Fin.↑ˡ Graph.size g₂) ListMem.∈ ((Graph.size g₁ ↑ʳᵉ Graph.edges g₂) List.++
+                                                      (List.cartesianProduct (Graph.outputs g₁ ↑ˡⁱ Graph.size g₂)
+                                                                             (Graph.size g₁ ↑ʳⁱ Graph.inputs g₂)))
+help g₂ idx₁ idx idx,idx₁∈g
+    with ListMemProp.∈-++⁻ (Graph.size (singleton []) ↑ʳᵉ Graph.edges g₂) idx,idx₁∈g
+...   | inj₁ idx,idx₁∈edges₂ = idx→f∉↑ʳᵉ idx idx₁ (Graph.edges g₂) idx,idx₁∈edges₂
+...   | inj₂ idx,idx₁∈cart = idx→f∉cart idx idx₁ (Graph.outputs (singleton [])) (Graph.inputs g₂) idx,idx₁∈cart
+
+helpAll : let g₁ = singleton [] in
+       ∀ (g₂ : Graph) (idx₁ : Graph.Index g₁) →
+       All (λ idx → ¬ (idx , idx₁ Fin.↑ˡ Graph.size g₂) ListMem.∈ ((Graph.size g₁ ↑ʳᵉ Graph.edges g₂) List.++
+                                                                   (List.cartesianProduct (Graph.outputs g₁ ↑ˡⁱ Graph.size g₂)
+                                                                                          (Graph.size g₁ ↑ʳⁱ Graph.inputs g₂)))) (indices (g₁ ↦ g₂))
+helpAll g₂ idx₁ = tabulate (λ {idx} _ → help g₂ idx₁ idx)
+
+module _ (g : Graph) where
+    wrap-preds-∅ : (idx : Graph.Index (wrap g)) →
+                   idx ListMem.∈ Graph.inputs (wrap g) → predecessors (wrap g) idx ≡ []
+    wrap-preds-∅ zero (here refl) =
+        filter-none (λ idx' → (idx' , zero) ∈?
+                              (Graph.edges (wrap g)))
+                    (helpAll (g ↦ singleton []) zero)
+        where open import Data.List.Membership.DecPropositional (ProdProp.≡-dec (FinProp._≟_ {Graph.size (wrap g)}) (FinProp._≟_ {Graph.size (wrap g)})) using (_∈?_)
+-- -------------- End ugly code to make this work ----------------
+
+
+module _ (g : Graph) where
+    wrap-input : Σ (Graph.Index (wrap g)) (λ idx → Graph.inputs (wrap g) ≡ idx ∷ [])
+    wrap-input = (_ , refl)
+
+    wrap-output : Σ (Graph.Index (wrap g)) (λ idx → Graph.outputs (wrap g) ≡ idx ∷ [])
+    wrap-output = (_ , refl)
 
 Trace-∙ˡ : ∀ {g₁ g₂ : Graph} {idx₁ idx₂ : Graph.Index g₁} {ρ₁ ρ₂ : Env} →
            Trace {g₁} idx₁ idx₂ ρ₁ ρ₂ →