Lean has trouble understanding intuitive sums (again)

Stream: new members

[Hanting Zhang]

I'm once again stuck on a terrible sum that should be obvious, but turns out to be frustratingly hard for Lean to understand:

import tactic
import data.mv_polynomial.rename
import data.mv_polynomial.comm_ring

noncomputable theory

open finset
open_locale big_operators

namespace mv_polynomial

variables (σ : Type*) (R : Type*) {τ : Type*} {S : Type*}
variables [comm_semiring R] [comm_semiring S] [fintype σ] [fintype τ]

def esymm (n : ℕ) : mv_polynomial σ R :=
∑ t in powerset_len n univ, ∏ i in t, X i

/-- A second definition of `esymm σ R n` with range over a subtype instead of `powerset_len`.
  Sometimes it's easier to reason with subtypes. -/
lemma esymm₂ (n : ℕ) : (esymm σ R n) =
  ∑ t : {s : finset σ // s.card = n}, ∏ i in (t : finset σ), X i :=
begin
  sorry
end

end mv_polynomial

I'm trying to convert the sum over powerset_len n univ to a sum over {s : finset σ // s.card = n}. Both literally count the subsets of σ that have cardinality n. But the first is a finset of finset σ and the second is a subtype σ. I've tried using congr, attach, etc, but it's just a mess. Is there a good way to do this?

[Hanting Zhang]

@Johan Commelin Do you think it's a good idea to use powerset_len? I've been using it because I'm stubborn and my original Vieta code uses it, but now I'm thinking it might not be worth it. Is there any preference for reasoning with subtypes in mathlib?

[Adam Topaz]

Maybe docs#finset.sum_bij or docs#finset.sum_bij' would help?

[Hanting Zhang]

Somehow I've missed these. D: Thanks!

[Hanting Zhang]

I'vee made some progress, but I've gotten stuck again ):
I need help reasoning with the big i function:

import tactic
import data.mv_polynomial.rename
import data.mv_polynomial.comm_ring

noncomputable theory

open finset
open_locale big_operators

namespace mv_polynomial

variables (σ : Type*) (R : Type*) {τ : Type*} {S : Type*}
variables [comm_semiring R] [comm_semiring S] [fintype σ] [fintype τ]

def esymm (n : ℕ) : mv_polynomial σ R :=
∑ t in powerset_len n univ, ∏ i in t, X i

/-- A second definition of `esymm σ R n` with range over a subtype instead of `powerset_len`.
  Sometimes it's easier to reason with subtypes. -/
lemma esymm₂ (n : ℕ) : (esymm σ R n) =
  ∑ t : {s : finset σ // s.card = n}, ∏ i in (t : finset σ), X i :=
begin
  rw esymm,
  have i : Π (a : finset σ), a ∈ powerset_len n univ → {s : finset σ // s.card = n} :=
  by {intros a ha, split, exact (mem_powerset_len.mp ha).2, apply_instance },
  apply sum_bij i,
  { intros, simp, },
  { intros,
    apply prod_congr,
    ext, split,
    { intro h,
      sorry },
    { intro h,
      sorry },
    intros, refl,},
  { intros,

    sorry },
  { intros, sorry },
end

end mv_polynomial

Maybe it's because I've been staring at it for too long, but how can I unwrap a_1 ∈ ↑(i a ha) at the first sorry? I want to change the membership statement into a logical one.

[Alex J. Best]

I'm not quite sure whats you are proving here but i is some function which constructs data right, so possibly the problem is that you want to remember the definition of i by using let i rather than have i? When you do that the first sorry is

      dsimp [i], --actually you don't even need this line
      exact h,

[Alex J. Best]

A small example of the difference is:

example : ∃ n, n = 2 :=
begin
  have i := 2,
  use i,
end

and you are left with an unprovable goal. But if you use let instead of have you get a proof.

[Hanting Zhang]

:fear: Oh... I didn't even know there was a difference.

[Alex J. Best]

Have forgets the term used whereas let doesn't, so for propositions have is more natural, in lean all proofs of the same proposition are equal so it doesn't matter what the original one was. But for things which are "data" like natural numbers, finsets, functions, you want to remember what their definition was mostly, so let is what you need.

[Hanting Zhang]

Thanks! :tada: