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
⊢ (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
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 : ℕ
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, a [S.prog]==>* Config.haltedOn m regs

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