counting permutations

Stream: new members

[Nathan]

I'm trying to use Fin n to write this problem, but am I shifting the indices correctly?

image.png

import Mathlib.Data.Fintype.Perm
import Mathlib.Data.Nat.Fib.Basic

open Equiv Finset
theorem POTD_1648 {n : ℕ} [NeZero n] :
    #{a : Perm (Fin n) | ∀ j k : Fin n, j < k → (j+1) * (a j + 1) ≤ (k+1) * (a k + 1)} =
    Nat.fib (n+1) := by
  sorry

[Nathan]

oh also, i just noticed, i think ≤ is comparing its arguments as Fins, but they need to be Nats. When i change it to Nat.le I get this error which i don't know how to fix:

Screenshot 2026-02-11 at 11.43.20 PM.png

[Nathan]

do i have to tell it that it's a decidable predicate somehow?

[Niels Voss]

I have not checked if you have set this problem up correctly, but I think the most recent problem you are getting is that the typeclass system can't find decidable instances for Nat.le, when it can for the regular LE.le. If you cast them explicitly, it seems to work:

#{a : Perm (Fin n) | ∀ j k : Fin n, j < k → ((j+1) * (a j + 1) : ℕ) ≤ ((k+1) * (a k + 1) : ℕ)}

(As a side note, sometimes you can resolve these issues with open Classical, which makes every proposition decidable, but this comes at a trade-off.)

More generally, I think Nat.le is poorly behaved with typeclass inference and tactics because it is not in a canonical form. For example, simp will rewrite away from Nat.le.

[Eric Wieser]

Now that the problem here was not that ≤ was the wrong comparison (they coincide) but that + and * were the wrong operators

[Niels Voss]

Yes, this is a good point; addition in Fin wraps (https://leanprover-community.github.io/extras/pitfalls.html#wrapping-arithmetic-in-fin) so you need to be careful

[Niels Voss]

Whatever approach you use, make sure that in the infoview you see the coercion arrow ↑ directly next to an element of Fin n, so that you have something like (↑j + 1) instead of something like ↑(j + 1). The former means convert to a natural number and add 1, and the latter means add 1 to j, wrapping to 0 if j = n - 1, and then convert to a natural number.

[Nathan]

thanks! :pray:

[Nathan]

I'm trying to use induction on a variable k, which is a Fin n. I wasn't really sure how to do that, but this is what I came up with. Is it reasonable? I'm not that comfortable with generalize.

    generalize hv : k.val = v
    induction v using Nat.strong_induction_on generalizing k with | h v ih

Here's the context (it's in claim1):

import Mathlib.Data.Fintype.Perm
import Mathlib.Data.Nat.Fib.Basic

--attribute [instance] Classical.propDecidable
open Equiv Finset

theorem POTD_1648 {n : ℕ} [NeZero n] :
    let p (a : Perm (Fin n)) :=
      ∀ j k : Fin n, j < k → (j.val+1) * (a j + 1) ≤ (k.val+1) * (a k + 1)
    #(filter p univ) = Nat.fib (n+1) := by
  intro p
  have claim1 : ∀ a, p a → ∀ k, k.val ≤ a k + 1 := by
    intro a ha k; generalize hv : k.val = v
    induction v using Nat.strong_induction_on generalizing k with | h v ih
    by_cases vz : v = 0
    · simp only [vz, zero_le]
    let vprev := Fin.ofNat n (v-1)
    have vval : vprev.val = v-1 := by
      unfold vprev; simp only [Fin.ofNat_eq_cast, Fin.val_natCast]
      apply Nat.mod_eq_of_lt
      apply lt_trans (Nat.sub_one_lt vz)
      rw[←hv]; exact k.is_lt
    have : vprev < k := by sorry
    specialize ha vprev k this; clear this
    specialize ih (v-1) (Nat.sub_one_lt vz) vprev (by sorry)
    rw[vval, show v-1+1 = v by grind] at ha; subst hv
    by_contra c; simp only [ge_iff_le, not_le] at c
    have := calc k.val * ((a vprev).val + 1)
      _ ≤ (k.val+1) * ((a k).val + 1) := ha
      _ = k.val * (a k).val + k.val + ((a k).val + 1) := by lia
      _ < k.val * (a k).val + k.val + k.val := by apply Nat.add_lt_add_left c
      _ = k.val * ((a k).val + 2) := by lia
    replace := Nat.succ_le_of_lt (Nat.lt_of_mul_lt_mul_left this)
    simp only [Nat.succ_eq_add_one, add_le_add_iff_right] at this
    replace : (a vprev).val < (a k).val := by
      by_contra c; simp only [not_lt] at c
      replace c := Fin.eq_of_val_eq (le_antisymm this c)
      replace c := congrArg a.invFun c; simp only [invFun_as_coe, symm_apply_apply] at c
      lia
    grind
  have claim2 : ∀ a, p a → ∀ k, a k ≤ k.val+1 := sorry
  let q (a : Perm (Fin n)) := ∀ k : Fin n, k.val-1 ≤ a k ∧ a k ≤ k.val+1
  have claim3 : filter p univ = filter q univ := by
    refine filter_inj'.mpr (fun a _ ↦ ?_)
    refine ⟨by grind, ?_⟩; intro qh j k hjk
    exact calc (j.val+1) * (a j + 1)
      _ ≤ (j.val+1) * (j.val + 2) := by
        apply Nat.mul_le_mul_left
        simp only [add_le_add_iff_right]; exact (qh j).2
      _ ≤ k.val * (k.val + 1) := by apply mul_le_mul <;> lia
      _ ≤ (k.val+1) * (a k + 1) := by
        rw[mul_comm]; apply Nat.mul_le_mul_left
        exact Nat.le_add_of_sub_le (qh k).1
  rw[claim3]; clear claim1 claim2 claim3 p

  sorry

[Aaron Liu]

docs#Fin.succRec would probably be a better fit here

[Aaron Liu]

actually this is docs#Fin.induction I think?

[Aaron Liu]

modulo the fact that you need a Fin (n + 1)

[Nathan]

oh thanks!

[Nathan]

it should be possible given that i have [NeZero n], but i'm not sure how

[Nathan]

like this?

import Mathlib.Data.Fintype.Perm
import Mathlib.Data.Nat.Fib.Basic

--attribute [instance] Classical.propDecidable
open Equiv Finset

theorem POTD_1648 {n : ℕ} [NeZero n] :
    let p (a : Perm (Fin n)) :=
      ∀ j k : Fin n, j < k → (j.val+1) * (a j + 1) ≤ (k.val+1) * (a k + 1)
    #(filter p univ) = Nat.fib (n+1) := by
  intro p
  have claim1 : ∀ a, p a → ∀ k, k.val ≤ a k + 1 := by
    intro a ha k
    have : Fin n = Fin (n-1+1) := by
      apply congrArg; symm
      apply Nat.sub_add_cancel; exact NeZero.one_le
    rw[this] at k
    induction k using Fin.induction with | zero | succ k ih
    · sorry
    · sorry
  sorry

[Nathan]

no this can't be right, because i can close succ with assumption

[Aaron Liu]

like this

  have claim1 : ∀ a, p a → ∀ k, k.val ≤ a k + 1 := by
    intro a ha k
    cases n with | zero => exact k.elim0 | succ n
    induction k using Fin.induction with | zero | succ k ih
    · sorry
    · sorry

the n is replaced with n + 1 (where n is a new variable with the same name)

[Nathan]

is cases making a substitution in all my hypotheses, like subst?

[Nathan]

Yeah that went smoother with Fin.induction, thanks

[Nathan]

mainly cause the other approach had extra variables flying around that confused me

[Nathan]

I'm working with the pigeonhole principle (Finset.exists_lt_card_fiber_of_mul_lt_card_of_maps_to) and i obtained the hypothesis yh : 1 < #({x ∈ {a | ↑a ≤ ↑k} | a.invFun x = y}) at line 63 (let ⟨y, _, yh⟩ := this). This should allow me to derive a contradiction since a is a bijection, but how do I grab two distinct elements from this set of cardinality > 1 ?

import Mathlib.Data.Fintype.Perm
import Mathlib.Data.Nat.Fib.Basic
import Mathlib.Combinatorics.Pigeonhole

--attribute [instance] Classical.propDecidable
open Equiv Finset

theorem POTD_1648 {n : ℕ} [NeZero n] :
    let p (a : Perm (Fin n)) :=
      ∀ j k : Fin n, j < k → (j.val+1) * (a j + 1) ≤ (k.val+1) * (a k + 1)
    #(filter p univ) = Nat.fib (n+1) := by
  intro p
  have claim1 : ∀ a, p a → ∀ k, k.val ≤ a k + 1 := by
    intro a ha k
    cases n with | zero => exact k.elim0 | succ n
    induction k using Fin.induction with | zero | succ k ih
    · simp only [Fin.coe_ofNat_eq_mod, Nat.zero_mod, le_add_iff_nonneg_left, zero_le]
    · by_contra c; simp only [Fin.val_succ, add_le_add_iff_right, not_le] at c
      specialize ha k.castSucc k.succ (by grind only [= Fin.val_castSucc, usr Fin.val_succ])
      rw[Fin.val_castSucc k] at ih ha; rw[Fin.val_succ k] at ha
      have : (k+1) * ((a k.castSucc).val + 1) < (k+1) * ((a k.succ).val + 2) := by lia
      replace := Nat.succ_le_of_lt (Nat.lt_of_mul_lt_mul_left this)
      simp only [Nat.succ_eq_add_one, add_le_add_iff_right, Fin.val_fin_le] at this
      replace : a k.castSucc < a k.succ := by
        by_contra c; simp only [not_lt] at c
        apply le_antisymm this at c
        apply congrArg a.invFun at c
        simp only [invFun_as_coe, symm_apply_apply] at c
        grind only [= Fin.val_castSucc, Fin.val_succ]
      grind only [= Fin.val_castSucc]
  have claim2 : ∀ a, p a → ∀ k, a k ≤ k.val+1 := by
    intro a ha k; by_contra c; simp only [not_le] at c
    by_cases knn : k = n-1
    · grind only
    obtain ⟨j, jh⟩ : ∃ j : Fin n, a j = k := by
      exists (a.invFun k)
      exact (apply_eq_iff_eq_symm_apply a).mpr rfl
    have jh2 : j.val = k+1 := by
      apply le_antisymm (jh ▸ claim1 a ha j)
      by_contra c2; simp only [not_le] at c2
      replace c2 : j.val < k.val := by
        apply Nat.lt_of_le_of_ne (Nat.le_of_lt_succ c2)
        grind only
      have := Finset.exists_lt_card_fiber_of_mul_lt_card_of_maps_to (s := {a : Fin n | a ≤ k.val})
        (t := {a : Fin n | a < k.val}) (f := a.invFun) (n := 1)
      specialize this ?_ ?_
      · simp only [Fin.val_fin_le, mem_filter, mem_univ, true_and, Fin.val_fin_lt, invFun_as_coe]
        intro l lh
        by_cases hlk : l = k
        · grind only [= symm_apply_apply]
        replace lh := Std.lt_of_le_of_ne lh hlk; clear hlk
        replace := claim1 a ha ((Equiv.symm a) l); simp only [apply_symm_apply] at this
        replace : ((Equiv.symm a) l) ≤ k := by lia
        grind only [= apply_symm_apply]
      · simp only [Fin.val_fin_lt, mul_one, Fin.val_fin_le]
        let s : Finset (Fin n) := {a : Fin n | a < k}
        let t : Finset (Fin n) := {a : Fin n | a = k}
        have : ({a : Fin n | a ≤ k} : Finset (Fin n)) = s ∪ t := Finset.ext_iff.mpr (by grind)
        rw[this]
        rw[Finset.card_union_eq_card_add_card.mpr (disjoint_filter.mpr (by grind))]
        simp only [lt_add_iff_pos_right, card_pos]; exists k
        simp only [mem_filter, mem_univ, and_self]
      let ⟨y, _, yh⟩ := this
      sorry
    have s : (k+1).val = k.val+1 := Fin.val_add_one_of_lt' (by grind only)
    have := calc (k.val+1)*(k.val+2)
      _ < (k.val+1)*((a k).val+1) := by
        refine Nat.mul_lt_mul_of_pos_left ?_ (by apply Nat.zero_lt_succ)
        exact Nat.lt_succ_of_le c
      _ ≤ ((k+1).val+1)*((a (k+1)).val + 1) := ha k (k+1) (by grind only)
      _ = (k.val+1)*(k.val+2) := by
        rw[mul_comm, s]
        simp only [mul_eq_mul_right_iff, Nat.add_right_cancel_iff, Nat.add_eq_zero_iff,
          Fin.val_eq_zero_iff, one_ne_zero, and_false, and_self, or_false]
        grind only
    grind only
  let q (a : Perm (Fin n)) := ∀ k : Fin n, k.val-1 ≤ a k ∧ a k ≤ k.val+1
  have claim3 : filter p univ = filter q univ := by
    refine filter_inj'.mpr (fun a _ ↦ ?_)
    refine ⟨by grind, ?_⟩; intro qh j k hjk
    exact calc (j.val+1) * (a j + 1)
      _ ≤ (j.val+1) * (j.val + 2) := by
        apply Nat.mul_le_mul_left
        simp only [add_le_add_iff_right]; exact (qh j).2
      _ ≤ k.val * (k.val + 1) := by apply mul_le_mul <;> lia
      _ ≤ (k.val+1) * (a k + 1) := by
        rw[mul_comm]; apply Nat.mul_le_mul_left
        exact Nat.le_add_of_sub_le (qh k).1
  rw[claim3]; clear claim1 claim2 claim3 p

  sorry