Unprovable termination goal using Monad · Beginner Questions

Hi :) I am using the time monad from Root_Balanced_Tree.Time_Monad, and having trouble with proving termination for one function. The following is a minimal example:

theory Scratch
  imports Root_Balanced_Tree.Time_Monad
begin

fun drop_tm :: "nat ⇒ 'a list ⇒ 'a list tm" where
"drop_tm n [] =1 return []"
| "drop_tm n (x # xs) =1 (case n of 0 ⇒ return (x # xs) | Suc m ⇒
    do {
      r ← drop_tm m xs;
      return r
    })"

function (sequential) test :: "'a list ⇒ 'a list list tm" where
"test [] = return []"
| "test xs = do {
    s ← drop_tm 1 xs;
    r ← (test s);
    return r
  }"
  by pat_completeness auto
termination
  apply (relation "measure length")
  subgoal by simp
  subgoal for x xs y by (cases xs; simp)
  done

end

The termination proof fails, because the second subgoal generated by apply (relation "measure length") is unsolvable. If I rewrite the test-function to

| "test xs = do {
    s ← drop_tm 1 xs;
    r ← (test (val (drop_tm 1 xs)));
    return r
  }"

(i.e. just change s to val (drop_tm 1 xs)) then the termination-proof succeeds flawlessly. What's going on here?

Jakob Schulz (Apr 17 2023 at 19:42):

@Emin Karayel was able to solve this problem :) For future reference: the trick was to prove the following congruence rule:

lemma bind_tm_cong[fundef_cong]:
  assumes "f1 = f2"
  assumes "g1 (val f1) = g2 (val f2)"
  shows "f1 ⤜ g1 = f2 ⤜ g2"
  using assms unfolding bind_tm_def
  by (cases f1;cases f2) auto

Stream: Beginner Questions

Topic: Unprovable termination goal using Monad

Jakob Schulz (Apr 15 2023 at 18:32):

Jakob Schulz (Apr 17 2023 at 19:42):