Zulip Chat Archive

Stream: new members

Topic: Lean has trouble understanding intuitive sums (again)


view this post on Zulip Hanting Zhang (Jan 17 2021 at 00:10):

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?

view this post on Zulip Hanting Zhang (Jan 17 2021 at 00:16):

@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?

view this post on Zulip Adam Topaz (Jan 17 2021 at 00:17):

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

view this post on Zulip Hanting Zhang (Jan 17 2021 at 00:22):

Somehow I've missed these. D: Thanks!

view this post on Zulip Hanting Zhang (Jan 17 2021 at 01:52):

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.

view this post on Zulip Alex J. Best (Jan 17 2021 at 01:59):

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,

view this post on Zulip Alex J. Best (Jan 17 2021 at 02:02):

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.

view this post on Zulip Hanting Zhang (Jan 17 2021 at 02:03):

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

view this post on Zulip Alex J. Best (Jan 17 2021 at 02:05):

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.

view this post on Zulip Hanting Zhang (Jan 17 2021 at 02:44):

Thanks! :tada:


Last updated: May 06 2021 at 22:13 UTC