## 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: Dec 07 2023 at 08:19 UTC