Help with double induction

Stream: new members

[Alena Gusakov]

Hi all,

I have a bit of a weird induction problem - in the theorem eval₂_one_eq_gauss I am trying to prove that (gauss n k).eval₂ (RingHom.id ℕ) 1 = choose n k, i.e. the Gaussian binomial coefficients are equal to the regular binomial coefficients when evaluated at 1. However, when I do induction' k and induction' n, I get a hypothesis of the form eval₂ (RingHom.id ℕ) 1 (gauss n k) = choose n k → eval₂ (RingHom.id ℕ) 1 (gauss n (succ k)) = choose n (succ k), when I would usually expect the two induction's to produce hypothesis eval₂ (RingHom.id ℕ) 1 (gauss n k) = choose n k and eval₂ (RingHom.id ℕ) 1 (gauss n (succ k)) = choose n (succ k). I assume I'm using induction' incorrectly?

/-
Copyright (c) 2024 Alena Gusakov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Alena Gusakov
-/
import Mathlib.Data.Nat.Factorial.Basic
import Mathlib.Data.Polynomial.Basic
import Mathlib.Data.Polynomial.Eval

#align_import data.nat.choose.basic from "leanprover-community/mathlib"@"2f3994e1b117b1e1da49bcfb67334f33460c3ce4"
#align_import data.polynomial.basic from "leanprover-community/mathlib"@"949dc57e616a621462062668c9f39e4e17b64b69"


/-!
# Gaussian Binomial Coefficients

This file defines Gaussian binomial coefficients and proves simple lemmas (i.e. those not
requiring more imports).

## Main definition and results

## Tags

gaussian binomial coefficient
-/

noncomputable section

open Nat

namespace Nat

open Polynomial

-- polynomials? this should output a polynomial, not a nat

/-- `gauss n k` is the number of `k`-dimensional subspaces in an `n`-dimensional vector space.
Also known as Gaussian binomial coefficients. -/
def gauss : ℕ → ℕ → ℕ[X]
  | _, 0 => 1
  | 0, _ + 1 => 0
  | n + 1, k + 1 => gauss n k + X ^ k * gauss n (k + 1)

@[simp]
theorem gauss_zero_right (n : ℕ) : gauss n 0 = 1 := by cases n <;> rfl

@[simp]
theorem gauss_zero_succ (k : ℕ) : gauss 0 (succ k) = 0 :=
  rfl

theorem gauss_succ_succ (n k : ℕ) : gauss (succ n) (succ k) = gauss n k + X ^ k * gauss n (succ k) :=
  rfl

theorem gauss_eq_zero_of_lt : ∀ {n k}, n < k → gauss n k = 0
  | _, 0, hk => absurd hk (Nat.not_lt_zero _)
  | 0, k + 1, _ => gauss_zero_succ _
  | n + 1, k + 1, hk => by
    have hnk : n < k := lt_of_succ_lt_succ hk
    have hnk1 : n < k + 1 := lt_of_succ_lt hk
    rw [gauss_succ_succ, gauss_eq_zero_of_lt hnk, gauss_eq_zero_of_lt hnk1, mul_zero, zero_add]

@[simp]
theorem gauss_self (n : ℕ) : gauss n n = 1 := by
  induction n <;> simp [*, gauss, gauss_eq_zero_of_lt (lt_succ_self _)]

@[simp]
theorem gauss_one_right (n : ℕ) : gauss n 1 = n := by induction n <;> simp [*, gauss, add_comm]

theorem eval₂_one_eq_gauss (n k : ℕ) :
(gauss n k).eval₂ (RingHom.id ℕ) 1 = choose n k := by
  induction' k with k hk
  · rw [gauss_zero_right, choose_zero_right, eval₂_one]
  · induction' n with n hn
    · sorry
    · rw [gauss_succ_succ, choose_succ_succ, eval₂_add, eval₂_mul, eval₂_X_pow, one_pow, one_mul, hk]
      sorry
  /-induction n with
  | zero =>
    induction k with
    | zero =>
      rw [gauss_self, choose_self, eval₂_one]
    | succ n ih =>
      rw [gauss_zero_succ, choose_zero_succ, eval₂_zero]
  | succ n ihn =>
    induction k with
    | zero =>
      rw [gauss_zero_right, choose_zero_right, eval₂_one]
    | succ n ihk =>
      rw [gauss_succ_succ, choose_succ_succ, eval₂_add, eval₂_mul, eval₂_X_pow, one_pow, one_mul,
        ihn, ihk]-/

end Nat

[Kevin Buzzard]

I'm not sure I understand the question yet. If you're doing induction on k then sure you'll get a hypothesis of the form P(k)->P(succ k) which is exactly what you got. Let's define P n k to be (gauss n k).eval₂ (RingHom.id ℕ) 1 = choose n k. What exactly is your mathematical strat for proving P n k for all n and k? Maybe we can tease that strat into Lean.

[Alena Gusakov]

Kevin Buzzard said:

What exactly is your mathematical strat for proving P n k for all n and k? Maybe we can tease that strat into Lean.

So I wanted to do induction on both n and k. With the first induction I start with k because it's easier, and I want hypothesis P n k in order to prove P n (succ k), which works fine. Then, within the proof of P n (succ k), I want to do induction on n to get a new hypothesis P n (succ k) in order to prove P (succ n) (succ k). I'll be able to prove P (succ n) (succ k) if I have those two hypotheses because I can transform P (succ n) (succ k) into the two goals P n k and P n (succ k).

Currently, when I do induction on n after doing induction on k, I get one hypothesis of the form P (succ n) k, and another in the form P n k -> P n (succ k), which is unhelpful

[Matt Diamond]

I understand the question, though unfortunately I don't have an answer... there's something about hk that causes issues. If you add clear hk before the induction' n step, then you get P n (succ k) as expected, but now you've lost hk...

or would P n (succ k) be sufficient?

[Alena Gusakov]

No unfortunately I need both

[Alena Gusakov]

I can rewrite P (succ n) (succ k) only in terms of both P n k and P n (succ k)

[Alena Gusakov]

Out of curiosity, is this just a quirk of Lean 4 induction? I feel like I remember being able to do induction over multiple variables in lean 3 without issue

[Matt Diamond]

I don't think it's a new issue but I can't say for sure

[Matt Diamond]

@Alena Gusakov this might be the wrong way to do this but I think you can get around the issue by doing induction' k with k hk generalizing n when you do induction on k

[Alena Gusakov]

Matt Diamond said:

Alena Gusakov this might be the wrong way to do this but I think you can get around the issue by doing induction' k with k hk generalizing n when you do induction on k

That works, thanks!!! I swapped it around to do induction' n with n hn generalizing k and then did induction on k

[Dan Velleman]

Alena Gusakov said:

Kevin Buzzard said:

What exactly is your mathematical strat for proving P n k for all n and k? Maybe we can tease that strat into Lean.

So I wanted to do induction on both n and k. With the first induction I start with k because it's easier, and I want hypothesis P n k in order to prove P n (succ k), which works fine. Then, within the proof of P n (succ k), I want to do induction on n to get a new hypothesis P n (succ k) in order to prove P (succ n) (succ k). I'll be able to prove P (succ n) (succ k) if I have those two hypotheses because I can transform P (succ n) (succ k) into the two goals P n k and P n (succ k).

Currently, when I do induction on n after doing induction on k, I get one hypothesis of the form P (succ n) k, and another in the form P n k -> P n (succ k), which is unhelpful

I think it might be enlightening to consider how we would explain this proof to undergraduates. We teach undergraduates that induction is for proving statements of the form ∀n, P n, not P n. So I would tell an undergraduate that the theorem you are proving is ∀k, ∀n, P n k. You start with induction on k, and in the induction step, you introduce an arbitrary k, assume hk : ∀n, P n k, and try to prove ∀n, P n (succ k). Notice that hk is ∀n, P n k, not P n k; that will be important. Now to prove ∀n, P n (succ k), you use induction again, and in the induction step, you introduce an arbitrary n, assume P n (succ k), and try to prove P (succ n) (succ k). Now you can take the arbitrary n you just introduced and plug it into hk to conclude P n k. Now you have what you need to prove P (succ n) (succ k). Notice that the n to which hk had to be applied wasn't available yet when hk was introduced; the arbitrary n wasn't introduced until the induction step of the induction on n. So hk had to say ∀n, P n k.

To me, what this suggests is that the Lean approach to induction can be confusing. For educational purposes, I think it would be good to have an induction tactic that proves ∀n, P n, rather than P n. (Is there such a tactic that I don't know about?) I want to complete the analogy induction : Nat.recOn :: __ : Nat.rec.

[Dan Velleman]

As I understand it, the suggestion to add generalizing n to the induction on k restores the ∀n that was missing, solving the problem.