Ssreflect Users Discussion List

[(Emilio Jesús Gallego Arias)]

Hi Epiphanie,

Epiphanie 
<>
 writes:

> 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|)`!.

You could also use this little hack to use the /big_rec principle to
perform induction over the elements of a finset:

8<--------------------------------------------------------------------8<
Implicit Types T : finType.

Lemma bigcup_decomp T (i : {set T}) : i = \bigcup_(x in i) [set x].
Proof.
apply/setP=> x; apply/idP/bigcupP=> [w | [w win]]; last by move/set1P->.
by exists x; rewrite ?in_set1.
Qed.

Lemma card_perm T (A : {set T}) : #|perm_on A| = (#|A|)`!.
Proof.
rewrite [A]bigcup_decomp; elim/big_rec: _ => [| x B x_in ihB].
8<--------------------------------------------------------------------8<

In my very personal opinion, I'm not sure that using induction in this
particular problem may not be the best path.

Something I've learned after being introduced to the ssreflect library
is to try to abandon induction in favor of more combinatorial proofs (as
noted, for example, in [1]).

It seems it is still common to find plenty of Coq practitioners that
enjoy writing "induction-fests". However, in most cases it seems to me
that the proofs there are better done using the proper lemmas that
encapsulate induction (like card_uniq_tuples does I believe for
card_perm) instead of calling induction so often.

I'm not sure where this advantage does come from, however I'd conjecture
that setting up the proper induction hypotheses is a hard and tedious
problem in general; using generic lemmas kind of eases this task.

Best,
E.

[1] Georges Gonthier. Point-Free, Set-Free Concrete Linear
    Algebra. Marko C. J. D. van Eekelen and Herman Geuvers and Julien
    Schmaltz and Freek Wiedijk. Interactive Theorem Proving - ITP 2011,
    Aug 2011, Berg en Dal, Netherlands. Springer, 6898, pp.103-118,
    2011, Lecture Notes in Computer Science; Interactive Theorem Proving
    - Second International Conference, ITP
    2011. <10.1007/978-3-642-22863-6 10>. <hal-00805966>