[opentheory-users] extracting intermediate theorems

[Joe Leslie-Hurd]

Hi Ramana,

Sure thing, thanks for letting me know you were able to solve your
problem in another way. Please let me know if you run across another
use-case for searching and/or extracting intermediate theorems.

Cheers,

Joe

On Wed, Jan 7, 2015 at 11:18 PM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> 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
>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>