Matthew Pocock (Aug 24 2023 at 22:03): Matthew Pocock (Aug 24 2023 at 22:03):I'm having a play learning isabelle/HOL by tinkering with the collatz conjecture. The central question is if a recursive function terminates or not. I've tried to capture it like this:
fun collatz_step :: "nat ⇒ nat"
where
"collatz_step n = (if even n then n div 2 else n * 3 + 1)"
function collatz_chain :: "nat ⇒ nat list"
where
"collatz_chain 0 = [0]" |
"collatz_chain (Suc 0) = [1]" |
"collatz_chain (Suc (Suc n)) = (Suc (Suc n)) # (collatz_chain (collatz_step (Suc (Suc n))))"
by
pat_completeness
auto
However, obviously I don't have a proof that collatz_chain terminates. If I did, I'd have solved the conjecture already. How should I tell Isabelle the problem without needing to already have the solution? I'm open to alternative representations and using different language constructs.
Thanks :D
Mathias Fleury (Aug 25 2023 at 04:47):You could sorrythe termination
Mathias Fleury (Aug 25 2023 at 04:54):Or you work on a locale context where you assume that it terminates:
locale test =
assumes t: ‹⋀x. collatz_chain_dom x›
begin
termination using t by auto
lemma ‹A = tl (collatz_chain 3)›
apply (auto simp: numeral_eq_Suc)
sorry
end
However your definition is not terminating
Mathias Fleury (Aug 25 2023 at 04:59):The argument of the function is never decreasing (3 -> 5 -> 7 -> .... in the third branch of the function)
Mathias Fleury (Aug 25 2023 at 05:04):(division by 2 is missing)
Wolfgang Jeltsch (Aug 25 2023 at 13:08):Would it help to construct a potentially infinite list of all intermediate values and, if it exists, the final value? Then the Collatz conjecture would be that for all start values the corresponding list is finite. The corec tutorial defines a Collatz function similar to what I described as an example (it leaves out the downward steps, from what I remember).
Matthew Pocock (Aug 26 2023 at 20:37):OK, so I think I'm going to re-write it as function collatz_chain_bounded:: "nat => nat => nat list" where the first nat is a counter. So instead of asking if it terminates at all, ask if it terminates within n steps, where we can choose n arbitrarily.
Matthew Pocock (Aug 27 2023 at 12:58):Wolfgang Jeltsch said:
Would it help to construct a potentially infinite list of all intermediate values and, if it exists, the final value?
Sorry for being an utter noob, but can you sketch what that would look like please?
Mathias Fleury (Aug 27 2023 at 13:03):I guess Wolfgang means https://isabelle.in.tum.de/dist/Isabelle2022/doc/corec.pdf (and page 7, search for Collatz)
Mathias Fleury (Aug 27 2023 at 13:04):From there you could extract a everything until you reach a one or something like that
Matthew Pocock (Aug 27 2023 at 13:15):Thanks :D Another thing I should read. But yes, the stream type seems like it much more naturally captures the way I'm thinking about this stuff than dealing with concrete lists. I think from this I can start to make some simple inductive proofs. Cheers.
Matthew Pocock (Aug 27 2023 at 14:10):I seem to hit problems with streams. I'm probably doing something wrong. Here's my code. When evaluating the value line it barfs with:
[Info - 15:07:31] Warning - Unable to increase stack - interrupting thread
I was expecting stake to just evaluate the minimum number of terms needed to construct the list, but it kind of seems like it is trying to evaluate the stream to termination. Is this a RTFM problem on my part? I'm finding the documentation quite difficult to follow in places so it could be.
imports
Main
"HOL-Library.Stream"
"HOL-Library.BNF_Corec"
begin
fun collatz_step :: "nat \<Rightarrow> nat" where
"collatz_step n = (if even n then n div 2 else 3 * n + 1)"
corec
collatz_chain :: "nat \<Rightarrow> nat stream"
where
"collatz_chain n = SCons n (collatz_chain(collatz_step n))"
value "stake 5 (collatz_chain 3)"
The default code generator does not handle corecursive function nicely
Mathias Fleury (Aug 27 2023 at 14:18):you probably have to export code to Haskell
Mathias Fleury (Aug 27 2023 at 14:19):To do it in Isabelle directly, I had to do unfolding by hand:
lemma "A = stake 5 (collatz_chain 3)"
apply (subst collatz_chain.corec.code)
apply (subst collatz_chain.corec.code)
apply (subst collatz_chain.corec.code)
apply (subst collatz_chain.corec.code)
apply (subst collatz_chain.corec.code)
apply simp
apply (simp add: numeral_eq_Suc )
done
Mathias Fleury said:
To do it in Isabelle directly, I had to do unfolding by hand:
Oh my! That's going to become a bit laborious. Thanks.
Mathias Fleury (Aug 27 2023 at 18:44):I don't really know why it is so weird
Mathias Fleury (Aug 27 2023 at 18:45):but you probably can solve the problem by a simp rules for stake (Suc n) (collatz_chain (Suc z))
Dmitriy Traytel (Aug 28 2023 at 06:48):The proper way would be to import HOL-Library.Code_Lazy and add the line code_lazy_type stream somewhere before the value command.
Dmitriy Traytel (Aug 28 2023 at 06:50):See also http://www.andreas-lochbihler.de/pub/lochbihler2018iw.pdf for a description of how this works.
Matthew Pocock (Aug 28 2023 at 13:27):Dmitriy Traytel said:
The proper way would be to import
HOL-Library.Code_Lazyand add the linecode_lazy_type streamsomewhere before thevaluecommand.
Thank you - I will try this. I was about to start learning COQ :D
Matthew Pocock (Aug 30 2023 at 13:48):Thank you for all your help. I feel a little less like I'm stumbling in the dark.
I have written a function that defines reaching 1 in a collatz chain, and then two lemmas for chains starting at 1 and at n. I've managed to stumble through proofs for these. Is this idiomatic isabelle or can I structure the proofs in a neater or more compact way? It feels very manual, although I'm sure it is doing a lot of work under the hood.
fun reaches_1 :: "nat \<Rightarrow> bool"
where "reaches_1 n = (1 \<in> sset (collatz_chain n))"
lemma collatz_chain_of_1_reaches_1 [simp]: "reaches_1 1"
apply simp
apply (subst collatz_chain.corec.code)
apply simp
done
lemma collatz_chain_induction[simp]: "reaches_1 (collatz_step n) --> reaches_1 n"
apply auto
apply (subst collatz_chain.corec.code)
apply (subst Collatz.collatz_step.simps)
apply auto
apply (subst collatz_chain.corec.code)
apply (subst Collatz.collatz_step.simps)
apply auto
done
Last updated: Apr 27 2024 at 20:14 UTC