From 07550bc214138ad995d47c1edd2c6cd6cd0379eb Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 28 Apr 2024 12:10:12 -0700 Subject: [PATCH] Prove 'sufficiency' for if-else. Signed-off-by: Danila Fedorin --- Language/Graphs.agda | 6 +++--- Language/Properties.agda | 9 +++++++++ 2 files changed, 12 insertions(+), 3 deletions(-) diff --git a/Language/Graphs.agda b/Language/Graphs.agda index 5fcd259..31f4afc 100644 --- a/Language/Graphs.agda +++ b/Language/Graphs.agda @@ -52,7 +52,7 @@ _↑ˡᵉ_ l m = List.map (_↑ˡ m) l _↑ʳᵉ_ : ∀ {m} n → List (Fin m × Fin m) → List (Fin (n Nat.+ m) × Fin (n Nat.+ m)) _↑ʳᵉ_ n l = List.map (n ↑ʳ_) l -infixl 5 _∙_ +infixr 5 _∙_ _∙_ : Graph → Graph → Graph _∙_ g₁ g₂ = record { size = Graph.size g₁ Nat.+ Graph.size g₂ @@ -65,7 +65,7 @@ _∙_ g₁ g₂ = record (Graph.size g₁ ↑ʳⁱ Graph.outputs g₂) } -infixl 5 _↦_ +infixr 5 _↦_ _↦_ : Graph → Graph → Graph _↦_ g₁ g₂ = record { size = Graph.size g₁ Nat.+ Graph.size g₂ @@ -84,7 +84,7 @@ loop g = record g List.cartesianProduct (Graph.outputs g) (Graph.inputs g) } -infixl 5 _skipto_ +infixr 5 _skipto_ _skipto_ : Graph → Graph → Graph _skipto_ g₁ g₂ = record (g₁ ∙ g₂) { edges = Graph.edges (g₁ ∙ g₂) List.++ diff --git a/Language/Properties.agda b/Language/Properties.agda index 42fe80e..6e147ab 100644 --- a/Language/Properties.agda +++ b/Language/Properties.agda @@ -112,6 +112,7 @@ Trace-loop {idx₁ = idx₁} {idx₁} (Trace-single ρ₁⇒ρ₂) = Trace-singl Trace-loop {g₁} {idx₁} (Trace-edge ρ₁⇒ρ idx₁→idx tr') = Trace-edge ρ₁⇒ρ (ListMemProp.∈-++⁺ˡ idx₁→idx) (Trace-loop tr') +infixr 5 _++_ _++_ : ∀ {g₁ g₂ : Graph} {ρ₁ ρ₂ ρ₃ : Env} → EndToEndTrace {g₁} ρ₁ ρ₂ → EndToEndTrace {g₂} ρ₂ ρ₃ → EndToEndTrace {g₁ ↦ g₂} ρ₁ ρ₃ @@ -152,3 +153,11 @@ buildCfg-sufficient (⇒ˢ-⟨⟩ ρ₁ ρ₂ bs ρ₁,bs⇒ρ₂) = Trace-singleton (ρ₁,bs⇒ρ₂ ∷ []) buildCfg-sufficient (⇒ˢ-then ρ₁ ρ₂ ρ₃ s₁ s₂ ρ₁,s₁⇒ρ₂ ρ₂,s₂⇒ρ₃) = buildCfg-sufficient ρ₁,s₁⇒ρ₂ ++ buildCfg-sufficient ρ₂,s₂⇒ρ₃ +buildCfg-sufficient (⇒ˢ-if-true ρ₁ ρ₂ _ _ s₁ s₂ _ _ ρ₁,s₁⇒ρ₂) = + Trace-singleton[] ρ₁ ++ + (EndToEndTrace-∙ˡ (buildCfg-sufficient ρ₁,s₁⇒ρ₂)) ++ + Trace-singleton[] ρ₂ +buildCfg-sufficient (⇒ˢ-if-false ρ₁ ρ₂ _ s₁ s₂ _ ρ₁,s₂⇒ρ₂) = + Trace-singleton[] ρ₁ ++ + (EndToEndTrace-∙ʳ {buildCfg s₁} (buildCfg-sufficient ρ₁,s₂⇒ρ₂)) ++ + Trace-singleton[] ρ₂