From 7ee8c466d0157d34d5c695f53594c3eb72382f9d Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Sat, 24 Aug 2024 13:48:54 +0900
Subject: [PATCH] =?UTF-8?q?inversion=20rule=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 2107bd0..3722e01 100644
--- a/ConcreteSemantics/RuleInversion.lean
+++ b/ConcreteSemantics/RuleInversion.lean
@@ -95,4 +95,15 @@ theorem while_iff {B S s u} : (whileDo B S, s) ==> u ↔
     · apply BigStep.while_true hcond hbody hrest
     · apply BigStep.while_false (hcond := by assumption)
 
+/-- while の条件式が真のときの inversion rule -/
+@[simp] theorem while_true_iff {B S s u} (hcond : B s) : (whileDo B S, s) ==> u ↔
+    (∃ t, (S, s) ==> t ∧ (whileDo B S, t) ==> u) := by
+  rw [while_iff]
+  simp [hcond]
+
+/-- while の条件式が偽のときの inversion rule -/
+@[simp] theorem while_false_iff {B S s t} (hcond : ¬ B s) : (whileDo B S, s) ==> t ↔ t = s := by
+  rw [while_iff]
+  simp [hcond]
+
 end BigStep