[opentheory-users] Local definitions in theory packages

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Tue Nov 25 14:39:39 UTC 2014
Previous message: [opentheory-users] Local definitions in theory packages
Next message: [opentheory-users] Local definitions in theory packages
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
Hi all,

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.

Cheers,
Ramana

On Mon, Nov 24, 2014 at 10:42 PM, Mario Carneiro <di.gama at gmail.com> wrote:

> Hi Joe,
>
> On Mon, Nov 24, 2014 at 5:19 PM, Joe Leslie-Hurd <joe at gilith.com> wrote:
>
>> 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.
>>
>
> 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 http://us2.metamath.org:88/mpegif/omxpen.html 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:
>
> The definition way:
>
>   |- c1 = (1+1)
>   |- 1 < (1+1)
>  |- 1 < c1
> |- ?x. 1 < x
>
> The temporary definition way:
>
>     c = (1+1) |- 1 < c <=> 1 < (1+1)
>     |- 1 < (1+1)
>    c = (1+1) |- 1 < c
>   c = (1+1) |- ?x. 1 < x
>  (1+1) = (1+1) |- ?x. 1 < x
>  |- (1+1) = (1+1)
> |- ?x. 1 < x
>
> 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.
>
> Mario
>
>
>> 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
>> >
>>
>> _______________________________________________
>> 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/20141125/f52f137c/attachment-0001.html>
Previous message: [opentheory-users] Local definitions in theory packages
Next message: [opentheory-users] Local definitions in theory packages
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
More information about the opentheory-users mailing list