[opentheory-users] Local definitions in theory packages

[Joe Leslie-Hurd]

Hi Ramana,

I appreciate the vote of support for theorem provers to support local
definitions, and it certainly makes it easier to compose "Little
Theories" without worrying about the names of local definitions
clashing.

However, I just want to clarify that the OpenTheory article spec is
deliberately agnostic about the implementation details of definitions.
Article readers can ensure soundness using a purely functional logical
kernel like the opentheory tool or a global symbol table like the HOL
family of theorem provers, and both implementations satisfy the
article spec.

To support the global symbol table approach I have made two changes to
the opentheory tool:

1. Every symbol referred to in a theory can be displayed using the
opentheory info --symbols command.
2. The opentheory tool will warn the user when creating an article
containing clashing symbols.

In addition, I am prepared to change my theories on the public repo if
they contain instances of symbols with the same name but different
definitions.

Cheers,

Joe









On Tue, Nov 25, 2014 at 6:39 AM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> 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
>>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>