internlm/Lean-Github huggingface dataset:
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)
this : c' = d
⊢ d [S.prog]==>* Config.haltedOn o2 regs2
Tactic:
rw [←this]
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
⊢ c' [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)
this : c' = d
⊢ c' [S.prog]==>* Config.haltedOn o2 regs2
Tactic:
exact 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
n : ℕ
hn : haltsOn S n
m : ℕ
⊢ eval S n hn = m ↔ evals S n m
Tactic:
suffices ∀ c hc,
  eval.aux S.prog ⟨c,hc⟩ = m ↔
    ∃ regs, c [S.prog]==>* Config.haltedOn m regs
  from this _ _
Proof state after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
n : ℕ
hn : haltsOn S n
m : ℕ
⊢ ∀ (c : Config (WithIO R) L) (hc : halts S.prog c),
    eval.aux S.prog { config := c, halts := hc } = m ↔ ∃ regs, c [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
n : ℕ
hn : haltsOn S n
m : ℕ
⊢ ∀ (c : Config (WithIO R) L) (hc : halts S.prog c),
    eval.aux S.prog { config := c, halts := hc } = m ↔ ∃ regs, c [S.prog]==>* Config.haltedOn m regs
Tactic:
clear hn n
Proof state after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
⊢ ∀ (c : Config (WithIO R) L) (hc : halts S.prog c),
    eval.aux S.prog { config := c, halts := hc } = m ↔ ∃ regs, c [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 : ℕ
⊢ ∀ (c : Config (WithIO R) L) (hc : halts S.prog c),
    eval.aux S.prog { config := c, halts := hc } = m ↔ ∃ regs, c [S.prog]==>* Config.haltedOn m regs
Tactic:
intro c hc
Proof state after:
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c : Config (WithIO R) L
hc : halts S.prog c
⊢ eval.aux S.prog { config := c, halts := hc } = m ↔ ∃ regs, c [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 : ℕ
c : Config (WithIO R) L
hc : halts S.prog c
⊢ eval.aux S.prog { config := c, halts := hc } = m ↔ ∃ regs, c [S.prog]==>* Config.haltedOn m regs
Tactic:
rcases hc with ⟨d,h,hd⟩
Proof state after:
case intro.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
h : c [S.prog]==>* d
hd : Config.is_halted d = true
⊢ eval.aux S.prog { config := c, halts := (_ : ∃ d, (c [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, c [S.prog]==>* Config.haltedOn m regs
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case intro.intro
R L : Type
P : Prog R L
inst✝ : DecidableEq R
S : Start (WithIO R) L
m : ℕ
c d : Config (WithIO R) L
h : c [S.prog]==>* d
hd : Config.is_halted d = true
⊢ eval.aux S.prog { config := c, halts := (_ : ∃ d, (c [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, c [S.prog]==>* Config.haltedOn m regs
Tactic:
induction h using Relation.ReflTransGen.head_induction_on
Proof state after:
case intro.intro.refl
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
⊢ eval.aux S.prog { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) } = m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs

case intro.intro.head
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✝¹ c✝ : Config (WithIO R) L
h'✝ : a✝¹ [S.prog]==> c✝
h✝ : Relation.ReflTransGen (stepsTo S.prog) c✝ d
a✝ :
  eval.aux S.prog { config := c✝, halts := (_ : ∃ d, (c✝ [S.prog]==>* d) ∧ Config.is_halted d = true) } = m ↔
    ∃ regs, c✝ [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 : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
⊢ eval.aux S.prog { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) } = m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs
Tactic:
case refl =>
  unfold eval.aux
  split
  case h_2 h =>
    rw [hd] at h
    contradiction
  next h =>
  clear h
  simp
  constructor <;> intro h
  . use fun r => d.regs (.internal r)
    have : d = Config.haltedOn m (fun r => d.regs (.internal r)) := by
      rcases d with ⟨ip,regs⟩
      simp at hd; cases hd
      simp [Config.haltedOn]
      funext r
      cases r <;> simp at h ⊢
      . exact h
    rw [this] at *
    cases this
    exact .refl
  . rcases h with ⟨regs,h⟩
    have := halt_is_fixpoint _ h hd
    clear h hd
    cases this
    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
⊢ eval.aux S.prog { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) } = m ↔
    ∃ regs, d [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 : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
⊢ (match hc :
        Config.is_halted
          { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config with
      | true =>
        Config.regs { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config
          WithIO.io
      | false =>
        let c' :=
          {
            config :=
              step S.prog
                { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config,
            halts :=
              (_ :
                halts S.prog
                  (step S.prog
                    { config := d,
                        halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config)) };
        let_fun this :=
          (_ :
            { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config.ip = none →
              False);
        eval.aux S.prog c') =
      m ↔
    ∃ regs, d [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 : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
⊢ (match hc :
        Config.is_halted
          { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config with
      | true =>
        Config.regs { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config
          WithIO.io
      | false =>
        let c' :=
          {
            config :=
              step S.prog
                { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config,
            halts :=
              (_ :
                halts S.prog
                  (step S.prog
                    { config := d,
                        halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config)) };
        let_fun this :=
          (_ :
            { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config.ip = none →
              False);
        eval.aux S.prog c') =
      m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs
Tactic:
split
Proof state after:
case h_1
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
heq✝ :
  Config.is_halted { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config =
    true
⊢ Config.regs { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config
        WithIO.io =
      m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs

case h_2
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
heq✝ :
  Config.is_halted { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config =
    false
⊢ (let c' :=
        {
          config :=
            step S.prog
              { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config,
          halts :=
            (_ :
              halts S.prog
                (step S.prog
                  { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config)) };
      let_fun this :=
        (_ :
          { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config.ip = none →
            False);
      eval.aux S.prog c') =
      m ↔
    ∃ regs, d [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 : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h :
  Config.is_halted { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config =
    false
⊢ (let c' :=
        {
          config :=
            step S.prog
              { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config,
          halts :=
            (_ :
              halts S.prog
                (step S.prog
                  { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config)) };
      let_fun this :=
        (_ :
          { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config.ip = none →
            False);
      eval.aux S.prog c') =
      m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs
Tactic:
case h_2 h =>
  rw [hd] at h
  contradiction
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 : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
heq✝ :
  Config.is_halted { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config =
    true
⊢ Config.regs { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config
        WithIO.io =
      m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs
Tactic:
next h =>
clear h
simp
constructor <;> intro h
. use fun r => d.regs (.internal r)
  have : d = Config.haltedOn m (fun r => d.regs (.internal r)) := by
    rcases d with ⟨ip,regs⟩
    simp at hd; cases hd
    simp [Config.haltedOn]
    funext r
    cases r <;> simp at h ⊢
    . exact h
  rw [this] at *
  cases this
  exact .refl
. rcases h with ⟨regs,h⟩
  have := halt_is_fixpoint _ h hd
  clear h hd
  cases this
  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
h :
  Config.is_halted { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config =
    false
⊢ (let c' :=
        {
          config :=
            step S.prog
              { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config,
          halts :=
            (_ :
              halts S.prog
                (step S.prog
                  { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config)) };
      let_fun this :=
        (_ :
          { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config.ip = none →
            False);
      eval.aux S.prog c') =
      m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs
Tactic:
rw [hd] at h
Proof state after:
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.is_halted { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config =
    false
h : true = false
⊢ (let c' :=
        {
          config :=
            step S.prog
              { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config,
          halts :=
            (_ :
              halts S.prog
                (step S.prog
                  { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config)) };
      let_fun this :=
        (_ :
          { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config.ip = none →
            False);
      eval.aux S.prog c') =
      m ↔
    ∃ regs, d [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 : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h✝ :
  Config.is_halted { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config =
    false
h : true = false
⊢ (let c' :=
        {
          config :=
            step S.prog
              { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config,
          halts :=
            (_ :
              halts S.prog
                (step S.prog
                  { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config)) };
      let_fun this :=
        (_ :
          { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config.ip = none →
            False);
      eval.aux S.prog c') =
      m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs
Tactic:
contradiction
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
h :
  Config.is_halted { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config =
    true
⊢ Config.regs { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config
        WithIO.io =
      m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs
Tactic:
clear h
Proof state after:
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
⊢ Config.regs { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config
        WithIO.io =
      m ↔
    ∃ regs, d [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 : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
⊢ Config.regs { config := d, halts := (_ : ∃ d_1, (d [S.prog]==>* d_1) ∧ Config.is_halted d_1 = true) }.config
        WithIO.io =
      m ↔
    ∃ regs, d [S.prog]==>* Config.haltedOn m regs
Tactic:
simp
Proof state after:
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
⊢ Config.regs d WithIO.io = m ↔ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) d (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 : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
⊢ Config.regs d WithIO.io = m ↔ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m regs)
Tactic:
constructor <;> intro h
Proof state after:
case mp
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
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m regs)

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
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 : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h : Config.regs d WithIO.io = m
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m regs)

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:
. use fun r => d.regs (.internal r)
  have : d = Config.haltedOn m (fun r => d.regs (.internal r)) := by
    rcases d with ⟨ip,regs⟩
    simp at hd; cases hd
    simp [Config.haltedOn]
    funext r
    cases r <;> simp at h ⊢
    . exact h
  rw [this] at *
  cases this
  exact .refl
Proof state after:
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
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⟩
  have := halt_is_fixpoint _ h hd
  clear h hd
  cases this
  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 : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h : Config.regs d WithIO.io = m
⊢ ∃ regs, Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m regs)
Tactic:
use fun r => d.regs (.internal r)
Proof state after:
case mp
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
⊢ Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m fun r => Config.regs d (WithIO.internal r))
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 : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h : Config.regs d WithIO.io = m
⊢ Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m fun r => Config.regs d (WithIO.internal r))
Tactic:
have : d = Config.haltedOn m (fun r => d.regs (.internal r)) := by
  rcases d with ⟨ip,regs⟩
  simp at hd; cases hd
  simp [Config.haltedOn]
  funext r
  cases r <;> simp at h ⊢
  . exact h
Proof state after:
case mp
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
this : d = Config.haltedOn m fun r => Config.regs d (WithIO.internal r)
⊢ Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m fun r => Config.regs d (WithIO.internal r))
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 : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h : Config.regs d WithIO.io = m
this : d = Config.haltedOn m fun r => Config.regs d (WithIO.internal r)
⊢ Relation.ReflTransGen (fun c d => step S.prog c = d) d (Config.haltedOn m fun r => Config.regs d (WithIO.internal r))
Tactic:
rw [this] at *
Proof state after:
case mp
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
this :
  (Config.haltedOn m fun r => Config.regs d (WithIO.internal r)) =
    Config.haltedOn m fun r =>
      Config.regs (Config.haltedOn m fun r => Config.regs d (WithIO.internal r)) (WithIO.internal r)
⊢ Relation.ReflTransGen (fun c d => step S.prog c = d) (Config.haltedOn m fun r => Config.regs d (WithIO.internal r))
    (Config.haltedOn m fun r =>
      Config.regs (Config.haltedOn m fun r => Config.regs d (WithIO.internal r)) (WithIO.internal r))
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 : ℕ
c d : Config (WithIO R) L
hd : Config.is_halted d = true
h : Config.regs d WithIO.io = m
this :
  (Config.haltedOn m fun r => Config.regs d (WithIO.internal r)) =
    Config.haltedOn m fun r =>
      Config.regs (Config.haltedOn m fun r => Config.regs d (WithIO.internal r)) (WithIO.internal r)
⊢ Relation.ReflTransGen (fun c d => step S.prog c = d) (Config.haltedOn m fun r => Config.regs d (WithIO.internal r))
    (Config.haltedOn m fun r =>
      Config.regs (Config.haltedOn m fun r => Config.regs d (WithIO.internal r)) (WithIO.internal r))
Tactic:
cases this
Proof state after:
case mp.refl
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
⊢ Relation.ReflTransGen (fun c d => step S.prog c = d) (Config.haltedOn m fun r => Config.regs d (WithIO.internal r))
    (Config.haltedOn m fun r =>
      Config.regs (Config.haltedOn m fun r => Config.regs d (WithIO.internal r)) (WithIO.internal r))
Theorem: RegMachine.Prog.Start.eval_eq
Proof state before:
case mp.refl
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
⊢ Relation.ReflTransGen (fun c d => step S.prog c = d) (Config.haltedOn m fun r => Config.regs d (WithIO.internal r))
    (Config.haltedOn m fun r =>
      Config.regs (Config.haltedOn m fun r => Config.regs d (WithIO.internal r)) (WithIO.internal r))
Tactic:
exact .refl
Proof state after:
no goals