Email Gateway (Aug 22 2022 at 19:16): Email Gateway (Aug 22 2022 at 19:16):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
in private conversation Manuel has pointed out to me that there is a
potential conflict in simp rules.
Have a look at
add_num_frac [field_simps]:
y ≠ 0 ⟹ z + x / y = (x + z * y) / y
(in class field)
div_mult_self1 [simp]:
b ≠ 0 ⟹ (a + c * b) div b = c + a div b
(in class euclidean_semiring_cancel)
where it is important to know that »_ / _« and »_ div _« is just
different surface syntax for the same operator.
Under normal circumstances, there are no types which are both instances
of field and ring classes, hence there is no problem; but certain
algebra applications require theory HOL-Library.Field_as_Ring, which
makes the field type classes subclasses of corresponding ring classes.
Thus any »(simp add: field_simps)« operates with both simp rules from
above which are effectively symmetric to each other, which is not a good
idea. (There are other similar pairs around, but this only example is
enough to understand the problem).
Generally, the rules in »field_simps« are directed towards establishing
common denominators, which is maybe what they are exactly intended for.
Hence the orientation of add_num_frac is sensible in its particular
context and div_mult_self1 should not be a default simp rule any longer
(it has been made such by me some time ago, not being aware of the issue
mentioned above). But it (or its symmetric) should still be available in
a rule collection.
So which one?
»algebra_simps« would be a fitting name but its rules currently do not
state anything about division, and I presume this is exactly the purpose
of it.
»field_simps« would make semantically sense but the name would be
misleading since there is no field involved in the general case.
»divide_simps« would be a quite fitting name, quoth Field.thy: ‹Lemmas
‹divide_simps› move division to the outside and eliminates them on
(in)equalities.›
I am currently inclined to pursue the latter option, which would also
suggest to generalize the relevant lemmas to a common ancestor type class.
Any further suggestions?
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 19:17):From: Lawrence Paulson <lp15@cam.ac.uk>
The problem is that divide_simps already exists, with the objective of eliminating all occurrences of the division sign in expressions. It is a good deal more effective than field_simps in many situations.
Larry Paulson
Email Gateway (Aug 22 2022 at 19:17):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
- »divide_simps« would be a quite fitting name, quoth Field.thy: ‹Lemmas
‹divide_simps› move division to the outside and eliminates them on
(in)equalities.›I am currently inclined to pursue the latter option, which would also
suggest to generalize the relevant lemmas to a common ancestor type
class.
The problem is that divide_simps already exists, with the objective of eliminating all occurrences of the division sign in expressions. It is a good deal more effective than field_simps in many situations.
Just to be more explicit: I suggest exactly to re-use the exisiting
divide_simps, because the rules in question are both structurally and by
purpose quite similar to those already gathered there.
Florian
signature.asc
Last updated: Apr 19 2024 at 12:27 UTC