Alternating sum over powerset and decidable instances

Stream: Is there code for X?

[Sophie Morel]

Hi, this is a combination "Is there code for X?/aaaaaah what did I do wrong" message. It all started when I wondered whether the calculation of the sum of the (-1)^{card t} over the powerset of a finset was in mathlib. So something like that:

lemma alternating_sum_powerset (s : finset α) :
finset.sum (finset.powerset s) (λ (t : finset α), (-1 : int)^(t.card)) =
ite (s = ∅) 1 0

Experienced Lean people will probably already sense trouble, because I am using ite on a Prop that has no reason to be decidable. But I have a local attribute [instance] classical.prop_decidable at the beginning of every file so I did not notice.

My first question is: is there something like that in mathlib ?

I did a quick search, didn't find it and decided to try and prove it. Here is my MWE:

import data.finset.powerset
import algebra.big_operators.basic
import algebra.big_operators.ring
import data.nat.choose.sum

local attribute [instance] classical.prop_decidable

variables {α : Type*}

lemma alternating_sum_powerset_aux (s : finset α) (j : ℕ) :
(finset.powerset_len j s).sum (λ (t : finset α), (-1 : int) ^ t.card) = (-1 : int)^j *
(s.card.choose j) :=
begin
  rw @finset.sum_congr _ _ (finset.powerset_len j s) (finset.powerset_len j s)
    (λ t, (-1 : int)^(t.card)) (λ t, (-1 : int)^j) _ (refl _) _,
    {rw finset.sum_const,
    rw finset.card_powerset_len,
    simp only [nsmul_eq_mul],
    rw mul_comm,
    },
    intro x,
    simp only,
    intro hx,
    rw finset.mem_powerset_len at hx,
    rw hx.2,
end


lemma alternating_sum_powerset (s : finset α) :
finset.sum (finset.powerset s) (λ (t : finset α), (-1 : int)^(t.card)) =
ite (s = ∅) 1 0 :=
begin
  rw finset.sum_powerset,
  rw @finset.sum_congr _ _ (finset.range (s.card+1)) (finset.range (s.card+1))
    (λ (m : ℕ), (finset.powerset_len m s).sum (λ (t : finset α), (-1 : int) ^ t.card))
    (λ (m : ℕ), (-1 : int)^m*(s.card.choose m)) _ (refl _) _,
    {rw ←finset.card_eq_zero,
    exact @int.alternating_sum_range_choose s.card,  ---- oh no ! :-((((
    },
    exact λ m hm, alternating_sum_powerset_aux s m,
end

And here is the beautiful error message that I got:

invalid type ascription, term has type
  (finset.range (s.card + 1)).sum (λ (m : ℕ), (-1) ^ m * ↑(s.card.choose m)) =
    @ite ℤ (s.card = 0) (nat.decidable_eq s.card 0) 1 0
but is expected to have type
  (finset.range (s.card + 1)).sum (λ (m : ℕ), (-1) ^ m * ↑(s.card.choose m)) =
    @ite ℤ (s.card = 0) (classical.prop_decidable (s.card = 0)) 1 0

My interpretation of it is: ite expects its Prop to be decidable. In the statement of my lemma, (s = ∅) was decidable because I told Lean at the beginning that every Prop should be decidable; this reason carried over when I did the rw to make the Prop equal to (s.card=0). But in the lemma that I was trying to use, the argument of ite is decidable because it is an equality between natural numbers, and there is an instance telling Lean that this is always decidable. So exact failed because the two Props in the ite were decidable for different reasons. At this point I threw my computer out of the window.

Okay, so assuming this interpretation is correct, is there any elegant way to get out of this one ? What I did in real life was get rid of the ite by cutting my lemma into two sublemmas, one for a nonempty finset and one for the empty finset; this feels somewhat unsatisfying so I wonder if there was a better way.

[Yaël Dillies]

What happens if you replace your local attribute by open_locale classical at the top of the file?

[Yaël Dillies]

They both mean (roughly) the same thing, except that the latter gives the classical instances lower priority to avoid the kind of pickle that you're finding yourself in.

[Sophie Morel]

Then the rw on the previous line fails, with the message:

rewrite tactic failed, motive is not type correct
  λ (_a : Prop),
    (finset.range (s.card + 1)).sum (λ (m : ℕ), (-1) ^ m * ↑(s.card.choose m)) = ite (s = ∅) 1 0 =
      ((finset.range (s.card + 1)).sum (λ (m : ℕ), (-1) ^ m * ↑(s.card.choose m)) = ite _a 1 0)

[Yaël Dillies]

What if you make it a simp_rw instead?

[Sophie Morel]

And this time I cannot make any sense of the error message. :-(

[Sophie Morel]

Now it works ! Woohoo !

[Sophie Morel]

I did not know about this simp_rw tactic, I will add it to my list. I've had a lot of trouble with rw lately and the error messages were unhelpful (motive is not type correct followed by long jumbles I could not understand), so maybe it will help there too. Thanks so much !

[Sophie Morel]

Do you know if the lemma is in mathlib already ?

[Yaël Dillies]

Long story short, these decidability issues are annoying but usually easily worked around. I say "easily" because it's often enough to turn a rw into a simp_rw, force unification of a proof term using convert or congr. And I say "usually" because I myself hit a case yesterday where the aforementioned tricks don't work :frown:.

[Yaël Dillies]

Yeah, "motive is not type correct" => use simp_rw. The reason behind this is that rewriting is the same as applying eq.rec with a suitable "motive" (understand, the argument to eq.rec). rw has some way of calculating what the motive should be, but it sometimes gets it wrong. simp_rw follows a more aggressive strategy and tends to succeed more often than rw.

[Sophie Morel]

Thank you also for mentioning convert, another tactic I did not know about but that will be immediately useful.

[Yaël Dillies]

Your lemma isn't in mathlib, but it's an easy corollary of an existing lemma. I have bad i
connection at the moment so I shall guess docs#finset.prod_add.

[Mauricio Collares]

docs#finset.sum_pow_mul_eq_add_pow for a more specialised version maybe?

[Sophie Morel]

Yes, both lemmas would imply my result pretty quickly. Thanks to both of you !

[Sophie Morel]

Well I'm really glad I asked that question, even though I had found a way around it. I just ran into a similar issue in a much more complicated situation (no MWE sorry, it would take a lot of time to extract one) where the problem was different instances of decidability but Lean didn't even tell me; I just had a rw that refused to work for unclear reasons. Thanks to this discussion I was able to figure it out, and open_locale classical (no simp_rw needed this time) solved the problem. Whew !

[Eric Wieser]

Sophie Morel said:

Experienced Lean people will probably already sense trouble, because I am using ite on a Prop that has no reason to be decidable.

Actually, it is always possible to decide if a finset is empty; we just don't have the instance because it causes diamonds

[Eric Wieser]

(the algorithm is just check whether S.card = 0)