Stream: Beginner Questions

Topic: arithmetic reasoning


view this post on Zulip zibo yang (Apr 27 2021 at 13:53):

Sorry, I always cannot get the point why isabelle cannot reason such a easy equation:

lemma delta4:
  fixes a b c ::real
  assumes"⋀t . a * t^2 + b * t + c ≥ 0"
  shows"b^2 ≤ 4 * a * c"
proof cases
  assume "a = 0"
  with assms have"⋀t . b * t + c ≥ 0"
    by auto
  have "b ≠ 0 ⟹ ∃t . b * t + c < 0"
  proof
    fix b c t::real
    assume "b ≠ 0"
    hence "t = (-1 - c) / b ⟷ b * t = -1 - c"
      by auto

view this post on Zulip Manuel Eberl (Apr 27 2021 at 13:59):

What you need to understand is that auto is not magic. It is not an automated theorem prover that uses everything at its disposal to prove what you give to it. It is a tool that uses only the facts that you give to it, plus various standard techniques (most importantly rewriting with the simplifier).

Your question is basically how to do arithmetic reasoning. The answer is to add suitable rewrite rules. There are a number of collections of such rewrite rules for arithmetic reasoning:

So in your case, the statement should go through with by (auto simp: field_simps).

view this post on Zulip Manuel Eberl (Apr 27 2021 at 14:01):

As a side note, you are not allowed to do fix b c t in that subproof. That would only be allowed if these variables were universally quantified, which they are not. Plus you're not allowed to fix t, rather you have to provide a suitable value for t. In any case, I am not sure what you are trying to achieve with that existential statement anyway.

view this post on Zulip Max Nowak (Apr 27 2021 at 14:10):

(Or if you're lazy like me, just do try or sledgehammer and let Isabelle do the work for you :P)

view this post on Zulip zibo yang (Apr 27 2021 at 14:16):

Thanks, but what should I do to prove the existence of t since it fails at blast:

 have "b ≠ 0 ⟹ ∃t . b * t + c < 0"
  proof-
    assume "b ≠ 0"
    hence "(t1::real) = (-1 - c) / b ⟷ b * t1 + c = -1"
      by (simp add: field_simps)
    thus "∃t. b * t + c < 0"
      by blast
  qed

view this post on Zulip zibo yang (Apr 27 2021 at 14:34):

Thanks, I get the prove


Last updated: Mar 29 2024 at 08:18 UTC