Stream: Beginner Questions

Topic: Working with "Least" for the towers of hanoi

view this post on Zulip Bob Rubbens (Feb 16 2025 at 13:09):

I have a definition that uses "Least" but I cannot get a witness from it. Here's a little repro that hopefully should get to the core of my problem, it depends on the LTS package from the AFP.

theory HanoiRepro
  imports Main "Labeled_Transition_Systems.LTS"
begin

context LTS
begin

fun T :: "'state ⇒ 'state ⇒ nat" where
"T p q = (LEAST i. ∃ls. (length ls = i ∧ (p, ls, q) ∈ trans_star))"

lemma
  assumes h: "1 < n" "p ≠ q"
  shows T_n: "T p q = ((2 * (T p q)) + 1)"
proof -
  have upper_bound: "T p q ≤ 2 * T p q + 1"
  proof -
    have witness_for_T: "∃ls. (T p q = length ls ∧ (p, ls, q) ∈ trans_star)" sorry
    then show ?thesis sorry
  qed
  have lower_bound: "T p q ≥ 2 * T p q + 1" sorry
  show ?thesis using lower_bound upper_bound by linarith
qed

end

end

Basically, I want to prove a recurrence relation over the function T (more or less following the outline on the proof wiki for the towers of hanoi proof: https://proofwiki.org/wiki/Tower_of_Hanoi#Setting_up_a_Recurrence_Rule). My plan was to, given some "T a b", get the "ls" associated with that and somehow convince isabelle of the lower and upper bounds.

My question is two-fold:

  1. On a practical level, how do I get a witness for the value that T returns? This essentially boils down to proving the witness_for_t fact in the example, I think.
  2. On a more theoretical level, is this the right way to go? Should I reformulate my T, or maybe not use "Least" at all?

For completeness, the T I'm using in the actual theory development looks like this:

fun T :: "nat ⇒ location ⇒ location ⇒ nat" where
"T n a b = (LEAST i. ∃ms. (length ms = i ∧ ([0..<n] ⊣ a, ms, [0..<n] ⊣ b) ∈ hanoi⇧*))"

Where ([0..<n] ⊣ a, ms, [0..<n] ⊣ b) ∈ hanoi⇧* means, a full tower on location a, using moves ms, to a full tower on location b, is an actual trace in the game of hanoi, implying ordered stacks and non-duplicate rings. I am not sure yet how I will prove something like "we must have moved the n−1 disks above it onto a vacant peg", but at least I'm pretty sure all the information I need is in the "hanoi⇧*" relation... I think at this point I might have to look at an existing formalization...!

The only example I've been able to find is https://lawrencecpaulson.github.io/2022/06/08/baby-descriptions.html, but that did not work for me. "try" just never completed the witness_for_t proof :/

view this post on Zulip Mathias Fleury (Feb 16 2025 at 13:46):

As usual, I'll refer to this thread: https://isabelle.zulipchat.com/#narrow/channel/238552-Beginner-Questions/topic/Proving.20lemma.20with.20definite.20description/near/291315915

view this post on Zulip Mathias Fleury (Feb 16 2025 at 13:47):

The pendant of (LEAST i. P i) is first ∃i. P i. This gives you a witness meaning that at least one element exists (depending of the typei, that also means that there is a least)

view this post on Zulip Bob Rubbens (Feb 16 2025 at 19:39):

As usual, I'll refer to this thread

That is helpful, thank you!

The pendant of (LEAST i. P i) is first ∃i. P i.

This is also a useful tip. Somehow I could only get a proof for this using sledgehammer. try would not find it for some reason. I'm guessing I have a few declarations that should be definitions instead of functions... Proof search has been deteriorating anyway.

Last updated: Mar 09 2025 at 12:28 UTC