Ssreflect Users Discussion List

[Boris Djalal <>]

Hi Epiphanie,

First generalize over A.
move: A

Then push (#|A|) = (#|A|) as your top assumption.
move: (erefl #|A|)

Then generalize over the second occurrence of #|A|.
move: {2}(#|A|)

All these steps are packed into a single line:
move: {2}(#|A|) (erefl #|A|) => card.

Finally, you make an induction on the natural number card.

Does it help ?


On 03/26/2016 03:55 AM, Epiphanie wrote:
> Dear all,
> I am sorry to ask such a basic question but I couldn't find the answer 
> anywhere, as I didn't find any mathcomp tutorial.
> Is there a way to induce on the cardinal of a finite type or sets? I 
> would basically like to say "Either my type is the empty type, or it 
> is a type of n elements on which the property holds to which I add an 
> element".
>
> I saw I could do an elim: (enum T), however that doesn't really 
> fulfill my need, as I could not find any way to retain the result of 
> the elimination (elim X: (enum T) did not work well either).
> To give some context I am currently studying permutations and attempt 
> to prove the card_perm theorem:
> #|perm_on A| = (#|A|)`!.
>
> I cannot directly do elim: (enum A) as that would yield 0 = (#|A|)`!
> I peaked at the proof of this lemma, but it seems however that they 
> solve this differently based on other lemmas. So I would like to know 
> how to do it my way. I found an idea to do a case: (A == set0) and 
> then on the induction use the fact that since (A != set0) I can 
> exhibit an element of A and disjoint this element from A, but that 
> does not give me induction, only case elimination.
>
> Thank you very much, and I appologize again if this question is too 
> simple, I am still learning
> Cheers
>
> Epiphanie