[opentheory-users] New principle of constant definition

[Mario Carneiro]

Could someone clue me in on why defineConstList (a.k.a
gen_new_specification) is necessary? From the paper, I read that it takes
as input

v1 = t1, ..., vn = tn |- p

and produces

|- p[c1/v1, ..., cn/vn]

Doesn't this trivially follow from the separate definitions c1 = t1, ...,
cn = tn? What is the purpose of a separate redundant axiom for this?

Mario

On Wed, Nov 5, 2014 at 6:21 PM, Rob Arthan <rda at lemma-one.com> wrote:

> Joe,
>
> On 5 Nov 2014, at 22:49, Joe Leslie-Hurd <joe at gilith.com> wrote:
>
> > Hi Rob,
> >
> > [I'm cc'ing the OpenTheory list because the discussion may be of
> > general interest.]
> >
> > I just finished implementing the new principle of constant definition
> > described in your paper "HOL Constant Definition Done Right":
> >
> > http://www.lemma-one.com/papers/hcddr.pdf
>
> Excellent!
>
> >
> > It all makes perfect sense to me and the instructions were
> > straightforward to follow, but I was wondering if you could explain
> > the rationale behind this constraint:
> >
> > "the free variables of p must be contained in the v_i"
> >
> > It seems sound to permit extra free variables, for example in the
> > following definition
> >
> > v = 0 |- n + v = n
>
> It would be sound to permit that, but I have a prejudice against
> free variables in defining properties, so I was deliberately requiring
> the user to take the universal closure w.r.t. the variable n in an
> example like the above, so that the resulting defining property
> would be a closed formula.
>
> >
> > Also, why "contained in" and not "exactly"? If there are extra
> > variables v_i that are not free in p, then it is a simple matter to
> > remove them from the hypotheses before calling gen_new_specification.
>
> Yes, but then the rule won’t introduce the corresponding constants.
> I don’t think this is very important, but I didn’t want to require
> the user to impose a constraint on all the new constants.
>
> >
> > Finally, a practical point that I ran into during implementation: in
> > the case where the set v_i is empty (i.e., there is nothing to
> > define), should the input theorem simply be returned or do you
> > consider that an error condition?
>
> The current ProofPower implementation allows the set to be empty
> and just stores the input theorem as a definition (of nothing) in that
> case. I think that is it how it is specified in the CakeML work too.
> Maybe Ramana could confirm that.
>
> Regards,
>
> Rob.
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141106/d473a9be/attachment.html>