Stream: Beginner Questions

Topic: A simple theorem about lists

view this post on Zulip Tingyou PAN (Jun 01 2024 at 14:24):

I am attempting to prove a very simple theorem about lists: summing up all elements in a list is the same as summing up all elements in a list rotated once.
I have written what is shown below:

primrec sum_list:: "real list ⇒ real" where
 "sum_list [] = 0"|
"sum_list (x # xs) = x + sum_list XS"

theorem "sum_list xs = sum_list (rotate1 xs)"
  proof (induction xs)
    case Nil
    then show ?case by auto
  next
    case (Cons a XS)
    have 1: "sum_list (a # xs) = a + sum_list xs" by auto
    have 2 : "rotate1 (x # xs) = xs @ [x]" by simp
    have 3 : "sum_list (xs @ ys) = sum_list xs + sum_list ys"
    proof (induction xs arbitrary: ys)
      case Nil
      then show ?case by auto
    next
      case (Cons a xs)
      then show ?case by auto
    qed
    from 2 and 3 have "sum_list (rotate1 (a # xs)) = sum_list xs + sum_list [a]" by try
    then show ?case by sorry
  qed

Unfortunately, Isabelle cannot verify 

sum_list (rotate1 (a # xs)) = sum_list xs + sum_list [a]

given the two verified facts

rotate1 (x # xs) = xs @ [x]

and

sum_list (xs @ ys) = sum_list xs + sum_list ys

I found this very surprising as it seems like the two facts are sufficient. I will be very grateful if anyone could explain this to me! Thank you.

view this post on Zulip Yong Kiam (Jun 01 2024 at 16:18):

the proof you've written is not syntactically well-formed, the variables a x XS xs look mixed up

view this post on Zulip Yong Kiam (Jun 01 2024 at 16:19):

theorem "sum_list xs = sum_list (rotate1 xs)"
  proof (induction xs)
    case Nil
    then show ?case by auto
  next
    case (Cons a xs)
    have 1: "sum_list (a # xs) = a + sum_list xs" by auto
    have 2 : "rotate1 (a # xs) = xs @ [a]" by simp
    have 3 : "sum_list (xs @ ys) = sum_list xs + sum_list ys" for ys
    proof (induction xs arbitrary: ys)
      case Nil
      then show ?case by auto
    next
      case (Cons a xs)
      then show ?case by auto
    qed
    from 2 and 3 have "sum_list (rotate1 (a # xs)) = sum_list xs + sum_list [a]"
      by auto
    then show ?case by auto
  qed

view this post on Zulip Yong Kiam (Jun 01 2024 at 16:20):

after fixing them it works fine, on the UI, you should have seen strange highlighting indicating the the variables are not what you think they are referring to

image.png

view this post on Zulip Tingyou PAN (Jun 09 2024 at 10:00):

Yong Kiam said:

after fixing them it works fine, on the UI, you should have seen strange highlighting indicating the the variables are not what you think they are referring to

image.png

Thank you Kiam for your help!

Last updated: Dec 21 2024 at 16:20 UTC