Theorem: Cpdt.Chapter7.Computation.run_fix (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
⊢ ∀ (x : α) (v : β), run (f (fix f) x) v → run (fix f x) v
Tactic:
intro x v h
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
x : α
v : β
h : run (f (fix f) x) v
⊢ run (fix f x) 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
x : α
v : β
h : run (f (fix f) x) v
⊢ run (fix f x) v
Tactic:
cases h with
| intro n h =>
  exists n.succ
  apply f_continious
  sorry
  sorry
  sorry
State after:
no goals

State before:
case intro
α β : 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
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ run (fix f x) v
Tactic:
exists n.succ
State after:
case intro
α β : 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
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ Subtype.val (fix f x) (Nat.succ n) = some v

State before:
case intro
α β : 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
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ Subtype.val (fix f x) (Nat.succ n) = some v
Tactic:
apply f_continious
State after:
case intro.a
α β : 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
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ runTo (f ?intro.v1 x) (Nat.succ n) v

case intro.a
α β : 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
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ ∀ (x : α), Subtype.val (?intro.v1 x) (Nat.succ n) ⊑ Subtype.val (fix' f n x) (Nat.succ n)

case intro.v1
α β : 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
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ α → Computation β

State before:
case intro.a
α β : 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
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ runTo (f ?intro.v1 x) (Nat.succ n) v

case intro.a
α β : 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
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ ∀ (x : α), Subtype.val (?intro.v1 x) (Nat.succ n) ⊑ Subtype.val (fix' f n x) (Nat.succ n)

case intro.v1
α β : 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
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ α → Computation β
Tactic:
sorry
State after:
case intro.a
α β : 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
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ ∀ (x : α), Subtype.val (?intro.v1 x) (Nat.succ n) ⊑ Subtype.val (fix' f n x) (Nat.succ n)

case intro.v1
α β : 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
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ α → Computation β

State before:
case intro.a
α β : 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
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ ∀ (x : α), Subtype.val (?intro.v1 x) (Nat.succ n) ⊑ Subtype.val (fix' f n x) (Nat.succ n)

case intro.v1
α β : 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
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ α → Computation β
Tactic:
sorry
State after:
case intro.v1
α β : 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
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ α → Computation β

State before:
case intro.v1
α β : 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
x : α
v : β
n : Nat
h : Subtype.val (f (fix f) x) n = some v
⊢ α → Computation β
Tactic:
sorry
State after:
no goals