From 7c9da08af07a616902bbb21866d55811a36847f4 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sun, 15 Sep 2024 04:30:26 +0900 Subject: [PATCH] =?UTF-8?q?`big=5Fstep`=20=E3=82=BF=E3=82=AF=E3=83=86?= =?UTF-8?q?=E3=82=A3=E3=82=AF=E3=81=8C=E3=80=81if=5Ftrue=20=E3=82=92?= =?UTF-8?q?=E9=81=A9=E7=94=A8=E3=81=99=E3=81=B9=E3=81=8D=E5=A0=B4=E9=9D=A2?= =?UTF-8?q?=E3=81=A7=20if=5Ffalse=20=E3=82=92=E9=81=A9=E7=94=A8=E3=81=97?= =?UTF-8?q?=E3=81=A6=E3=81=97=E3=81=BE=E3=81=A3=E3=81=A6=E8=A9=B0=E3=82=80?= =?UTF-8?q?=E3=83=90=E3=82=B0=E3=82=92=E4=BF=AE=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ConcreteSemantics/BigStep.lean | 12 ++++++++++-- ConcreteSemantics/RuleInversion.lean | 4 ++-- 2 files changed, 12 insertions(+), 4 deletions(-) diff --git a/ConcreteSemantics/BigStep.lean b/ConcreteSemantics/BigStep.lean index 9f1075d..807841f 100644 --- 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 index 652059c..a575e16 100644 --- a/ConcreteSemantics/RuleInversion.lean +++ b/ConcreteSemantics/RuleInversion.lean @@ -39,7 +39,7 @@ 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])] @@ -47,7 +47,7 @@ add_aesop_rules norm [simp if_iff_of_true (rule_sets := [BigStepRules])] 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])]