[isabelle-dev] Numeral simplification: neg and iszero
Quoting Tobias Nipkow nipkow at in.tum.de:
They have been on my get-rid-of list for some time, but when I initially
tried, I noticed they were needed for doing arithmetic. Now that
somebody (Florian?) added less_int_code, it may indeed be a simple job.
Go for it!
Tobias
I figured I should give a progress report on my efforts to get rid of
iszero and neg.
For simplification of inequalities of numerals in class
{number_ring,ordered_idom}, getting rid of neg was indeed simple. The
old rules were
less_number_of_eq_neg: number_of x number_of y -- neg (number_of
(x + - y))
le_number_of_eq: number_of x = number_of y -- ~ neg (number_of (y + - x))
The new rules are
less_number_of: number_of x number_of y -- x y
le_number_of: number_of x = number_of y -- x = y
Fortunately, the new rules hold in the same class
{number_ring,ordered_idom} as the old ones. The same is not true for
testing equality, however. The original rule is
eq_number_of_eq:
(number_of x::'a::number_ring) = number_of y -- iszero (number_of
(x + - y)::'a)
I wanted to replace this with
eq_number_of:
(number_of x::'a::{number_ring,ring_char_0}) = number_of y -- x = y
But as you can see, eq_number_of has an additional class constraint
requiring that of_int be injective, while eq_number_of_eq works in any
number ring. Since the iszero function is polymorphic, this lets us
solve numeral equalities on, for example, word types (where of_int is
not injective) by defining special simp rules for iszero at those
types. Even without any additional simp rules, eq_number_of_eq can be
used to prove inequalities like -1 ~= 0 or 5 ~= 6 at any number_ring
instance (since 1 is required to be nonzero in every unital ring). Any
replacement for eq_number_of_eq must still be able to solve such
subgoals.
I did try modifying eq_number_of_eq to use subtraction, replacing (x +
- y) with (x - y). But subtraction on the binary representation causes
another problem: We would like to rewrite (Int.Min - Int.Min) to
Int.Pls, but the simplifier rewrites this to (0::int) instead, leaving
us with ill-formed terms like number_of (Int.Bit0 (0::int)). For
these reasons, I have left eq_number_of_eq in its original form, and
iszero will stay (at least for now).
I do think that we can get rid of neg. The other place where neg
was used a lot was in NatBin.thy, for simplifying binary arithmetic at
type nat. I replaced many occurrences of neg (number_of v::int) with
v Int.Pls; I also simplified more awkward constructions like neg
(number_of (- v)) to Int.Pls v, and neg (number_of v::int) |
iszero (number_of v::int) to v = Int.Pls.
NatBin.thy is now nearly neg-free, but there are still some other
places with lemmas that use neg. For example,
Tools/ComputeNumeral.thy seems to be a complete re-implementation of
the simpset defined in NatBin.thy for arithmetic at type nat. If such
other lemmas involving neg can be made redundant, or merged into
NatBin.thy, then we will be able to remove neg.
- Brian
[isabelle-dev] Numeral simplification: neg and iszero
NatBin.thy is now nearly neg-free, but there are still some other places with lemmas that use neg. For example, Tools/ ComputeNumeral.thy seems to be a complete re-implementation of the simpset defined in NatBin.thy for arithmetic at type nat. If such other lemmas involving neg can be made redundant, or merged into NatBin.thy, then we will be able to remove neg. The rules in Tools/ComputeNumeral.thy are used within ML code for the HOL computing oracle. It's true, they are basically a cleaned up version of the NatBin.thy rules; simplification with these rules is supposed to work together with the oracle, not necessarily with the simplifier. Changes here might break my part of the proof of the Kepler Conjecture; but chances are it does not run with the current version of Isabelle anyway :-) Steven
[isabelle-dev] Numeral simplification: neg and iszero
When I introduced these constants, they were certainly necessary.
Then, binary arithmetic executed by pure rewriting. I don't object to
getting rid of them if they are now unnecessary. But it hardly seems
worth investing a significant effort. They don't cause a problem, do
they? It may be best to leave well enough alone.
Larry
On 9 Dec 2008, at 16:40, Brian Huffman wrote:
I figured I should give a progress report on my efforts to get rid
of iszero and neg.
For simplification of inequalities of numerals in class
{number_ring,ordered_idom}, getting rid of neg was indeed simple.
The old rules were
less_number_of_eq_neg: number_of x number_of y -- neg
(number_of (x + - y))
le_number_of_eq: number_of x = number_of y -- ~ neg (number_of
(y + - x))
The new rules are
less_number_of: number_of x number_of y -- x y
le_number_of: number_of x = number_of y -- x = y
Fortunately, the new rules hold in the same class
{number_ring,ordered_idom} as the old ones. The same is not true for
testing equality, however. The original rule is
eq_number_of_eq:
(number_of x::'a::number_ring) = number_of y -- iszero (number_of
(x + - y)::'a)
I wanted to replace this with
eq_number_of:
(number_of x::'a::{number_ring,ring_char_0}) = number_of y -- x =
y
But as you can see, eq_number_of has an additional class constraint
requiring that of_int be injective, while eq_number_of_eq works in
any number ring. Since the iszero function is polymorphic, this lets
us solve numeral equalities on, for example, word types (where
of_int is not injective) by defining special simp rules for iszero
at those types. Even without any additional simp rules,
eq_number_of_eq can be used to prove inequalities like -1 ~= 0 or 5
~= 6 at any number_ring instance (since 1 is required to be nonzero
in every unital ring). Any replacement for eq_number_of_eq must
still be able to solve such subgoals.
I did try modifying eq_number_of_eq to use subtraction, replacing (x
+ - y) with (x - y). But subtraction on the binary representation
causes another problem: We would like to rewrite (Int.Min - Int.Min)
to Int.Pls, but the simplifier rewrites this to (0::int) instead,
leaving us with ill-formed terms like number_of (Int.Bit0
(0::int)). For these reasons, I have left eq_number_of_eq in its
original form, and iszero will stay (at least for now).
I do think that we can get rid of neg. The other place where neg
was used a lot was in NatBin.thy, for simplifying binary arithmetic
at type nat. I replaced many occurrences of neg (number_of v::int)
with v Int.Pls; I also simplified more awkward constructions
like neg (number_of (- v)) to Int.Pls v, and neg (number_of
v::int) | iszero (number_of v::int) to v = Int.Pls.
NatBin.thy is now nearly neg-free, but there are still some other
places with lemmas that use neg. For example, Tools/
ComputeNumeral.thy seems to be a complete re-implementation of the
simpset defined in NatBin.thy for arithmetic at type nat. If such
other lemmas involving neg can be made redundant, or merged into
NatBin.thy, then we will be able to remove neg.
[isabelle-dev] Numeral simplification: neg and iszero
I would agree that changing simp rules to avoid using neg is not a huge improvement in and of itself. At best, it can reduce the number of rewrite steps needed to solve some arithmetic subgoals. However, speeding up simplification was not my primary goal. I share the opinion of Makarius that we would be much better off with numerals based on the natural numbers, rather than the integers. This would let us have a nice, clean way of doing arithmetic on arbitrary semirings - the ad-hoc, ugly, and inefficient rewrite rules in NatBin would no longer be needed. I think that the transition to nat-based numerals will be facilitated by cleaning up the simplification rules for arithmetic, and removing any unnecessary uses of subtraction (e.g. less_number_of_eq_neg and friends). - Brian Quoting Lawrence Paulson lp15 at cam.ac.uk: When I introduced these constants, they were certainly necessary. Then, binary arithmetic executed by pure rewriting. I don't object to getting rid of them if they are now unnecessary. But it hardly seems worth investing a significant effort. They don't cause a problem, do they? It may be best to leave well enough alone. Larry
[isabelle-dev] Numeral simplification: neg and iszero
They have been on my get-rid-of list for some time, but when I initially tried, I noticed they were needed for doing arithmetic. Now that somebody (Florian?) added less_int_code, it may indeed be a simple job. Go for it! Tobias Brian Huffman schrieb: Is there any good reason why the constants neg and iszero (defined in Int.thy) are needed anymore? Currently they are used to simplify (in)equalities on numerals; for example, number_of x number_of y rewrites to neg (x + - y). However, Int.thy also provides separate sets of rules like this: lemma less_int_code [code]: Int.Pls Int.Pls \longleftrightarrow False Int.Pls Int.Min \longleftrightarrow False Int.Pls Int.Bit0 k \longleftrightarrow Int.Pls k Int.Pls Int.Bit1 k \longleftrightarrow Int.Pls \le k Int.Min Int.Pls \longleftrightarrow True Int.Min Int.Min \longleftrightarrow False Int.Min Int.Bit0 k \longleftrightarrow Int.Min k Int.Min Int.Bit1 k \longleftrightarrow Int.Min k Int.Bit0 k Int.Pls \longleftrightarrow k Int.Pls Int.Bit1 k Int.Pls \longleftrightarrow k Int.Pls Int.Bit0 k Int.Min \longleftrightarrow k \le Int.Min Int.Bit1 k Int.Min \longleftrightarrow k Int.Min Int.Bit0 k1 Int.Bit0 k2 \longleftrightarrow k1 k2 Int.Bit0 k1 Int.Bit1 k2 \longleftrightarrow k1 \le k2 Int.Bit1 k1 Int.Bit0 k2 \longleftrightarrow k1 k2 Int.Bit1 k1 Int.Bit1 k2 \longleftrightarrow k1 k2 These are declared with the [code] attribute; wouldn't they also work just as well as simp rules? It seems that the old rewrite strategy using neg and iszero was designed to minimize the total number of rewrite rules in the simp set; I'm not sure whether this was done for performance reasons, or just for the fact that it was easier to implement, because there were fewer lemmas to prove. I would propose that we change the simplification strategy for (in)equalities on numerals to use the code lemmas instead, and completely get rid of neg and iszero. I think the code lemmas are cleaner and easier to understand, and they will also make the transition to unsigned numerals easier (since we no longer need to rely on subtraction to do comparisons). - Brian ___ Isabelle-dev mailing list Isabelle-dev at mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Numeral simplification: neg and iszero
Hi Brian, Is there any good reason why the constants neg and iszero (defined in Int.thy) are needed anymore? if there is a chance to get rid of those, go ahead and try. Perhaps they play a role for numerals and natural numbers, but this is just a suspicion. Cheers Florian -- Home: http://wwwbroy.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de -- next part -- A non-text attachment was scrubbed... Name: signature.asc Type: application/pgp-signature Size: 252 bytes Desc: OpenPGP digital signature URL: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20081203/850e8800/attachment.pgp
[isabelle-dev] Numeral simplification: neg and iszero
Is there any good reason why the constants neg and iszero (defined in Int.thy) are needed anymore? Currently they are used to simplify (in)equalities on numerals; for example, number_of x number_of y rewrites to neg (x + - y). However, Int.thy also provides separate sets of rules like this: lemma less_int_code [code]: Int.Pls Int.Pls \longleftrightarrow False Int.Pls Int.Min \longleftrightarrow False Int.Pls Int.Bit0 k \longleftrightarrow Int.Pls k Int.Pls Int.Bit1 k \longleftrightarrow Int.Pls \le k Int.Min Int.Pls \longleftrightarrow True Int.Min Int.Min \longleftrightarrow False Int.Min Int.Bit0 k \longleftrightarrow Int.Min k Int.Min Int.Bit1 k \longleftrightarrow Int.Min k Int.Bit0 k Int.Pls \longleftrightarrow k Int.Pls Int.Bit1 k Int.Pls \longleftrightarrow k Int.Pls Int.Bit0 k Int.Min \longleftrightarrow k \le Int.Min Int.Bit1 k Int.Min \longleftrightarrow k Int.Min Int.Bit0 k1 Int.Bit0 k2 \longleftrightarrow k1 k2 Int.Bit0 k1 Int.Bit1 k2 \longleftrightarrow k1 \le k2 Int.Bit1 k1 Int.Bit0 k2 \longleftrightarrow k1 k2 Int.Bit1 k1 Int.Bit1 k2 \longleftrightarrow k1 k2 These are declared with the [code] attribute; wouldn't they also work just as well as simp rules? It seems that the old rewrite strategy using neg and iszero was designed to minimize the total number of rewrite rules in the simp set; I'm not sure whether this was done for performance reasons, or just for the fact that it was easier to implement, because there were fewer lemmas to prove. I would propose that we change the simplification strategy for (in)equalities on numerals to use the code lemmas instead, and completely get rid of neg and iszero. I think the code lemmas are cleaner and easier to understand, and they will also make the transition to unsigned numerals easier (since we no longer need to rely on subtraction to do comparisons). - Brian
