From 85fdf544b9c23671ad34f843323b5e348783f921 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 8 Apr 2024 20:57:08 -0700 Subject: [PATCH] Translate informal proof of (node) transitivity into formal one. Signed-off-by: Danila Fedorin --- Language.agda | 53 +++++++++++++++++++++++++++------------------------ 1 file changed, 28 insertions(+), 25 deletions(-) diff --git a/Language.agda b/Language.agda index ce3b1a4..202acf5 100644 --- a/Language.agda +++ b/Language.agda @@ -6,7 +6,7 @@ open import Data.Integer using (ℤ; +_) renaming (_+_ to _+ᶻ_; _-_ to _-ᶻ_) open import Data.String using (String) renaming (_≟_ to _≟ˢ_) open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂) open import Data.Vec using (Vec; foldr; lookup; _∷_; []; _++_; cast) -open import Data.Vec.Properties using (++-assoc; ++-identityʳ; lookup-++ˡ) +open import Data.Vec.Properties using (++-assoc; ++-identityʳ; lookup-++ˡ; lookup-cast₁) open import Data.Vec.Relation.Binary.Equality.Cast using (cast-is-id) open import Data.List using ([]; _∷_; List) renaming (foldr to foldrˡ; map to mapˡ; _++_ to _++ˡ_) open import Data.List.Properties using () renaming (++-assoc to ++ˡ-assoc; map-++ to mapˡ-++ˡ; ++-identityʳ to ++ˡ-identityʳ) @@ -19,7 +19,7 @@ open import Data.Fin.Properties using (suc-injective) open import Relation.Binary.PropositionalEquality as Eq using (subst; cong; _≡_; sym; trans; refl) open import Relation.Nullary using (¬_) open import Function using (_∘_) -open Eq.≡-Reasoning using (begin_; step-≡; _∎) +open Eq.≡-Reasoning open import Lattice open import Utils using (Unique; Unique-map; empty; push; x∈xs⇒fx∈fxs; _⊗_; _,_) @@ -121,36 +121,39 @@ module Graphs where e ∈ˡ (Graph.edges g₁) → (↑ˡ-Edge e n) ∈ˡ (subst (λ m → List (Fin m × Fin m)) sg₂≡sg₁+n (Graph.edges g₂)) - flatten-casts : ∀ {s₁ s₂ s₃ n₁ n₂ : ℕ} - (p : s₂ +ⁿ n₂ ≡ s₃) (q : s₁ +ⁿ n₁ ≡ s₂) (r : s₁ +ⁿ (n₁ +ⁿ n₂) ≡ s₃) - (idx : Fin s₁) → - castᶠ p ((castᶠ q (idx ↑ˡ n₁)) ↑ˡ n₂) ≡ castᶠ r (idx ↑ˡ (n₁ +ⁿ n₂)) - flatten-casts refl refl r zero = refl - flatten-casts {(suc s₁)} {s₂} {s₃} {n₁} {n₂} refl refl r (suc idx') - rewrite flatten-casts refl refl (sym (+-assoc s₁ n₁ n₂)) idx' = refl - ⊆-trans : ∀ {g₁ g₂ g₃ : Graph} → g₁ ⊆ g₂ → g₂ ⊆ g₃ → g₁ ⊆ g₃ ⊆-trans {MkGraph s₁ ns₁ es₁} {MkGraph s₂ ns₂ es₂} {MkGraph s₃ ns₃ es₃} (Mk-⊆ n₁ p₁@refl g₁[]≡g₂[] e∈g₁⇒e∈g₂) (Mk-⊆ n₂ p₂@refl g₂[]≡g₃[] e∈g₂⇒e∈g₃) = record { n = n₁ +ⁿ n₂ ; sg₂≡sg₁+n = +-assoc s₁ n₁ n₂ - ; g₁[]≡g₂[] = {!!} + ; g₁[]≡g₂[] = λ idx → + begin + lookup ns₁ idx + ≡⟨ g₁[]≡g₂[] _ ⟩ + lookup (cast p₁ ns₂) (idx ↑ˡ n₁) + ≡⟨ lookup-cast₁ p₁ ns₂ _ ⟩ + lookup ns₂ (castᶠ (sym p₁) (idx ↑ˡ n₁)) + ≡⟨ g₂[]≡g₃[] _ ⟩ + lookup (cast p₂ ns₃) ((castᶠ (sym p₁) (idx ↑ˡ n₁)) ↑ˡ n₂) + ≡⟨ lookup-cast₁ p₂ _ _ ⟩ + lookup ns₃ (castᶠ (sym p₂) (((castᶠ (sym p₁) (idx ↑ˡ n₁)) ↑ˡ n₂))) + ≡⟨ cong (lookup ns₃) (flatten-casts (sym p₂) (sym p₁) (sym (+-assoc s₁ n₁ n₂)) idx) ⟩ + lookup ns₃ (castᶠ (sym (+-assoc s₁ n₁ n₂)) (idx ↑ˡ (n₁ +ⁿ n₂))) + ≡⟨ sym (lookup-cast₁ (+-assoc s₁ n₁ n₂) _ _) ⟩ + lookup (cast (+-assoc s₁ n₁ n₂) ns₃) (idx ↑ˡ (n₁ +ⁿ n₂)) + ∎ ; e∈g₁⇒e∈g₂ = {!!} - -- lookup ns₁ idx ≡ lookup (cast p₁ ns₂) (idx ↑ˡ n) -- by g₁[]≡g₂[] - - -- lookup (cast p₁ ns₂) (idx ↑ˡ n) ≡ lookup ns₂ (Fin.cast (sym p₁) (idx ↑ˡ n)) -- by lookup-cast₁ - -- -------- s₁ + n₁ → s₂ - -- ---------- Fin (s₁ + n₁) - -- ----------------------------- Fin s₂ - - -- lookup ns₂ (Fin.cast (sym p₁) (idx ↑ˡ n)) ≡ lookup (cast p₂ ns₃) ((Fin.cast (sym p₁) (idx ↑ˡ n₁) ↑ˡ n₂)) -- by g₂[]≡g₃[] - - -- lookup (cast p₂ ns₃) ((Fin.cast (sym p₁) (idx ↑ˡ n₁) ↑ˡ n₂)) ≡ lookup ns₃ (Fin.cast (sym p₂) ((Fin.cast (sym p₁) (idx ↑ˡ n₁) ↑ˡ n₂))) -- by lookup-cast₂ - - -- lookup ns₃ (Fin.cast (sym p₂) ((Fin.cast (sym p₁) (idx ↑ˡ n₁) ↑ˡ n₂))) ≡ lookup ns₃ (Fin.cast (sym (+-assoc s₁ n₁ n₂)) (idx ↑ˡ (n₁ + n₂))) -- by flatten-casts - -- - -- lookup ns₃ (Fin.cast (sym (+-assoc s₁ n₁ n₂)) (idx ↑ˡ (n₁ + n₂))) ≡ lookup (cast (+-assoc s₁ n₁ n₂) ns₃) (idx ↑ˡ (n₁ + n₂)) ∎ } + where + flatten-casts : ∀ {s₁ s₂ s₃ n₁ n₂ : ℕ} + (p : s₂ +ⁿ n₂ ≡ s₃) (q : s₁ +ⁿ n₁ ≡ s₂) + (r : s₁ +ⁿ (n₁ +ⁿ n₂) ≡ s₃) + (idx : Fin s₁) → + castᶠ p ((castᶠ q (idx ↑ˡ n₁)) ↑ˡ n₂) ≡ castᶠ r (idx ↑ˡ (n₁ +ⁿ n₂)) + flatten-casts refl refl r zero = refl + flatten-casts {(suc s₁)} {s₂} {s₃} {n₁} {n₂} refl refl r (suc idx') + rewrite flatten-casts refl refl (sym (+-assoc s₁ n₁ n₂)) idx' = refl + record Relaxable (T : Graph → Set) : Set where field relax : ∀ {g₁ g₂ : Graph} → g₁ ⊆ g₂ → T g₁ → T g₂