## Stream: new members

### Topic: turing machine proof

#### Harold Cooper (Oct 26 2021 at 19:15):

Hi all! I'm learning Lean, and playing around with computability.turing_machine

I made the simplest possible machine M1 which just immediately halts (i.e. returns none).

It was easy for me to prove the theorem M1_halts_immediately that it halts after a single call to step, but I'd also like to prove the theorem M1_halts that the higher-level eval also halts, since I want to play with more complicated machines next.

Anyway here's my code:

import computability.turing_machine

inductive Λ -- states
| initial : Λ
| a : Λ
| b : Λ
instance Λ.inhabited : inhabited Λ := ⟨Λ.initial⟩

inductive Γ -- symbols
| zero : Γ
| one : Γ
instance Γ.inhabited : inhabited Γ := ⟨Γ.zero⟩

-- initial state and empty tape:
def initial_cfg : turing.TM0.cfg Γ Λ := turing.TM0.init []

-- machine that halts immediately:
def M1 : turing.TM0.machine Γ Λ
| _ _ := none

theorem M1_halts_immediately : turing.TM0.step M1 initial_cfg = none :=
rfl

theorem M1_halts : turing.TM0.eval M1 [] ≠ part.none :=
begin
sorry
end


How can I replace the sorry at the end? I have no idea what tactics are relevant here.

And am I even trying to prove the correct statement? I also considered ∃ x, turing.TM0.eval M1 [] = part.some x

#### Harold Cooper (Oct 26 2021 at 19:22):

(docs#turing.TM0.eval is implemented on top of docs#turing.eval which uses docs#pfun.fix and I have no idea what tactics can run/reduce pfun.fix to get to a part.some result)

#### Mario Carneiro (Oct 26 2021 at 19:31):

The main theorem for proving things about pfun.fix is docs#pfun.mem_fix_iff

#### Mario Carneiro (Oct 26 2021 at 19:32):

at least for "positive" statements, i.e. "this program halts and returns x". For negative statements you need docs#pfun.fix_induction

#### Harold Cooper (Oct 26 2021 at 19:43):

okay thanks, I'll try that!

#### Mario Carneiro (Oct 26 2021 at 19:47):

Here's one way to state and prove the theorem:

theorem M1_halts : (turing.TM0.eval M1 []).dom :=
begin
rw [turing.TM0.eval, part.map_dom, part.dom_iff_mem],
existsi _,
rw [turing.mem_eval],
refine ⟨relation.refl_trans_gen.refl, _⟩,
refl,
end


#### Harold Cooper (Oct 26 2021 at 19:52):

oh awesome, I think this will teach me a lot.

so is the theorem(…).dom saying that the partial function has a non-empty domain, and thus halts?

#### Mario Carneiro (Oct 26 2021 at 20:01):

part A is actually a "partial value", kind of like a partial function but over just one point. So if p : part A then p.dom is a proposition that says whether the value exists, and p.get : p.dom -> A is either the empty function or a function on a singleton returning a single value of type A

#### Mario Carneiro (Oct 26 2021 at 20:02):

So turing.TM0.eval M1 [] is "the value that results from executing M1 on [], if it exists", and (turing.TM0.eval M1 []).dom is asserting that the value exists, i.e. the machine halts

#### Mario Carneiro (Oct 26 2021 at 20:03):

A partial function A ->. B is defined as A -> part B

#### Harold Cooper (Oct 26 2021 at 20:05):

ah okay got it, that makes sense

#### YJ (Oct 26 2021 at 20:52):

Hello all! I am new to Lean and am currently following the tutorials from the theorem proving in lean 3, are there any published solutions with the questions?

#### Kevin Buzzard (Oct 26 2021 at 21:09):

You're in the wrong thread (hint: start a new one) but the answer to your question is that as far as I know there aren't; however if you're stuck on something you could ask in a new thread in #new members

#### Harold Cooper (Nov 30 2021 at 17:48):

I did a bit more with this recently, including proving that a simple looping machine doesn't halt which was more fun than proving that things do halt :p

However, I was only able to do that using an alternative formulation of halting, which I'm pretty sure is equivalent to what we used earlier in this thread, but now I would like to prove that it is!

Specifically, the two definitions of halting which I want to prove are equivalent are:

def halts (M : turing.TM0.machine Γ Λ) : Prop :=
∃ n, multistep M n [] = none

def halts''' (M : turing.TM0.machine Γ Λ) : Prop :=
∃ x, turing.TM0.eval M [] = part.some x


(multistep M n just steps the machine n times—I'll include the full code below.)

#### Harold Cooper (Nov 30 2021 at 17:49):

In the following code, I started an attempt at the proof halts_iff''', where the sorry statements are. Based on @Mario Carneiro's tips above, I'm guessing I need to do something with docs#pfun.mem_fix_iff or docs#pfun.fix_induction ?

import computability.turing_machine

inductive Λ -- states
| A : Λ
| B : Λ
| C : Λ
instance Λ.inhabited : inhabited Λ := ⟨Λ.A⟩

inductive Γ -- symbols
| zero : Γ
| one : Γ
instance Γ.inhabited : inhabited Γ := ⟨Γ.zero⟩

-- initial state and empty tape:
def cfg₀ : turing.TM0.cfg Γ Λ := turing.TM0.init []

-- chainable step function:
def step' (M : turing.TM0.machine Γ Λ) (x : option (turing.TM0.cfg Γ Λ)) :
option (turing.TM0.cfg Γ Λ) :=
x.bind (turing.TM0.step M)

def multistep (M : turing.TM0.machine Γ Λ) :
ℕ → option (turing.TM0.cfg Γ Λ) → option (turing.TM0.cfg Γ Λ) :=
nat.repeat (λ _, step' M)

theorem multistep_none_add {cfg M n m} (hn : multistep M n cfg = none) :
multistep M (n + m) cfg = none :=
begin
induction m with m hm,
{ exact hn, },
{ rw [multistep, nat.add_succ, nat.repeat, ← multistep, hm],
refl, },
end

theorem multistep_none_ge {cfg M n} {m ≥ n} (hn : multistep M n cfg = none) :
multistep M m cfg = none :=
begin
end

-- equivalent definitions of halting:

def halts (M : turing.TM0.machine Γ Λ) : Prop :=
∃ n, multistep M n cfg₀ = none

def halts' (M : turing.TM0.machine Γ Λ) : Prop :=
(turing.TM0.eval M []).dom

def halts'' (M : turing.TM0.machine Γ Λ) : Prop :=
turing.TM0.eval M [] ≠ part.none

def halts''' (M : turing.TM0.machine Γ Λ) : Prop :=
∃ x, turing.TM0.eval M [] = part.some x

theorem halts'_iff'' {M} : halts' M ↔ halts'' M :=
begin
rw [halts'', ne.def, part.eq_none_iff', ← halts'],
exact not_not.symm,
end

theorem halts''_iff''' {M} : halts'' M ↔ halts''' M :=
part.ne_none_iff

theorem halts_iff''' {M} : halts M ↔ halts''' M :=
begin
rw [halts, halts'''],
split; intro h,
{ cases h with n h,
induction n with n hn,
{ sorry, },
{ sorry, },
},
{ cases h with x h,
sorry, },
end

-- machine that halts immediately:
def M₁ : turing.TM0.machine Γ Λ
| _ _ := none

theorem M₁_halts_immediately : turing.TM0.step M₁ cfg₀ = none :=
rfl

theorem M₁_halts : halts M₁ :=
⟨1, rfl⟩

theorem M₁_halts' : halts' M₁ :=
begin
rw [halts', turing.TM0.eval, part.map_dom, part.dom_iff_mem],
existsi _,
rw turing.mem_eval,
split,
{ exact relation.refl_trans_gen.refl, },
{ refl, },
end

theorem M₁_halts'' : halts'' M₁ :=
halts'_iff''.mp M₁_halts'

theorem M₁_halts''' : halts''' M₁ :=
halts''_iff'''.mp M₁_halts''

-- machine that goes A → B → halt:
def M₂ : turing.TM0.machine Γ Λ
| Λ.A symbol := some ⟨Λ.B, turing.TM0.stmt.write symbol⟩
| _ _ := none

theorem M₂_halts : halts M₂ :=
⟨2, rfl⟩

theorem M₂_halts' : halts' M₂ :=
begin
rw [halts', turing.TM0.eval, part.map_dom, part.dom_iff_mem],
existsi turing.TM0.cfg.mk Λ.B (turing.tape.mk₁ []),
rw turing.mem_eval,
split,
{ sorry, },
{ refl, },
end

-- machine that loops A → B → A → B → ⋯:
def M₃ : turing.TM0.machine Γ Λ
| Λ.A symbol := some ⟨Λ.B, turing.TM0.stmt.write symbol⟩
| Λ.B symbol := some ⟨Λ.A, turing.TM0.stmt.write symbol⟩
| _ _ := none

lemma M₃_AB_only {n} : ∃ tape,
multistep M₃ n cfg₀ = some ⟨Λ.A, tape⟩ ∨ multistep M₃ n cfg₀ = some ⟨Λ.B, tape⟩ :=
begin
induction n with n hn,
{ existsi _,
left,
refl, },
{ cases hn with tape_n hn,
cases hn; existsi _,
{
right,
rw [multistep, nat.repeat, ← multistep, hn, step', option.bind, turing.TM0.step],
simp,
existsi _,
existsi _,
split; refl, },
{
left,
rw [multistep, nat.repeat, ← multistep, hn, step', option.bind, turing.TM0.step],
simp,
existsi _,
existsi _,
split; refl, },
},
end

theorem M₃_not_halts : ¬ halts M₃ :=
begin
intro h,
cases h with n hn,
cases M₃_AB_only with tape h_tape,
cases h_tape; {
rw h_tape at hn,
exact option.no_confusion hn,
},
end


(There's also an unfinished proof M₂_halts' of a machine halting in two steps, just because I felt like I should be able to figure it out after proving M₁_halts' that a machine halts in one step, but I couldn't… am curious to learn what I'm missing)

#### Harold Cooper (Nov 30 2021 at 17:49):

Sorry this is a bit long, any tips appreciated!

#### Harold Cooper (Dec 01 2021 at 20:26):

Here's a much more concise version of what I'm trying to prove in case anyone has some tips:

import computability.turing_machine

inductive Λ -- states
| A : Λ
| B : Λ
| C : Λ
instance Λ.inhabited : inhabited Λ := ⟨Λ.A⟩

inductive Γ -- symbols
| zero : Γ
| one : Γ
instance Γ.inhabited : inhabited Γ := ⟨Γ.zero⟩

-- initial state and empty tape:
def cfg₀ : turing.TM0.cfg Γ Λ := turing.TM0.init []

-- chainable step function (since both its input and output have the same option type):
def step' (M : turing.TM0.machine Γ Λ) (x : option (turing.TM0.cfg Γ Λ)) :
option (turing.TM0.cfg Γ Λ) :=
x.bind (turing.TM0.step M)

-- step a given number of times:
def multistep (M : turing.TM0.machine Γ Λ) :
ℕ → option (turing.TM0.cfg Γ Λ) → option (turing.TM0.cfg Γ Λ) :=
nat.repeat (λ _, step' M)

-- I'm trying to prove this:
example {M} : (∃ n, multistep M n cfg₀ = none) ↔ (∃ x, turing.TM0.eval M [] = part.some x) :=
begin
sorry
end

-- or this if it's easier, since I've already proven (turing.TM0.eval M []).dom ↔ (∃ x, turing.TM0.eval M [] = part.some x)
example {M} : (∃ n, multistep M n cfg₀ = none) ↔ (turing.TM0.eval M []).dom :=
begin
sorry
end


Thanks!

#### Mario Carneiro (Dec 01 2021 at 21:04):

Sorry, I forgot to respond to this one. I made some minor tweaks but it's essentially the same theorem:

def multistep (M : turing.TM0.machine Γ Λ) :
ℕ → option (turing.TM0.cfg Γ Λ) → option (turing.TM0.cfg Γ Λ) :=
nat.iterate (step' M)

example {M} : (∃ n, multistep M n (some cfg₀) = none) ↔ (turing.TM0.eval M []).dom :=
begin
simp [turing.TM0.eval, cfg₀, multistep],
split,
{ rintro ⟨n, e⟩,
generalize_hyp : turing.TM0.init [] = k at e ⊢,
induction n with n IH generalizing k, {cases e},
rw [nat.iterate, step', option.bind] at e,
cases e' : turing.TM0.step M k; rw e' at e,
{ exact part.dom_iff_mem.2 ⟨_, turing.mem_eval.2 ⟨relation.refl_trans_gen.refl, e'⟩⟩ },
{ rw turing.reaches_eval (relation.refl_trans_gen.single e'),
exact IH _ e } },
{ intro h,
obtain ⟨a, h⟩ := part.dom_iff_mem.1 h,
refine turing.eval_induction h (λ k h IH, _),
cases e : turing.TM0.step M k,
{ exact ⟨1, e⟩ },
{ obtain ⟨n, hn⟩ := IH _ _ e,
{ exact ⟨n+1, by simp [nat.iterate, step', e, hn]⟩ },
{ rwa ← turing.reaches_eval (relation.refl_trans_gen.single e) } } }
end


#### Harold Cooper (Dec 01 2021 at 21:14):

Oh awesome, thanks as always @Mario Carneiro!

I'll step through this and likely learn quite a few things

#### Harold Cooper (Dec 01 2021 at 21:22):

oh and good call on nat.iterate, I didn't know about that

Last updated: Dec 20 2023 at 11:08 UTC