Zulip Chat Archive

Stream: new members

Topic: Induction question


Ching-Tsun Chou (Feb 01 2025 at 23:47):

I have a function foo (s : Finset x) : Finset y and I want to prove a property of foo by induction on s.card, rather than on s, because there is no simple relationship between foo s and foo (insert a s). How do I do it? I tried induction s.card, but it does not give me meaningful goals.

One idea I have is to define foo' (s : Finset x) (n : ℕ) (h : s.card = n) : Finset y and induct on n. Is this the only way?

Kyle Miller (Feb 01 2025 at 23:48):

You could do generalize h : s.card = n and then do induction on n

There's probably also an induction principle somewhere in mathlib you could use with a using clause.

Kevin Buzzard (Feb 01 2025 at 23:48):

This is a great question in the sense that (a) I have run into this before (induction on size of finset is strictly more powerful than the default induction theorem for finsets) (b) I've asked about it before and (c) there's definitely an answer on this server somewhere ;-) but i've forgotten it :-(

Kyle Miller (Feb 01 2025 at 23:49):

docs#Finset.induction is insert-based induction

Kyle Miller (Feb 01 2025 at 23:50):

so induction s using Finset.induction

Kevin Buzzard (Feb 01 2025 at 23:51):

yeah that was what I meant by "the default induction theorem". The issue comes when the proof for insert a s follows from e.g. the proof for all subsets of insert a s of size |s|, rather than just s itself.

Aaron Liu (Feb 01 2025 at 23:56):

The can be done with docs#Finset.strongInduction (which should be renamed to Finset.strongRec).

Ching-Tsun Chou (Feb 02 2025 at 00:02):

Let me give some more details: foo s is the set of permutations of the elements of s, represented as a Finset of bijective maps from s to the set {0, 1, ..., s.card - 1}. What I want to prove is that (foo s).card = s.card.factorial. I don't think any of the Finset induction schemes is really usable (including the strong one), because the recurrence relation that results are complicated. The informal argument is to induct on s.card and write foo s as the disjoint union indexed by the last element of the permutation. Hence my question.

Ching-Tsun Chou (Feb 02 2025 at 00:05):

I have spent a lot of time trying to reduce my goal to some theorems about permutations already in mathlib, but so far in vain.

Aaron Liu (Feb 02 2025 at 00:09):

Ching-Tsun Chou said:

The informal argument is to induct on s.card and write foo s as the disjoint union indexed by the last element of the permutation. Hence my question.

Is this not just docs#Finset.induction
You are writing the argument to p as insert a s where a ∉ s

Aaron Liu (Feb 02 2025 at 00:10):

Oh you need access to all of the subcases

Kyle Miller (Feb 02 2025 at 00:11):

Kyle Miller said:

You could do generalize h : s.card = n and then do induction on n

Did you try this? This is how you do what you asked in your question.

Kyle Miller (Feb 02 2025 at 00:14):

Or you could do induction' h : s.card. (Unfortunately induction doesn't yet support h : syntax)

Ching-Tsun Chou (Feb 02 2025 at 00:32):

I have not finished the proof, but I think the following should work (in the sense that the resulting goals do look like true statements):
``lean4
generalize h : s.card = n
revert s
induction' n with n ih
...


Ching-Tsun Chou (Feb 02 2025 at 00:36):

Without the revert s, the induction hypothesis will not be usable because it refers to the same s as in the assumption s.card = n + 1.

Aaron Liu (Feb 02 2025 at 00:41):

You can say induction' n generalizing s to do the revert automatically.


Last updated: May 02 2025 at 03:31 UTC