Stream: Beginner Questions

Topic: arithmetic reasoning

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

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:

• algebra_simps contains basic algebraic facts for rings, such as commutativity, associativity, distributivity.
• field_simps additionally contains facts about division in fields and performs e.g. cross-multiplication but only when it can show that the divisor is non-zero.
• divide_simps does a bit less than field_simps (notably no distributivity) and unlike field_simps does a case distinction for the zeroness of the divisor. This can sometimes make the automation work better, but for most cases I would just go with field_simps.

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

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.

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)

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

zibo yang (Apr 27 2021 at 14:34):

Thanks, I get the prove

Last updated: Dec 21 2024 at 16:20 UTC