Re: [isabelle] universal quantifiers vs. schematic variables



Dear Users,

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

This for me is a very good explanation for something that has always
puzzled me, i.e., the way induction rules are formalized
in Isabelle. For instance, the rule nat_induct0 is formalized as follows:

lemma nat_induct0:
  fixes n
  assumes "P 0" and "ân. P n â P (Suc n)"
  shows "P n"

If I would formulate this rule, I would (unnecessarily I see), write the
conclusion as "!n. P n", since this is what the rule allows me
to infer if the premises are satisfied. From the logical point of view, it
would have a clearer and more natural reading.

Indeed, once the theorem is proved,  the object logic variable 'n' is
lifted into a schematic variable by Isabelle.

Best!

On Sun, Oct 4, 2015 at 3:44 PM, David Cock <david.cock at inf.ethz.ch> wrote:

> 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
>>>
>>>
>>
>>
>
>


-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
www.inf.pucrs.br/alfio
Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica
90619-900 -Porto Alegre - RS - Brasil



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