[opentheory-users] Local definitions in theory packages

[Joe Leslie-Hurd]

Hi Mario,

I agree that local definitions serve an important need in forgetting
about constructions, and I expect that it will be impossible to
eliminate them completely.

However, perhaps a future version of the article spec will incorporate
Rob's new type operator specification principle which defines a new
type without also defining abs/rep constants, and this will at least
offer the theory developer a simple way to eliminate a large class of
local definitions.

Cheers,

Joe

On Mon, Nov 24, 2014 at 11:32 AM, 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
>