From 2addc785aac4a0dd1e97832a4fb4b2cd2324ee13 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Sun, 15 Sep 2024 18:18:52 +0900
Subject: [PATCH] =?UTF-8?q?rule=20inversion=20=E3=81=AE=E3=81=99=E3=81=B9?=
 =?UTF-8?q?=E3=81=A6=E3=81=AE=E5=91=BD=E9=A1=8C=E3=82=92=20big=5Fstep=20?=
 =?UTF-8?q?=E3=81=A7=E7=A4=BA=E3=81=9B=E3=82=8B=E3=82=88=E3=81=86=E3=81=AB?=
 =?UTF-8?q?=E3=81=99=E3=82=8B?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 ConcreteSemantics/RuleInversion.lean | 60 +++++++++++-----------------
 1 file changed, 23 insertions(+), 37 deletions(-)

diff --git a/ConcreteSemantics/RuleInversion.lean b/ConcreteSemantics/RuleInversion.lean
index 297dffa..7bfa0b0 100644
--- a/ConcreteSemantics/RuleInversion.lean
+++ b/ConcreteSemantics/RuleInversion.lean
@@ -65,54 +65,40 @@ add_aesop_rules unsafe 30% [apply and_excluded (rule_sets := [BigStepRules])]
     (B s ∧ (S, s) ==> t) ∨ (¬ B s ∧ (T, s) ==> t) := by
   big_step
 
-/-- while に関する inversion rule。
-条件式が真か偽かで場合分けをする
-
-TODO: aesop に自動的に使用してもらう方法を見つける -/
-theorem while_iff {B S s u} : (whileDo B S, s) ==> u ↔
-    (∃ t, B s ∧ (S, s) ==> t ∧ (whileDo B S, t) ==> u) ∨ (¬ B s ∧ u = s) := by
-  constructor <;> intro h
-
-  case mp =>
-    -- 条件式が成り立つかどうかで場合分けする
-    by_cases hcond : B s
-
-    -- 成り立つ場合
-    case pos =>
-      left
-      -- `(whileDo B S,s) ==> u` という仮定を条件式が真ということを使って分解
-      cases h <;> try contradiction
+/-- while の BigStep が仮定にあるときに簡単な状態の式を導く(条件式が偽のとき) -/
+theorem cases_while_of_false {B S s t} (hcond : ¬ B s) : (whileDo B S, s) ==> t → s = t := by
+  intro h
+  rcases h with h | h
+  · simp_all
+  · rfl
 
-      -- 変数が死ぬが、aesop は rename_i を使ってくれるので通る
-      big_step
+add_aesop_rules safe [destruct cases_while_of_false (rule_sets := [BigStepRules])]
 
-    -- 成り立たない場合
-    case neg =>
-      right
+/-- while の BigStep が仮定にあるときに簡単な状態の式を導く(条件式が真のとき) -/
+theorem cases_while_of_true {B S s u} (hcond : B s) : (whileDo B S, s) ==> u →
+    (∃ t, (S, s) ==> t ∧ (whileDo B S, t) ==> u) := by
+  intro h
+  cases h
+  · aesop
+  · simp_all
 
-      -- 条件式が成立しないことと `(whileDo B S,s) ==> u` という仮定から、
-      -- `u = s` であることがわかる
-      cases h <;> try contradiction
-      simp_all
+-- 再帰的に while 文が出てくるので、unsafe ルールとして登録する
+add_aesop_rules unsafe 20% [apply cases_while_of_true (rule_sets := [BigStepRules])]
 
-  case mpr => big_step
+/-- while に関する inversion rule。
+条件式が真か偽かで場合分けをする -/
+theorem while_iff {B S s u} : (whileDo B S, s) ==> u ↔
+    (∃ t, B s ∧ (S, s) ==> t ∧ (whileDo B S, t) ==> u) ∨ (¬ B s ∧ u = s) := by
+  big_step
 
 /-- 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]
+  big_step
 
 /-- 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]
+  big_step
 
 /- inversion rule を使って次のような命題が証明できる -/