Induction question

Stream: new members

[Ching-Tsun Chou]

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]

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]

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]

docs#Finset.induction is insert-based induction

[Kyle Miller]

so induction s using Finset.induction

[Kevin Buzzard]

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]

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

[Ching-Tsun Chou]

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]

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]

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]

Oh you need access to all of the subcases

[Kyle Miller]

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]

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

[Ching-Tsun Chou]

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]

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]

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