Re: [isabelle] Cancellation lemmas for setprod and setsum



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?

On 13/08/12 14:04, Tobias Nipkow wrote:
> 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
>>>






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.