Email Gateway (Aug 19 2022 at 15:21): Email Gateway (Aug 19 2022 at 15:21):From: Tobias Nipkow <nipkow@in.tum.de>
Dear Andres,
It is what it is mostly for historical reasons, but I also seem to recall that
=simp=> lead to nontermination in same cases (unsurprisingly) and that therefore
we restricted its usage. You could try to replace map_cong by your map_cong' and
see if anything breaks. If not, that would be a strong indication that the
map-congruence rules generated by datatype should always use =simp=>.
Tobias
Email Gateway (Aug 19 2022 at 15:22):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Tobias,
Thanks for the background infos. I pushed the replacement of ==> with =simp=> to testboard
(see http://isabelle.in.tum.de/testboard/Isabelle/rev/1cbcd78f8d3c). I expect a few proofs
in the AFP to break, because they use apply(rule map_cong), but let's see.
Even if that is the only problem, I doubt that this will be a strong indication either
way. A grep over the sources revealed just a few places where map_cong is used (map_cong
is not a default congruence rule); probably because the [simp] rule map_eq_conv takes
already care of map equalities.
Andreas
Email Gateway (Aug 19 2022 at 15:23):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Tobias,
Here is the summary of =simp=> vs. ==> in the congruence rule for map. I replaced map_cong
by map_cong' in List.thy and ran all of the Isabelle distribution (isabelle makeall) and
the AFP, thereby fixing what was broken.
Whenenver map_cong was used as a congruence rule, map_cong' also works, without looping.
I found three occurrences where map_cong was not used as [cong] that fail with map_cong'.
a) In HOL/Word/Word.thy, it is used with rule. Using it as a congruence rule causes the
simplifier to loop, but this is independent of whether ==> or =simp=> is used.
b) In the AFP entry Affine_Arithmetic is used with subst followed by auto.
(simp cong: map_cong') does not solve the goal, either.
c) In the AFP entry Matrix, there is an instance of the pattern
by(rule map_cong)(auto ...)
Both (simp cong: map_cong) and (simp cong: map_cong') solve the goal, too.
In conclusion, =simp=> does not break anything in the tested theories when map_cong is
used as a congruence rule. Since [fundef_cong] does not handle =simp=> and map_cong seems
to be useful in some cases (2a,b), we should keep the version with ==>. Possibly, BNF
could also generate the congruence rule list.strong_map_cong with =simp=>. The name follow
the existing naming convention for ball, bex, SUP, INF, ... (Although I would prefer
map_cong_strong because the main operator does not hide somewhere in the middle of the
theorem name.)
Andreas
Email Gateway (Aug 19 2022 at 15:23):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi Andreas,
Thanks for your thorough investigation.
In conclusion, =simp=> does not break anything in the tested theories when map_cong is used as a congruence rule. Since [fundef_cong] does not handle =simp=> and map_cong seems to be useful in some cases (2a,b), we should keep the version with ==>. Possibly, BNF could also generate the congruence rule list.strong_map_cong with =simp=>. The name follow the existing naming convention for ball, bex, SUP, INF, ... (Although I would prefer map_cong_strong because the main operator does not hide somewhere in the middle of the theorem name.)
Good idea. I would also prefer "_strong" as a suffix, for consistency with other "_strong"ly-suffixed properties in BNF. We'll add it to our list. If nobody objects, I could also rename "strong_ball_cong" etc. to "ball_cong_strong" etc. (once Isabelle2014 is out).
Cheers,
Jasmin
Email Gateway (Aug 19 2022 at 15:23):From: Tobias Nipkow <nipkow@in.tum.de>
Hi Andreas,
Thanks for that. For me it sounds pretty conclusive that we should follow your
recommendation: let BNF generate both map_cong and map_cong_strong.
Thanks!
Tobias
Email Gateway (Aug 19 2022 at 15:23):From: Tobias Nipkow <nipkow@in.tum.de>
It would improve uniformity.
Tobias
Email Gateway (Aug 19 2022 at 15:23):From: Dmitriy Traytel <traytel@in.tum.de>
I would even argue that there is nothing "strong" about those rules
(since op =simp=> = op ==>). So if renaming anyway, maybe ball_cong_simp
or even ball_cong_simp_implies is a better name?
Dmitriy
Email Gateway (Aug 19 2022 at 15:24):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
I have no strong opinion about the naming schema itself, but it should
be uniform afterwards.
Also note that the situation with sum and prod and sets is a little
delicate and demands a suffix pattern due to interpretation, e.g.
foo.strong_cong.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 15:46):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
I wondered why the congruence rule for map does not enable the simplifier to solve
statements such as the following. Such statements occur naturally with the induction rules
from the new datatype package when recursion goes through a list.
lemma "(⋀x. x ∈ set xs ⟹ f x = g x) ⟹ h (map f (rev xs)) = h (map g (rev xs))"
apply(simp cong: list.map_cong)
Then, I found he following comment on op =simp=> in HOL.thy:
text {*
The following copy of the implication operator is useful for
fine-tuning congruence rules. It instructs the simplifier to simplify
its premise.
*}
definition simp_implies :: "[prop, prop] => prop" (infixr "=simp=>" 1) where
"simp_implies ≡ op ==>"
A look at the usages of op =simp=> showed that it is only used in congruence rules for the
big operators and bounded quantification. In particular, all of them use it in the form
!!x. x : ?B =simp=> ?f x = ?g x
and the same form shows up in list.map_cong. And indeed, if list.map_cong were
lemma map_cong': "⟦xs = ys; ⋀x. x ∈ set ys =simp=> f x = g x⟧ ⟹ map f xs = map g ys"
unfolding simp_implies_def by(rule list.map_cong)
then simp would be able to solve the above goal:
by(simp cong: map_cong')
My question now is: What is the advantage of op ==> over op =simp=> in congruence rules,
i.e., list.map_cong over map_cong'? Since the BNF package generates congruence rules with
the structure
!!x. x : set_type ?A ==> f x = g x
would it be sensible to use =simp=> there?
By the way, I noticed that [fundef_cong] cannot deal with =simp=>. But that should not be
the only reason for having the weaker cong rule.
Best,
Andreas
Last updated: Apr 16 2024 at 12:28 UTC