From 91b5d108f61a37dda9dfa5d2667fa3da47b4c4c0 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 29 Apr 2024 21:28:21 -0700 Subject: [PATCH] Simplify proofs about 'loop' using concatenation lemma Signed-off-by: Danila Fedorin --- Language/Properties.agda | 32 +++++++++++++++++++++++++++----- Utils.agda | 7 ++++++- 2 files changed, 33 insertions(+), 6 deletions(-) diff --git a/Language/Properties.agda b/Language/Properties.agda index b282460..ca82ec7 100644 --- a/Language/Properties.agda +++ b/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)))) - 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))))) + zero→idx₁' = x∈xs⇒fx∈fxs (zero ,_) + (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 diff --git a/Utils.agda b/Utils.agda index d1c7c09..60edd25 100644 --- a/Utils.agda +++ b/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')