Email Gateway (Aug 18 2022 at 16:39): Email Gateway (Aug 18 2022 at 16:39):From: Joachim Breitner <mail@joachim-breitner.de>
Hi,
I’m trying to add the Nielsen-Schreier theorem to the FreeGroups theory
in AFP. I’m following a proof in a modern text book¹ which seems to be
sufficiently rigorous to base on. Yet, I needed almost 500 lines and a
whole day just to almost proof the first item in the first lemma – that
is less than half a page of proof-related definitions and lemmata in the
book. I get the feeling that I’m doing it wrong.
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.
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?
Are there work-arounds or other best practice to handle such a problem?
Thanks,
Joachim
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?
¹ http://books.google.de/books?id=RGzK_DOTijsC&lpg=PA285&dq=schreier-nielsen&pg=PA285#v=onepage&q&f=false
signature.asc
Email Gateway (Aug 18 2022 at 16:39):From: Alexander Krauss <krauss@in.tum.de>
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
Email Gateway (Aug 18 2022 at 16:39):From: Joachim Breitner <mail@joachim-breitner.de>
Hi Alexander,
Am Samstag, den 11.12.2010, 12:39 +0100 schrieb Alexander Krauss:
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.
great, I am looking forward to that. And at least I’m not doing
something stupid :-).
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.
Ok, just asking.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 18 2022 at 16:39):From: Gerwin Klein <gerwin.klein@nicta.com.au>
Hi Joachim,
I'll leave the content questions to others on the list who know more about the formalisation.
To expand a bit on Alex's answer for the AFP question:
No, the AFP will not support branches, definitely not in-repository branches. As Alex said, this would be a maintenance nightmare, but it also does not make sense for what the AFP is -- a public archive of reviewed entries.
It may be a reasonable idea to use a branch locally for development, but publishing it for citing it separately and using the name AFP for it would be very much discouraged. The point of the AFP is that it is quality controlled and edited.
We give authors access to the development version of the AFP for maintenance, but we trust them to make maintenance changes only and we monitor all commits. Adding major developments is not what this access if for, much less adding new entries. Any such activities need to be coordinated with the editors.
Technically, to create a branch, you could make a local clone of the repository (not an in-repository branch) and work on that.
I don't quite see the point in such a branch, though. An additional major theorem like this should be a new AFP submission, based on the existing entry. It should be based on the released version of the archive and the released version of Isabelle, not on http://afp.hg.sourceforge.net/hgweb/afp/afp/ which is the development version and unstable, often changing daily based on the development version of Isabelle.
From the sound of it, we'd be more than happy to accept a new submission with the development you're working on.
Cheers,
Gerwin
Email Gateway (Aug 18 2022 at 16:40):From: Joachim Breitner <mail@joachim-breitner.de>
Hi Gerwin,
ok, that wasn’t fully clear to me (and I already violated that rule by
finishing the free-group-isomorphism result in this commit:
http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/132265dbbf80, sorry for
that).
So at least in this case, I’d like to continue basing my work on
Isabelle-devel and AFP-devel (otherwise I’d have to undo compatibility
changes and add all the auxiliary lemmas that went into HOL by now), but
I’ll not push my changes but rather put my repository somewhere and ask
the editors to review and merge once (and if) I’m done.
Should such a new theorem be submitted as a new AFP entry or as an
update of the existing FreeGroup entry?
Greetings,
Joachim
signature.asc
Email Gateway (Aug 18 2022 at 16:40):From: Gerwin Klein <gerwin.klein@nicta.com.au>
Hi Joachim,
On 12/12/2010, at 5:10 AM, Joachim Breitner wrote:
ok, that wasn’t fully clear to me (and I already violated that rule by
finishing the free-group-isomorphism result in this commit:
http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/132265dbbf80, sorry for
that).
I guess the question is what is a "major new theorem" or "major new addition".
This commit above is ok as an incremental change, and naturally fits into the development entry, so nobody had a problem with it. If you have similar things but just a bit bigger, you should coordinate with the editors, and we're very likely to give you an ok for the change. It should be noted in the public history/changelog of the entry, though.
Your description sounded like major new work to me, in size at least on the order of the existing entry. I would not say that this is just a small addition or maintenance change then. One indication for this was that you wanted to cite the change. If it's big enough for that, I'd usually think that it is a new entry. It is possible that in some cases (maybe this one too) that it makes sense to merge the new work with an existing entry, and if there are good reasons for it we'll be happy to do that. In any case it at least needs discussion and review, and needs to be marked in the public history of the entry again.
The main concern is that AFP entries need to be citable. For that to work, it must be clear what a citation refers to, that target must be unchangeable, and it must be reproducible for readers. For an evolving system like Isabelle the last two are in conflict, so we make regular releases and allow maintenance changes. Those that want (convenient) reproducible can download the current version, those that want to know exactly what was described in the paper can download the version that was submitted or cited (a citation will contain the entry name and URL and a year, maybe a month, so that should be clearly defined).
For this to make sense, even the maintenance version must still at least be close to the cited version. If we accept silent major changes, this breaks.
As evidenced by our discussion, "major" doesn't have a precise meaning and we're happy to be flexible. As a solution to changes that don't warrant a new entry, but that do significantly change what a reader would reasonably expect in an entry, we've introduced a public history/changelog for entries where these changes can be marked and it is made clear for readers what happened when (the version control changelog would be way to low-level for that). As editors we want to know of things that go in there. We haven't had a case yet where we violently disagreed, only cases where we had suggestions for change and usually no problem at all.
So from a practical point of view, we should discuss off-list how big your change really is and if it should be merged or not. It's hard to say without seeing the new development or knowing more about it.
So at least in this case, I’d like to continue basing my work on
Isabelle-devel and AFP-devel (otherwise I’d have to undo compatibility
changes and add all the auxiliary lemmas that went into HOL by now),
This happens from time to time. We can do that, but it has a major disadvantage for you until the next release: you can't really cite the new development yet, even if it is in the afp repository. It only becomes properly visible to site users with the next Isabelle release. The next release is rumoured to be planned for early next year, so this might not be a big deal this time.
The reason it is not citable is that it is not reproducible. It would be major work for a reader or referee to figure out which exact hg id of the entry and of Isabelle you are referring to. It would be hard now, and it would be very hard in 10 years (who knows what version control system we're running then). With just the data of a normal citation it would be pretty much impossible.
but I’ll not push my changes but rather put my repository somewhere and ask
the editors to review and merge once (and if) I’m done.
If that is what you want to do, a local hg clone of the afp development repository is probably the right way to go, because you can pull in Isabelle related changes.
Cheers,
Gerwin
Email Gateway (Aug 18 2022 at 16:40):From: Joachim Breitner <mail@joachim-breitner.de>
Hi,
Am Sonntag, den 12.12.2010, 10:54 +1100 schrieb Gerwin Klein:
Your description sounded like major new work to me, in size at least
on the order of the existing entry. I would not say that this is just
a small addition or maintenance change then. One indication for this
was that you wanted to cite the change.
ah, there is a misunderstanding, cause by unclear wording on my side.
With “cite” I meant that I want to show my current development state
easily when asking technical questions (which started this thread), and
it would be convenient to have it available in some publicly readable
repository with hgweb access. I did not mean or plan citing in the
academical sense.
(But I still see that with hg it is inconvenient to have personal
branches in the AFP repository and that I will host my branch somewhere
else.)
So from a practical point of view, we should discuss off-list how big
your change really is and if it should be merged or not. It's hard to
say without seeing the new development or knowing more about it.
I’ll raise that once it’s ready.
but I’ll not push my changes but rather put my repository somewhere
and ask the editors to review and merge once (and if) I’m done.If that is what you want to do, a local hg clone of the afp
development repository is probably the right way to go, because you
can pull in Isabelle related changes.
yes, this is already what I’m doing.
Greetings,
Joachim
signature.asc
Last updated: Apr 20 2024 at 12:26 UTC