<div dir="ltr">It looks like Number.Real.inv and realax$inv will suffer from the same problem, since in HOL4 we can prove inv 0 = 0.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 13 April 2016 at 15:38, Konrad Slind <span dir="ltr"><<a href="mailto:konrad.slind@gmail.com" target="_blank">konrad.slind@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Re: MAP2 in HOL4. This is an example of an underspecified function. I recall having<div>to redefine map2 to completely specify it in order to get it through the HOL-->CakeML translator.</div><div><br></div><div>So, presumably, different systems can and will define common partial functions differently, as</div><div>either underspecified or completely specified. Is there an OpenTheory policy on this, for</div><div>its standard library?</div><span class="HOEnZb"><font color="#888888"><div><br></div><div>Konrad.</div><div><br></div></font></span></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Apr 12, 2016 at 11:56 PM, Ramana Kumar <span dir="ltr"><<a href="mailto:ramana@member.fsf.org" target="_blank">ramana@member.fsf.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">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.<br></div><div><div><div class="gmail_extra"><br><div class="gmail_quote">On 13 April 2016 at 13:56, Ramana Kumar <span dir="ltr"><<a href="mailto:ramana@member.fsf.org" target="_blank">ramana@member.fsf.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div>The HOL4 base library has its own version of constants like Data.List.take and Number.Natural.- because it needs to prove theorems like:<br><p><span title="Theorem proved in hol-base-1.0">⊦</span> <span title="Data.List.length : A list → natural">length</span> <span>(</span><span title="HOL4.list.TAKE : natural → A list → A list">list.TAKE</span> <span title="n : natural">n</span> <span title="xs : A list">xs</span><span>)</span> <span><span title="= : natural → natural → bool">=</span></span> <span>if</span> <span title="n : natural">n</span> <span><span title="Number.Natural.<= : natural → natural → bool">≤</span></span> <span title="Data.List.length : A list → natural">length</span> <span title="xs : A list">xs</span> <span>then</span> <span title="n : natural">n</span> <span>else</span> <span title="Data.List.length : A list → natural">length</span> <span title="xs : A list">xs</span></p><p></p><p><span title="Theorem proved in hol-base-1.0">⊦</span> <span>(</span><span><span title="Data.Bool.! : (natural → bool) → bool">∀</span></span><span title="m : natural">m</span><span>.</span> <span title="HOL4.arithmetic.- : natural → natural → natural">arithmetic.-</span> <span title="0 : natural">0</span> <span title="m : natural">m</span> <span><span title="= : natural → natural → bool">=</span></span> <span title="0 : natural">0</span><span>)</span> <span><span title="Data.Bool./\ : bool → bool → bool">∧</span></span><br>  <span><span title="Data.Bool.! : (natural → bool) → bool">∀</span></span><span title="m : natural">m</span> <span title="n : natural">n</span><span>.</span><br>    <span title="HOL4.arithmetic.- : natural → natural → natural">arithmetic.-</span> <span>(</span><span title="Number.Natural.suc : natural → natural">suc</span> <span title="m : natural">m</span><span>)</span> <span title="n : natural">n</span> <span><span title="= : natural → natural → bool">=</span></span> <span>if</span> <span title="m : natural">m</span> <span><span title="Number.Natural.< : natural → natural → bool"><</span></span> <span title="n : natural">n</span> <span>then</span> <span title="0 : natural">0</span> <span>else</span> <span title="Number.Natural.suc : natural → natural">suc</span> <span>(</span><span title="HOL4.arithmetic.- : natural → natural → natural">arithmetic.-</span> <span title="m : natural">m</span> <span title="n : natural">n</span><span>)</span></p>I don't think these theorems are provable using the OpenTheory standard library versions of those constants.<br><br></div>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.<br><br></div><div>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 :)<br><br></div><div>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?<br><br></div><div>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.<br></div></div><div><div><div class="gmail_extra"><br><div class="gmail_quote">On 13 April 2016 at 04:11, Joe Leslie-Hurd <span dir="ltr"><<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Ramana,<br>
<br>
The intent is for the standard theory library to always be evolving,<br>
but slowly, because it's supposed to contain the base theories that<br>
*every* HOL theorem prover supports.<br>
<br>
Looking through the theory I see a lot of defined constants that also<br>
occur in the OpenTheory standard library (e.g., list.UNZIP), and I was<br>
wondering why the HOL4 base theory has its own version?<br>
<br>
Cheers,<br>
<br>
Joe<br>
<div><div><br>
On Sun, Apr 10, 2016 at 1:54 PM, Ramana Kumar <<a href="mailto:ramana@member.fsf.org" target="_blank">ramana@member.fsf.org</a>> wrote:<br>
> Hi Joe,<br>
><br>
> You will have seen that the HOL developers have uploaded a package called<br>
> hol-base to the Gilith repo. The purpose of this package is twofold:<br>
><br>
> It proves many useful theorems as found in the basic libraries of the HOL<br>
> theorem prover.<br>
> It serves to satisfy the assumptions of further theories developed in the<br>
> HOL theorem prover, by proving those assumptions using only the theorems of<br>
> the OpenTheory standard library base package.<br>
><br>
> For purpose 1 in particular, it seems to me that many of the constants<br>
> defined by hol-base would benefit from residing in an appropriate place in<br>
> OpenTheory's namespace hierarchy, and indeed some of the proofs from<br>
> hol-base might beneficially be moved into the base package itself.<br>
> (Currently, all constants defined by hol-base are in their own namespace.)<br>
><br>
> Is the design of the standard library still evolving, and is it open to<br>
> extension? Would you be willing to copy over any useful-looking constants?<br>
> And/or settle on some namespace decisions?<br>
><br>
> Cheers,<br>
> Ramana<br>
><br>
</div></div>> _______________________________________________<br>
> opentheory-users mailing list<br>
> <a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a><br>
> <a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
><br>
<br>
_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
</blockquote></div><br></div>
</div></div></blockquote></div><br></div>
</div></div><br>_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
<br></blockquote></div><br></div>
</div></div><br>_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
<br></blockquote></div><br></div>