Email Gateway (Aug 22 2022 at 11:37): Email Gateway (Aug 22 2022 at 11:37):From: noam neer <noamneer@gmail.com>
if "P" is a previously defined predicate and I want to prove it always
holds, it seems I can do it in two ways. the first uses the universal
quantifier as in
lemma "!x. P(x)"
....
and the second uses schematic variables, as in
lemma "P(x)"
...
if I'm not mistaken each of these can be used to prove the other, so they
are logically equivalent. the only differences I could find were in the way
the proved lemmas can be used in proofs, where usually the second
formulation is easier to use. my question is if this is indeed the case,
and if so why does Isabelle offer two different ways to say the same thing.
comparing to the case of --> and ==>, the different arrows are also
logically equivalent but they are intended for different situations, but I
couldn't find such distinction in the universal case.
thanx.
Email Gateway (Aug 22 2022 at 11:38):From: David Cock <david.cock@inf.ethz.ch>
Noam,
You'll probably get answers from more knowledgable persons than I,
but you've just discovered one of Isabelle's most fundamental quirks.
As theorems, you're right that they're (logically) equivalent, but they
differ if they appear as assumptions i.e.
(!x. P x) => P y
holds, but
P ?x => P y
does not (necessarily) hold. In the second case, you know that P holds
for some (particular, unspecified) x, but you don't know whether that is
equal to y.
David
Email Gateway (Aug 22 2022 at 11:39):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
David,
Huh?
schematic_lemma "P ?x ==> P y"
by assumption
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 11:39):From: David Cock <david.cock@inf.ethz.ch>
Grr, sorry, hit send without proofreading. That second one should have
been
P x => P y
i.e. an unbound, not a schematic name.
Noam: in your example, it's not clear whether you have an actual
schematic, or just an unbound (blue) variable.
David
Email Gateway (Aug 22 2022 at 11:39):From: Lars Hupel <hupel@in.tum.de>
Hi,
if "P" is a previously defined predicate and I want to prove it always
holds, it seems I can do it in two ways. the first uses the universal
quantifier as in
lemma "!x. P(x)"
....
and the second uses schematic variables, as in
lemma "P(x)"
...
if I'm not mistaken each of these can be used to prove the other, so they
are logically equivalent. the only differences I could find were in the way
the proved lemmas can be used in proofs, where usually the second
formulation is easier to use.
first of all, your assessment is correct. Nitpicking: In the second
formulation, you use the free variable 'x', which – after proving the
lemma – gets generalized to a schematic variable. You can recognize
schematic variables by the prefixed question mark (e.g. '?x').
and if so why does Isabelle offer two different ways to say the same thing.
comparing to the case of --> and ==>, the different arrows are also
logically equivalent but they are intended for different situations, but I
couldn't find such distinction in the universal case.
I don't have an insight into the early history of Isabelle. I have the
understanding that the notion of schematic has been there for a long
time. The only explanation I can offer is that schematic variables can
be easily instantiated. For example, if you have the theorem 'P ?x', you
can substitute '?x' by something arbitrary, without having to know about
the universal quantifier. In the explicitly-quantified case (be it HOL
quantification or Pure quantification), the 'x' would be a bound
variable and you would need to know more. Essentially, schematic
variables allow for easy outermost quantification.
Cheers
Lars
Email Gateway (Aug 22 2022 at 11:39):From: David Cock <david.cock@inf.ethz.ch>
Let's try that again.
If you prove:
lemma "P x"
by(whatever)
then (assuming x was completely unbound at that point), you've obviously
done something at least as hard as proving
lemma "!x. P x"
i.e. proving something about a concrete x, without assuming anything in
particular about it, and thus your proof could in principle be reapplied
to any other concrete value. Isabelle "knows" this, and thus
transparently lifts your result to the schematic lemma "P ?x", ie. a
lemma with a named hole where x should be. That hole can be filled with
whatever you like, and so, as Jasmin pointed out, you've effectively got
a universally quantified result.
Schematics in the conclusion (e.g. in a subgoal) can work differently.
If at some point you end up with a subgoal of the form "P ?x", you can
prove it by substituting a particular x that satisfies (P x). For
example, you can prove "?x = (0::nat)" with "by(refl)" (i.e.
substituting 0), but that proof obviously doesn't generalise to all
possible substitutions.
In summary, propositions with schematics are a bit like universally
quantified formulae, but not quite. The semantics get more complicated
when a given schematic appears multiple times e.g. in assumption and
conclusions. In that case, by instantiating a schematic, you're making
a (potentially unsafe) choice in your proof - you may end up in an
unprovable state, even for a true theorem.
Larry could presumably shine more light on the design decisions here,
but schematics are (as far as I understand) a more fundamental part of
the term rewriting system, with something more of an "operational"
semantics i.e. it does what it does, while "!" is the quantifier of
Pure, with a specific logical interpretation.
Dave
Email Gateway (Aug 22 2022 at 11:39):From: Alfio Martini <alfio.martini@acm.org>
Dear Users,
Let's try that again.
Email Gateway (Aug 22 2022 at 11:39):From: Lars Noschinski <noschinl@in.tum.de>
On 04.10.2015 20:02, David Cock wrote:
Noam,
You'll probably get answers from more knowledgable persons than I, but
you've just discovered one of Isabelle's most fundamental quirks. As
theorems, you're right that they're (logically) equivalent, but they
differ if they appear as assumptions i.e.
Schematic variables are equivalent to outermost universal quantifiers.
(!x. P x) => P y
holds, but
P ?x => P y
That is, the theorem "P ?x ==> P y" is equivalent to the theorem "!!x. P
x ==> P y" which is equivalent (in HOL) to "(?x. P x) ==> P y".
-- Lars
Email Gateway (Aug 22 2022 at 11:40):From: Lars Noschinski <noschinl@in.tum.de>
Indeed, Isabelle normalizes all rules by (a) moving universal
quantifiers as far outside as possible and (b) replacing outermost
universal quantifiers by schematic variables. This canonical format (I
believe it is called Hereditarily Harrop Formula in the sources) allows
a consistent handling of such formulas in the implementation.
Email Gateway (Aug 22 2022 at 11:40):From: Lars Noschinski <noschinl@in.tum.de>
Schematic variables allow you to delay your choice of instantiation.
Moreover, they can be used to synthesize terms, which is regularly used
in program verification, e.g. to compute the weakest precondition of a
Hoare triple.
Email Gateway (Aug 22 2022 at 11:40):From: Larry Paulson <lp15@cam.ac.uk>
Schematic variables have been part of Isabelle from the very beginning. The idea has always been that it should be possible to prove something by transitivity, without first knowing what the intermediate term would be. From a strictly logical point of view, schematic variables are simply variables (necessarily free variables, as there is no way of binding them).
Larry Paulson
Email Gateway (Aug 22 2022 at 11:40):From: Larry Paulson <lp15@cam.ac.uk>
The nice thing is that what appears to be different behaviours is different aspects of one single operation, namely higher-order Horn clause resolution. Some historical details are available in my 1989 paper The Foundation of a Generic Theorem Prover
http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf
See section 4.
Larry Paulson
Email Gateway (Aug 22 2022 at 11:40):From: Larry Paulson <lp15@cam.ac.uk>
The answer to this question is simple: induction rules are formulated in this way in Isabelle because Martin-Löf used the same approach in his constructive type theory. He arrived at this formulation by following the idea of natural deduction consistently. In natural deduction, every inference rule introduces or eliminates a distinguished symbol, and Martin-Löf recognised that in the case of induction rules, the symbol being eliminated was the premise “n is a natural number”. He used a similar approach with the elimination rules for finite sums and products, generalised sums, etc.
One does not have to be a constructivist to to recognise that his was the right approach, and that attaching a universal quantifier to the conclusion is superfluous.
Larry Paulson
Email Gateway (Aug 22 2022 at 11:41):From: David Cock <david.cock@inf.ethz.ch>
Thanks for that, interesting.
David
Last updated: Nov 21 2024 at 12:39 UTC