[opentheory-users] Local definitions in theory packages

[Mario Carneiro]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141124/de8f742a/attachment-0001.html>