Re: [isabelle] How to avoid x \<in> carrier G proofs



Hi Joachim,

Most of the time I seem to be spending with proving that some element is
in the carrier of the group, i.e. "x \<in> carrier (free_group gens)",
which is “obvious” to the mathematician. Most group-related lemmata have
such a proposition in their premises, so I need to careful cite the
right carrier-statements before any kind of automation would work.

This is a notorious problem, and there is no satisfactory solution. From 2011 on I'll be working on an infrastructure to deal with this (basically recovering what type systems do on the level of reasoning), but I am not expecting to have something usable for quite some time.

To me it seems that if I had a type for the set of group elements, then
type inference would had no trouble showing these requirements. But, if
I understand correctly, that would require dependent types (because the
type would encapsulate the parameter "gens"), which are not supported in
Isabelle. Is that right? Is it also right within a locale, or can locale
contexts introduce types?

Yes, that's right. Dependent types arise naturally in this kind of reasoning. "free_group gens" is one example. Another is "matrix n m A" etc. There are no dependent types in HOL, and putting locales on top does not help (Currently, local typedefs are permitted, but they may not depend on locale parameters, so it is just a formal locality).

Are there work-arounds or other best practice to handle such a problem?

Well, not really. Sometimes a term dependency can be modelled as a type dependency, e.g. the famous R^n (where n is modelled as a type). But this has a number of limitations and does not make sense in many cases.

Another thing that may help a bit is to write a simproc that discharges membership proof obligations. Then at least the simplifier works a bit better in these situations. But it requires some ML, and unfortunately other tools cannot easily be extended like this.

PS: Is it ok to create personal branches, named appropriately, on
http://afp.hg.sourceforge.net/hgweb/afp/afp/ where I could push my work
to cite it here?

Please don't do this! Having everybody's private branches centrally is a maintenance nightmare. Instead you can easily publish your own branch (read: clone of the repository with your own changes) on the web. This is what Mercurial is good at. If you don't have a server, there are also public hosting sites.

Alex






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