[opentheory-users] extending the standard library

[Ramana Kumar]

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
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20160413/f24d4fe5/attachment-0001.html>