[opentheory-users] Local definitions in theory packages

[Joe Leslie-Hurd]

Hi Konrad,

I agree that this is a scoping issue, but it seems like there are two
kinds of scopes manifesting, which I shall call micro-scopes and
macro-scopes.

An example of micro-scopes are the abs/rep functions of HOL Light's
type operator definition principle, and can be dealt with using a new
inference rule that does not define extra constants (such as Rob's
proposed new type definition or following Peter's approach in
HOL-Omega).

An example of macro-scopes is the construction of the real numbers,
where you have to develop a big formalization (including definitions)
to construct some mathematical object, and then you throw away that
construction and export a few characteristic properties ("axioms").
This leaves a bunch of locally defined symbols in the theory (an
example in the standard theory library is the HOLLight.hreal type).

Cleaning up the micro-scopes is certainly desirable for a theory
package designed to be shared between theorem provers, but I wonder
how much it is possible to clean up the macro-scopes too? It would
involve factoring the construction formalization into theories useful
in their own right, rather than making definitions that are tailored
to the construction of one particular mathematical object.

In the case of the real numbers in HOL Light, one stepping stone is
the construction of the positive real numbers (the "half-real" numbers
represented by the HOLLight.hreal type above), which doesn't sound
particularly useful in its own right, so would fail that test. I
wonder if there is another construction of the real numbers that is
based solely on generally useful mathematical objects? The one I
remember from my undergraduate days makes the type definition

real = rational set

where each rational set must be downward-closed (i.e., if a rational
set S contains x then S also contains every rational less than x).
This construction might be more involved than the one in HOL Light,
but has the advantage of being based only on generally useful objects
(sets and rational numbers).

Cheers,

Joe


On Mon, Nov 24, 2014 at 11:49 AM, Konrad Slind <konrad.slind at gmail.com> wrote:
> It's a scoping issue. I think that Peter Homeier's HOL-Omega
> can quantify/bind the local constants used to construct datatypes,
> for example. So its rules may provide guidance on what OpenTheory
> should do.
>
> Sorry, I know I am not answering the original question.
>
> Konrad.
>
>
> On Mon, Nov 24, 2014 at 1:32 PM, Mario Carneiro <di.gama at gmail.com> wrote:
>>
>> I expect that it will be impossible to remove most of the local
>> definitions that you are talking about, because they serve an important
>> purpose: they are useful for "forgetting" about constructions. Once you've
>> proven that the reals have the desired properties, it no longer becomes
>> important what sequence of embeddings was used to build the Real type in the
>> first place, and indeed there is an aesthetic in proofs which avoid any
>> reference to such "construction-dependent" properties. (This process is made
>> explicit in Metamath, where we derive the basic properties of the reals,
>> then ignore these proofs and replace them with axioms so that you can't use
>> the construction any more but are forced to use only the properties.) A
>> similar argument applies to the abstraction and representation functions -
>> unless you are going to be moving between the types often, you may as well
>> forget about these functions once the basic properties of the new type are
>> established.
>>
>> These are new constants whose construction is mandated by the language.
>> You can't make a new type without getting abs,rep functions out. You can't
>> construct a derived type without constructing the base type first. Once you
>> have the constants, but you no longer need them, what are you supposed to do
>> with them?
>>
>> Mario
>>
>> On Mon, Nov 24, 2014 at 2:13 PM, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>>
>>> There have been several discussions on this list about symbols (i.e.,
>>> type operators and constants) that are defined in a theory but are not
>>> mentioned in any exported theorem, which Rob named local definitions.
>>> Since most of the HOL family of theorem provers maintain a global
>>> symbol table, these local definitions can cause problems if they have
>>> clashing names.
>>>
>>> Up until now it's been difficult to see the complete set of symbols
>>> referred to inside a theory, but this can now be displayed with the
>>> opentheory info --symbols command (I append the output for the most
>>> recent version of the standard theory library: base-1.169). As can be
>>> seen, most of the local definitions (which are the symbols in the
>>> HOLLight namespace) are abstraction and representation functions for
>>> type definitions, but there are also others such as those that are
>>> used to construct the real numbers.
>>>
>>> In my opinion it would make theories more elegant if (some of) these
>>> local definitions could be removed, but in the meantime I'd like to
>>> know of any instances with clashing local definitions (these could
>>> occur either in the same theory or across different theories). My
>>> current belief is that these should be easy to fix in a natural way,
>>> but I need to see some concrete examples.
>>>
>>> Cheers,
>>>
>>> Joe
>>>
>>> ______________________________________________________
>>>
>>> $ opentheory info --symbols base
>>> 3 external type operators: -> bool ind
>>> 2 external constants: = select
>>> 11 defined type operators: Data.List.list Data.Option.option Data.Pair.*
>>>   Data.Sum.+ Data.Unit.unit HOLLight.hreal HOLLight.nadd
>>> HOLLight.recspace
>>>   Number.Natural.natural Number.Real.real Set.set
>>> 210 defined constants: ! /\ ==> ? ?! \/ ~ cond F T Data.List.::
>>> Data.List.@
>>>   Data.List.[] Data.List.all Data.List.any Data.List.case.[].::
>>>   Data.List.concat Data.List.drop Data.List.filter Data.List.foldl
>>>   Data.List.foldr Data.List.fromSet Data.List.head Data.List.interval
>>>   Data.List.last Data.List.length Data.List.map Data.List.member
>>>   Data.List.nth Data.List.nub Data.List.nubReverse Data.List.null
>>>   Data.List.replicate Data.List.reverse Data.List.tail Data.List.take
>>>   Data.List.toSet Data.List.zip Data.List.zipWith
>>>   Data.Option.case.none.some Data.Option.isNone Data.Option.isSome
>>>   Data.Option.map Data.Option.none Data.Option.some Data.Pair.,
>>>   Data.Pair.fst Data.Pair.snd Data.Sum.case.left.right Data.Sum.destLeft
>>>   Data.Sum.destRight Data.Sum.isLeft Data.Sum.isRight Data.Sum.left
>>>   Data.Sum.right Data.Unit.() Function.^ Function.const Function.flip
>>>   Function.id Function.injective Function.o Function.surjective
>>>   Function.Combinator.s Function.Combinator.w HOLLight._dest_list
>>>   HOLLight._dest_option HOLLight._dest_rec HOLLight._dest_sum
>>>   HOLLight._mk_list HOLLight._mk_option HOLLight._mk_rec HOLLight._mk_sum
>>>   HOLLight.dest_hreal HOLLight.dest_nadd HOLLight.dest_num
>>>   HOLLight.dest_real HOLLight.dest_set HOLLight.hreal_add
>>>   HOLLight.hreal_inv HOLLight.hreal_le HOLLight.hreal_mul
>>>   HOLLight.hreal_of_num HOLLight.is_nadd HOLLight.mk_hreal
>>> HOLLight.mk_nadd
>>>   HOLLight.mk_num HOLLight.mk_pair HOLLight.mk_real HOLLight.nadd_add
>>>   HOLLight.nadd_eq HOLLight.nadd_inv HOLLight.nadd_le HOLLight.nadd_mul
>>>   HOLLight.nadd_of_num HOLLight.nadd_rinv HOLLight.one_ABS
>>> HOLLight.one_REP
>>>   HOLLight.treal_add HOLLight.treal_eq HOLLight.treal_inv
>>> HOLLight.treal_le
>>>   HOLLight.treal_mul HOLLight.treal_neg HOLLight.treal_of_num
>>>   HOLLight.ABS_prod HOLLight.BOTTOM HOLLight.CONSTR HOLLight.FCONS
>>>   HOLLight.FINREC HOLLight.FNIL HOLLight.IND_0 HOLLight.IND_SUC
>>>   HOLLight.INJA HOLLight.INJF HOLLight.INJN HOLLight.INJP HOLLight.NUMFST
>>>   HOLLight.NUMLEFT HOLLight.NUMPAIR HOLLight.NUMRIGHT HOLLight.NUMSND
>>>   HOLLight.NUMSUM HOLLight.NUM_REP HOLLight.REP_prod HOLLight.ZBOT
>>>   HOLLight.ZCONSTR HOLLight.ZRECSPACE Number.Natural.* Number.Natural.+
>>>   Number.Natural.- Number.Natural.< Number.Natural.<= Number.Natural.>
>>>   Number.Natural.>= Number.Natural.^ Number.Natural.bit0
>>>   Number.Natural.bit1 Number.Natural.distance Number.Natural.div
>>>   Number.Natural.even Number.Natural.factorial Number.Natural.isSuc
>>>   Number.Natural.log Number.Natural.max Number.Natural.min
>>>   Number.Natural.minimal Number.Natural.mod Number.Natural.odd
>>>   Number.Natural.pre Number.Natural.suc Number.Natural.zero Number.Real.*
>>>   Number.Real.+ Number.Real.- Number.Real./ Number.Real.< Number.Real.<=
>>>   Number.Real.> Number.Real.>= Number.Real.^ Number.Real.~
>>> Number.Real.abs
>>>   Number.Real.fromNatural Number.Real.inv Number.Real.max Number.Real.min
>>>   Number.Real.sup Relation.bigIntersect Relation.bigUnion Relation.empty
>>>   Relation.fromSet Relation.intersect Relation.irreflexive
>>> Relation.measure
>>>   Relation.reflexive Relation.subrelation Relation.toSet
>>>   Relation.transitive Relation.transitiveClosure Relation.union
>>>   Relation.universe Relation.wellFounded Set.{} Set.bigIntersect
>>>   Set.bigUnion Set.bijections Set.choice Set.cross Set.delete
>>>   Set.difference Set.disjoint Set.finite Set.fold Set.fromPredicate
>>>   Set.hasSize Set.image Set.infinite Set.injections Set.insert
>>>   Set.intersect Set.member Set.properSubset Set.rest Set.singleton
>>> Set.size
>>>   Set.subset Set.surjections Set.union Set.universe
>>>
>>> _______________________________________________
>>> 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
>