From bfef4831a387ef2d06954aa88cd3c66c03df0492 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Sat, 24 Aug 2024 16:01:32 +0900
Subject: [PATCH] =?UTF-8?q?7.2.3=20Rule=20Inversion=20=E7=B5=82=E4=BA=86?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 ConcreteSemantics/RuleInversion.lean | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/ConcreteSemantics/RuleInversion.lean b/ConcreteSemantics/RuleInversion.lean
index 3722e01..2070cf8 100644
--- a/ConcreteSemantics/RuleInversion.lean
+++ b/ConcreteSemantics/RuleInversion.lean
@@ -106,4 +106,15 @@ theorem while_iff {B S s u} : (whileDo B S, s) ==> u ↔
   rw [while_iff]
   simp [hcond]
 
+/- inversion rule を使って次のような命題が証明できる -/
+
+example (c₁ c₂ : Stmt) (s₁ s₃ : State) : (c₁;; c₂, s₁) ==> s₃ →
+    ∃s₂, (c₁, s₁) ==> s₂ ∧ (c₂, s₂) ==> s₃ := by
+  aesop
+
+/-- seq `;;` を左結合にしても右結合にしても意味論の観点からは変化がない。 -/
+theorem seq_assoc (c₁ c₂ c₃ : Stmt) (s u : State) :
+    ((c₁;; c₂);; c₃, s) ==> u ↔ (c₁;; (c₂;; c₃), s) ==> u := by
+  aesop
+
 end BigStep