進捗 10/01

ConcreteSemantics/SmallStep.lean

@@ -1,5 +1,6 @@
 import ConcreteSemantics.Stmt
 import ConcreteSemantics.Tactic.SmallStep
+import Mathlib.Logic.Relation
 
 /- ## 7.3 Small Step Semantics -/
 
@@ -34,6 +35,7 @@ inductive SmallStep : Stmt → State → Stmt → State → Prop
   | protected whileDo {B S s} :
     SmallStep (whileDo B S) s (ifThenElse B (S ;; whileDo B S) skip) s
 
+set_option linter.unusedTactic false
 
 -- `small_step` タクティクにコンストラクタを登録する
 add_aesop_rules safe apply [
@@ -52,3 +54,52 @@ add_aesop_rules safe tactic [
 
 -- SmallStep のための見やすい記法を用意する
 @[inherit_doc] notation:55 "(" c1:55 "," s1:55 ")" " =>ₛ " "(" c2:55 "," s2:55 ")" => SmallStep c1 s1 c2 s2
+
+
+/-- コマンドと状態を組にしたもの。configuration -/
+abbrev Config := Stmt × State
+
+-- /-- SmallStep の二項関係バージョン -/
+-- abbrev smallStepBin (conf₁ conf₂ : Config) : Prop := SmallStep conf₁.1 conf₁.2 conf₂.1 conf₂.2
+
+-- add_aesop_rules safe tactic [(by dsimp [smallStepBin]) (rule_sets := [SmallStepRules])]
+
+open Relation
+
+/-- `smallStepBin` という二項関係の反射的推移的閉包 -/
+@[reducible] def smallStepStar : Config → Config → Prop :=
+  ReflTransGen (fun conf₁ conf₂ => SmallStep conf₁.1 conf₁.2 conf₂.1 conf₂.2)
+
+@[inherit_doc] infix:30 " ⇒* " => smallStepStar
+
+#check sillyLoop
+
+example : (sillyLoop, (fun _ => 0)["x" ↦ 1]) ⇒* (skip, (fun _ => 0)) := by
+  dsimp [sillyLoop]
+
+  generalize hB : (fun s : State ↦ s "x" > s "y") = B0
+  generalize hS : (skip;; assign "x" (fun s ↦ s "x" - 1)) = S0
+  generalize hs : (fun v ↦ (if v = "x" then 1 else 0)) = s0
+
+  have : (whileDo B0 S0, s0) ⇒* (skip, fun x ↦ 0) := calc
+    _ ⇒* (ifThenElse B0 (S0 ;; whileDo B0 S0) skip, s0) := ?step1
+    _ ⇒* (S0 ;; whileDo B0 S0, s0) := ?step2
+    _ ⇒* (whileDo B0 S0, fun _ ↦ 0) := ?step3
+    _ ⇒* (skip, fun x ↦ 0) := by sorry
+
+  case step1 =>
+    apply ReflTransGen.head (a := (whileDo B0 S0, s0)) (hbc := ReflTransGen.refl)
+    apply SmallStep.whileDo
+
+  case step2 =>
+    apply ReflTransGen.head (a := (ifThenElse B0 (S0 ;; whileDo B0 S0) skip, s0)) (hbc := ReflTransGen.refl)
+    apply SmallStep.if_true
+    rw [← hB, ← hs]
+    simp
+
+  case step3 =>
+    have : (S0,s0) =>ₛ (skip, fun x ↦ 0) := by sorry
+    have := @SmallStep.seq_step (S := S0) (s := s0) (S' := skip) (s' := fun _ ↦ 0)
+    sorry
+
+  sorry