Re: [isabelle] universal quantifiers vs. schematic variables



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

On 04/10/15 11:22, David Cock wrote:
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

On 04/10/15 11:19, Jasmin Blanchette wrote:
David,

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.
Huh?

schematic_lemma "P ?x ==> P y"
   by assumption

Cheers,

Jasmin








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