α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
b : β
s : Computation α
e : α
h : Results (bind (pure e) f) b Nat.zero
⊢ ∃ a m n, Results (pure e) a m ∧ Results (f a) b n ∧ Nat.zero = n + m

α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
b : β
s e : Computation α
h : Results (bind (think e) f) b Nat.zero
⊢ ∃ a m n, Results (think e) a m ∧ Results (f a) b n ∧ Nat.zero = n + m

α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, Results (bind s f) b n → ∃ a m n_1, Results s a m ∧ Results (f a) b n_1 ∧ n = n_1 + m
s : Computation α
e : α
h : Results (bind (pure e) f) b (Nat.succ n)
⊢ ∃ a m n_1, Results (pure e) a m ∧ Results (f a) b n_1 ∧ Nat.succ n = n_1 + m

α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, Results (bind s f) b n → ∃ a m n_1, Results s a m ∧ Results (f a) b n_1 ∧ n = n_1 + m
s e : Computation α
h : Results (bind (think e) f) b (Nat.succ n)
⊢ ∃ a m n_1, Results (think e) a m ∧ Results (f a) b n_1 ∧ Nat.succ n = n_1 + m
α : Type u
β : Type v
γ : Type w
s : Computation α
f : α → Computation β
b : β
k : ℕ
⊢ Results (bind s f) b k → ∃ a m n, Results s a m ∧ Results (f a) b n ∧ k = n + m
induction' k with n IH generalizing s <;> apply recOn s (fun a => _) fun s' => _ <;> intro e h
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
b : β
s : Computation α
e : α
h : Results (f e) b 0
⊢ ∃ a m n, Results (pure e) a m ∧ Results (f a) b n ∧ Nat.zero = n + m
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
b : β
s : Computation α
e : α
h : Results (bind (pure e) f) b Nat.zero
⊢ ∃ a m n, Results (pure e) a m ∧ Results (f a) b n ∧ Nat.zero = n + m
simp [thinkN] at h
no goals
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
b : β
s : Computation α
e : α
h : Results (f e) b 0
⊢ ∃ a m n, Results (pure e) a m ∧ Results (f a) b n ∧ Nat.zero = n + m
refine' ⟨e, _, _, results_pure _, h, rfl⟩
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
b : β
s e : Computation α
h : Results (bind (think e) f) b Nat.zero
this : head (bind (think e) f) = head (thinkN (pure b) Nat.zero)
⊢ ∃ a m n, Results (think e) a m ∧ Results (f a) b n ∧ Nat.zero = n + m
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
b : β
s e : Computation α
h : Results (bind (think e) f) b Nat.zero
⊢ ∃ a m n, Results (think e) a m ∧ Results (f a) b n ∧ Nat.zero = n + m
have := congr_arg head (eq_thinkN h)
no goals
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
b : β
s e : Computation α
h : Results (bind (think e) f) b Nat.zero
this : head (bind (think e) f) = head (thinkN (pure b) Nat.zero)
⊢ ∃ a m n, Results (think e) a m ∧ Results (f a) b n ∧ Nat.zero = n + m
contradiction
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, Results (bind s f) b n → ∃ a m n_1, Results s a m ∧ Results (f a) b n_1 ∧ n = n_1 + m
s : Computation α
e : α
h : Results (f e) b (Nat.succ n)
⊢ ∃ a m n_1, Results (pure e) a m ∧ Results (f a) b n_1 ∧ Nat.succ n = n_1 + m
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, Results (bind s f) b n → ∃ a m n_1, Results s a m ∧ Results (f a) b n_1 ∧ n = n_1 + m
s : Computation α
e : α
h : Results (bind (pure e) f) b (Nat.succ n)
⊢ ∃ a m n_1, Results (pure e) a m ∧ Results (f a) b n_1 ∧ Nat.succ n = n_1 + m
simp at h
no goals
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, Results (bind s f) b n → ∃ a m n_1, Results s a m ∧ Results (f a) b n_1 ∧ n = n_1 + m
s : Computation α
e : α
h : Results (f e) b (Nat.succ n)
⊢ ∃ a m n_1, Results (pure e) a m ∧ Results (f a) b n_1 ∧ Nat.succ n = n_1 + m
refine' ⟨e, _, n + 1, results_pure _, h, rfl⟩
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, Results (bind s f) b n → ∃ a m n_1, Results s a m ∧ Results (f a) b n_1 ∧ n = n_1 + m
s e : Computation α
h : Results (bind e f) b n
⊢ ∃ a m n_1, Results (think e) a m ∧ Results (f a) b n_1 ∧ Nat.succ n = n_1 + m
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, Results (bind s f) b n → ∃ a m n_1, Results s a m ∧ Results (f a) b n_1 ∧ n = n_1 + m
s e : Computation α
h : Results (bind (think e) f) b (Nat.succ n)
⊢ ∃ a m n_1, Results (think e) a m ∧ Results (f a) b n_1 ∧ Nat.succ n = n_1 + m
simp at h
no goals
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, Results (bind s f) b n → ∃ a m n_1, Results s a m ∧ Results (f a) b n_1 ∧ n = n_1 + m
s e : Computation α
h : Results (bind e f) b n
⊢ ∃ a m n_1, Results (think e) a m ∧ Results (f a) b n_1 ∧ Nat.succ n = n_1 + m
exact by
  let ⟨a, m, n', h1, h2, e'⟩ := IH h
  rw [e'] ; exact ⟨a, m.succ, n', results_think h1, h2, rfl⟩
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, Results (bind s f) b n → ∃ a m n_1, Results s a m ∧ Results (f a) b n_1 ∧ n = n_1 + m
s e : Computation α
h : Results (bind e f) b n
a : α
m n' : ℕ
h1 : Results e a m
h2 : Results (f a) b n'
e' : n = n' + m
⊢ ∃ a m n_1, Results (think e) a m ∧ Results (f a) b n_1 ∧ Nat.succ n = n_1 + m
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, Results (bind s f) b n → ∃ a m n_1, Results s a m ∧ Results (f a) b n_1 ∧ n = n_1 + m
s e : Computation α
h : Results (bind e f) b n
⊢ ∃ a m n_1, Results (think e) a m ∧ Results (f a) b n_1 ∧ Nat.succ n = n_1 + m
let ⟨a, m, n', h1, h2, e'⟩ := IH h
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, Results (bind s f) b n → ∃ a m n_1, Results s a m ∧ Results (f a) b n_1 ∧ n = n_1 + m
s e : Computation α
h : Results (bind e f) b n
a : α
m n' : ℕ
h1 : Results e a m
h2 : Results (f a) b n'
e' : n = n' + m
⊢ ∃ a m_1 n, Results (think e) a m_1 ∧ Results (f a) b n ∧ Nat.succ (n' + m) = n + m_1
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, Results (bind s f) b n → ∃ a m n_1, Results s a m ∧ Results (f a) b n_1 ∧ n = n_1 + m
s e : Computation α
h : Results (bind e f) b n
a : α
m n' : ℕ
h1 : Results e a m
h2 : Results (f a) b n'
e' : n = n' + m
⊢ ∃ a m n_1, Results (think e) a m ∧ Results (f a) b n_1 ∧ Nat.succ n = n_1 + m
rw [e']
no goals
α : Type u
β : Type v
γ : Type w
s✝ : Computation α
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, Results (bind s f) b n → ∃ a m n_1, Results s a m ∧ Results (f a) b n_1 ∧ n = n_1 + m
s e : Computation α
h : Results (bind e f) b n
a : α
m n' : ℕ
h1 : Results e a m
h2 : Results (f a) b n'
e' : n = n' + m
⊢ ∃ a m_1 n, Results (think e) a m_1 ∧ Results (f a) b n ∧ Nat.succ (n' + m) = n + m_1
exact ⟨a, m.succ, n', results_think h1, h2, rfl⟩