How to use Finset.induction_on

Stream: new members

[Timothy Chow]

In Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof, Alexeev and Mixon mention how they had trouble vibe proving "if f is an involution on a finite set s with odd cardinality then f must have a fixed point." This sounded like a good exercise for me to try. Below is the beginning of my first attempt, but I'm not even sure that I've even formulated a correct statement. Assuming that I have, my thought is to prove the result using Finset.induction_on. If the new element is a, then the way I want the proof to go is to split into two cases depending on whether f a = a or not. If f a = a then I'm done because a is my fixed point. Otherwise, if b = f a, then I can delete a and b and get a smaller odd set t, and f restricted to t must have a fixed point by induction. But it seems that the way I've set things up, the expression f a makes no sense. What am I doing wrong?

theorem fpf {α : Type _} [DecidableEq α] (x : Finset α) (f : x → x) :
   (Odd #x) ∧ (∀ y : x, f (f y) = y) → ∃ y : x, f y = y := by
   induction x using Finset.induction_on with
   | empty => have h : #(∅ : Finset α) = 0 := by apply card_empty
              intro z
              rw [h] at z
              by_contra
              apply Nat.not_odd_zero
              apply z.left
   | @insert a s ha ih =>
              have a_in_insert_a_s : a ∈ insert a s := by
                 apply mem_insert_self a s
              let b := f a
              sorry

[Robin Arnez]

You made this a bit more difficult for yourself by using the Finset x as a type. What that means is { a : α // a ∈ x }, i.e. a subtype. To construct values of that type then, you need to use the constructor with the value and the proof, e.g. let b := f ⟨a, a_in_insert_a_s⟩

[Philippe Duchon]

This exact problem (an involution on a set of odd size must have a fixed point) was also one I briefly tried to solve as an exercise in Rocq, and didn't find an extra easy solution. I just tried to see if there was a theorem in Mathlib saying the cycle type of an involution must include only cycles of lengths 1 and 2 (with the idea of using Equiv.Perm.sum_cycleType), but my Mathlib-searching skills are still very weak.

[Kenny Lau]

Timothy Chow said:

What am I doing wrong?

getting the statement of a theorem right is an art in and of itself, and getting it wrong can impact greatly the difficulty of both proving the theorem and using the theorem

[Kenny Lau]

if you're just starting out, I would recommend you get the statement from someone more experienced, then you can try whatever you want to prove it

[Kenny Lau]

the way you used induction was also wrong because it didn't give you access to the theorem for #x - 2 (you should be using strong induction on the cardinality of the finset, not the finset itself)

[Kenny Lau]

actually since you are doing induction then using Finset is the correct choice but just that as mentioned above you'll need to include a proof every time you want to mention one of its elements

[Vlad]

Use finset membership instead of subtypes:

example {α : Type*} [DecidableEq α] {s : Finset α} {f : α → α} (hf : ∀ x ∈ s, f x ∈ s)
    (h₁ : Odd s.card) (h₂ : ∀ x ∈ s, f (f x) = x) : ∃ x ∈ s, f x = x := by
  sorry

Proof

import Mathlib

example {α : Type*} [DecidableEq α] {s : Finset α} {f : α → α} (hf : ∀ x ∈ s, f x ∈ s)
    (h₁ : Odd s.card) (h₂ : ∀ x ∈ s, f (f x) = x) : ∃ x ∈ s, f x = x := by
  choose n h₁ using h₁; induction n generalizing s
  · obtain ⟨x, rfl⟩ := s.card_eq_one.mp h₁; simp_all
  rename_i n ih; have H : ∀ x y, x ∈ s → y ∈ s → f x = f y → x = y
  · intro x y hx hy h; rw [←h₂ x hx, ←h₂ y hy, h]
  rw [Finset.card_eq_succ] at h₁; obtain ⟨x, s, hx, rfl, h₁⟩ := h₁
  by_cases h₃ : f x = x; use x; simp [h₃]; simp [h₃] at hf h₂
  obtain ⟨s, hs, rfl⟩ : ∃ s', f x ∉ s' ∧ insert (f x) s' = s
  · use s.erase (f x); simp [Finset.ext_iff]; intro y
    by_cases hy : y = f x <;> simp [hy, hf.1]
  rw [Finset.card_insert_of_notMem hs] at h₁
  specialize @ih s _ _ (by linarith)
  · intro y hy; simp [h₂] at hf; specialize H x y
    rcases hf y hy with rfl | _ | _ <;> simp_all
  · intro y hy; apply h₂.2 y; simp [hy]
  choose y hy ih using ih; use y; simp [ih, hy]

[Jakub Nowak]

Vlad said:

Use finset membership instead of subtypes:

Isn't the ability to use subtypes one of the arguments often raised in favor of Lean when comparing it to Rocq?

[Kenny Lau]

that doesn't mean you should use it in every situation

[Timothy Chow]

Robin Arnez said:

To construct values of that type then, you need to use the constructor with the value and the proof, e.g. let b := f ⟨a, a_in_insert_a_s⟩

Okay, I think I understand what you're saying. But I guess that means that a = b doesn't make sense if a : α and b : { x // x ∈ insert a s } where s : Finset α. It seems I want to coerce a to have type { x // x ∈ insert a s } but how do I do that? There doesn't seem to be much documentation in MIL about subtypes and coercion.

[Aaron Liu]

why not coerce b instead?

[Timothy Chow]

Aaron Liu said:

why not coerce b instead?

Good point. I guess your suggestion is in the same vein as Vlad's suggestion to treat everything as having type α and imposing membership hypotheses as needed? That sounds sensible (for this theorem at least), but Vlad's proof uses a lot of techniques that are unfamiliar to me. I'd like to start by understanding the mechanics of coercing from one type to another, which as I said I have had some trouble finding documentation about.

[Jakub Nowak]

f : α → α and f : s → s where s : Finset α is not the same. It might be problematic to define the former if the type doesn't have Inhabited instance. One could use f : s → α to only use subtypes when necessary and avoid them when not. Or f : (x : α) → x ∈ s → α, but that's just the same.

[Timothy Chow]

Okay, I'm having enough trouble with subtypes and coercion that I'm going to set those aside for now, and instead use Vlad's formulation of the theorem (which bypasses subtypes), but I'd like to build my own proof.

I see what Kenny Lau is saying about strong induction being the natural way to go, at least for the proof I have in mind, but I'm not sure how to formulate it. Finset.induction_on doesn't have a "strong induction version" does it? So how do I set up the induction?

[Aaron Liu]

@loogle Finset, "strong"

[loogle]

:search: Finset.strongInduction, Finset.strongInductionOn, and 29 more

[Aaron Liu]

oh look a strong induction version

[Philippe Duchon]

For what it's worth (and I realize it isn't much), I beat ChatGPT in terms of lines of code for the "an involution with no fixed points must operate on a type of even cardinality" proof - about 60 lines instead of 250. I went a very different way though, spending a lot of effort finding the useful facts in Mathlib (my real goal was to get better at using Mathlib, so I think I didn't completely lose my time).

(I need to work on my proof style though, it's an ugly mix of forward and backward reasoning, some facts get their own lemmas and others don't for no good reason)

import Mathlib

open Function

section on_fixed_points_in_involutions

variable {α: Type} [Fintype α] [DecidableEq α]
variable {f : Equiv.Perm α} (hfi: Involutive f)

omit [Fintype α] [DecidableEq α] in theorem order_invol_le_two (hfi: Involutive f):
  orderOf f ≤ 2 := by
  apply orderOf_le_of_pow_eq_one; norm_num
  ext x
  simp
  apply hfi

omit [Fintype α] [DecidableEq α] in theorem order_invol_dvd_two (hfi : Involutive f) :
   orderOf f ∣ 2 := by
  have ole2: orderOf f ≤ 2 := order_invol_le_two hfi
  have zero_lto : 0 < orderOf f := by
    refine orderOf_pos_iff.mpr ?_
    refine isOfFinOrder_iff_zpow_eq_one.mpr ?_
    use 2
    constructor
    norm_num
    ext x; simp; apply hfi
  interval_cases using zero_lto, ole2
  · use 2
  · use 1

theorem cycle_type_of_invo {f : Equiv.Perm α} (hfi : Involutive f) :
   ∀ j ∈ f.cycleType, j = 2
  := by
  intro j hj
  apply Nat.le_antisymm
  · apply Nat.le_of_dvd; norm_num
    apply Nat.dvd_trans _ (order_invol_dvd_two hfi)
    apply Equiv.Perm.dvd_of_mem_cycleType hj
  apply Equiv.Perm.two_le_of_mem_cycleType hj

theorem sum_cycle_type {f : Equiv.Perm α} :
  f.cycleType.sum ≤ Fintype.card α := by
  rw [Equiv.Perm.sum_cycleType]
  apply Finset.card_le_univ -- f.support

theorem counting_fixedPoints {f: Equiv.Perm α} (hfi : Involutive f)
  (h₀: fixedPoints f = ∅) :
  Even (Fintype.card α) := by
  have hcfp: Fintype.card (fixedPoints f) = 0 := by
    simp [h₀]  -- black magic: rw [h₀] fails, but simp [h₀] succeeds
  have sm : Fintype.card α = Fintype.card (fixedPoints f) + f.cycleType.sum := by
    apply (Nat.sub_eq_iff_eq_add (sum_cycle_type)).mp
    rw [Equiv.Perm.card_fixedPoints]
  rw [sm, Nat.even_add, hcfp]
  simp
  rw [even_iff_two_dvd]
  apply Multiset.dvd_sum
  intro x hx
  rw [cycle_type_of_invo hfi x hx]

end on_fixed_points_in_involutions

[Timothy Chow]

Thanks to all of you for your help. I have constructed a proof of Vlad's version of the theorem that, by virtue of generous use of grind, is fairly short. There are probably several places where I've done something in an unnecessarily clumsy or laborious manner; I welcome more experienced people to point out simple improvements.

variable {α : Type*} [DecidableEq α]
theorem fpf {s : Finset α} {f : α → α} (hf : ∀ x ∈ s, f x ∈ s)
    (h₁ : Odd s.card) (h₂ : ∀ x ∈ s, f (f x) = x) :
     ∃ x ∈ s, f x = x := by
  induction s using Finset.strongInduction with
  | H s ih =>  -- ih is the strong induction hypothesis
     -- split into cases according to whether s is empty
     by_cases h : ∃ x, x ∈ s
     -- Case 1: s is nonempty
     · rcases h with ⟨x, hx⟩   -- s is nonempty; pick x ∈ s
       let y := f x
       have fxy : f x = y := by rfl
       by_cases h₃ : x = y
       · use y                -- case 1a: x = y
         apply And.intro
         {rw [h₃] at hx; exact hx}    -- show that y ∈ s
         {rw [h₃] at fxy; exact fxy}  -- show that f y = y
       · let t := s \ {x, y}  -- case 1b: ¬(x = y)
        -- To apply the induction hypothesis,
        -- we have to check 4 things:
        --   1. t is a proper subset of s
        --   2. f f x = x for all x in t
        --   3. t is closed under f
        --   4. t has odd cardinality
         have t_subset_s : t ⊂ s := by grind
         have t_invol : ∀ z ∈ t, f (f z) = z := by grind
         have t_closed : ∀ z ∈ t, f z ∈ t := by grind
         have t_odd : Odd #t := by grind
         grind
     -- Case 2: s is empty.
     · have s_empty : s = ∅ := by exact not_nonempty_iff_eq_empty.mp h
     -- This case is vacuous because #∅ is not odd.
       rw [s_empty] at h₁            -- h₁ : Odd #∅
       rw [Finset.card_empty] at h₁  -- h₁ : Odd 0
       by_contra
       apply Nat.not_odd_zero -- Theorem: 0 is not odd
       exact h₁

[Timothy Chow]

I may go back and try to prove the "subtype version" of the theorem that I originally posted. It occurs to me that type-theory enthusiasts often try to argue that type theory more naturally reflects "how mathematicians actually think" than set theory does, but this example seems to be a small bit of evidence in the other direction. I claim that, in the context of the theorem we're discussing here, a mathematician naturally thinks of f as a function from a finite set S to itself, not as a function from U to U (where U is the universe of objects from which S is drawn) that just happens to send every element of S to S. But it seems that the latter choice makes the Lean user's life a lot easier.

Now of course, there are many ways to rebut what I've just said. For starters, the theorem can be formulated and proved either way, and perhaps there are settings where the subtype formulation turns out to be preferable after all. One could also argue that this is an artifact of Lean and not of type theory per se (apparently Rocq does it differently?).

Nevertheless, I'm sure that I'm not the only mathematician who will instinctively want to define f as a function from S to S, so teachers of Lean should probably take note that this is likely to be a common stumbling block for learners of Lean.

[Bryan Gin-ge Chen]

You may have already seen this, there was a bit of discussion on the Alexeev and Mixon paper a few weeks ago. Here's a link to the part of the thread discussing (yet another) a variant of the result you're working on here #general > Erdos 707 @ 💬

[Timothy Chow]

No, I hadn't seen that thread...thanks for the pointer! Very interesting discussion.

[Terence Tao]

Conceptually, working with {s : Type*} [Fintype s] may be better than {α : Type*} [DecidableEq α] {s : Finset α}, but one would have to find a different induction tool to run the argument then.

[Jakub Nowak]

Terence Tao said:

Conceptually, working with {s : Type*} [Fintype s] may be better than {α : Type*} [DecidableEq α] {s : Finset α}, but one would have to find a different induction tool to run the argument then.

The proof here uses induction over size of the set. I think the same induction works in both cases.