[opentheory-users] extending the standard library

[Ramana Kumar]

It looks like Number.Real.inv and realax$inv will suffer from the same
problem, since in HOL4 we can prove inv 0 = 0.

On 13 April 2016 at 15:38, Konrad Slind <konrad.slind at gmail.com> wrote:

> Re: MAP2 in HOL4. This is an example of an underspecified function. I
> recall having
> to redefine map2 to completely specify it in order to get it through the
> HOL-->CakeML translator.
>
> So, presumably, different systems can and will define common partial
> functions differently, as
> either underspecified or completely specified. Is there an OpenTheory
> policy on this, for
> its standard library?
>
> Konrad.
>
>
> On Tue, Apr 12, 2016 at 11:56 PM, Ramana Kumar <ramana at member.fsf.org>
> wrote:
>
>> It looks like list.ZIP can't be mapped to Data.List.zip because the
>> latter is curried. But I'm still looking into unzip.
>>
>> On 13 April 2016 at 13:56, Ramana Kumar <ramana at member.fsf.org> wrote:
>>
>>> The HOL4 base library has its own version of constants like
>>> Data.List.take and Number.Natural.- because it needs to prove theorems like:
>>>
>>> ⊦ length (list.TAKE n xs) = if n ≤ length xs then n else length xs
>>>
>>> ⊦ (∀m. arithmetic.- 0 m = 0) ∧
>>>   ∀m n.
>>>     arithmetic.- (suc m) n = if m < n then 0 else suc (arithmetic.- m n)
>>> I don't think these theorems are provable using the OpenTheory standard
>>> library versions of those constants.
>>>
>>> However, I don't know whether Data.List.unzip suffers from this problem.
>>> If not, then the HOL4 base package should be updated to use the standard
>>> library constant. It would be helpful if you could make a list of any other
>>> similar updates that should be made.
>>>
>>> I don't think the current OpenTheory standard library base contains
>>> theories that every HOL theorem prover supports. There are constants like
>>> Data.List.nub, for example, which are not supported by HOL4. I'm not
>>> entirely sure whether being the intersection of what every HOL theorem
>>> prover supports is a good goal, but if that is the rule it should at least
>>> be followed :)
>>>
>>> However, my question was not solely about the base package, but about
>>> the naming scheme for the standard library. If there are useful constants
>>> from other theorem provers (like, say, HOL4's list.GENLIST or list.MAP2), I
>>> think their name and characterising theorems should be fit into the
>>> OpenTheory namespace (Data.List, for example) in a standardised way, even
>>> if they don't make it into the base package itself. What do you think of
>>> that?
>>>
>>> I envision OpenTheory being used for the twin goals of portability
>>> (where being an intersection is good) and designing a rich, cleanly
>>> organised, useful standard library of HOL theorems (where being a union is
>>> good). These activities can happen simultaneously in different OpenTheory
>>> standard packages.
>>>
>>> On 13 April 2016 at 04:11, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>>
>>>> Hi Ramana,
>>>>
>>>> The intent is for the standard theory library to always be evolving,
>>>> but slowly, because it's supposed to contain the base theories that
>>>> *every* HOL theorem prover supports.
>>>>
>>>> Looking through the theory I see a lot of defined constants that also
>>>> occur in the OpenTheory standard library (e.g., list.UNZIP), and I was
>>>> wondering why the HOL4 base theory has its own version?
>>>>
>>>> Cheers,
>>>>
>>>> Joe
>>>>
>>>> On Sun, Apr 10, 2016 at 1:54 PM, Ramana Kumar <ramana at member.fsf.org>
>>>> wrote:
>>>> > Hi Joe,
>>>> >
>>>> > You will have seen that the HOL developers have uploaded a package
>>>> called
>>>> > hol-base to the Gilith repo. The purpose of this package is twofold:
>>>> >
>>>> > It proves many useful theorems as found in the basic libraries of the
>>>> HOL
>>>> > theorem prover.
>>>> > It serves to satisfy the assumptions of further theories developed in
>>>> the
>>>> > HOL theorem prover, by proving those assumptions using only the
>>>> theorems of
>>>> > the OpenTheory standard library base package.
>>>> >
>>>> > For purpose 1 in particular, it seems to me that many of the constants
>>>> > defined by hol-base would benefit from residing in an appropriate
>>>> place in
>>>> > OpenTheory's namespace hierarchy, and indeed some of the proofs from
>>>> > hol-base might beneficially be moved into the base package itself.
>>>> > (Currently, all constants defined by hol-base are in their own
>>>> namespace.)
>>>> >
>>>> > Is the design of the standard library still evolving, and is it open
>>>> to
>>>> > extension? Would you be willing to copy over any useful-looking
>>>> constants?
>>>> > And/or settle on some namespace decisions?
>>>> >
>>>> > Cheers,
>>>> > Ramana
>>>> >
>>>> > _______________________________________________
>>>> > 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
>>>>
>>>
>>>
>>
>> _______________________________________________
>> 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20160510/22a08f3b/attachment.html>