Stream: Beginner Questions

Topic: Proving an Inequality

Tingyou PAN (May 31 2024 at 17:27):

I am trying to use Isabelle to prove an inequality

$$2x_1y_1+ \cdots + 2x_ny_n \le x_1^2 + \cdots + x_n^2 + y_1^2 + \cdots + y_n^2$$

The informal proof is simply applying the basic inequality

$$a^2 + b^2 \ge 2ab$$

multiple times.
However, in Isabelle, when I tried to prove this using induction , I had a skeleton program like this:

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

fun sum_list_pair:: "(real × real) list ⇒ real" where
"sum_list_pair [] = 0"|
"sum_list_pair ((x, y) # xys) = x * y + sum_list_pair xys"

theorem ineq:
  assumes "length (xs::real list) = (n::nat)" and "length (ys::real list) = (n::nat)"
  shows "sum_list (map (λx. x^2) ys) + sum_list (map (λx. x^2) zs) ≥
2 * sum_list_pair (zip ys zs)"
proof (induction n)
  case 0
  then show ?case by sorry
next
  case (Suc n)
  then show ?case sorry
qed

I am stumped by even the most trivial base case where n = 0: when I apply the proof methods auto, even the base case cannot be verified directly. May I ask how I should prove this trivial case? Also, I would really appreciate it if some suggestions could be given on how to solve the inductive step.

David Wang (May 31 2024 at 17:42):

Tingyou PAN said:

I am trying to use Isabelle to prove an inequality

$$2x_1y_1+ \cdots + 2x_ny_n \le x_1^2 + \cdots + x_n^2 + y_1^2 + \cdots + y_n^2$$

The informal proof is simply applying the basic inequality

$$a^2 + b^2 \ge 2ab$$

multiple times.
However, in Isabelle, when I tried to prove this using induction , I had a skeleton program like this:

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

fun sum_list_pair:: "(real × real) list ⇒ real" where
"sum_list_pair [] = 0"|
"sum_list_pair ((x, y) # xys) = x * y + sum_list_pair xys"

theorem ineq:
  assumes "length (xs::real list) = (n::nat)" and "length (ys::real list) = (n::nat)"
  shows "sum_list (map (λx. x^2) ys) + sum_list (map (λx. x^2) zs) ≥
2 * sum_list_pair (zip ys zs)"
proof (induction n)
  case 0
  then show ?case by sorry
next
  case (Suc n)
  then show ?case sorry
qed

I am stumped by even the most trivial base case where n = 0: when I apply the proof methods auto, even the base case cannot be verified directly. May I ask how I should prove this trivial case? Also, I would really appreciate it if some suggestions could be given on how to solve the inductive step.

You need to include the assumptions before you start the proof with using assms.

You also need to generalise the induction hypothesis by making xs and ys arbitrary, to apply it to xs' and ys'. Otherwise, you would need the specific xs and ys.

Also, be careful about variable naming: x, y, z.

A lot of the steps were solved with try, in particular the basic inequality.

moreover and ultimately store the previous line in a calculation variable and ultimately also adds the variable to the assumptions.

theorem ineq:
  assumes "length (xs::real list) = (n::nat)" and "length (ys::real list) = (n::nat)"
  shows "sum_list (map (λx. x^2) xs) + sum_list (map (λx. x^2) ys) ≥
2 * sum_list_pair (zip xs ys)"
  using assms
proof (induction n arbitrary: xs ys)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then obtain x xs' y ys' where
    "x#xs' = xs"
    "y#ys' = ys"
    "length xs' = n"
    "length ys' = n"
    using length_Suc_conv by metis
  with Suc.IH
  have "2 * sum_list_pair (zip xs' ys') ≤ Scratch.sum_list (map power2 xs') + Scratch.sum_list (map power2 ys')" by blast
  moreover have "2 * sum_list_pair (zip xs ys) = 2 * (x * y + sum_list_pair (zip xs' ys'))"
    using ‹x # xs' = xs› ‹y # ys' = ys› by force
  moreover have "Scratch.sum_list (map power2 xs) + Scratch.sum_list (map power2 ys)
    = Scratch.sum_list (map power2 xs') + x^2 + Scratch.sum_list (map power2 ys') + y^2"
    using ‹x # xs' = xs› ‹y # ys' = ys› by force
  moreover have "2 * x * y ≤ x^2 + y^2"
    by (smt (verit, ccfv_SIG) power2_diff sum_power2_ge_zero)
  ultimately show ?case by simp
qed

Tingyou PAN (May 31 2024 at 18:26):

Thank you so much for your advice! Just a quick follow up question so that I can solve similar questions in the future: when I tried using "try" or "sledgehammer", it would fail for most of time. I need to break up the goal into smaller subgoals. I often find this process intimidating since when the automatic proof methods fail, they don't provide any "feedback". Thus, may I ask how you chose the subtasks, and how you verify them? I apologize if my question is too vague. Perhaps you may recommend some Isabelle tutorials with more than toy examples?

David Wang (May 31 2024 at 18:32):

Tingyou PAN said:

Thank you so much for your advice! Just a quick follow up question so that I can solve similar questions in the future: when I tried using "try" or "sledgehammer", it would fail for most of time. I need to break up the goal into smaller subgoals. I often find this process intimidating since when the automatic proof methods fail, they don't provide any "feedback". Thus, may I ask how you chose the subtasks, and how you verify them? I apologize if my question is too vague. Perhaps you may recommend some Isabelle tutorials with more than toy examples?

Try concrete semantics: http://concrete-semantics.org/
and functional data structures and algorithms: https://functional-algorithms-verified.org/

Part 2 of the old Tutorial, which you can find in Documentation > Old Isabelle Manuals > tutorial was useful to make sense of the "Output" panel.

Tingyou PAN (May 31 2024 at 18:39):

Thanks again for your recommendation! I am currently reading concrete semantics, and I will try functional data structures and algorithms. Making sense of the output panel would help a lot as well. Also, about the "Output" panel, after I tries running the code in Isabelle, after

 have "2 * sum_list_pair (zip xs' ys') ≤ Scratch.sum_list (map power2 xs') + Scratch.sum_list (map power2 ys')" by blast

there is an error message

Illegal application of proof command in "chain" mode

I have encountered similar error messages before, including ones about "state" mode instead of "chain" mode. After carefully inspecting the code and comparing it to the error-free ones, I cannot find anything improper. How can I resolve this issue? Thank you!

David Wang (May 31 2024 at 18:41):

Tingyou PAN said:

Thanks again for your recommendation! I am currently reading concrete semantics, and I will try functional data structures and algorithms. Making sense of the output panel would help a lot as well. Also, about the "Output" panel, after I tries running the code in Isabelle, after

 have "2 * sum_list_pair (zip xs' ys') ≤ Scratch.sum_list (map power2 xs') + Scratch.sum_list (map power2 ys')" by blast

there is an error message

Illegal application of proof command in "chain" mode

I have encountered similar error messages before, including ones about "state" mode instead of "chain" mode. After carefully inspecting the code and comparing it to the error-free ones, I cannot find anything improper. How can I resolve this issue? Thank you!

I honestly have no idea what "state" and "chain" mode are, but I think that the issue in this case can be resolved by deleting Scratch..

If this is any indication, then it refers to whether you are including previously proven statements.

Tingyou PAN (May 31 2024 at 18:44):

Oh! It worked after I deleted "Scratch.". Sorry for my absent-mindedness. From the book Concrete Semantics, I have a vague idea about what "chain" mode is, and it is quite similar to what you described. Perhaps I will learn more about this from other online sources.

David Wang (May 31 2024 at 18:48):

Tingyou PAN said:

Oh! It worked after I deleted "Scratch.". Sorry for my absent-mindedness. From the book Concrete Semantics, I have a vague idea about what "chain" mode is, and it is quite similar to what you described. Perhaps I will learn more about this from other online sources.

I should not have included Scratch..

Last updated: Dec 21 2024 at 16:20 UTC