Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] "PROOF FAILED for depth4"

Email Gateway (Aug 18 2022 at 15:02):

From: Steve W <s.wong.731@googlemail.com>
Hi,

I'm experimenting with a simple proof, but I keep getting an error saying
"PROOF FAILED for depth 4". Here's my theory:

consts
s :: real
f :: real
F :: "real => real"
Y :: "real => real"
Z :: "real => real"

axioms
ax1 : "F t = Y t + Z t"
ax2 : "Y s = -1"
ax3 : "Z s = 1"

lemma funczero: "EX func t. func t = 0"
using ax1 ax2 ax3
by auto

I suspect providing ax1 ax2 ax3 and using auto is not sufficient to prove
the lemma. However, if I do:

lemma te_zero: "EX func t. func t = 0"
proof
show "F s = 0"

I get an error saying:

*** Local statement will fail to refine any pending goal
*** Failed attempt to solve goal by exported rule:
*** F s = 0
*** At command "show".

Isn't "F s = 0" a witness for the existential statement?

Thanks
Steve

Email Gateway (Aug 18 2022 at 15:02):

From: Alexander Krauss <krauss@in.tum.de>
Hi Steve,

The implicit step at the "proof" command introduces one existential
quantifier. Thus, in the body, you are expected to prove
"EX t. ?func t = 0" which does not match what you have in your
show-statement. When experimenting, you can look at the goal state to
see what you are expected to prove at a given point.

Here are a few options that work:

• Replace the implicit step with an explicit method, which does what you
  need:

lemma te_zero: "EX func t. func t = 0"
proof (intro exI)
show "F s = 0"

• Explicitly decompose the goal step by step (tedious):

lemma te_zero: "EX func t. func t = 0"
proof
show "EX t. F t = 0"
proof
show "F s = 0"
...

qed
qed

• Use an intermediate statement and let automation deal with quantifiers:

lemma te_zero: "EX func t. func t = 0"
proof -
have "F s = 0"
...

then show ?thesis by blast
qed

What you use depends on taste and the concrete problem.

See also the Isar tutorial for Isar basics:
http://isabelle.in.tum.de/dist/Isabelle/doc/isar-overview.pdf

Alex

Email Gateway (Aug 18 2022 at 15:02):

From: Alexander Krauss <krauss@in.tum.de>
You may need to add type annotations to make sure that the types in your
lemma statement are not more general than you want. Switch on "Isabelle
-> Settings -> Show Types".

Alex

Email Gateway (Aug 18 2022 at 15:02):

From: Alexander Krauss <krauss@in.tum.de>
The variable func is existentially quantified, but the type variables 'a
and 'b are (implicitly) universally quantified. So you cannot
instantiate them.

In HOL it is not possible to express existential quantification over types.

Alex

Email Gateway (Aug 18 2022 at 15:02):

From: Steve W <s.wong.731@googlemail.com>
On Thu, Apr 8, 2010 at 12:34 PM, Alexander Krauss <krauss@in.tum.de> wrote:

lemma te_zero: "EX func t. func t = 0"

proof (intro exI)

show "F s = 0"

Thanks for the help. Unfortunately, I get an error from this, saying that
it can't solve goal by exported rule: F s = 0. Any hint on this will be
appreciated.

You may need to add type annotations to make sure that the types in your
lemma statement are not more general than you want. Switch on "Isabelle ->
Settings -> Show Types".

I see. However, why can't the types in the lemma be more general even the
function is existentially quantified? Can't a' and b' be instantiated to
real for F s = 0 in the proof?

Thanks
Steve

Alex

Last updated: Nov 21 2024 at 12:39 UTC