big_step タクティクが、if_true を適用すべき場面で if_false を適用してしまって詰むバグを修正

Seasawher · Sep 14, 2024 · 7c9da08 · 7c9da08
1 parent d83a3e2
commit 7c9da08
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 4 deletions.
diff --git a/ConcreteSemantics/BigStep.lean b/ConcreteSemantics/BigStep.lean
@@ -64,8 +64,16 @@ inductive BigStep : Stmt → State → State → Prop where
 add_aesop_rules safe [apply BigStep.skip (rule_sets := [BigStepRules])]
 add_aesop_rules safe [apply BigStep.assign (rule_sets := [BigStepRules])]
 add_aesop_rules safe [apply BigStep.seq (rule_sets := [BigStepRules])]
-add_aesop_rules safe [apply BigStep.if_true (rule_sets := [BigStepRules])]
-add_aesop_rules safe [apply BigStep.if_false (rule_sets := [BigStepRules])]
+add_aesop_rules safe [
+  tactic
+  (by apply BigStep.if_true (hcond := by assumption) (hbody := by assumption))
+  (rule_sets := [BigStepRules]),
+]
+add_aesop_rules safe [
+  tactic
+  (by apply BigStep.if_false (hcond := by assumption) (hbody := by assumption))
+  (rule_sets := [BigStepRules]),
+]
 add_aesop_rules safe [apply BigStep.while_false (rule_sets := [BigStepRules])]
 add_aesop_rules unsafe 50% [apply BigStep.while_true (rule_sets := [BigStepRules])]
 

diff --git a/ConcreteSemantics/RuleInversion.lean b/ConcreteSemantics/RuleInversion.lean
@@ -39,15 +39,15 @@ add_aesop_rules safe [destruct eq_of_skip (rule_sets := [BigStepRules])]
 theorem if_iff_of_true {B S T s t} (hcond : B s) : (ifThenElse B S T, s) ==> t ↔ (S, s) ==> t := by
   constructor <;> intro h
   · cases h <;> simp_all
-  · apply BigStep.if_true (hcond := by assumption) (hbody := by assumption)
+  · big_step
 
 add_aesop_rules norm [simp if_iff_of_true (rule_sets := [BigStepRules])]
 
 /-- if に関する inversion rule (条件式が偽の場合) -/
 theorem if_iff_of_false {B S T s t} (hcond : ¬ B s) : (ifThenElse B S T, s) ==> t ↔ (T, s) ==> t := by
   constructor <;> intro h
   · cases h <;> simp_all
-  · apply BigStep.if_false (hcond := by assumption) (hbody := by assumption)
+  · big_step
 
 add_aesop_rules norm [simp if_iff_of_false (rule_sets := [BigStepRules])]