Re: [isabelle] proving existentially quantified statements using 'obtain'ed witness fails

The reason for this failure is consistency: when proving P(?x), you delay the
point at which you give the actual witness t for ?x. But that is just an
operational rearrangement of the proof. Logically it must be possible to
construct that t right away. Hence t must not depend on anything that only came
into existence while proving P(?x). Otherwise you could prove EX x. ALL y. x=y:

apply(rule exI)

1. ALL y. ?x = y

apply(rule allI)

1. !!y. ?x = y

apply(rule refl)

fails because you would need to instantiate ?x with the local y, which Isabelle
prevents. (Contrast this with a proof of ALL x. EX y. x=y)

Your failed proof attempt was morally correct, but you need to convince the
system that the witness could have been constructed up front, usually by
rearranging your proof text, eg as Lars suggested.


Am 12/11/2012 20:21, schrieb Julian Brunner:
> Hello,
> While using Isabelle, I keep running into the problem of not being able to
> prove existentially quantified statements using a witness with the show
> statement telling me that the "Local statement will fail to refine any
> pending goal".
> For instance:
> theorem "EX x. x = (0 :: nat)"
> proof
>   obtain x where x_def: "x = (0 :: nat)" by simp
>   show "x = 0" using x_def by simp
> qed
> This example results in "Local statement will fail to refine any pending
> goal" in line 4 of the proof. Furthermore, replacing line 3 with
> def x == "0 :: nat"
> makes everything work just fine. This is a minimal example built from a
> bigger proof where the witness used for proving the existential statement
> was an expression containing variables that originated in an obtain
> statement. From what I've observed so far, it appears that whenever
> variables from an obtain statement are part of the witness, the show
> statement fails. I've used [[show_types]] to confirm that the types aren't
> part of the issue, both x and 0 are of type nat. Also, the output doesn't
> give me the usual "Failed attempt to solve goal by exported rule" line
> stating why the show statement failed, as is the case with assume
> statements that don't match any assumption in the goal.
> Of course I can work around this by invoking proof with the '-' method and
> using automation to prove the existentially quantified statement using the
> witness, but it'd be nicer if it'd work like this, I feel like this is just
> a minor technical issue, but I couldn't figure out what's going on.
> I think I've also run into a similar problem that didn't involve obtain
> statements but I can't find the theory where that happened right now, maybe
> I'll post again if I run into that issue once more. For now, I'd be happy
> with figuring this one out.
> Cheers,
>  Julian

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.