internlm/Lean-Github huggingface dataset:
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 : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h : Config.regs d WithIO.io = m
⊢ d = Config.haltedOn m fun r => Config.regs d (WithIO.internal r)
Tactic:
rcases d with ⟨ip,regs⟩
Proof state after:
case mk
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
ip : Option L
regs : WithIO R → ℕ
hd : Config.is_halted { ip := ip, regs := regs } = true
h : Config.regs { ip := ip, regs := regs } WithIO.io = m
⊢ { ip := ip, regs := regs } = Config.haltedOn m fun r => Config.regs { ip := ip, regs := 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 : ℕ
c : Config (WithIO R) L
ip : Option L
regs : WithIO R → ℕ
hd : Config.is_halted { ip := ip, regs := regs } = true
h : Config.regs { ip := ip, regs := regs } WithIO.io = m
⊢ { ip := ip, regs := regs } = Config.haltedOn m fun r => Config.regs { ip := ip, regs := regs } (WithIO.internal r)
Tactic:
simp at hd
Proof state after:
case mk
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
ip : Option L
regs : WithIO R → ℕ
h : Config.regs { ip := ip, regs := regs } WithIO.io = m
hd : ip = none
⊢ { ip := ip, regs := regs } = Config.haltedOn m fun r => Config.regs { ip := ip, regs := 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 : ℕ
c : Config (WithIO R) L
ip : Option L
regs : WithIO R → ℕ
h : Config.regs { ip := ip, regs := regs } WithIO.io = m
hd : ip = none
⊢ { ip := ip, regs := regs } = Config.haltedOn m fun r => Config.regs { ip := ip, regs := regs } (WithIO.internal r)
Tactic:
cases hd
Proof state after:
case mk.refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
regs : WithIO R → ℕ
h : Config.regs { ip := none, regs := regs } WithIO.io = m
⊢ { ip := none, regs := regs } = Config.haltedOn m fun r => Config.regs { ip := none, regs := regs } (WithIO.internal r)
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case mk.refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
regs : WithIO R → ℕ
h : Config.regs { ip := none, regs := regs } WithIO.io = m
⊢ { ip := none, regs := regs } = Config.haltedOn m fun r => Config.regs { ip := none, regs := regs } (WithIO.internal r)
Tactic:
simp [Config.haltedOn]
Proof state after:
case mk.refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
regs : WithIO R → ℕ
h : Config.regs { ip := none, regs := regs } WithIO.io = m
⊢ 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.refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
regs : WithIO R → ℕ
h : Config.regs { ip := none, regs := regs } WithIO.io = m
⊢ regs = fun x =>
    match x with
    | WithIO.io => m
    | WithIO.internal r => regs (WithIO.internal r)
Tactic:
funext r
Proof state after:
case mk.refl.h
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
regs : WithIO R → ℕ
h : Config.regs { ip := none, regs := regs } WithIO.io = m
r : WithIO R
⊢ regs r =
    match r with
    | WithIO.io => m
    | WithIO.internal r => regs (WithIO.internal r)
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case mk.refl.h
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
regs : WithIO R → ℕ
h : Config.regs { ip := none, regs := regs } WithIO.io = m
r : WithIO R
⊢ regs r =
    match r with
    | WithIO.io => m
    | WithIO.internal r => regs (WithIO.internal r)
Tactic:
cases r <;> simp at h ⊢
Proof state after:
case mk.refl.h.io
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
regs : WithIO R → ℕ
h : regs WithIO.io = m
⊢ regs WithIO.io = m
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case mk.refl.h.io
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
regs : WithIO R → ℕ
h : regs WithIO.io = m
⊢ regs WithIO.io = m
Tactic:
. exact h
Proof state after:
no goals
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case mk.refl.h.io
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
regs : WithIO R → ℕ
h : regs WithIO.io = m
⊢ regs WithIO.io = 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 : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h : ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m regs)
⊢ Config.regs d WithIO.io = 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 : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
regs : R → ℕ
h : Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m regs)
⊢ Config.regs d WithIO.io = m
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case mpr.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
regs : R → ℕ
h : Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m regs)
⊢ Config.regs d WithIO.io = m
Tactic:
have := halt_is_fixpoint _ h hd
Proof state after:
case mpr.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
regs : R → ℕ
h : Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m regs)
this : d = Config.haltedOn m regs
⊢ Config.regs d WithIO.io = m
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case mpr.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
regs : R → ℕ
h : Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m regs)
this : d = Config.haltedOn m regs
⊢ Config.regs d WithIO.io = m
Tactic:
clear h hd
Proof state after:
case mpr.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
regs : R → ℕ
this : d = Config.haltedOn m regs
⊢ Config.regs d WithIO.io = m
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case mpr.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
regs : R → ℕ
this : d = Config.haltedOn m regs
⊢ Config.regs d WithIO.io = m
Tactic:
cases this
Proof state after:
case mpr.intro.refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
regs : R → ℕ
⊢ Config.regs (Config.haltedOn m regs) WithIO.io = m
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case mpr.intro.refl
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
regs : R → ℕ
⊢ Config.regs (Config.haltedOn m regs) WithIO.io = m
Tactic:
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 : ℕ
c 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
⊢ eval.aux S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, a [S.prog]==>* Config.haltedOn m regs
Tactic:
clear c
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
⊢ eval.aux S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, a [S.prog]==>* Config.haltedOn m regs
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
⊢ eval.aux S.prog { config := a, halts := (_ : ∃ d, (a [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, a [S.prog]==>* Config.haltedOn m regs
Tactic:
unfold eval.aux
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
⊢ (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 ↔
    ∃ regs, a [S.prog]==>* Config.haltedOn m regs
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⟩
  split
  next ha =>
    simp only at *
    have := halt_is_fixpoint _ h ha
    simp [this]
  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:
case mp
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 :
  (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
this : ∃ regs, b [S.prog]==>* Config.haltedOn m regs
⊢ ∃ regs, a [S.prog]==>* Config.haltedOn m regs
Tactic:
rcases this with ⟨regs,h⟩
Proof state after:
case mp.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
h✝ :
  (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
regs : R → ℕ
h : b [S.prog]==>* Config.haltedOn m regs
⊢ ∃ regs, a [S.prog]==>* Config.haltedOn m regs
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case mp.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
h✝ :
  (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
regs : R → ℕ
h : b [S.prog]==>* Config.haltedOn m regs
⊢ ∃ regs, a [S.prog]==>* Config.haltedOn m regs
Tactic:
use regs
Proof state after:
case mp.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
h✝ :
  (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
regs : R → ℕ
h : b [S.prog]==>* Config.haltedOn m regs
⊢ a [S.prog]==>* Config.haltedOn m regs
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case mp.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
h✝ :
  (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
regs : R → ℕ
h : b [S.prog]==>* Config.haltedOn m regs
⊢ a [S.prog]==>* Config.haltedOn m regs
Tactic:
exact .head ha_to_b h
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
h :
  (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
⊢ ∃ regs, b [S.prog]==>* Config.haltedOn m regs
Tactic:
simp 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, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
h :
  (match hc : Config.is_halted a with
    | true => Config.regs a WithIO.io
    | 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
⊢ ∃ 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:
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)
h :
  (match hc : Config.is_halted a with
    | true => Config.regs a WithIO.io
    | 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
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)
Tactic:
split at h
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
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) b (Config.haltedOn m regs)

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)