<div dir="ltr"><div>Hi all,<br><br>I would like to add my voice to this issue, noting that I am a big fan of local definitions (both macro- and micro-scopes, though the former are more important), and I don't think there should be any pressure to remove them from articles. In fact, I see the hiding of local scopes as a great advantage of the semantics of OpenTheory packages. It allows us to implement Bill Farmer's "Little Theories" idea naturally in HOL. I don't think reducing the number of local names should be a weighty factor in deciding how to formalise the reals. Rather, I think article readers and writers should just implement the OpenTheory semantics correctly.<br><br></div>Cheers,<br>Ramana<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Nov 24, 2014 at 10:42 PM, Mario Carneiro <span dir="ltr"><<a href="mailto:di.gama@gmail.com" target="_blank">di.gama@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">Hi Joe,<br><div><div class="gmail_extra"><br><div class="gmail_quote"><span class="">On Mon, Nov 24, 2014 at 5:19 PM, 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:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">An example of macro-scopes is the construction of the real numbers,<br>
where you have to develop a big formalization (including definitions)<br>
to construct some mathematical object, and then you throw away that<br>
construction and export a few characteristic properties ("axioms").<br>
This leaves a bunch of locally defined symbols in the theory (an<br>
example in the standard theory library is the HOLLight.hreal type).<br>
<br>
Cleaning up the micro-scopes is certainly desirable for a theory<br>
package designed to be shared between theorem provers, but I wonder<br>
how much it is possible to clean up the macro-scopes too? It would<br>
involve factoring the construction formalization into theories useful<br>
in their own right, rather than making definitions that are tailored<br>
to the construction of one particular mathematical object.<br></blockquote><div><br></div></span><div>It may be instructive to see how Metamath does this, since there are no macro-scopes for definitions: all definitions are global. Instead, we use hypotheses that set a variable equal to the object being temporarily defined, then discharge the assumption when we are done with an equality theorem. See <a href="http://us2.metamath.org:88/mpegif/omxpen.html" target="_blank">http://us2.metamath.org:88/mpegif/omxpen.html</a> for an example of this in action. For an OT example, consider the following sketch of a proof that there is a number greater than 1:<br><br></div><div>The definition way:<br></div><div><br></div><div>  |- c1 = (1+1)<br></div><div><div><div>  |- 1 < (1+1)<br></div><div><div><div><div><div> |- 1 < c1<br></div><div><div><div><div>|- ?x. 1 < x<br></div><div><br></div><div>The temporary definition way:<br><br><div>    c = (1+1) |- 1 < c <=> 1 < (1+1)</div><div>    |- 1 < (1+1)<br></div><div>   c = (1+1) |- 1 < c<br></div>  c = (1+1) |- ?x. 1 < x<br> (1+1) = (1+1) |- ?x. 1 < x<br> |- (1+1) = (1+1)<br>|- ?x. 1 < x<br><br></div><div>Basically you carry the term "c = definition" as an antecedent through the proof, where "c" is a free variable, then discharge it when you have derived your goal statement that is independent of the definition.<span class="HOEnZb"><font color="#888888"><br></font></span></div><span class="HOEnZb"><font color="#888888"><div><div><br></div><div>Mario<br></div><br></div></font></span></div></div></div></div></div></div></div></div></div><div><div class="h5"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<br>
In the case of the real numbers in HOL Light, one stepping stone is<br>
the construction of the positive real numbers (the "half-real" numbers<br>
represented by the HOLLight.hreal type above), which doesn't sound<br>
particularly useful in its own right, so would fail that test. I<br>
wonder if there is another construction of the real numbers that is<br>
based solely on generally useful mathematical objects? The one I<br>
remember from my undergraduate days makes the type definition<br>
<br>
real = rational set<br>
<br>
where each rational set must be downward-closed (i.e., if a rational<br>
set S contains x then S also contains every rational less than x).<br>
This construction might be more involved than the one in HOL Light,<br>
but has the advantage of being based only on generally useful objects<br>
(sets and rational numbers).<br>
<br>
Cheers,<br>
<br>
Joe<br>
<div><div><br>
<br>
On Mon, Nov 24, 2014 at 11:49 AM, Konrad Slind <<a href="mailto:konrad.slind@gmail.com" target="_blank">konrad.slind@gmail.com</a>> wrote:<br>
> It's a scoping issue. I think that Peter Homeier's HOL-Omega<br>
> can quantify/bind the local constants used to construct datatypes,<br>
> for example. So its rules may provide guidance on what OpenTheory<br>
> should do.<br>
><br>
> Sorry, I know I am not answering the original question.<br>
><br>
> Konrad.<br>
><br>
><br>
> On Mon, Nov 24, 2014 at 1:32 PM, Mario Carneiro <<a href="mailto:di.gama@gmail.com" target="_blank">di.gama@gmail.com</a>> wrote:<br>
>><br>
>> I expect that it will be impossible to remove most of the local<br>
>> definitions that you are talking about, because they serve an important<br>
>> purpose: they are useful for "forgetting" about constructions. Once you've<br>
>> proven that the reals have the desired properties, it no longer becomes<br>
>> important what sequence of embeddings was used to build the Real type in the<br>
>> first place, and indeed there is an aesthetic in proofs which avoid any<br>
>> reference to such "construction-dependent" properties. (This process is made<br>
>> explicit in Metamath, where we derive the basic properties of the reals,<br>
>> then ignore these proofs and replace them with axioms so that you can't use<br>
>> the construction any more but are forced to use only the properties.) A<br>
>> similar argument applies to the abstraction and representation functions -<br>
>> unless you are going to be moving between the types often, you may as well<br>
>> forget about these functions once the basic properties of the new type are<br>
>> established.<br>
>><br>
>> These are new constants whose construction is mandated by the language.<br>
>> You can't make a new type without getting abs,rep functions out. You can't<br>
>> construct a derived type without constructing the base type first. Once you<br>
>> have the constants, but you no longer need them, what are you supposed to do<br>
>> with them?<br>
>><br>
>> Mario<br>
>><br>
>> On Mon, Nov 24, 2014 at 2:13 PM, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>> wrote:<br>
>>><br>
>>> There have been several discussions on this list about symbols (i.e.,<br>
>>> type operators and constants) that are defined in a theory but are not<br>
>>> mentioned in any exported theorem, which Rob named local definitions.<br>
>>> Since most of the HOL family of theorem provers maintain a global<br>
>>> symbol table, these local definitions can cause problems if they have<br>
>>> clashing names.<br>
>>><br>
>>> Up until now it's been difficult to see the complete set of symbols<br>
>>> referred to inside a theory, but this can now be displayed with the<br>
>>> opentheory info --symbols command (I append the output for the most<br>
>>> recent version of the standard theory library: base-1.169). As can be<br>
>>> seen, most of the local definitions (which are the symbols in the<br>
>>> HOLLight namespace) are abstraction and representation functions for<br>
>>> type definitions, but there are also others such as those that are<br>
>>> used to construct the real numbers.<br>
>>><br>
>>> In my opinion it would make theories more elegant if (some of) these<br>
>>> local definitions could be removed, but in the meantime I'd like to<br>
>>> know of any instances with clashing local definitions (these could<br>
>>> occur either in the same theory or across different theories). My<br>
>>> current belief is that these should be easy to fix in a natural way,<br>
>>> but I need to see some concrete examples.<br>
>>><br>
>>> Cheers,<br>
>>><br>
>>> Joe<br>
>>><br>
>>> ______________________________________________________<br>
>>><br>
>>> $ opentheory info --symbols base<br>
>>> 3 external type operators: -> bool ind<br>
>>> 2 external constants: = select<br>
>>> 11 defined type operators: Data.List.list Data.Option.option Data.Pair.*<br>
>>>   Data.Sum.+ Data.Unit.unit HOLLight.hreal HOLLight.nadd<br>
>>> HOLLight.recspace<br>
>>>   Number.Natural.natural Number.Real.real Set.set<br>
>>> 210 defined constants: ! /\ ==> ? ?! \/ ~ cond F T Data.List.::<br>
>>> Data.List.@<br>
>>>   Data.List.[] Data.List.all Data.List.any Data.List.case.[].::<br>
>>>   Data.List.concat Data.List.drop Data.List.filter Data.List.foldl<br>
>>>   Data.List.foldr Data.List.fromSet Data.List.head Data.List.interval<br>
>>>   Data.List.last Data.List.length Data.List.map Data.List.member<br>
>>>   Data.List.nth Data.List.nub Data.List.nubReverse Data.List.null<br>
>>>   Data.List.replicate Data.List.reverse Data.List.tail Data.List.take<br>
>>>   Data.List.toSet Data.List.zip Data.List.zipWith<br>
>>>   Data.Option.case.none.some Data.Option.isNone Data.Option.isSome<br>
>>>   Data.Option.map Data.Option.none Data.Option.some Data.Pair.,<br>
>>>   Data.Pair.fst Data.Pair.snd Data.Sum.case.left.right Data.Sum.destLeft<br>
>>>   Data.Sum.destRight Data.Sum.isLeft Data.Sum.isRight Data.Sum.left<br>
>>>   Data.Sum.right Data.Unit.() Function.^ Function.const Function.flip<br>
>>>   Function.id Function.injective Function.o Function.surjective<br>
>>>   Function.Combinator.s Function.Combinator.w HOLLight._dest_list<br>
>>>   HOLLight._dest_option HOLLight._dest_rec HOLLight._dest_sum<br>
>>>   HOLLight._mk_list HOLLight._mk_option HOLLight._mk_rec HOLLight._mk_sum<br>
>>>   HOLLight.dest_hreal HOLLight.dest_nadd HOLLight.dest_num<br>
>>>   HOLLight.dest_real HOLLight.dest_set HOLLight.hreal_add<br>
>>>   HOLLight.hreal_inv HOLLight.hreal_le HOLLight.hreal_mul<br>
>>>   HOLLight.hreal_of_num HOLLight.is_nadd HOLLight.mk_hreal<br>
>>> HOLLight.mk_nadd<br>
>>>   HOLLight.mk_num HOLLight.mk_pair HOLLight.mk_real HOLLight.nadd_add<br>
>>>   HOLLight.nadd_eq HOLLight.nadd_inv HOLLight.nadd_le HOLLight.nadd_mul<br>
>>>   HOLLight.nadd_of_num HOLLight.nadd_rinv HOLLight.one_ABS<br>
>>> HOLLight.one_REP<br>
>>>   HOLLight.treal_add HOLLight.treal_eq HOLLight.treal_inv<br>
>>> HOLLight.treal_le<br>
>>>   HOLLight.treal_mul HOLLight.treal_neg HOLLight.treal_of_num<br>
>>>   HOLLight.ABS_prod HOLLight.BOTTOM HOLLight.CONSTR HOLLight.FCONS<br>
>>>   HOLLight.FINREC HOLLight.FNIL HOLLight.IND_0 HOLLight.IND_SUC<br>
>>>   HOLLight.INJA HOLLight.INJF HOLLight.INJN HOLLight.INJP HOLLight.NUMFST<br>
>>>   HOLLight.NUMLEFT HOLLight.NUMPAIR HOLLight.NUMRIGHT HOLLight.NUMSND<br>
>>>   HOLLight.NUMSUM HOLLight.NUM_REP HOLLight.REP_prod HOLLight.ZBOT<br>
>>>   HOLLight.ZCONSTR HOLLight.ZRECSPACE Number.Natural.* Number.Natural.+<br>
>>>   Number.Natural.- Number.Natural.< Number.Natural.<= Number.Natural.><br>
>>>   Number.Natural.>= Number.Natural.^ Number.Natural.bit0<br>
>>>   Number.Natural.bit1 Number.Natural.distance Number.Natural.div<br>
>>>   Number.Natural.even Number.Natural.factorial Number.Natural.isSuc<br>
>>>   Number.Natural.log Number.Natural.max Number.Natural.min<br>
>>>   Number.Natural.minimal Number.Natural.mod Number.Natural.odd<br>
>>>   Number.Natural.pre Number.Natural.suc Number.Natural.zero Number.Real.*<br>
>>>   Number.Real.+ Number.Real.- Number.Real./ Number.Real.< Number.Real.<=<br>
>>>   Number.Real.> Number.Real.>= Number.Real.^ Number.Real.~<br>
>>> Number.Real.abs<br>
>>>   Number.Real.fromNatural Number.Real.inv Number.Real.max Number.Real.min<br>
>>>   Number.Real.sup Relation.bigIntersect Relation.bigUnion Relation.empty<br>
>>>   Relation.fromSet Relation.intersect Relation.irreflexive<br>
>>> Relation.measure<br>
>>>   Relation.reflexive Relation.subrelation Relation.toSet<br>
>>>   Relation.transitive Relation.transitiveClosure Relation.union<br>
>>>   Relation.universe Relation.wellFounded Set.{} Set.bigIntersect<br>
>>>   Set.bigUnion Set.bijections Set.choice Set.cross Set.delete<br>
>>>   Set.difference Set.disjoint Set.finite Set.fold Set.fromPredicate<br>
>>>   Set.hasSize Set.image Set.infinite Set.injections Set.insert<br>
>>>   Set.intersect Set.member Set.properSubset Set.rest Set.singleton<br>
>>> Set.size<br>
>>>   Set.subset Set.surjections Set.union Set.universe<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" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
>><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" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
>><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" 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" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
</div></div></blockquote></div></div></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" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
<br></blockquote></div><br></div>