CODEWITHSUNDEEP
isabelle
user1868607
user1868607

Reputation: 2600

Reindexing sums in Isabelle

I'm trying to translate the argument I gave in this answer into Isabelle and I managed to prove it almost completely. However, I still need to prove:

"(∑k | k ∈ {1..n} ∧ d dvd k. f (k/n)) =
        (∑q | q ∈ {1..n/d}. f (q/(n/d)))" for d :: nat

My idea was to use this theorem:

sum.reindex_bij_witness

however, I cannot instantiate the transformations i,j that relate the sets S,T of the theorem. In principle, the setting should be:

S = {k. k ∈ {1..n} ∧ d dvd k}
T = {q. q ∈ {1..n/d}}
i k = k/d
j q = q d

I believe there is a typing error. Perhaps I should be using div?

Upvotes: 0

Views: 151

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8248

First of all, note that instead of gcd a b = 1, you should write coprime a b. That is equivalent (at least for all types that have a GCD), but it is more convenient to use.

Second, I would not write assumptions like ⋀n. F n = …. It makes more sense to write that as a defines, i.e.

lemma
  fixes F :: "nat ⇒ complex"
  defines "F ≡ (λn. …)"

Third, {q. q ∈ {1..n/d}} is exactly the same as {1..n/d}, so I suggest you write it that way.

To answer your actual question: If what you have written in your question is how you wrote it in Isabelle and n and d are of type nat, you should be aware that {q. q ∈ {1..n/d}} actually means {1..real n / real d}. If n / d > 1, this is actually an infinite set of real numbers and probably not what you want.

What you actually want is probably the set {1..n div d} where div denotes division on natural numbers. This is then a finite set of natural numbers.

Then you can prove the following fairly easily:

lemma
  fixes f :: "real ⇒ complex" and n d :: nat
  assumes "d > 0" "d dvd n"
  shows "(∑k | k ∈ {1..n} ∧ d dvd k. f (k/n)) =
           (∑q∈{1..n div d}. f (q/(n/d)))"
  by (rule sum.reindex_bij_witness[of _ "λk. k * d" "λk. k div d"])
     (use assms in ‹force simp: div_le_mono›)+

A note on div

div and / denote the same function, namely Rings.divide.divide. However, / for historic reasons (and perhaps in fond memory of Pascal), / additionally imposes the type class restriction inverse, i.e. it only works on types that have an inverse function.

In most practical cases, this means that div is a general kind of division operation on rings, whereas / only works in fields (or division rings, or things that are ‘almost’ fields like formal power series).

If you write a / b for natural numbers a and b, this is therefore a type error. The coercion system of Isabelle then infers that you probably meant to write real a / real b and that's what you get.

It's a good idea to look at the output in such cases to ensure that the inferred coercions match what you intended.

Debugging non-matching rules

If you apply some rule (e.g. with apply (rule …)) and it fails and you don't understand why, there is a little trick to find out. If you add a using [[unify_trace_failure]] before the apply, you get an error message that indicates where exactly the unification failed. In this case, the message is

The following types do not unify:
(nat ⇒ complex) ⇒ nat set ⇒ complex
(real ⇒ complex) ⇒ real set ⇒ complex

This indicates that there is a summation over a set of reals somewhere that should be a summation over a set of naturals.

Upvotes: 2

Related Questions