Email Gateway (Aug 23 2022 at 08:35): Email Gateway (Aug 23 2022 at 08:35):From: Jose Manuel Rodriguez Caballero <jose.manuel.rodriguez.caballero@ut.ee>
Hi,
I noticed the following minor problem in the proof of lemma "blinfun_of_matrix_works" (HOL/Analysis/Bounded_Linear_Function.thy):
also have "… = (∑i∈Basis. (x ∙ i * (f i ∙ b)))"
using b by (simp add: sum.delta)
It is enough to write
also have "… = (∑i∈Basis. (x ∙ i * (f i ∙ b)))"
using b by simp
Kind regards,
José M.
Email Gateway (Aug 23 2022 at 08:36):From: Makarius <makarius@sketis.net>
There have been a lot of changes to HOL-Analysis by multiple people, but no
tangible NEWS entries so far. It is still time to improve the situation (by
sending me changes).
Also note that release candidates become obsolete rather quickly: presently we
are are Isabelle2020-RC3. It does not make sense to continue testing older ones.
Makarius
Email Gateway (Aug 23 2022 at 08:36):From: Tobias Nipkow <nipkow@in.tum.de>
Thanks, I have removed the simp rule but I suspect it will not go into the
release as it is not significant enough.
Tobiass
smime.p7s
Email Gateway (Aug 23 2022 at 08:36):From: Manuel Eberl <eberlm@in.tum.de>
I suspect there are probably many hundreds of instances of such things.
It does not really cause any problems, so I personally don't think it's
worth to go through these on the mailing list or even to report them in
the first place.
(If anyone disagrees, feel free to correct me, of course)
Cheers,
Manuel
Email Gateway (Aug 23 2022 at 08:36):From: Tobias Nipkow <nipkow@in.tum.de>
I have on more than one occasion been confused by such superfluous rules when I
tried to understand a proof, hence I do think it is worth removing them.
But I agree that because there will be many of them, one should not post it on
the mainling list if it can be avoided: eg collect them first (if one is
actively weeding them out), send them to an known maintainer or the author of
the theory.
Tobias
smime.p7s
Email Gateway (Aug 23 2022 at 08:36):From: Manuel Eberl <eberlm@in.tum.de>
Well, a maintainer could also simply go through the list and look at all
the warnings. Most of them will probably either be something like this
or something like "rule xyz was already declared as an intro rule" when
somebody does "auto intro!: continuous_intros" (which is unavoidable).
Manuel
Email Gateway (Aug 23 2022 at 08:36):From: Lawrence Paulson <lp15@cam.ac.uk>
As a general rule, it’s preferable for proofs to be as simple as possible: not short in characters, but simple in logical structure and dependencies. Suggestions of simpler and clearer proofs are always welcome. Generalisations (removing unnecessary assumptions or relaxing type class constraints) are especially valuable.
Larry
Email Gateway (Aug 23 2022 at 08:36):From: Tjark Weber <tjark.weber@it.uu.se>
It could be nice to have tool support to address this (and similar
issues) systematically. A student project, perhaps?
Best,
Tjark
När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/
E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy
Email Gateway (Aug 23 2022 at 08:36):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
On 30 Mar 2020, at 17:46, Manuel Eberl <eberlm@in.tum.de> wrote:
[..]
or something like "rule xyz was already declared as an intro rule" when
somebody does "auto intro!: continuous_intros" (which is unavoidable).
Speaking of which: this is a warning we though about removing a while ago. Should we? I can’t remember a case where I have found it useful. Or we could make it configurable whether there is a warning.
Cheers,
Gerwin
Email Gateway (Aug 23 2022 at 08:36):From: Tobias Nipkow <nipkow@in.tum.de>
On 30/03/2020 11:56, Klein, Gerwin (Data61, Kensington NSW) wrote:
On 30 Mar 2020, at 17:46, Manuel Eberl <eberlm@in.tum.de> wrote:
[..]
or something like "rule xyz was already declared as an intro rule" when
somebody does "auto intro!: continuous_intros" (which is unavoidable).Speaking of which: this is a warning we though about removing a while ago. Should we? I can’t remember a case where I have found it useful. Or we could make it configurable whether there is a warning.
I agree, that one could go.
Tobias
Cheers,
Gerwin
Email Gateway (Aug 23 2022 at 08:37):From: Lawrence Paulson <lp15@cam.ac.uk>
I would leave this message but only for situations where the insertion is absolutely redundant. It is useful in those situations.
Larry
Email Gateway (Aug 23 2022 at 08:37):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
So when you add an intro! rule again as an intro! rule, etc? Yes, that would make sense.
Cheers,
Gerwin
Email Gateway (Aug 23 2022 at 08:37):From: Manuel Eberl <eberlm@in.tum.de>
It's not quite that simple.
I think there are e.g. some "intro" rules that are also in
"continuous_intros". So if I do "apply (auto intro: continuous_intros)",
I get a warning.
You might suggest removing that rule from "continuous_intros", but that
would then mean that doing something like "apply (intro
continuous_intros)" or "apply (rule continuous_intros | simp)+" (which I
occasionally do with derivative_eq_intros, don't judge me) would not
work as intended anymore.
I guess for continuous_intros/derivative_intros etc. the general idea is
that all rules should be safe introduction rules anyway, so doing
"intro" instead of "intro!" doesn't make much sense, but for other
theorem collections that might not be case.
On a related note: Perhaps we should make a little "derivative" method
based on "derivative_eq_intros", similarly to what I sketched above.
Cheers,
Manuel
Email Gateway (Aug 23 2022 at 08:37):From: Lawrence Paulson <lp15@cam.ac.uk>
Good idea. Currently, tricks like
apply (intro derivative_eq_intros | simp)+
are folklore and not everybody knows about them.
Larry
Email Gateway (Aug 23 2022 at 08:37):From: Dominique Unruh <unruh@ut.ee>
Hi,
I think the warning should only show if removing the simpl/auto argument
does not change the actions of the method.
That is:
for "simp: X" "intro: X" "intro!: X", there should be a warning if
all the theorems in X already are already in the corresponding
category. (In particular, lemmas X = A B declare A[simp] ... by (simp
add: X) should not give a warning. Also declare A[intro] ... by (auto
intro!: A) should not give a warning, but by (auto intro: A) should.
for "simp del: X" and friends, there should be a warning if none of
the theorems in X are in the corresponding category.
If I am not mistaken, this will mean that you never get a warning that
something is redundant, and then if you remove it, things stop working.
Best wishes,
Dominique.
Email Gateway (Aug 23 2022 at 08:37):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
I agree, that would be nice. We do have the intro issue Manuel mentions already with simp collections, with similar problems.
Not sure if this check would be expensive to implement for larger sets of rule. Probably not more than the current check, though.
Cheers,
Gerwin
Last updated: Apr 25 2024 at 12:23 UTC