[opentheory-users] Status of derived syntax

[Rob Arthan]

Joe,

On 22 Nov 2013, at 18:58, Joe Leslie-Hurd wrote:

> Hi Rob,
> 
> The derived syntax in OpenTheory is rather ad-hoc: I just hard-coded some common mathematical syntax such as numerals, pairs and sets which is triggered by specific names in the OpenTheory namespace.
> 
> When exporting HOL Light theories to the OpenTheory library, one of the more involved things I had to do is remove as many HOL Light-specific tags as possible. So for example, the NUMERAL tag is easily removed, and OpenTheory numerals are instead recognized by sequences of bit0 and bit1 functions terminated by natural number zero.
> 
> The OpenTheory version of GSPEC is called fromPredicate, and you can see the standard library renamings in the OpenTheory fork of HOL Light in the file
> 
> opentheory/stdlib/stdlib.int
> 
> This is how sets are recognized for printing purposes (assuming that the term argument to fromPredicate has the right shape).
> 
> Finally, I'm rather pleased by my scheme for recognizing let expressions, although it sounds like it might be causing you problems displaying your theory.

I haven't got that far yet. I have just been looking at the article files and HTML pages in the repo.

> Lets are simply terms that can be beta-reduced, so
> 
> (\v. t[v]) x
> 
> is printed as
> 
> let v = x in t[v]
> 
> No need for any special term tags, and in all the theories I have so far encountered there are no subterms in theorems that can be beta-reduced (and thus accidentally print as let).

Nice idea. I don't think you would want that feature while doing interactive theorem-proving, but it makes sense in your context. I have just had a go with the ProofPower theorem finder and it supports your approach: there are no theorems saved in the ProofPower-HOL theory hierarchy containing beta-redexes.

However, some packages contain assumptions that do contain beta-redexes and hence have been printed out as let-expressions in the HTML. See:

http://opentheory.gilith.com/opentheory/packages/axiom-choice-1.7/axiom-choice-1.7.html
http://opentheory.gilith.com/opentheory/packages/axiom-extensionality-1.8/axiom-extensionality-1.8.html
http://opentheory.gilith.com/opentheory/packages/natural-1.81/natural-1.81.html

The assumption in the last one of these is a real monster. They all look like intermediate lemmas generated by some proof procedure whose proofs have somehow gone missing.

> 
> Hope that helps,

It does indeed. I have some other questions about using the article files in the repo, but I think I will start a separate thread for that.

Regards,

Rob.

> 
> Joe
> 
> 
> 
> 
> On Fri, Nov 22, 2013 at 8:08 AM, Rob Arthan <rda at lemma-one.com> wrote:
> What is the status of things like let-terms and set comprehensions in the Gilith Open Theory Repo. I can't see the definitions of the magic constants that are used to represent these things (LET and GSPEC in HOL Light and HOL4)? A peculiar sequence of complicated assumptions involving let builds up in the HTML listings.
> 
> Regards,
> 
> Rob.
> 
> _______________________________________________
> 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/20131123/76fd8c12/attachment.html>