internlm/Lean-Github huggingface dataset:
Theorem: RegMachine.stepsToTrans_of_not_halts_stepsToTransRefl_halts
Proof state before:
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
h : c [P]==>* d
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
⊢ c [P]==>+ d
Tactic:
cases Relation.ReflTransGen.cases_head h
Proof state after:
case inl
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
h : c [P]==>* d
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
h✝ : c = d
⊢ c [P]==>+ d

case inr
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
h : c [P]==>* d
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
h✝ : ∃ c_1, (c [P]==> c_1) ∧ Relation.ReflTransGen (stepsTo P) c_1 d
⊢ c [P]==>+ d
Theorem: RegMachine.stepsToTrans_of_not_halts_stepsToTransRefl_halts
Proof state before:
case inl
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
h : c [P]==>* d
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
h✝ : c = d
⊢ c [P]==>+ d

case inr
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
h : c [P]==>* d
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
h✝ : ∃ c_1, (c [P]==> c_1) ∧ Relation.ReflTransGen (stepsTo P) c_1 d
⊢ c [P]==>+ d
Tactic:
clear h
Proof state after:
case inl
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
h✝ : c = d
⊢ c [P]==>+ d

case inr
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
h : c [P]==>* d
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
h✝ : ∃ c_1, (c [P]==> c_1) ∧ Relation.ReflTransGen (stepsTo P) c_1 d
⊢ c [P]==>+ d
Theorem: RegMachine.stepsToTrans_of_not_halts_stepsToTransRefl_halts
Proof state before:
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
heq : c = d
⊢ c [P]==>+ d
Tactic:
case inl heq =>
  cases heq; contradiction
Proof state after:
no goals
Theorem: RegMachine.stepsToTrans_of_not_halts_stepsToTransRefl_halts
Proof state before:
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
h✝ : c [P]==>* d
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
h : ∃ c_1, (c [P]==> c_1) ∧ Relation.ReflTransGen (stepsTo P) c_1 d
⊢ c [P]==>+ d
Tactic:
case inr h =>
  rcases h with ⟨c',hc_c',hc'_d⟩
  exact Relation.TransGen.head' hc_c' hc'_d
Proof state after:
no goals
Theorem: RegMachine.stepsToTrans_of_not_halts_stepsToTransRefl_halts
Proof state before:
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
heq : c = d
⊢ c [P]==>+ d
Tactic:
cases heq
Proof state after:
case refl
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c : Config R L
hc : ¬Config.is_halted c = true
hd : Config.is_halted c = true
⊢ c [P]==>+ c
Theorem: RegMachine.stepsToTrans_of_not_halts_stepsToTransRefl_halts
Proof state before:
case refl
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c : Config R L
hc : ¬Config.is_halted c = true
hd : Config.is_halted c = true
⊢ c [P]==>+ c
Tactic:
contradiction
Proof state after:
no goals
Theorem: RegMachine.stepsToTrans_of_not_halts_stepsToTransRefl_halts
Proof state before:
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
h✝ : c [P]==>* d
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
h : ∃ c_1, (c [P]==> c_1) ∧ Relation.ReflTransGen (stepsTo P) c_1 d
⊢ c [P]==>+ d
Tactic:
rcases h with ⟨c',hc_c',hc'_d⟩
Proof state after:
case intro.intro
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
h : c [P]==>* d
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
c' : Config R L
hc_c' : c [P]==> c'
hc'_d : Relation.ReflTransGen (stepsTo P) c' d
⊢ c [P]==>+ d
Theorem: RegMachine.stepsToTrans_of_not_halts_stepsToTransRefl_halts
Proof state before:
case intro.intro
R✝ L✝ : Type
Start✝ : ?m.51733
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.51747) true
R L : Type
x✝ : Sort ?u.51732
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.51747) true
c d : Config R L
h : c [P]==>* d
hc : ¬Config.is_halted c = true
hd : Config.is_halted d = true
c' : Config R L
hc_c' : c [P]==> c'
hc'_d : Relation.ReflTransGen (stepsTo P) c' d
⊢ c [P]==>+ d
Tactic:
exact Relation.TransGen.head' hc_c' hc'_d
Proof state after:
no goals
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
i o1 o2 : ℕ
h1 : evals S i o1
h2 : evals S i o2
⊢ o1 = o2
Tactic:
match h1, h2 with
| ⟨regs1,h1'⟩, ⟨regs2,h2'⟩ =>
clear h1 h2
generalize Config.init _ _ = c1 at h1' h2'
clear i
induction h1' using Relation.ReflTransGen.head_induction_on
  <;> clear c1
case refl =>
  have : o1 = (Config.haltedOn (L := L) o1 regs1).regs .io :=
    by simp [Config.haltedOn]
  rw [this]
  have := halt_is_fixpoint _ h2' (by simp)
  rw [this]
  simp
case head c d h _ ih =>
  apply ih; clear ih
  cases Relation.ReflTransGen.cases_head h2' <;> clear h2'
  case inl h2' =>
    cases h2'
    have : _ = d := by
      apply halt_is_fixpoint _ (Relation.ReflTransGen.single h)
      simp
    rw [←this]
  case inr h2' =>
    rcases h2' with ⟨c',hc,h⟩
    have : c' = d := stepsTo_functional _ hc ‹_›
    rw [←this]
    exact h
Proof state after:
no goals
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
i o1 o2 : ℕ
h1 : evals S i o1
h2 : evals S i o2
regs1 : R → ℕ
h1' : Config.init i (some S.start) [S.prog]==>* Config.haltedOn o1 regs1
regs2 : R → ℕ
h2' : Config.init i (some S.start) [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2
Tactic:
clear h1 h2
Proof state after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
i o1 o2 : ℕ
regs1 : R → ℕ
h1' : Config.init i (some S.start) [S.prog]==>* Config.haltedOn o1 regs1
regs2 : R → ℕ
h2' : Config.init i (some S.start) [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
i o1 o2 : ℕ
regs1 : R → ℕ
h1' : Config.init i (some S.start) [S.prog]==>* Config.haltedOn o1 regs1
regs2 : R → ℕ
h2' : Config.init i (some S.start) [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2
Tactic:
generalize Config.init _ _ = c1 at h1' h2'
Proof state after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
i o1 o2 : ℕ
regs1 regs2 : R → ℕ
c1 : Config (WithIO R) L
h1' : c1 [S.prog]==>* Config.haltedOn o1 regs1
h2' : c1 [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
i o1 o2 : ℕ
regs1 regs2 : R → ℕ
c1 : Config (WithIO R) L
h1' : c1 [S.prog]==>* Config.haltedOn o1 regs1
h2' : c1 [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2
Tactic:
clear i
Proof state after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c1 : Config (WithIO R) L
h1' : c1 [S.prog]==>* Config.haltedOn o1 regs1
h2' : c1 [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c1 : Config (WithIO R) L
h1' : c1 [S.prog]==>* Config.haltedOn o1 regs1
h2' : c1 [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2
Tactic:
induction h1' using Relation.ReflTransGen.head_induction_on
  <;> clear c1
Proof state after:
case refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2

case head
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
a✝¹ c✝ : Config (WithIO R) L
h'✝ : a✝¹ [S.prog]==> c✝
h✝ : Relation.ReflTransGen (stepsTo S.prog) c✝ (Config.haltedOn o1 regs1)
a✝ : c✝ [S.prog]==>* Config.haltedOn o2 regs2 → o1 = o2
h2' : a✝¹ [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2
Tactic:
case refl =>
  have : o1 = (Config.haltedOn (L := L) o1 regs1).regs .io :=
    by simp [Config.haltedOn]
  rw [this]
  have := halt_is_fixpoint _ h2' (by simp)
  rw [this]
  simp
Proof state after:
no goals
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
ih : d [S.prog]==>* Config.haltedOn o2 regs2 → o1 = o2
h2' : c [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2
Tactic:
case head c d h _ ih =>
  apply ih; clear ih
  cases Relation.ReflTransGen.cases_head h2' <;> clear h2'
  case inl h2' =>
    cases h2'
    have : _ = d := by
      apply halt_is_fixpoint _ (Relation.ReflTransGen.single h)
      simp
    rw [←this]
  case inr h2' =>
    rcases h2' with ⟨c',hc,h⟩
    have : c' = d := stepsTo_functional _ hc ‹_›
    rw [←this]
    exact h
Proof state after:
no goals
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2
Tactic:
have : o1 = (Config.haltedOn (L := L) o1 regs1).regs .io :=
  by simp [Config.haltedOn]
Proof state after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
this : o1 = Config.regs (Config.haltedOn o1 regs1) WithIO.io
⊢ o1 = o2
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
this : o1 = Config.regs (Config.haltedOn o1 regs1) WithIO.io
⊢ o1 = o2
Tactic:
rw [this]
Proof state after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
this : o1 = Config.regs (Config.haltedOn o1 regs1) WithIO.io
⊢ Config.regs (Config.haltedOn o1 regs1) WithIO.io = o2
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
this : o1 = Config.regs (Config.haltedOn o1 regs1) WithIO.io
⊢ Config.regs (Config.haltedOn o1 regs1) WithIO.io = o2
Tactic:
have := halt_is_fixpoint _ h2' (by simp)
Proof state after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
this✝ : o1 = Config.regs (Config.haltedOn o1 regs1) WithIO.io
this : Config.haltedOn o1 regs1 = Config.haltedOn o2 regs2
⊢ Config.regs (Config.haltedOn o1 regs1) WithIO.io = o2
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
this✝ : o1 = Config.regs (Config.haltedOn o1 regs1) WithIO.io
this : Config.haltedOn o1 regs1 = Config.haltedOn o2 regs2
⊢ Config.regs (Config.haltedOn o1 regs1) WithIO.io = o2
Tactic:
rw [this]
Proof state after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
this✝ : o1 = Config.regs (Config.haltedOn o1 regs1) WithIO.io
this : Config.haltedOn o1 regs1 = Config.haltedOn o2 regs2
⊢ Config.regs (Config.haltedOn o2 regs2) WithIO.io = o2
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
this✝ : o1 = Config.regs (Config.haltedOn o1 regs1) WithIO.io
this : Config.haltedOn o1 regs1 = Config.haltedOn o2 regs2
⊢ Config.regs (Config.haltedOn o2 regs2) WithIO.io = o2
Tactic:
simp
Proof state after:
no goals
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = Config.regs (Config.haltedOn o1 regs1) WithIO.io
Tactic:
simp [Config.haltedOn]
Proof state after:
no goals
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
h2' : Config.haltedOn o1 regs1 [S.prog]==>* Config.haltedOn o2 regs2
this : o1 = Config.regs (Config.haltedOn o1 regs1) WithIO.io
⊢ Config.is_halted (Config.haltedOn o1 regs1) = true
Tactic:
simp
Proof state after:
no goals
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
ih : d [S.prog]==>* Config.haltedOn o2 regs2 → o1 = o2
h2' : c [S.prog]==>* Config.haltedOn o2 regs2
⊢ o1 = o2
Tactic:
apply ih
Proof state after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
ih : d [S.prog]==>* Config.haltedOn o2 regs2 → o1 = o2
h2' : c [S.prog]==>* Config.haltedOn o2 regs2
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
ih : d [S.prog]==>* Config.haltedOn o2 regs2 → o1 = o2
h2' : c [S.prog]==>* Config.haltedOn o2 regs2
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Tactic:
clear ih
Proof state after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h2' : c [S.prog]==>* Config.haltedOn o2 regs2
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h2' : c [S.prog]==>* Config.haltedOn o2 regs2
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Tactic:
cases Relation.ReflTransGen.cases_head h2' <;> clear h2'
Proof state after:
case inl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h : c [S.prog]==> d
h✝¹ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h✝ : c = Config.haltedOn o2 regs2
⊢ d [S.prog]==>* Config.haltedOn o2 regs2

case inr
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h : c [S.prog]==> d
h✝¹ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h✝ : ∃ c_1, (c [S.prog]==> c_1) ∧ Relation.ReflTransGen (stepsTo S.prog) c_1 (Config.haltedOn o2 regs2)
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h2' : c = Config.haltedOn o2 regs2
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Tactic:
case inl h2' =>
  cases h2'
  have : _ = d := by
    apply halt_is_fixpoint _ (Relation.ReflTransGen.single h)
    simp
  rw [←this]
Proof state after:
no goals
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h2' : ∃ c_1, (c [S.prog]==> c_1) ∧ Relation.ReflTransGen (stepsTo S.prog) c_1 (Config.haltedOn o2 regs2)
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Tactic:
case inr h2' =>
  rcases h2' with ⟨c',hc,h⟩
  have : c' = d := stepsTo_functional _ hc ‹_›
  rw [←this]
  exact h
Proof state after:
no goals
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h2' : c = Config.haltedOn o2 regs2
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Tactic:
cases h2'
Proof state after:
case refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
d : Config (WithIO R) L
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h : Config.haltedOn o2 regs2 [S.prog]==> d
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
case refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
d : Config (WithIO R) L
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h : Config.haltedOn o2 regs2 [S.prog]==> d
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Tactic:
have : _ = d := by
  apply halt_is_fixpoint _ (Relation.ReflTransGen.single h)
  simp
Proof state after:
case refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
d : Config (WithIO R) L
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h : Config.haltedOn o2 regs2 [S.prog]==> d
this : Config.haltedOn o2 regs2 = d
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
case refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
d : Config (WithIO R) L
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h : Config.haltedOn o2 regs2 [S.prog]==> d
this : Config.haltedOn o2 regs2 = d
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Tactic:
rw [←this]
Proof state after:
no goals
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
d : Config (WithIO R) L
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h : Config.haltedOn o2 regs2 [S.prog]==> d
⊢ ?m.54568 = d
Tactic:
apply halt_is_fixpoint _ (Relation.ReflTransGen.single h)
Proof state after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
d : Config (WithIO R) L
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h : Config.haltedOn o2 regs2 [S.prog]==> d
⊢ Config.is_halted (Config.haltedOn o2 regs2) = true
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
d : Config (WithIO R) L
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h : Config.haltedOn o2 regs2 [S.prog]==> d
⊢ Config.is_halted (Config.haltedOn o2 regs2) = true
Tactic:
simp
Proof state after:
no goals
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
h2' : ∃ c_1, (c [S.prog]==> c_1) ∧ Relation.ReflTransGen (stepsTo S.prog) c_1 (Config.haltedOn o2 regs2)
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Tactic:
rcases h2' with ⟨c',hc,h⟩
Proof state after:
case intro.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h✝¹ : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
c' : Config (WithIO R) L
hc : c [S.prog]==> c'
h : Relation.ReflTransGen (stepsTo S.prog) c' (Config.haltedOn o2 regs2)
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Theorem: RegMachine.Prog.Start.evals_functional
Proof state before:
case intro.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h✝¹ : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
c' : Config (WithIO R) L
hc : c [S.prog]==> c'
h : Relation.ReflTransGen (stepsTo S.prog) c' (Config.haltedOn o2 regs2)
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Tactic:
have : c' = d := stepsTo_functional _ hc ‹_›
Proof state after:
case intro.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
o1 o2 : ℕ
regs1 regs2 : R → ℕ
c d : Config (WithIO R) L
h✝¹ : c [S.prog]==> d
h✝ : Relation.ReflTransGen (stepsTo S.prog) d (Config.haltedOn o1 regs1)
c' : Config (WithIO R) L
hc : c [S.prog]==> c'
h : Relation.ReflTransGen (stepsTo S.prog) c' (Config.haltedOn o2 regs2)
this : c' = d
⊢ d [S.prog]==>* Config.haltedOn o2 regs2