Theorem: Cpdt.Chapter7.Computation.fix'_ok (Cpdt/Chapter7/DomainTheory.lean)

State before:
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
⊢ ∀ (steps n : Nat) (x : α) (v : β),
    Subtype.val (fix' f n x) steps = some v → ∀ (n' : Nat), n' ≥ n → Subtype.val (fix' f n' x) steps = some v
Tactic:
intro steps n x v h1 n' h2
State after:
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
steps n : Nat
x : α
v : β
h1 : Subtype.val (fix' f n x) steps = some v
n' : Nat
h2 : n' ≥ n
⊢ Subtype.val (fix' f n' x) steps = some v

State before:
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
steps n : Nat
x : α
v : β
h1 : Subtype.val (fix' f n x) steps = some v
n' : Nat
h2 : n' ≥ n
⊢ Subtype.val (fix' f n' x) steps = some v
Tactic:
induction n with
| zero => simp_all_arith[fix', bottom]
| succ m ih =>
  simp_all[fix', runTo]
  sorry
State after:
no goals

State before:
case zero
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
steps : Nat
x : α
v : β
n' : Nat
h1 : Subtype.val (fix' f Nat.zero x) steps = some v
h2 : n' ≥ Nat.zero
⊢ Subtype.val (fix' f n' x) steps = some v
Tactic:
simp_all_arith[fix', bottom]
State after:
no goals

State before:
case succ
α β : Type
f : (α → Computation β) → α → Computation β
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    runTo (f v1 x) n v →
      ∀ (v2 : α → Computation β), (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → runTo (f v2 x) n v
steps : Nat
x : α
v : β
n' m : Nat
ih : Subtype.val (fix' f m x) steps = some v → n' ≥ m → Subtype.val (fix' f n' x) steps = some v
h1 : Subtype.val (fix' f (Nat.succ m) x) steps = some v
h2 : n' ≥ Nat.succ m
⊢ Subtype.val (fix' f n' x) steps = some v
Tactic:
simp_all[fix', runTo]
State after:
case succ
α β : Type
f : (α → Computation β) → α → Computation β
steps : Nat
x : α
v : β
n' m : Nat
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    Subtype.val (f v1 x) n = some v →
      ∀ (v2 : α → Computation β),
        (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → Subtype.val (f v2 x) n = some v
ih : Subtype.val (fix' f m x) steps = some v → n' ≥ m → Subtype.val (fix' f n' x) steps = some v
h1 : Subtype.val (f (fix' f m) x) steps = some v
h2 : n' ≥ Nat.succ m
⊢ Subtype.val (fix' f n' x) steps = some v

State before:
case succ
α β : Type
f : (α → Computation β) → α → Computation β
steps : Nat
x : α
v : β
n' m : Nat
f_continious :
  ∀ (n : Nat) (v : β) (v1 : α → Computation β) (x : α),
    Subtype.val (f v1 x) n = some v →
      ∀ (v2 : α → Computation β),
        (∀ (x : α), Subtype.val (v1 x) n ⊑ Subtype.val (v2 x) n) → Subtype.val (f v2 x) n = some v
ih : Subtype.val (fix' f m x) steps = some v → n' ≥ m → Subtype.val (fix' f n' x) steps = some v
h1 : Subtype.val (f (fix' f m) x) steps = some v
h2 : n' ≥ Nat.succ m
⊢ Subtype.val (fix' f n' x) steps = some v
Tactic:
sorry
State after:
no goals