Cook Levin library · General · Zulip Chat Archive

I’ve been trying to use AI to prove a simple theorem using the Cook Levin library - if a Turing machine outputs a certain bit at a certain location, then the Turing machine must read that bit. Chat GPT and Claude AI haven’t been able to do it. Anyone know how to do this?

Yiran Duan (Jun 18 2025 at 11:29):

I'm interested in your question as well, and just to check whether I've understood it correctly: I can prove the following lemma by simp, is it somewhat relevant to what you are proving?

Craig Alan Feinstein (Jun 20 2025 at 01:54):

Yiran, the way I understand that statement, it means "If you write symbol w to a tape without moving the head, then reading from the tape returns w". When I asked my question, I meant if the Turing machine outputs w, then beforehand it must have read bit w. To give an idea of what I had in mind, I would like to use this to prove in Isabelle that if a Turing machine take the OR function of n bits and all n bits are zero, then the Turing machine must read all of the bits beforehand.

Yiran Duan (Jun 21 2025 at 22:31):

Thank you for explaning it again! So is it something like the following (I randomly chose some tm_copy_paste as an example)?

Here's more details including my definition for tm_copy_paste and start_cfg, where I managed to prove this lemma above in my awkward way.

Scratch.thy

theory Scratch
  imports Cook_Levin.Basics
begin

text ‹"print_tape cfg n m" prints the first m symbols of n-th tape in cfg›
fun print_tape :: "config ⇒ nat ⇒ nat ⇒ symbol list" where
  "print_tape cfg n 0 = []" |
  "print_tape cfg n (Suc m) = (print_tape cfg n m) @ [(cfg <:> n) m]"

definition copy_paste_command :: command where
  "copy_paste_command = (
    λ symbols_read_from_tapes.
      (if symbols_read_from_tapes ! 0 = □ then 1 else 0, ― ‹new state›
       [(symbols_read_from_tapes ! 0, Right), ― ‹0-th tape remains the same›
        (symbols_read_from_tapes ! 0, Right)]) ― ‹copies the symbol from 0-th tape to the 1st tape›
   )"

― ‹copy_paste_command is a well-formed command for a 2-tape TM with 1 state (excluding q_f)›
lemma "wf_command 2 1 copy_paste_command"
  unfolding copy_paste_command_def
  unfolding wf_command_def
  by simp

― ‹copy_paste_command is a Turing command for a 2-tape TM with 1 state (excluding q_f),
    and with the alphabet set containing only 4 symbols (□, ▹, 𝟬, 𝟭)›
lemma cp_tm_cmd_214: "turing_command 2 1 4 copy_paste_command"
  unfolding copy_paste_command_def
  unfolding turing_command_def
  unfolding wf_command_def
  apply auto
  by (metis One_nat_def diff_Suc_1 fst_conv less_2_cases_iff nth_Cons_0 nth_Cons_numeral numerals(1))

definition tm_copy_paste :: machine where
  "tm_copy_paste = [copy_paste_command]"

― ‹The copy-paste machine is a well-formed 2-tape TM for the alphabet set of size 4›
lemma turing_machine_tm_copy_paste: "turing_machine 2 4 tm_copy_paste"
  unfolding turing_machine_def tm_copy_paste_def
  using cp_tm_cmd_214 by auto

definition start_content :: "symbol list" where
  "start_content = [𝟭, 𝟬, 𝟭, 𝟬, 𝟬, 𝟬, 𝟭, 𝟬]"

definition start_cfg :: "config" where
  "start_cfg = start_config 2 start_content"

value "print_tape start_cfg 0 10"
value "print_tape start_cfg 1 10"
value "print_tape (execute tm_copy_paste start_cfg 10) 1 10 = print_tape start_cfg 0 10"

lemma zip2: "length xs ≥ 2 ⟹ zip [a, b] xs = [(a, xs ! 0), (b, xs ! 1)]"
  apply (induction xs)
   apply auto
  by (metis Suc_le_length_iff nth_Cons_0 zip_Cons_Cons zip_Nil)

lemma aux:
  assumes "t < 10"
  shows "fst (execute tm_copy_paste start_cfg t) = 0 ∧
         (execute tm_copy_paste start_cfg t) <#> 0 = t"
  using assms
proof (induction t)
  case 0
  then show ?case
    by (simp add: start_cfg_def start_config_def)
next
  case (Suc t)
  have "□ ∉ set start_content"
    unfolding start_content_def by simp
  let ?cfg = "execute tm_copy_paste start_cfg t"
  have "||?cfg|| = 2"
    by (metis execute_num_tapes less_2_cases_iff start_cfg_def start_config_length turing_machine_tm_copy_paste)
  from Suc have IH': "fst ?cfg = 0" "?cfg <#> 0 = t"
    by simp+
  from turing_machine_tm_copy_paste
  have "?cfg <:> 0 = start_cfg <:> 0"
    by (simp add: input_tape_constant start_cfg_def start_config_length)
  with IH'(2) have "?cfg <.> 0 = (start_cfg <:> 0) t"
    by presburger
  moreover
  have "(start_cfg <:> 0) t ≠ □"
  proof (cases "t = 0")
    case True
    then show ?thesis
      by (simp add: start_cfg_def start_config2)
  next
    case False
    from ‹Suc t < 10› have "t - 1 < length start_content"
      by (simp add: start_content_def)
    with ‹□ ∉ set start_content› have "start_content ! (t - 1) ≠ □"
      by (simp add: in_set_conv_nth)
    with start_config3[where ?cfg = start_cfg and ?k = 2 and ?xs = start_content and ?i = t]
    show ?thesis
      using False ‹t - 1 < length start_content› start_cfg_def by auto
  qed
  ultimately
  have "?cfg <.> 0 ≠ □"
    by argo
  then have "config_read ?cfg ! 0 ≠ □"
    by (metis execute_num_tapes start_cfg_def start_config_length
        tapes_at_read' turing_machine_tm_copy_paste zero_less_numeral)
  then have "[*] copy_paste_command (config_read ?cfg) = 0"
    unfolding copy_paste_command_def by simp
  then have 1: "fst (sem copy_paste_command ?cfg) = 0"
    by (simp add: sem')

  from Suc have "execute tm_copy_paste start_cfg (Suc t) =
                 sem copy_paste_command ?cfg"
    by (simp add: exe_def tm_copy_paste_def)
  also have "... = (fst (sem copy_paste_command ?cfg),
                    map (λ(a, tp). act a tp) (zip (snd (copy_paste_command (read (snd ?cfg)))) (snd ?cfg)))"
    by (simp add: sem')
  also have "... = (0, map (λ(a, tp). act a tp) (zip (snd (copy_paste_command (read (snd ?cfg)))) (snd ?cfg)))"
    using 1 by blast
  also have "... = (0, map (λ(a, tp). act a tp) (zip [(?cfg <.> 0, Right), (?cfg <.> 0, Right)] (snd ?cfg)))"
    unfolding copy_paste_command_def
    by (metis (no_types, lifting) One_nat_def Suc_1 execute_num_tapes
        less_add_Suc2 plus_1_eq_Suc read_abbrev sndI start_cfg_def
        start_config_length turing_machine_tm_copy_paste)
  also have "... = (0, [act (?cfg <.> 0, Right) (?cfg <!> 0), act (?cfg <.> 0, Right) (?cfg <!> 1)])"
    using ‹||?cfg|| = 2› zip2[where ?a = "(?cfg <.> 0, Right)" and ?b = "(?cfg <.> 0, Right)" and ?xs = "snd ?cfg"]
    by simp
  also have "... = (0, [?cfg <!> 0 |+| 1, act (?cfg <.> 0, Right) (?cfg <!> 1)])"
    using act_Right by simp
  also have "... <#> 0 = Suc (?cfg <#> 0)"
    by simp
  also have "... = Suc t"
    using ‹?cfg <#> 0 = t› by blast
  finally have "execute tm_copy_paste start_cfg (Suc t) <#> 0 = Suc t" .
  moreover
  from ‹execute tm_copy_paste start_cfg (Suc t) = sem copy_paste_command ?cfg› 1
  have "fst (execute tm_copy_paste start_cfg (Suc t)) = 0"
    by presburger
  ultimately
  show ?case by blast
qed

end

Yiran Duan (Jun 21 2025 at 22:54):

Lemma aux is much stronger than (what I understood from) your statement, but I guess it provides a way to easily prove your goal. However if the ultimate goal is to prove that the turing machine terminates with some results, I think there might be better ways without having to prove such intermediate lemmas explicitly (but that's beyond my current experience with the Cook_Levin entry; I would be happy if I get the chance to learn about it in this discussion)

Craig Alan Feinstein (Jun 22 2025 at 09:43):

Yiran, It isn’t exactly what I was thinking, but it probably will be helpful. My question seems conceptually easy and obvious at first, but I couldn’t get ai to do it and it isn’t always true. What if Turing machine M prints out bit x? Then one might think M has to read bit x. But then what if it is mathematically provable that another bit y equals bit x. Then the Turing machine doesn’t have to read bit x. It could just read bit y and print it out. So there have to be extra assumptions.

Craig Alan Feinstein (Jun 22 2025 at 20:12):

Yiran, to give a better example of what I have in mind, suppose you want to determine whether there exists a nonzero x such that given square matrix A, Ax=0, where A and x are composed of zeroes and ones and we are using mod 2 arithmetic. You don’t have to check all possibilities for x to get the answer. You can do Gaussian elimination on A to see if it is non singular. In other words if you consider a bit y for each x as to whether Ax = 0 and take the or operators of these bits y you get the answer, but you don’t have to do it this way and in fact it is better that you don’t do it this way. This is why you need extra assumptions for what I’m trying to do in Isabelle to work, namely that there are no other ways of formulating the problem other than taking the or operator. Does this make sense?

Craig Alan Feinstein (Jun 23 2025 at 01:45):

Also, look up “adversary argument” as this is the type of argument that is necessary for this to work.

Craig Alan Feinstein (Jun 24 2025 at 01:24):

Another problem I just realized is that to output bit x, a Turing machine can read not x. So technically the Turing machine doesn’t have to read bit x.

Craig Alan Feinstein (Jun 24 2025 at 01:57):

Craig Alan Feinstein (Jun 27 2025 at 20:18):

A better way of phrasing it - before a Turing machine outputs bit x, it must “know” what bit x is. Similar to before a person speaks, he has to know what he is going to say.

Stream: General

Topic: Cook Levin library

Craig Alan Feinstein (Jun 15 2025 at 17:05):