From 4f14a7b7658084bcd0d250722d4d25b08ee6aef3 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 8 Apr 2024 00:24:52 -0700 Subject: [PATCH] Successfully prove that monotonic updates preserve existing indices Signed-off-by: Danila Fedorin --- Language.agda | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/Language.agda b/Language.agda index 3b593fc..ce3b1a4 100644 --- a/Language.agda +++ b/Language.agda @@ -179,6 +179,14 @@ module Graphs where ) } + open Relaxable {{...}} public + + relax-preserves-[]≡ : ∀ (g₁ g₂ : Graph) (g₁⊆g₂ : g₁ ⊆ g₂) (idx : Graph.Index g₁) → + g₁ [ idx ] ≡ g₂ [ relax g₁⊆g₂ idx ] + relax-preserves-[]≡ g₁ g₂ (Mk-⊆ n refl g₁[]≡g₂[] _) idx = + trans (g₁[]≡g₂[] idx) (cong (λ vec → lookup vec (idx ↑ˡ n)) + (cast-is-id refl (Graph.nodes g₂))) + MonotonicGraphFunction : (Graph → Set) → Set MonotonicGraphFunction T = (g₁ : Graph) → Σ Graph (λ g₂ → T g₂ × g₁ ⊆ g₂) @@ -259,8 +267,6 @@ module Graphs where addEdges g ((idx , idx') ∷ (idx₂ , idx) ∷ []) }) map (λ { g ((idx₁ , idx₂) , idx , idx') → (idx , idx') }) - -- open Relaxable {{...}} public - open import Lattice.MapSet _≟ˢ_ renaming ( MapSet to StringSet