aesop を使って BigStep を示せるようにする

ConcreteSemantics/BigStep.lean

@@ -69,6 +69,9 @@ inductive BigStep : Stmt → State → State → Prop where
 -- BigStep のための見やすい記法を用意する
 @[inherit_doc] notation:55 "(" S:55 "," s:55 ")" " ==> " t:55 => BigStep S s t
 
+-- BigStep がゴールにある場合にそれを aesop が扱えるようにする
+attribute [aesop safe constructors] BigStep
+
 /-- `sillyLoop` コマンドにより、`x = 1, y = 0` という状態は `x = y = 0` という状態に変わる。 -/
 example : (sillyLoop, (fun _ ↦ 0)["x" ↦ 1]) ==> (fun _ ↦ 0) := by
   -- sillyLoop の定義を展開する
@@ -79,14 +82,9 @@ example : (sillyLoop, (fun _ ↦ 0)["x" ↦ 1]) ==> (fun _ ↦ 0) := by
   apply BigStep.while_true
 
   -- 条件式 `x > y` が真であること
-  case hcond =>
-    simp
+  case hcond => simp
 
-  case hbody =>
-    -- `;` でつながっているのを分解する
-    apply BigStep.seq
-    · apply BigStep.skip
-    · apply BigStep.assign
+  case hbody => aesop
 
   case hrest =>
     simp only [gt_iff_lt, ↓reduceIte, Nat.sub_self]
@@ -97,8 +95,7 @@ example : (sillyLoop, (fun _ ↦ 0)["x" ↦ 1]) ==> (fun _ ↦ 0) := by
 
     -- このとき状態は `x ↦ 0, y ↦ 0` なので条件式は偽。
     -- したがって while_false を使う
-    apply BigStep.while_false
-    simp
+    apply BigStep.while_false (hcond := by simp)
 
 /- ### 7.2.2 Deriving IMP Executions -/
 
@@ -111,4 +108,4 @@ example (s : State) : (set_to_five, s) ==> (s["x" ↦ 5]["y" ↦ 5]) := by
   -- set_to_five の定義を展開する
   dsimp [set_to_five]
 
-  apply BigStep.seq <;> apply BigStep.assign
+  aesop

ConcreteSemantics/Equivalence.lean

@@ -37,7 +37,7 @@ instance : Setoid Stmt where
 /-- `≈` 記号の中身を展開するタクティク -/
 syntax "unfold" "≈" : tactic
 macro_rules
-  | `(tactic|unfold ≈) => `(tactic|dsimp only [(· ≈ ·), Setoid.r, equivCmd])
+  | `(tactic|unfold ≈) => `(tactic| dsimp only [(· ≈ ·), Setoid.r, equivCmd])
 
 /-- ### Lemma 7.3
 `while` 文の意味は、
@@ -84,9 +84,7 @@ theorem while_congr {B : State → Prop} {c c' : Stmt} {s t : State} (h : c ≈
   induction h_while <;> cases hx
 
   -- 条件式が偽の場合
-  case while_false s' hcond =>
-    apply BigStep.while_false
-    assumption
+  case while_false s' hcond => aesop
 
   -- 条件式が真の場合
   case while_true s' t' u' hcond' hbody' _ _hrest ih =>
@@ -123,14 +121,12 @@ theorem while_eq_of_eq (B : State → Prop) (c c' : Stmt) (h : c ≈ c') : while
     specialize h s w
 
     -- aesop で片を付ける
-    aesop
     all_goals sorry
 
   case mpr =>
     -- whileDo の定義を展開する
     rw [while_iff]
     -- aesop で片を付ける
-    aesop
     sorry
 
 end BigStep

ConcreteSemantics/RuleInversion.lean

@@ -22,7 +22,7 @@ namespace BigStep
     -- s = t なので、BigStep.skip の定義から従う
     rw [h]
 
-    apply BigStep.skip
+    aesop
 
 /-- seq に関する inversion rule -/
 @[simp] theorem seq_iff {S T s u} :
@@ -40,9 +40,7 @@ namespace BigStep
   -- 右から左を示す
   case mpr =>
     obtain ⟨t, hS, hT⟩ := h
-
-    -- big_step タクティクを使わない証明
-    apply BigStep.seq <;> assumption
+    aesop
 
 /-- if に関する inversion rule -/
 @[simp] theorem if_iff {B S T s t} : (ifThenElse B S T, s) ==> t ↔