Hello! I want to convert this from N to Z!

Stream: new members

[Jasin Jiang]

I am a newbie in Lean4 and I want to solve this problem. Can someone helps me?

(n m r : ℕ) : ∑ k in Finset.Ico 0 (n + 1), choose k m * choose (n - k) r =
  ∑ k in Finset.Ico (0:ℤ) (n + 1), Ring.choose k m  * Ring.choose (n - k) r := by

[Martin Dvořák]

Please copy the entire header. We cannot compile it.

[Jasin Jiang]

This is my code and my task is to prove idt_77 which needs to prove the idt_61_int.
my idea is to prove idt_61_equal first which is my question

import Mathlib
open Finset Nat BigOperators Set


theorem idt_61 (n m r : ℕ) :
    ∑ k in Finset.range (n + 1), (choose k m) * (choose (n - k) r) = choose (n + 1) (m + r + 1) := by sorry


theorem idt_61_int (n m r : ℕ) : ∑ k in Finset.Ico (0:ℤ) (n + 1), Ring.choose k m  * Ring.choose (n-k) r  = (n+1).choose (m + r + 1)  := by
  sorry

theorem idt_61_equal
  (n m r : ℕ) : ∑ k in Finset.Ico 0 (n + 1), choose k m * choose (n - k) r =
  ∑ k in Finset.Ico (0:ℤ) (n + 1), Ring.choose k m  * Ring.choose (n - k) r := by
  sorry

theorem idt_77 (n m r s : ℕ) : ∑ k in Finset.Ico (-m : ℤ) (n + 1), Ring.choose (m + k) r * Ring.choose (n - k) s = choose (m + n + 1) (r + s + 1) := by
  have h₁ : ∑ k in Finset.Ico (-m : ℤ) (n + 1), Ring.choose (m + k) r * Ring.choose (n - k) s
          = ∑ k in Finset.Ico (0:ℤ) (n + m + 1), Ring.choose k r  * Ring.choose (n + m - k) s := by
    let g := λ k => k + (m:ℤ)

    have hg_inj : ∀ x ∈ Finset.Ico (-m:ℤ) (n+1), ∀ y ∈ Finset.Ico (-m:ℤ) (n+1), g x = g y → x = y := by
      intro x
      intro hx
      intro y
      intro hy
      intro hxy
      unfold g at hxy
      rw [add_left_inj] at hxy
      exact hxy
    have : (Finset.Ico (-m:ℤ) (n+1)).image g = Finset.Ico (0:ℤ) (n+m+1) := by
      ext x
      simp only [Finset.mem_image, Finset.mem_Ico]
      constructor
      · rintro ⟨y, hy, rfl⟩
        unfold g
        have h11: 0 ≤ y + (m:ℤ) := by linarith
        have h12: y + (m:ℤ) < n + m + 1 := by linarith
        exact ⟨h11, h12⟩
      · intro hasDerivAt_exp
        unfold g
        let y := x - (m:ℤ)
        have h11: -(m:ℤ) ≤ y := by unfold y; linarith
        have h12: y < n + 1 := by unfold y; linarith
        use y
        constructor
        . exact ⟨h11, h12⟩
        . unfold y
          simp

    rw [←this]
    rw [Finset.sum_image hg_inj]
    unfold g
    simp
    apply sum_congr rfl
    intro k hk
    congr 2
    rw [add_comm]

  rw [h₁]
  rw [←cast_add]
  rw [idt_61_int (n + m) r s]
  ring_nf

[Martin Dvořák]

#mwe

import Mathlib

example (k m : ℕ) : Nat.choose k m = (Ring.choose k m : ℤ) :=
  (Ring.choose_natCast k m).symm

[Jasin Jiang]

It seems that I can't use it because there is a summation function outside the binomial coefficient. Then, on the right side, the k in the summation function is an integer, while on the left side, it is a natural number. I want to make these two equal.

[Jasin Jiang]

It seems that I can't use it because there is a summation function outside the binomial coefficient. Then, on the right side, the k in the summation function is an integer, while on the left side, it is a natural number. I want to make these two equal.

[Martin Dvořák]

Maybe something like

import Mathlib
open Finset Nat BigOperators Set

theorem idt_61_equal (n m r : ℕ) :
    ∑ k in Finset.Ico 0 (n + 1), choose k m * choose (n - k) r =
    ∑ k in Finset.Ico (0:ℤ) (n + 1), Ring.choose k m  * Ring.choose (n - k) r := by
  zify
  simp_rw [← Ring.choose_natCast]
  apply sum_bij

will work. Should I try to finish it?

[Jasin Jiang]

wait me for a while.I will be soon back home and test it. btw ， thank you so much

[Jasin Jiang]

image.png
hello，I've tried this code and found I will prove 4 situations which maybe hard for me. Could you give me some further provements?
orz

[Martin Dvořák]

You need to provide a bijection between the natural indexing set and the integer indexing set.

[Jasin Jiang]

could you give me an example?

[Martin Dvořák]

import Mathlib
open Finset Nat BigOperators Set

theorem idt_61_equal (n m r : ℕ) :
    ∑ k in Finset.Ico 0 (n + 1), choose k m * choose (n - k) r =
    ∑ k in Finset.Ico (0:ℤ) (n + 1), Ring.choose k m  * Ring.choose (n - k) r := by
  zify
  simp_rw [← Ring.choose_natCast]
  apply sum_bij
  case i =>
    intro i hi
    exact (i : ℤ)
  case hi =>
    intro a ha
    rw [Finset.mem_Ico] at ha ⊢
    constructor
    · exact Int.ofNat_zero_le a
    · linarith
  aesop
  · intro b hb
    use b.toNat
    aesop
  · intro j hj
    congr
    rw [Finset.mem_Ico] at hj
    apply Int.ofNat_sub
    exact le_of_lt_succ hj.right

[Jasin Jiang]

Thank you for helping me! Maybe I will pay a whole day to understand this code. orz.

[Martin Dvořák]

If you want to study the code, I should write a better code.

[Jasin Jiang]

I am a complete beginner in Lean 4, and I guess I will have more questions to ask in the future. Thank you and this community for answering my questions!

[Jasin Jiang]

please write for me thank you!

[Martin Dvořák]

You are welcome! I just wanted to say that I didn't give you a well-written proof. I just sent you the first thing that worked.

[Jasin Jiang]

Lean 4 is so strict that I often find many theorems unusable due to normalization issues. Just converting between integers and natural numbers requires so much effort! I feel like Lean 4 is really hard to learn.

[Martin Dvořák]

Well, the strictness is necessary. Subtracting natural numbers is not the same as subtracting integers. Hence it matters whether you coërce first and then subtract, or you subtract first and then coërce

[Luigi Massacci]

(the solution is not to use natural number subtraction, which is almost never needed anyway)

[Martin Dvořák]

I don't like it when people tell me to solve my problem by changing the statement or definitions.

For me, the statement of the theorem is the task I want to solve. The existing definitions and the statement are like the rules of the game I am playing. We can do whatever we want to do as long as we comply with the rules of the game. I want to win the game. However, it is not cool to win a game by changing its rules.

[Johan Commelin]

If you are aware what the rules of the game mean, then sure. But I think some rules of the game (like Nat subtraction) are surprising to newcomers. And after discovering this rule, they might be very happy to switch to the game that they really intended to play.

[Kevin Buzzard]

Another way of thinking about it: the formal statement of the theorem is merely some kind of attempt to push the actual mathematical idea into a formal system. People can attempt this insertion in different ways; there are often many distinct formal statements that correspond to the same mathematical idea. Personally I would like to turn my mathematical statement into Lean in the most idiomatic and usable statement, so I am grateful when people tell me to change my definitions because it will make my life easier. For me the ultimate goal is not the formal statement, but the mathematical idea, so I am very open to changing formal statements as long as they correspond to the same mathematical idea.

[Johan Commelin]

Kevin! Are you secretly signalling to us that you are not a formalist after all?

[Martin Dvořák]

Very well pointed out! I think this is exactly the thing that makes me a formalist.

[Mauricio Collares]

Luigi Massacci said:

(the solution is not to use natural number subtraction, which is almost never needed anyway)

Concretely, I think the suggestion here is to look at docs#Finset.antidiagonal. Mathlib has a binomial theorem with subtraction (docs#add_pow) and one using the antidiagonal construction (docs#Commute.add_pow').

[Notification Bot]

This topic was moved here from #general > Hello! I want to convert this from N to Z! by Yury G. Kudryashov.