From bbfba34e0539e02f690076e98397fc7b0e7fd0ec Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 28 Apr 2024 13:37:03 -0700 Subject: [PATCH] Prove another (simple) case Signed-off-by: Danila Fedorin --- Language/Properties.agda | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/Language/Properties.agda b/Language/Properties.agda index b2f14fd..65641d3 100644 --- a/Language/Properties.agda +++ b/Language/Properties.agda @@ -140,6 +140,17 @@ EndToEndTrace-loop² {g} etr₁ etr₂ = record EndToEndTrace.trace etr₁ ++⟨ oi∈es ⟩ EndToEndTrace.trace etr₂ } +Trace-optional : ∀ {g : Graph} {idx₁ idx₂ : Graph.Index g} {ρ₁ ρ₂ : Env} → + Trace {g} idx₁ idx₂ ρ₁ ρ₂ → Trace {optional g} (2 Fin.↑ʳ idx₁) (2 Fin.↑ʳ idx₂) ρ₁ ρ₂ +Trace-optional = {!!} + +EndToEndTrace-optional : ∀ {g : Graph} {ρ₁ ρ₂ : Env} → + EndToEndTrace {g} ρ₁ ρ₂ → EndToEndTrace {optional g} ρ₁ ρ₂ +EndToEndTrace-optional = {!!} + +EndToEndTrace-optional-ε : ∀ {g : Graph} {ρ : Env} → EndToEndTrace {optional g} ρ ρ +EndToEndTrace-optional-ε = {!!} + infixr 5 _++_ _++_ : ∀ {g₁ g₂ : Graph} {ρ₁ ρ₂ ρ₃ : Env} → EndToEndTrace {g₁} ρ₁ ρ₂ → EndToEndTrace {g₂} ρ₂ ρ₃ → @@ -189,3 +200,6 @@ buildCfg-sufficient (⇒ˢ-if-false ρ₁ ρ₂ _ s₁ s₂ _ ρ₁,s₂⇒ρ₂ Trace-singleton[] ρ₁ ++ (EndToEndTrace-∙ʳ {buildCfg s₁} (buildCfg-sufficient ρ₁,s₂⇒ρ₂)) ++ Trace-singleton[] ρ₂ +buildCfg-sufficient (⇒ˢ-while-true ρ₁ ρ₂ ρ₃ _ _ s _ _ ρ₁,s⇒ρ₂ ρ₂,ws⇒ρ₃) = {!!} +buildCfg-sufficient (⇒ˢ-while-false ρ _ s _) = + EndToEndTrace-optional-ε {loop (buildCfg s)} {ρ}