[opentheory-users] New principle of constant definition

[Joe Leslie-Hurd]

Hi Mario,

Quoting from Rob Arthan when I asked the same question some months ago:

"It doesn't claim to be more expressive. What it is designed to offer
is abstraction. The OpenTheory kernel has a different way of hiding
representation details, but HOL4, HOL Light, ProofPower and the
OpenTheory article format don't have that option."

The latest release of the opentheory tool does indeed compile
instances of defineConstList to defineConst exactly as you describe,
if you feed it a version 6 article and ask for a version 5 article as
output:

opentheory info --article -o foo5.art --output-version 5 foo6.art

Cheers,

Joe

On Wed, Nov 5, 2014 at 10:50 PM, Mario Carneiro <di.gama at gmail.com> wrote:
> 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
>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>