Re: [isabelle] Types-To-Sets: a question about further development of the framework (may be of interest to the topic Re: abelian_group)



Dear Andrei Popescu/All,

After using Types-To-Sets for the relativisation of the results from the
main library of Isabelle/HOL for a little while, I came to a conclusion
that the two main problems with the existing methodology are the
'boilerplate' code associated with having to restate the names of the
relativised theorems at least twice and, more importantly, forward
compatibility with the potential changes to the class/locale that is being
relativised (of course, it would also be interesting to understand if there
could be a negative impact associated with the extension of HOL logic and I
would like to know more about the arguments that were presented on this
subject in the past). I must admit that I am not certain whether further
automation, i.e. automatic generation of the relativised definitions, would
be beneficial and make the framework more user-friendly than it is at the
moment: usually there are several equivalent ways to present a given
relativised definition and I see no reason to force the users to use a
pre-defined default.

In the short-/mid-term, I would like to provide the following functionality
that will not require any modifications to the critical code:
1. For the relativisation of definitions, I would like to discharge the
necessary proof obligations automatically and store a 'connection' between
the original and the relativised definitions as (retrievable) data.
2. For the relativisation of theorems, I would like to combine the
application of a chain of attributes in a single parameterisable
command/attribute and (provide an option to) discharge the proof
obligations for further user amendments of the relativised results (e.g.
consider the case of an empty carrier set for topological spaces)
automatically. Naturally, this would also include the automation of the
naming conventions and, therefore, result in a significant reduction of the
boilerplate code. Also, the 'connection' between the relativised and
non-relativised theorems would be made available as retrievable data.

I believe that having an ability to see whether a given const/theorem was
relativised or not and where should be sufficient to make the framework
forward compatible with changes to the original class/locale, which, for
me, is the main problem with the large scale application of the framework.
The relativised definitions would still need to be provided by the user and
the transfer rules would still need to be proven manually. However, at
least, the user will not need to provide the statements of the theorems for
the transfer rules explicitly.

In summary, my plan is to introduce several changes to the interface
associated with the methodology and not the critical code.

I am not, specifically, asking for any help with the technical matters, but
I would appreciate any insight. I am merely trying to do understand whether
or not there are any active R&D projects related to "Types-To-Sets". Given
that this project does not have the highest priority for me and I have much
to learn about Isabelle at the ML level, it is likely that I will be
working on this project for several months to come in small intervals. I am
merely trying to reassure myself that this will not be a wasted effort
because someone else is already working on something better. As a side
note, of course, as I mentioned previously, if anyone has any particular
ideas about what can be done beyond what is suggested in [1] and in this
email, I would be interested in learning about them. Also, if you suspect
that I might be trying to take this work in the wrong direction, I would be
thankful to hear from you.

Thank you

[1] F. Immler and B. Zhan, “Smooth Manifolds and Types to Sets for Linear
Algebra in Isabelle/HOL,” in Proceedings of the 8th ACM SIGPLAN
International Conference on Certified Programs and Proofs, ser. CPP 2019.
New York, NY, USA: ACM, 2019, pp. 65–77, event-place: Cascais, Portugal.


On Mon, Apr 15, 2019 at 4:53 PM Andrei Popescu <A.Popescu at mdx.ac.uk> wrote:

> Dear Makarius, Larry and Anonymous Contributor,
>
> I thank you for your support of, and contribution to the types-to-sets
> methodology. I believe the underlying local typedef rule is a very useful
> (yet gentle) upgrade of HOL, and have always advocated its candidacy for
> HOL citizenship. (Incidentally, one of my original motivations was to
> simplify our BNF/(co)datatype package constructions back in 2011, but in
> the end the package was developed without it.)
>
> However, I cannot help with making the types-to-sets machinery more
> user-friendly since I am not fluent in Isabelle/ML. It is Ondrej Kuncar who
> has implemented the local typedef rule and the accompanying "unoverloading"
> rule. And since Ondrej is also a co-developer of the lifting and transfer
> package, he is in an ideal position to make things happen; or to share some
> insights with people who might be interested in taking on such a
> development. Without more progress on this front, only power-users will use
> types-to-sets -- this is a shame, since types-to-sets could be part of the
> regular users' daily menu.
>
> Best wishes,
>
> Andrei
>
>

-- 
Please accept my apologies for posting anonymously. This is done to protect
my privacy. I can make my identity and my real contact details available
upon request in private communication under the condition that they are not
to be mentioned on the mailing list.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.