[opentheory-users] extracting intermediate theorems

[Ramana Kumar]

I was mainly just being lazy about trying to generate an article for a
theorem that I "know must be somewhere as an intermediate in the standard
library" (although maybe it actually wasn't). I ended up generating an
article for it in HOL4, so I don't have a particularly strong need for
these features any more. Thanks for your help though - the tips for putting
together packages with exact dependencies etc. were useful.

On Fri, Jan 2, 2015 at 7:31 PM, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Ramana,
>
> What you're proposing is certainly possible, but first I'd like to
> understand a bit more about your use-case for accessing intermediate
> theorems.
>
> At present the article standard and opentheory tool conspire to create
> an illusion that the intermediate theorems of the theory are
> irrelevant, and that only the imported assumptions and exported
> theorems are important. As a consequence of this abstraction, tools
> that process articles may feel free to replace any or all intermediate
> theorems so long as the assumption/theorem interface is maintained.
>
> Supporting post-hoc extraction of intermediate theorems and promoting
> them to exported theorems goes against this philosophy, because an
> article processing tool that changed intermediate theorems could break
> something downstream that was relying on them having a particular form
> to extract and export.
>
> Given the above, could you please elaborate on your use-case for
> accessing intermediate theorems of articles?
>
> Cheers,
>
> Joe
>
> On Sat, Dec 20, 2014 at 9:31 PM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
> wrote:
> > Hi Joe,
> >
> > On Sat, Dec 20, 2014 at 9:09 PM, Joe Leslie-Hurd <joe at gilith.com> wrote:
> >>
> >> > Show me the intermediate (i.e. unexported) theorems that arise when
> >> > running
> >> > an article.
> >>
> >> No, unfortunately not. The best it can do is tell you *how many*
> >> theorems are generated, by using the --inference option.
> >>
> >> Did you have any thoughts on a way to present intermediate theorems to
> the
> >> user?
> >
> >
> > What would be useful to me is if I could search for intermediate theorems
> > with a pattern. I'd guess you'd rather stay away from specifying parsing
> of
> > such patterns. I wouldn't mind, however, writing my pattern as OpenTheory
> > article commands for creating a term. I'd then like to get back all
> > intermediate theorems that match.
> >
> >>
> >> > Create an article that exports a previously unexported theorem, taking
> >> > an
> >> > existing article as input.
> >>
> >> Also no I'm afraid.
> >
> >
> > That's a pity. Would it be hard to add? Presuming we solve the problem
> above
> > of specifying an intermediate theorem.
> >
> > I guess for the moment I can get around this by using a custom reader
> that
> > looks for the theorem I want and cuts off the article as soon as it
> finds it
> > (and adds on an export). It would be nice if the opentheory tool had
> enough
> > features to support this itself, but maybe it's a little outside your
> design
> > goals? On the other hand, I think a good suite of powerful manipulations
> on
> > OpenTheory packages for a variety of purposes would help buy-in.
> >
> >>
> >> > Minimise an article for what is required for a particular theorem (I
> >> > think
> >> > the answer here is yes, by creating a package with the desired theorem
> >> > and
> >> > then asking for an article for it to be generated...?)
> >>
> >> Indeed. Suppose article foo.art exports a set of theorems containing a
> >> theorem T of interest, then you can create an article bar.art that
> >> proves T by axiom, and then run
> >>
> >> echo 'a { article: "foo.art" } main { import: a article: "bar.art" }'
> >> | opentheory info --article -o baz.art theory:-
> >>
> >> to get a minimal article baz.art proving T.
> >
> >
> > Great, thanks.
> >
> > _______________________________________________
> > 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/20150108/736f36fa/attachment-0001.html>