Email Gateway (Aug 19 2022 at 08:17): Email Gateway (Aug 19 2022 at 08:17):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I recently needed something like a "cancellation lemma" for setprod but
was unable to find anyting like it in the libraries.
The lemma I needed and proved was the following:
lemma setprod_cancel: fixes A::"nat set" and B::"nat set"
assumes "B ⊆ A" and "finite A" and "0 ∉ B" shows "∏A / ∏B = ∏(A-B)"
Is there a lemma like this somewhere? If yes, what is it called? If not,
it might be a good idea to add this (or a generalised version of this)
and a version for setsum to the libraries, since it seems like something
one needs quite often when dealing with products and sums.
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 08:17):From: Lars Noschinski <noschinl@in.tum.de>
Did you mean "div" instead of "/" or do you an implicit conversion to
real in there?
Is there a lemma like this somewhere? If yes, what is it called? If not,
it might be a good idea to add this (or a generalised version of this)
and a version for setsum to the libraries, since it seems like something
one needs quite often when dealing with products and sums.
For sums, there is setsum_diff. For products, there is the question what
the type class of the base type of A,B should be -- probably would need
to be a field, to be useful (which then excludes the naturals).
Maybe one could generically prove "∏A = ∏(A-B) * ∏B" and derive your
variant from there for specific types.
-- Lars
Email Gateway (Aug 19 2022 at 08:18):From: Tobias Nipkow <nipkow@in.tum.de>
I agree that this looks like the right approach. Your suggested lemma in
(generalized form) is a direct consequence of setprod_Un_disjoint:
[| finite A; finite B; A Int B = {} |]
==> setprod f (A Un B) = setprod f A * setprod f B
because A-B and B are disjoint.
Tobias
Email Gateway (Aug 19 2022 at 08:18):From: Manuel Eberl <eberlm@in.tum.de>
(Replied directly at first instead of to the list, sorry about that)
No, I really meant /. I have coercions from nat to real in there. But
yes, the generalisation you proposed seems like a good idea, that should
work for any abelian semigroup with multiplication, I think. (as long as
the underlying lemmas for setprod are that general as well)
I was just very surprised that something like this didn't exist already.
Who is responsible for maintaining these libraries, i.e. whom do I have
to contact if I have a lemma that I think should be included in the library?
Email Gateway (Aug 19 2022 at 08:18):From: Tobias Nipkow <nipkow@in.tum.de>
Am 13/08/2012 12:51, schrieb Manuel Eberl:
(Replied directly at first instead of to the list, sorry about that)
No, I really meant /. I have coercions from nat to real in there. But
yes, the generalisation you proposed seems like a good idea, that should
work for any abelian semigroup with multiplication, I think. (as long as
the underlying lemmas for setprod are that general as well)I was just very surprised that something like this didn't exist already.
Who is responsible for maintaining these libraries, i.e. whom do I have
to contact if I have a lemma that I think should be included in the library?
You can try to send it to one of the people who created the theory. Which would
be me in this case.
Tobias
On 13/08/12 11:44, Lars Noschinski wrote:
On 12.08.2012 23:59, Manuel Eberl wrote:
Hallo,
I recently needed something like a "cancellation lemma" for setprod but
was unable to find anyting like it in the libraries.The lemma I needed and proved was the following:
lemma setprod_cancel: fixes A::"nat set" and B::"nat set"
assumes "B ⊆ A" and "finite A" and "0 ∉ B" shows "∏A / ∏B = ∏(A-B)"Did you mean "div" instead of "/" or do you an implicit conversion to
real in there?Is there a lemma like this somewhere? If yes, what is it called? If
not,
it might be a good idea to add this (or a generalised version of this)
and a version for setsum to the libraries, since it seems like
something
one needs quite often when dealing with products and sums.For sums, there is setsum_diff. For products, there is the question
what the type class of the base type of A,B should be -- probably
would need to be a field, to be useful (which then excludes the
naturals).Maybe one could generically prove "∏A = ∏(A-B) * ∏B" and derive your
variant from there for specific types.-- Lars
Email Gateway (Aug 19 2022 at 08:18):From: Manuel Eberl <eberlm@in.tum.de>
It can indeed be proven for comm_monoid_mult in a rather straightforward
fashion:
lemma setprod_diff: "⟦B ⊆ A; finite A⟧ ⟹
setprod f A = setprod f (A - B) * setprod f B"
by (subgoal_tac "A - B ∪ B = A", subst setprod_Un_disjoint[symmetric],
auto intro: finite_subset)
And the corresponding cancellation lemmas for products over nat, int and
real. I was unable to prove a general version of this with arbitrary
types because the correctness lemmas for the real type coercion seem to
be only available for specific types such as nat and int. (note the
implicit coercion to real)
lemma setprod_cancel_nat: fixes f::"'a ⇒ nat"
assumes "B ⊆ A" and "finite A" and "∀x∈B. f x ≠ 0"
shows "setprod f A / setprod f B = setprod f (A - B)" (is "?A / ?B =
?C")
proof-
from setprod_diff[OF assms(1,2)] have "?A = ?C * ?B" by auto
moreover have "?B ≠ 0" using assms by (simp add: finite_subset)
ultimately show ?thesis by simp
qed
(and similarly for int and real)
To be more precise, if I tried to prove this for arbitrary types with
some sort constraint, i.e. 'b::comm_monoid_mult, I always got stuck at
some subgoal like "real (a * b) = real a * real b" which seemed to be
unprovable. Do I really have to write three separate lemmas for nat, int
and real or is there a way to do this once for arbitrary types?
Last updated: Apr 24 2024 at 16:18 UTC