Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

sillyLoopの証明をいい感じに書いた #2

Merged
merged 1 commit into from
Oct 1, 2024
Merged

sillyLoopの証明をいい感じに書いた #2

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
51 changes: 20 additions & 31 deletions ConcreteSemantics/SmallStep.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,51 +55,40 @@ 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
/-- SmallStep の二項関係バージョン -/
abbrev smallStepBin (conf₁ conf₂ : Config) : Prop := SmallStep conf₁.1 conf₁.2 conf₂.1 conf₂.2

@[inherit_doc] infix:30 " ⇒ " => smallStepBin

-- 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)
ReflTransGen smallStepBin

@[inherit_doc] infix:30 " ⇒* " => smallStepStar

instance : Trans smallStepBin smallStepBin smallStepStar where
trans a_b b_c := ReflTransGen.head a_b (ReflTransGen.head b_c .refl)
instance : Trans smallStepBin smallStepStar smallStepStar where
trans a_b b__c := ReflTransGen.head a_b b__c
instance : Trans smallStepStar smallStepBin smallStepStar where
trans a__b b_c := ReflTransGen.tail a__b b_c

#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
calc
_ ⇒ (_, _) := by dsimp [smallStepBin]; small_step
_ ⇒ (_, _) := by dsimp [smallStepBin]; apply SmallStep.if_true; simp
_ ⇒ (_, _) := by dsimp [smallStepBin]; small_step
_ ⇒ (_, _) := by dsimp [smallStepBin]; small_step
_ ⇒ (_, _) := by dsimp [smallStepBin]; small_step
_ ⇒ (_, _) := by dsimp [smallStepBin]; small_step
_ ⇒ (_, _) := by dsimp [smallStepBin]; apply SmallStep.if_false; simp