Email Gateway (Aug 18 2022 at 15:37): Email Gateway (Aug 18 2022 at 15:37):From: Steve W <s.wong.731@gmail.com>
Hi,
Does anyone know how one would go about finding the instantiation of a
variable in ML? Say, if I can obtain the proof term for the theorem 'EX f x.
f x > 0', how do I work with the proof term in order to find the
instantiations of 'f' and 'x'?
Thanks
Steve
Email Gateway (Aug 18 2022 at 15:38):From: Steve W <s.wong.731@gmail.com>
On Thu, Jul 8, 2010 at 3:38 PM, Steve W <s.wong.731@gmail.com> wrote:
Hi,
Does anyone know how one would go about finding the instantiation of a
variable in ML? Say, if I can obtain the proof term for the theorem 'EX f x.
f x > 0', how do I work with the proof term in order to find the
instantiations of 'f' and 'x'?Would the first step be to reconstruct the proof using
Reconstruct.reconstruct_proof? If so, what would subsequent steps involve?
Any help will be appreciated.
Thanks
Steve
Thanks
Steve
Email Gateway (Aug 18 2022 at 15:38):From: Alexander Krauss <krauss@in.tum.de>
Hi Steve,
Does anyone know how one would go about finding the instantiation of a
variable in ML? Say, if I can obtain the proof term for the theorem 'EX f x.
f x > 0', how do I work with the proof term in order to find the
instantiations of 'f' and 'x'?
There are at least two ways in which your question can be understood:
a) Given a proof of "EX x. P x", you want to extract the term "t" that
was used to prove the existential statement
b) Given a proof of "EX x. P x", you want to find any term t such that
"P t" holds.
to a) This is not possible in general. Note that Isabelle/HOL implements
classical logic, which allows existential statements without providing
the values that are proved to exists. So there is no "instantiation"
that can be extracted, at least in general. You can find a simple
example of such a proof (of the well-known Drinker's Principle) in the
file "HOL/Isar_Examples/Drinker.thy".
If the proof you have does not involve classical reasoning, then your
problem can be solved in principle. But even then, the proof may be more
than just an application of the rule "exI". Then the following paper is
probably relevant:
Stefan Berghofer. Program Extraction in simply-typed Higher Order Logic.
TYPES 2002
http://www4.informatik.tu-muenchen.de/~berghofe/papers/TYPES2002.pdf
to b) If you just need some value that satisfies the property, then you
can of course always use the choice operator and write "SOME x. P x". Of
course this does not contain any information, but sometimes it is
sufficient.
Would the first step be to reconstruct the proof using
Reconstruct.reconstruct_proof? If so, what would subsequent steps involve?
Reconstructing is usually the first thing to do if you want to do
anything useful with a proof term. Further, I don't know. Maybe the
extraction described in the paper above does what you want (but I am not
sure what exactly you want).
Any help will be appreciated.
Actually, what is your application for this? It seems to be a rather
unusual way of using Isabelle. If you give us some more concrete
information about the big picture, i.e., what functionality do you want
to realise in the end, then you might get more helpful answers.
Alex
Email Gateway (Aug 18 2022 at 15:39):From: Steve W <s.wong.731@gmail.com>
Hi Alexander,
I think my situation is similar to a). How about in the following:
axiomatization
f :: "real => real" and
c :: real where
ax1: "f c = 0"
lemma lem1: "EX x. f x = 0"
using ax1
apply auto
done
Can one extract the term that was used to prove the existential statement by
auto? I.e., that term should be 'c' due to ax1. I've tried running
'full_prf' after 'apply auto', but I get an error about 'minimal proof
object' even I have Full Proof switched on in PG. Does auto instantiate the
existential variable to 'c'?
Now, if I have the following instead:
lemma lem1: "EX x. f x = 0"
using ax1
apply (rule exI [where x = c])
done
full_prf gives:
protectI % EX x::real. f x = (0::real) %%
(exI % TYPE(real) % (%a::real. f a = (0::real)) % c %% (OfClass type_class
% TYPE(real)) %% thm.Test.ax1)
It's clearer now that 'x' is instantiated to 'c' (because the instantiation
is explicit in the proof), which is a lambda term. However, how should 'c'
be extracted from the proof?
Thanks again.
Steve
Email Gateway (Aug 18 2022 at 15:40):From: Alexander Krauss <krauss@in.tum.de>
Steve W wrote:
Can one extract the term that was used to prove the existential statement by
auto? I.e., that term should be 'c' due to ax1.
I think in general the answer is no, since auto may perform classical
reasoning. In special cases, this may be possible but is certainly not
trivial. You would probably have to study some decent proof theory...
I've tried running
'full_prf' after 'apply auto', but I get an error about 'minimal proof
object' even I have Full Proof switched on in PG.
I am surprised by this myself. I would also have expected a full proof
here. Maybe someone else has an idea?
Does auto instantiate the
existential variable to 'c'?Now, if I have the following instead:
lemma lem1: "EX x. f x = 0"
using ax1
apply (rule exI [where x = c])
donefull_prf gives:
protectI % EX x::real. f x = (0::real) %%
(exI % TYPE(real) % (%a::real. f a = (0::real)) % c %% (OfClass type_class
% TYPE(real)) %% thm.Test.ax1)It's clearer now that 'x' is instantiated to 'c' (because the instantiation
is explicit in the proof), which is a lambda term. However, how should 'c'
be extracted from the proof?
You can read about the format of proof terms in the paper that I
mentioned. From this, I guess, you will have to work out the details
yourself (starting from a precise problem definition), since it hasn't
been done yet AFAIK.
Alex
Email Gateway (Aug 18 2022 at 15:45):From: Makarius <makarius@sketis.net>
If this is Isabelle2009-2, then you need to build HOL-Proofs explicitly,
via "Isabelle2009-2/build -m HOL-Proofs" on the command lines.
In the past proof terms used to be part of the default HOL image, but we
had to discontinue that due to resource limitations.
Makarius
Last updated: May 01 2024 at 20:18 UTC