Simplify proofs about 'loop' using concatenation lemma

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

Language/Properties.agda

@@ -8,6 +8,7 @@ open import Language.Traces
 open import Data.Fin as Fin using (suc; zero)
 open import Data.List as List using (List; _∷_; [])
 open import Data.List.Relation.Unary.Any using (here; there)
+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.Vec as Vec using (_∷_)
@@ -15,7 +16,7 @@ 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 Utils using (x∈xs⇒fx∈fxs; ∈-cartesianProduct)
+open import Utils using (x∈xs⇒fx∈fxs; ∈-cartesianProduct; concat-∈)
 
 
 buildCfg-input : ∀ (s : Stmt) → let g = buildCfg s in Σ (Graph.Index g) (λ idx → Graph.inputs g ≡ idx ∷ [])
@@ -108,6 +109,19 @@ Trace-↦ʳ {g₁} {g₂} {idx₁} (Trace-edge ρ₁⇒ρ idx₁→idx tr')
                                         (ListMemProp.∈-++⁺ˡ (x∈xs⇒fx∈fxs (Graph.size g₁ ↑ʳ_) idx₁→idx)))
                     (Trace-↦ʳ {g₁} {g₂} tr')
 
+loop-edge-groups : ∀ (g : Graph) → List (List (Graph.Edge (loop g)))
+loop-edge-groups g =
+    (2 ↑ʳᵉ Graph.edges g) ∷
+    (List.map (zero ,_) (2 ↑ʳⁱ Graph.inputs g)) ∷
+    (List.map (_, suc zero) (2 ↑ʳⁱ Graph.outputs g)) ∷
+    ((suc zero , zero) ∷ (zero , suc zero) ∷ []) ∷
+    []
+
+loop-edge-help : ∀ (g : Graph) {l : List (Graph.Edge (loop g))} {e : Graph.Edge (loop g)} →
+                 e ListMem.∈ l → l ListMem.∈ loop-edge-groups g →
+                 e ListMem.∈ Graph.edges (loop g)
+loop-edge-help g e∈l l∈ess = concat-∈ e∈l l∈ess
+
 Trace-loop : ∀ {g : Graph} {idx₁ idx₂ : Graph.Index g} {ρ₁ ρ₂ : Env} →
              Trace {g} idx₁ idx₂ ρ₁ ρ₂ → Trace {loop g} (2 Fin.↑ʳ idx₁) (2 Fin.↑ʳ idx₂) ρ₁ ρ₂
 Trace-loop {g} {idx₁} {idx₁} (Trace-single ρ₁⇒ρ₂)
@@ -122,8 +136,14 @@ EndToEndTrace-loop : ∀ {g : Graph} {ρ₁ ρ₂ : Env} →
                      EndToEndTrace {g} ρ₁ ρ₂ → EndToEndTrace {loop g} ρ₁ ρ₂
 EndToEndTrace-loop {g} etr =
     let
-        zero→idx₁ = ListMemProp.∈-++⁺ʳ (2 ↑ʳᵉ Graph.edges g) (ListMemProp.∈-++⁺ˡ (x∈xs⇒fx∈fxs (zero ,_) (x∈xs⇒fx∈fxs (2 Fin.↑ʳ_) (EndToEndTrace.idx₁∈inputs etr))))
+        zero→idx₁' = x∈xs⇒fx∈fxs (zero ,_)
-        idx₂→suc = ListMemProp.∈-++⁺ʳ (2 ↑ʳᵉ Graph.edges g) (ListMemProp.∈-++⁺ʳ (List.map (zero ,_) (2 ↑ʳⁱ Graph.inputs g)) (ListMemProp.∈-++⁺ˡ (x∈xs⇒fx∈fxs (_, suc zero) (x∈xs⇒fx∈fxs (2 Fin.↑ʳ_) (EndToEndTrace.idx₂∈outputs etr)))))
+                                 (x∈xs⇒fx∈fxs (2 Fin.↑ʳ_)
+                                              (EndToEndTrace.idx₁∈inputs etr))
+        zero→idx₁ = loop-edge-help g zero→idx₁' (there (here refl))
+        idx₂→suc' = x∈xs⇒fx∈fxs (_, suc zero)
+                               (x∈xs⇒fx∈fxs (2 Fin.↑ʳ_)
+                                            (EndToEndTrace.idx₂∈outputs etr))
+        idx₂→suc = loop-edge-help g idx₂→suc' (there (there (here refl)))
     in
         record
             { idx₁ = zero
@@ -143,7 +163,8 @@ EndToEndTrace-loop² : ∀ {g : Graph} {ρ₁ ρ₂ ρ₃ : Env} →
 EndToEndTrace-loop² {g} (MkEndToEndTrace zero (here refl) (suc zero) (here refl) tr₁)
                         (MkEndToEndTrace zero (here refl) (suc zero) (here refl) tr₂) =
     let
-        suc→zero = ListMemProp.∈-++⁺ʳ (2 ↑ʳᵉ Graph.edges g) (ListMemProp.∈-++⁺ʳ (List.map (zero ,_) (2 ↑ʳⁱ Graph.inputs g)) (ListMemProp.∈-++⁺ʳ (List.map (_, suc zero) (2 ↑ʳⁱ Graph.outputs g)) (here refl)))
+        suc→zero = loop-edge-help g (here refl)
+                                    (there (there (there (here refl))))
     in
         record
             { idx₁ = zero
@@ -157,7 +178,8 @@ EndToEndTrace-loop⁰ : ∀ {g : Graph} {ρ : Env} →
                       EndToEndTrace {loop g} ρ ρ
 EndToEndTrace-loop⁰ {g} {ρ} =
     let
-        zero→suc = ListMemProp.∈-++⁺ʳ (2 ↑ʳᵉ Graph.edges g) (ListMemProp.∈-++⁺ʳ (List.map (zero ,_) (2 ↑ʳⁱ Graph.inputs g)) (ListMemProp.∈-++⁺ʳ (List.map (_, suc zero) (2 ↑ʳⁱ Graph.outputs g)) (there (here refl))))
+        zero→suc = loop-edge-help g (there (here refl))
+                                    (there (there (there (here refl))))
     in
         record
             { idx₁ = zero

Utils.agda

@@ -3,7 +3,7 @@ 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; []; _∷_; _++_) renaming (map to mapˡ)
+open import Data.List using (List; cartesianProduct; []; _∷_; _++_; foldr) 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)
@@ -86,3 +86,8 @@ proj₂ (_ , v) = v
                      x ∈ xs → y ∈ ys → (x Prod., y) ∈ cartesianProduct xs ys
 ∈-cartesianProduct {x = x} (here refl) y∈ys = ListMemProp.∈-++⁺ˡ (x∈xs⇒fx∈fxs (x Prod.,_) y∈ys)
 ∈-cartesianProduct {x = x} {xs = x' ∷ _} {ys = ys} (there x∈rest) y∈ys = ListMemProp.∈-++⁺ʳ (mapˡ (x' Prod.,_) ys) (∈-cartesianProduct x∈rest y∈ys)
+
+concat-∈ : ∀ {a} {A : Set a} {x : A} {l : List A} {ls : List (List A)} →
+           x ∈ l → l ∈ ls → x ∈ foldr _++_ [] ls
+concat-∈ x∈l (here refl) = ListMemProp.∈-++⁺ˡ x∈l
+concat-∈ {ls = l' ∷ ls'} x∈l (there l∈ls') = ListMemProp.∈-++⁺ʳ l' (concat-∈ x∈l l∈ls')