internlm/Lean-Github huggingface dataset:
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case mpr.intro.h_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
heq✝ :
  Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ (let c' :=
      {
        config :=
          step S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config,
        halts :=
          (_ :
            halts S.prog
              (step S.prog
                { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) };
    let_fun this :=
      (_ :
        { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config.ip = none → False);
    eval.aux S.prog c') =
    m
Tactic:
next ha =>
  simp
  cases ha_to_b
  apply ih.mpr
  use regs
  have := stepsToTrans_of_not_halts_stepsToTransRefl_halts _ h ?_ ?_
  . rcases Relation.TransGen.head'_iff.mp this with ⟨e,rfl,he⟩
    exact he
  . simp at ha; simp [ha]
  . simp
Proof state after:
no goals
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = true
⊢ Config.regs { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config WithIO.io = m
Tactic:
simp only at *
Proof state after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted a = true
⊢ Config.regs a WithIO.io = m
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted a = true
⊢ Config.regs a WithIO.io = m
Tactic:
have := halt_is_fixpoint _ h ha
Proof state after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted a = true
this : a = Config.haltedOn m regs
⊢ Config.regs a WithIO.io = m
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted a = true
this : a = Config.haltedOn m regs
⊢ Config.regs a WithIO.io = m
Tactic:
simp [this]
Proof state after:
no goals
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ (let c' :=
      {
        config :=
          step S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config,
        halts :=
          (_ :
            halts S.prog
              (step S.prog
                { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) };
    let_fun this :=
      (_ :
        { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config.ip = none → False);
    eval.aux S.prog c') =
    m
Tactic:
simp
Proof state after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ eval.aux S.prog
      { config := step S.prog a,
        halts :=
          (_ :
            halts S.prog
              (step S.prog
                { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) } =
    m
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a b : Config (WithIO R) L
ha_to_b : a [S.prog]==> b
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) b d
ih :
  eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, b [S.prog]==>* Config.haltedOn m regs
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ eval.aux S.prog
      { config := step S.prog a,
        halts :=
          (_ :
            halts S.prog
              (step S.prog
                { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) } =
    m
Tactic:
cases ha_to_b
Proof state after:
case refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ eval.aux S.prog
      { config := step S.prog a,
        halts :=
          (_ :
            halts S.prog
              (step S.prog
                { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) } =
    m
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ eval.aux S.prog
      { config := step S.prog a,
        halts :=
          (_ :
            halts S.prog
              (step S.prog
                { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config)) } =
    m
Tactic:
apply ih.mpr
Proof state after:
case refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
Tactic:
use regs
Proof state after:
case refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ step S.prog a [S.prog]==>* Config.haltedOn m regs
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ step S.prog a [S.prog]==>* Config.haltedOn m regs
Tactic:
have := stepsToTrans_of_not_halts_stepsToTransRefl_halts _ h ?_ ?_
Proof state after:
case refl.refine_3
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
this : a [S.prog]==>+ Config.haltedOn m regs
⊢ step S.prog a [S.prog]==>* Config.haltedOn m regs

case refl.refine_1
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ ¬Config.is_halted a = true

case refl.refine_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ Config.is_halted (Config.haltedOn m regs) = true
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case refl.refine_1
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ ¬Config.is_halted a = true

case refl.refine_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ Config.is_halted (Config.haltedOn m regs) = true
Tactic:
. simp at ha; simp [ha]
Proof state after:
case refl.refine_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ Config.is_halted (Config.haltedOn m regs) = true
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case refl.refine_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ Config.is_halted (Config.haltedOn m regs) = true
Tactic:
. simp
Proof state after:
no goals
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case refl.refine_3
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
this : a [S.prog]==>+ Config.haltedOn m regs
⊢ step S.prog a [S.prog]==>* Config.haltedOn m regs
Tactic:
rcases Relation.TransGen.head'_iff.mp this with ⟨e,rfl,he⟩
Proof state after:
case refl.refine_3.intro.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
this : a [S.prog]==>+ Config.haltedOn m regs
he : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) (Config.haltedOn m regs)
⊢ step S.prog a [S.prog]==>* Config.haltedOn m regs
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case refl.refine_3.intro.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
this : a [S.prog]==>+ Config.haltedOn m regs
he : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) (Config.haltedOn m regs)
⊢ step S.prog a [S.prog]==>* Config.haltedOn m regs
Tactic:
exact he
Proof state after:
no goals
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case refl.refine_1
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ ¬Config.is_halted a = true
Tactic:
simp at ha
Proof state after:
case refl.refine_1
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted a = false
⊢ ¬Config.is_halted a = true
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case refl.refine_1
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted a = false
⊢ ¬Config.is_halted a = true
Tactic:
simp [ha]
Proof state after:
no goals
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case refl.refine_2
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
d : Config (WithIO R) L
hd : Config.is_halted d = true
a : Config (WithIO R) L
regs : R → ℕ
h : a [S.prog]==>* Config.haltedOn m regs
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) (step S.prog a) d
ih :
  eval.aux S.prog
        { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, step S.prog a [S.prog]==>* Config.haltedOn m regs
ha : Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config = false
⊢ Config.is_halted (Config.haltedOn m regs) = true
Tactic:
simp
Proof state after:
no goals
Theorem: injective_def
Proof state before:
X Y Z : Type
f : X → Y
⊢ Injective f ↔ ∀ (a b : X), f a = f b → a = b
Tactic:
rfl
Proof state after:
no goals
Theorem: surjective_def
Proof state before:
X Y Z : Type
f : X → Y
⊢ Surjective f ↔ ∀ (b : Y), ∃ a, f a = b
Tactic:
rfl
Proof state after:
no goals
Theorem: id_eval
Proof state before:
X Y Z : Type
x : X
⊢ id x = x
Tactic:
rfl
Proof state after:
no goals
Theorem: comp_eval
Proof state before:
X Y Z : Type
f : X → Y
g : Y → Z
x : X
⊢ (g ∘ f) x = g (f x)
Tactic:
rfl
Proof state after:
no goals
Theorem: tends_to_def
Proof state before:
a : ℕ → ℝ
t : ℝ
⊢ tends_to a t ↔ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
Tactic:
rfl
Proof state after:
no goals
Theorem: tends_to_thirtyseven
Proof state before:
⊢ tends_to (fun x => 37) 37
Tactic:
rw [tends_to_def]
Proof state after:
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |37 - 37| < ε
Theorem: tends_to_thirtyseven
Proof state before:
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |37 - 37| < ε
Tactic:
intro ε hε
Proof state after:
ε : ℝ
hε : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |37 - 37| < ε
Theorem: tends_to_thirtyseven
Proof state before:
ε : ℝ
hε : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |37 - 37| < ε
Tactic:
use 0
Proof state after:
case h
ε : ℝ
hε : 0 < ε
⊢ ∀ (n : ℕ), 0 ≤ n → |37 - 37| < ε
Theorem: tends_to_thirtyseven
Proof state before:
case h
ε : ℝ
hε : 0 < ε
⊢ ∀ (n : ℕ), 0 ≤ n → |37 - 37| < ε
Tactic:
intro n _
Proof state after:
case h
ε : ℝ
hε : 0 < ε
n : ℕ
a✝ : 0 ≤ n
⊢ |37 - 37| < ε
Theorem: tends_to_thirtyseven
Proof state before:
case h
ε : ℝ
hε : 0 < ε
n : ℕ
a✝ : 0 ≤ n
⊢ |37 - 37| < ε
Tactic:
norm_num
Proof state after:
case h
ε : ℝ
hε : 0 < ε
n : ℕ
a✝ : 0 ≤ n
⊢ 0 < ε