From dabd13eea367ea1eef2025bdbb40fe5351fe01a3 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Tue, 27 Aug 2024 23:03:40 +0900
Subject: [PATCH] =?UTF-8?q?Aug27=20=E9=80=B2=E6=8D=97?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 ConcreteSemantics/Equivalence.lean | 70 ++++++++++++++++++++++++++++++
 1 file changed, 70 insertions(+)
 create mode 100644 ConcreteSemantics/Equivalence.lean

diff --git a/ConcreteSemantics/Equivalence.lean b/ConcreteSemantics/Equivalence.lean
new file mode 100644
index 0000000..76ad413
--- /dev/null
+++ b/ConcreteSemantics/Equivalence.lean
@@ -0,0 +1,70 @@
+/- ### 7.2.4 Equivalence of Commands -/
+import ConcreteSemantics.Stmt
+import ConcreteSemantics.BigStep
+import ConcreteSemantics.RuleInversion
+
+namespace BigStep
+
+/-- コマンドの BigStep 意味論における同値性 -/
+def equivCmd (S T : Stmt) : Prop := ∀s t : State, (S, s) ==> t ↔ (T, s) ==> t
+
+/-- `equivCmd` は反射的である -/
+theorem equivCmd_refl (S : Stmt) : equivCmd S S := by
+  intro s t
+  rfl
+
+/-- `equivCmd` は対称的である -/
+theorem equivCmd_symm {S T : Stmt} (h : equivCmd S T) : equivCmd T S := by
+  intro s t
+  rw [h]
+
+/-- `equivCmd` は推移的である -/
+theorem equivCmd_trans {S T U : Stmt} (hST : equivCmd S T) (hTU : equivCmd T U) : equivCmd S U := by
+  intro s t
+  rw [hST, hTU]
+
+/-- `equivCmd` は同値関係である -/
+def equivCmd_equiv : Equivalence equivCmd := ⟨equivCmd_refl, equivCmd_symm, equivCmd_trans⟩
+
+/-- `Stmt` という型に同値関係 `equivCmd` が付随しているということを宣言した -/
+instance : Setoid Stmt where
+  r := equivCmd
+  iseqv := equivCmd_equiv
+
+-- このように、`Stmt` の要素が同値であることを示すために `≈` を使うことができる
+#check skip ≈ skip
+
+/-- `≈` 記号の中身を展開するタクティク -/
+syntax "unfold" "≈" : tactic
+macro_rules
+  | `(tactic|unfold ≈) => `(tactic|dsimp only [(· ≈ ·), Setoid.r, equivCmd])
+
+/-- `while` 文の意味は、
+* 条件式が真なら `S` を実行して再び `while` ループを実行
+* 条件式が偽なら `skip`
+というコマンドに等しい。 -/
+theorem while_eq_if_then_skip (B : State → Prop) (S : Stmt) :
+  whileDo B S ≈ ifThenElse B (S;; whileDo B S) skip := by
+  -- ≈ の定義を展開する
+  unfold ≈
+
+  -- 状態 `s, t` が与えられたとする
+  intro s t
+
+  -- 両方向を示す
+  constructor <;> intro h
+
+  case mp =>
+    -- B が真かどうかで分岐
+    rw [while_iff] at h
+    -- aesop で片を付ける
+    aesop
+
+  case mpr =>
+    -- 条件が真かどうかで分岐する
+    -- while_iff を追加
+    aesop (add safe [while_iff])
+
+    done
+
+end BigStep