Stream: General

Topic: delta

zibo yang (Apr 26 2021 at 12:41):

Hi! can anyone explain to me why it fails since there is nothing about failure indication.

lemma delta:"∀ t::real. a * t^2 + b * t + c ≥ 0 ⟹ b^2 ≥ 4 * a * c"
proof-
  assume "∀ t::real. a * t^2 + b * t + c ≥ 0 "
  hence "∀ t::real. a * (t + b / (2*a))^2 ≥ a * ( b^2 / (4 * a^2) - c / a)" by blast

Jakub Kądziołka (Apr 26 2021 at 13:13):

this is not the type of statement that blast is good at — it's a tableau prover, so it deals with things that are true because of first-order logic

Jakub Kądziołka (Apr 26 2021 at 13:13):

First, let me say that there are some theorems that may help you in HOL-Library.Quadratic_Discriminant

Jakub Kądziołka (Apr 26 2021 at 13:16):

Second, your theorem is false:

lemma delta:"∀ t::real. a * t^2 + b * t + c ≥ 0 ⟹ b^2 ≥ 4 * a * c"
  sorry

thm delta[where a=1 and b=0 and c=1, simplified] (* outputs False *)

Jakub Kądziołka (Apr 26 2021 at 13:21):

You can make this particular inference with by (simp add: power2_eq_square algebra_simps)

Jakub Kądziołka (Apr 26 2021 at 13:22):

Also, note that it's usually preferred to use the meta-quantifiers where possible:

lemma delta:"(⋀t::real. a * t^2 + b * t + c ≥ 0) ⟹ b^2 ≥ 4 * a * c"

zibo yang (Apr 26 2021 at 13:54):

ok, but I am not very clear about the difference between \and t and $\forall t$

Max Nowak (Apr 27 2021 at 10:52):

\And t is meta-level.

Last updated: Oct 12 2024 at 20:18 UTC