internlm/Lean-Github huggingface dataset:
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case 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, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
heq✝ : Config.is_halted a = false
h :
  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
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
Tactic:
. apply ih.mp
  cases ha_to_b
  exact h
Proof state after:
no goals
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case h_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 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, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
heq✝ : Config.is_halted a = true
h : Config.regs a WithIO.io = m
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
Tactic:
have : a = b := halt_is_fixpoint _ (.single ha_to_b) ‹_›
Proof state after:
case h_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 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, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
heq✝ : Config.is_halted a = true
h : Config.regs a WithIO.io = m
this : a = b
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case h_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 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, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
heq✝ : Config.is_halted a = true
h : Config.regs a WithIO.io = m
this : a = b
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
Tactic:
cases this
Proof state after:
case h_1.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
heq✝ : Config.is_halted a = true
h : Config.regs a WithIO.io = m
ha_to_b : a [S.prog]==> a
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) a d
ih :
  eval.aux S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) a (Config.haltedOn m regs)
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) a (Config.haltedOn m regs)
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case h_1.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
heq✝ : Config.is_halted a = true
h : Config.regs a WithIO.io = m
ha_to_b : a [S.prog]==> a
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) a d
ih :
  eval.aux S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) a (Config.haltedOn m regs)
this : a = Config.haltedOn m fun x => Config.regs a (WithIO.internal x)
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) a (Config.haltedOn m regs)
Tactic:
rw [this]
Proof state after:
case h_1.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
heq✝ : Config.is_halted a = true
h : Config.regs a WithIO.io = m
ha_to_b : a [S.prog]==> a
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) a d
ih :
  eval.aux S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) a (Config.haltedOn m regs)
this : a = Config.haltedOn m fun x => Config.regs a (WithIO.internal x)
⊢ ∃ regs,
    Relation.ReflTransGen (fun c d => step S.prog c = d) (Config.haltedOn m fun x => Config.regs a (WithIO.internal x))
      (Config.haltedOn m regs)
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case h_1.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
heq✝ : Config.is_halted a = true
h : Config.regs a WithIO.io = m
ha_to_b : a [S.prog]==> a
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) a d
ih :
  eval.aux S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) a (Config.haltedOn m regs)
this : a = Config.haltedOn m fun x => Config.regs a (WithIO.internal x)
⊢ ∃ regs,
    Relation.ReflTransGen (fun c d => step S.prog c = d) (Config.haltedOn m fun x => Config.regs a (WithIO.internal x))
      (Config.haltedOn m regs)
Tactic:
refine ⟨_, Relation.ReflTransGen.refl⟩
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 : Config (WithIO R) L
heq✝ : Config.is_halted a = true
h : Config.regs a WithIO.io = m
ha_to_b : a [S.prog]==> a
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) a d
ih :
  eval.aux S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) a (Config.haltedOn m regs)
⊢ a = Config.haltedOn m fun x => Config.regs a (WithIO.internal x)
Tactic:
cases a
Proof state after:
case mk
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
ip✝ : Option L
regs✝ : WithIO R → ℕ
heq✝ : Config.is_halted { ip := ip✝, regs := regs✝ } = true
h : Config.regs { ip := ip✝, regs := regs✝ } WithIO.io = m
ha_to_b : { ip := ip✝, regs := regs✝ } [S.prog]==> { ip := ip✝, regs := regs✝ }
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) { ip := ip✝, regs := regs✝ } d
ih :
  eval.aux S.prog
        { config := { ip := ip✝, regs := regs✝ },
          halts := (_ : ∃ d, ({ ip := ip✝, regs := regs✝ } [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) { ip := ip✝, regs := regs✝ } (Config.haltedOn m regs)
⊢ { ip := ip✝, regs := regs✝ } = Config.haltedOn m fun x => Config.regs { ip := ip✝, regs := regs✝ } (WithIO.internal x)
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case mk
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
ip✝ : Option L
regs✝ : WithIO R → ℕ
heq✝ : Config.is_halted { ip := ip✝, regs := regs✝ } = true
h : Config.regs { ip := ip✝, regs := regs✝ } WithIO.io = m
ha_to_b : { ip := ip✝, regs := regs✝ } [S.prog]==> { ip := ip✝, regs := regs✝ }
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) { ip := ip✝, regs := regs✝ } d
ih :
  eval.aux S.prog
        { config := { ip := ip✝, regs := regs✝ },
          halts := (_ : ∃ d, ({ ip := ip✝, regs := regs✝ } [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) { ip := ip✝, regs := regs✝ } (Config.haltedOn m regs)
⊢ { ip := ip✝, regs := regs✝ } = Config.haltedOn m fun x => Config.regs { ip := ip✝, regs := regs✝ } (WithIO.internal x)
Tactic:
simp at *
Proof state after:
case mk
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
ip✝ : Option L
regs✝ : WithIO R → ℕ
h : regs✝ WithIO.io = m
ha_to_b : step S.prog { ip := ip✝, regs := regs✝ } = { ip := ip✝, regs := regs✝ }
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) { ip := ip✝, regs := regs✝ } d
ih :
  eval.aux S.prog
        { config := { ip := ip✝, regs := regs✝ },
          halts := (_ : ∃ d, ({ ip := ip✝, regs := regs✝ } [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) { ip := ip✝, regs := regs✝ } (Config.haltedOn m regs)
heq✝ : ip✝ = none
⊢ { ip := ip✝, regs := regs✝ } = Config.haltedOn m fun x => regs✝ (WithIO.internal x)
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case mk
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
ip✝ : Option L
regs✝ : WithIO R → ℕ
h : regs✝ WithIO.io = m
ha_to_b : step S.prog { ip := ip✝, regs := regs✝ } = { ip := ip✝, regs := regs✝ }
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) { ip := ip✝, regs := regs✝ } d
ih :
  eval.aux S.prog
        { config := { ip := ip✝, regs := regs✝ },
          halts := (_ : ∃ d, ({ ip := ip✝, regs := regs✝ } [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) { ip := ip✝, regs := regs✝ } (Config.haltedOn m regs)
heq✝ : ip✝ = none
⊢ { ip := ip✝, regs := regs✝ } = Config.haltedOn m fun x => regs✝ (WithIO.internal x)
Tactic:
simp [Config.haltedOn, *]
Proof state after:
case mk
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
ip✝ : Option L
regs✝ : WithIO R → ℕ
h : regs✝ WithIO.io = m
ha_to_b : step S.prog { ip := ip✝, regs := regs✝ } = { ip := ip✝, regs := regs✝ }
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) { ip := ip✝, regs := regs✝ } d
ih :
  eval.aux S.prog
        { config := { ip := ip✝, regs := regs✝ },
          halts := (_ : ∃ d, ({ ip := ip✝, regs := regs✝ } [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) { ip := ip✝, regs := regs✝ } (Config.haltedOn m regs)
heq✝ : ip✝ = none
⊢ regs✝ = fun x =>
    match x with
    | WithIO.io => m
    | WithIO.internal r => regs✝ (WithIO.internal r)
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case mk
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
ip✝ : Option L
regs✝ : WithIO R → ℕ
h : regs✝ WithIO.io = m
ha_to_b : step S.prog { ip := ip✝, regs := regs✝ } = { ip := ip✝, regs := regs✝ }
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) { ip := ip✝, regs := regs✝ } d
ih :
  eval.aux S.prog
        { config := { ip := ip✝, regs := regs✝ },
          halts := (_ : ∃ d, ({ ip := ip✝, regs := regs✝ } [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) { ip := ip✝, regs := regs✝ } (Config.haltedOn m regs)
heq✝ : ip✝ = none
⊢ regs✝ = fun x =>
    match x with
    | WithIO.io => m
    | WithIO.internal r => regs✝ (WithIO.internal r)
Tactic:
funext x
Proof state after:
case mk.h
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
ip✝ : Option L
regs✝ : WithIO R → ℕ
h : regs✝ WithIO.io = m
ha_to_b : step S.prog { ip := ip✝, regs := regs✝ } = { ip := ip✝, regs := regs✝ }
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) { ip := ip✝, regs := regs✝ } d
ih :
  eval.aux S.prog
        { config := { ip := ip✝, regs := regs✝ },
          halts := (_ : ∃ d, ({ ip := ip✝, regs := regs✝ } [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) { ip := ip✝, regs := regs✝ } (Config.haltedOn m regs)
heq✝ : ip✝ = none
x : WithIO R
⊢ regs✝ x =
    match x with
    | WithIO.io => m
    | WithIO.internal r => regs✝ (WithIO.internal r)
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case mk.h
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
ip✝ : Option L
regs✝ : WithIO R → ℕ
h : regs✝ WithIO.io = m
ha_to_b : step S.prog { ip := ip✝, regs := regs✝ } = { ip := ip✝, regs := regs✝ }
hb_to_d : Relation.ReflTransGen (stepsTo S.prog) { ip := ip✝, regs := regs✝ } d
ih :
  eval.aux S.prog
        { config := { ip := ip✝, regs := regs✝ },
          halts := (_ : ∃ d, ({ ip := ip✝, regs := regs✝ } [S.prog]==>* d) ∧ Config.is_halted d = true) } =
      m ↔
    ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) { ip := ip✝, regs := regs✝ } (Config.haltedOn m regs)
heq✝ : ip✝ = none
x : WithIO R
⊢ regs✝ x =
    match x with
    | WithIO.io => m
    | WithIO.internal r => regs✝ (WithIO.internal r)
Tactic:
split <;> simp [*]
Proof state after:
no goals
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case 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, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
heq✝ : Config.is_halted a = false
h :
  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
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
Tactic:
apply ih.mp
Proof state after:
case 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, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
heq✝ : Config.is_halted a = false
h :
  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
⊢ eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case 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, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
heq✝ : Config.is_halted a = false
h :
  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
⊢ eval.aux S.prog { config := b, halts := (_ : ∃ d, (b [S.prog]==>* d) ∧ Config.is_halted d = true) } = m
Tactic:
cases ha_to_b
Proof state after:
case h_2.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
heq✝ : Config.is_halted a = false
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, Relation.ReflTransGen (fun c d => step S.prog c = d) (step S.prog a) (Config.haltedOn m regs)
h :
  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
⊢ eval.aux S.prog
      { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
    m
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case h_2.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
heq✝ : Config.is_halted a = false
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, Relation.ReflTransGen (fun c d => step S.prog c = d) (step S.prog a) (Config.haltedOn m regs)
h :
  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
⊢ eval.aux S.prog
      { config := step S.prog a, halts := (_ : ∃ d, (step S.prog a [S.prog]==>* d) ∧ Config.is_halted d = true) } =
    m
Tactic:
exact h
Proof state after:
no goals
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case mpr
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
h : ∃ regs, a [S.prog]==>* Config.haltedOn m regs
⊢ (match hc :
      Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config with
    | true =>
      Config.regs { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config WithIO.io
    | 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:
rcases h with ⟨regs,h⟩
Proof state after:
case mpr.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 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
⊢ (match hc :
      Config.is_halted { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config with
    | true =>
      Config.regs { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config WithIO.io
    | 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
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case mpr.intro.h_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 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 = true
⊢ Config.regs { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) }.config WithIO.io = m

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 only at *
  have := halt_is_fixpoint _ h ha
  simp [this]
Proof state after:
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