Email Gateway (Aug 18 2022 at 15:54): Email Gateway (Aug 18 2022 at 15:54):From: Peter Lammich <peter.lammich@uni-muenster.de>
Recently, auto left me a goal of the form
f (x+(y+z)) = f ((x+y)+z)
x,y,z :: nat
I always thought the simplifier would rewrite the right sum automatically.
However, when searching for the corresponding theorem, I cannot find it:
find_theorems "_ + (_ + (_::nat)) = _ + _ + _"
searched for:
"_ + (_ + _) = _ + _ + _"
nothing found in 0.111 secs
What's going on here, how is associativity of + on nats implemented?
btw: I now prove this goal by (rule arg_cong, simp) or by adding "intro:
arg_cong" to auto's arguments,
but I would have much more liked to write: "simp add: add_a" or
something like this
Best, Peter
Email Gateway (Aug 18 2022 at 15:54):From: Brian Huffman <brianh@cs.pdx.edu>
On Tue, Aug 31, 2010 at 9:32 AM, Peter Lammich
<peter.lammich@uni-muenster.de> wrote:
Recently, auto left me a goal of the form
f (x+(y+z)) = f ((x+y)+z)
x,y,z :: natI always thought the simplifier would rewrite the right sum automatically.
However, when searching for the corresponding theorem, I cannot find it:find_theorems "_ + (_ + (_::nat)) = _ + _ + _"
searched for:
"_ + (_ + _) = _ + _ + _"
nothing found in 0.111 secs
What's going on here, how is associativity of + on nats implemented?
Hi Peter,
You didn't find the theorem "add_assoc" because it is oriented the other way:
"(x + y) + z = x + (y + z)"
As far as I know, all associativity theorems (for multiplication,
etc.) in the main libraries are oriented like this.
btw: I now prove this goal by (rule arg_cong, simp) or by adding "intro:
arg_cong" to auto's arguments,
but I would have much more liked to write: "simp add: add_a" or something
Try "simp add: add_ac", which will rewrite additions to a normal form,
with terms in sorted order and additions grouped to the right.
Email Gateway (Aug 18 2022 at 15:55):From: Tobias Nipkow <nipkow@in.tum.de>
Peter Lammich schrieb:
Recently, auto left me a goal of the form
f (x+(y+z)) = f ((x+y)+z)
x,y,z :: natI always thought the simplifier would rewrite the right sum automatically.
No, it does not normalize with associativity or communtativity
automatically.
However, when searching for the corresponding theorem, I cannot find it:
find_theorems "_ + (_ + (_::nat)) = _ + _ + _"
searched for:
"_ + (_ + _) = _ + _ + _"
nothing found in 0.111 secs
Associativity happens to be oriented the other way around:
searched for:
"_ + _ + _ = _ + (_ + _)"
found 1 theorem(s) in 0.080 secs:
Nat.nat_add_assoc: ?m + ?n + ?k = ?m + (?n + ?k)
What's going on here, how is associativity of + on nats implemented?
btw: I now prove this goal by (rule arg_cong, simp) or by adding "intro:
arg_cong" to auto's arguments,
but I would have much more liked to write: "simp add: add_a" or
something like this
In such situations do
(simp add: algebra_simps)
The list algebra_simps contains all simp rules like AC that are not
included by default and covers many algebraic structures.
Tobias
Best, Peter
Last updated: Apr 25 2024 at 16:19 UTC