From 04bafb2d555ac919538f622d8d95f66a69c85a96 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 10 May 2024 21:25:40 -0700 Subject: [PATCH] Prove that the inputs to wrap are empty Signed-off-by: Danila Fedorin --- Language/Properties.agda | 73 ++++++++++++++++++++++++++++++++++++---- 1 file changed, 67 insertions(+), 6 deletions(-) diff --git a/Language/Properties.agda b/Language/Properties.agda index b1309a8..b777adc 100644 --- a/Language/Properties.agda +++ b/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₂ ρ₁ ρ₂ →