Sep 24 進捗

ConcreteSemantics/SmallStep.lean

@@ -1,4 +1,5 @@
 import ConcreteSemantics.Stmt
+import ConcreteSemantics.Tactic.SmallStep
 
 /- ## 7.3 Small Step Semantics -/
 
@@ -11,12 +12,43 @@ import ConcreteSemantics.Stmt
 -/
 inductive SmallStep : Stmt → State → Stmt → State → Prop
   /-- 代入文 `x := a s` の意味論 -/
-  | assign {x a s} : SmallStep (assign x a) s skip (s[x ↦ a s])
+  | protected assign {x a s} : SmallStep (assign x a) s skip (s[x ↦ a s])
 
   /-- seq の意味論 -/
-  | seq_step {S S' T s s'} (hS : SmallStep S s S' s') :
+  | protected seq_step {S S' T s s'} (hS : SmallStep S s S' s') :
     SmallStep (S ;; T) s (S' ;; T) s'
 
   /-- skip の意味論。skip を seq してもコマンドの意味は変わらない -/
-  | seq_skip {T s} : SmallStep (skip ;; T) s T s
+  | protected seq_skip {T s} : SmallStep (skip ;; T) s T s
 
+  /-- 条件式が true のときの if の意味論。状態は変化せず、実行するコマンドが変化する。-/
+  | protected if_true {B S T s} (hcond : B s) :
+    SmallStep (ifThenElse B S T) s S s
+
+  /-- 条件式が false のときの if の意味論。状態は変化せず、実行するコマンドが変化する。-/
+  | protected if_false {B S T s} (hcond : ¬ B s) :
+    SmallStep (ifThenElse B S T) s T s
+
+  /-- while の意味論。`whileDo B S` は、`B` が真なら `S ;; whileDo B S` に等しく、
+  `B` が偽なら `skip` に等しい。-/
+  | protected whileDo {B S s} :
+    SmallStep (whileDo B S) s (ifThenElse B (S ;; whileDo B S) skip) s
+
+
+-- `small_step` タクティクにコンストラクタを登録する
+add_aesop_rules safe apply [
+  SmallStep.assign,
+  SmallStep.seq_skip,
+  SmallStep.whileDo (rule_sets := [SmallStepRules])
+]
+add_aesop_rules unsafe 70% apply [
+  SmallStep.seq_step (rule_sets := [SmallStepRules])
+]
+add_aesop_rules safe tactic [
+  (by apply SmallStep.if_true (hcond := by assumption)),
+  (by apply SmallStep.if_false (hcond := by assumption))
+  (rule_sets := [SmallStepRules])
+]
+
+-- SmallStep のための見やすい記法を用意する
+@[inherit_doc] notation:55 "(" c1:55 "," s1:55 ")" " =>ₛ " "(" c2:55 "," s2:55 ")" => SmallStep c1 s1 c2 s2

ConcreteSemantics/SmallStepStar.lean

@@ -0,0 +1,20 @@
+import ConcreteSemantics.SmallStep
+import Mathlib.Logic.Relation
+
+/-- コマンドと状態を組にしたもの。configuration -/
+abbrev Config := Stmt × State
+
+/-- SmallStep の二項関係バージョン -/
+abbrev smallStepBin (conf₁ conf₂ : Config) : Prop := SmallStep conf₁.1 conf₁.2 conf₂.1 conf₂.2
+
+open Relation
+
+/-- `smallStepBin` という二項関係の反射的推移的閉包 -/
+def smallStepStar : Config → Config → Prop := ReflTransGen smallStepBin
+
+@[inherit_doc] infix:30 " ⇒* " => smallStepStar
+
+#check sillyLoop
+
+example : (sillyLoop, (fun _ => 0)["x" ↦ 1]) ⇒* (skip, (fun _ => 0)) := by
+  sorry

ConcreteSemantics/Tactic/SmallStep.lean

@@ -0,0 +1,14 @@
+/- # small step に応用するための aesop ラッパーを作る
+
+`aesop` をカスタマイズして、`small_step` というタクティクを作成する。
+-/
+import Aesop
+
+-- SmallStepRules という名前のルールセットを登録する
+declare_aesop_rule_sets [SmallStepRules]
+
+/-- `SmallStep` 用の aesop ラッパー -/
+macro "small_step" : tactic => do `(tactic| aesop (rule_sets := [SmallStepRules]))
+
+/-- `small_step` が使用した補題を生成する -/
+macro "small_step?" : tactic => `(tactic| aesop? (rule_sets := [SmallStepRules]))

lake-manifest.json

@@ -4,13 +4,23 @@
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "fa571ea02a804b52a59e58012b1e21fe4f0514f2",
+   "scope": "leanprover-community",
+   "rev": "35d1cd731ad832c9f1d860c4d8ec1c7c3ab96823",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
@@ -20,6 +30,56 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": false,
-   "configFile": "lakefile.toml"}],
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.42",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "2ba60fa2c384a94735454db11a2d523612eaabff",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "a6954b3788a62acda6a0e99ab1548255a1d1e8ae",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
  "name": "concreteSemantics",
  "lakeDir": ".lake"}

lakefile.lean

@@ -15,6 +15,8 @@ package «concreteSemantics» where
     ⟨`pp.unicode.fun, true⟩
   ]
 
+require mathlib from git "https://github.com/leanprover-community/mathlib4.git"
+
 require aesop from git "https://github.com/leanprover-community/aesop"
 
 @[default_target]