## Stream: math-comp users

### Topic: Induction & counting with ordinals

#### Quim (Dec 01 2020 at 18:54):

For learning purposes, and to satisfy my curiosity, I am trying to get acquainted with FinTypes and the cardinal operator. In particular I am trying to prove the following:

Definition P n := [pred p : ('I_n * 'I_n) | match p with (x,y) => x != y end].
Lemma counting n : #| (P n) | = (n*(n-1)).


I am trying to prove it by induction on n. The trouble I am running into is that in the inductive case I am tasked with proving #| (P n.+1) | = (n.+1*n) and the domains of P n and P n.+1 are of different types, namely ('I_n * 'I_n)  and ('I_n.+1 * 'I_n.+1). In my head I would prove this by using the fact that P n is a "subset" of P n.+1 and thus

#| (P n.+1) | =  # | P n | + #| [ pred (x,y) : 'I_n.+1 * 'I_n.+1 | ((P n.+1) x y) && y == n] |  +  #| [ pred (y,x) : 'I_n.+1 * 'I_n.+1 |  ((P n.+1) y x) && y == n]|


but I haven't succeed in proving this decomposition in Coq. I think that what I am trying to prove ought to be quite straight forward so I feel I am missing the big picture here. Any guidance is appreciated.

#### Christian Doczkal (Dec 01 2020 at 20:54):

Indeed, doing this kind of counting argument by induction is usually not the best idea. I would slightly change your definition to make it easier to work with and then prove it by exploiting that P n is the complement of the diagonal set. Below is a partial proof:

Definition P n := [set p : 'I_n * 'I_n | p.1 != p.2].
Lemma counting n : #|P n| = n*(n-1).
Proof.
have -> : P n = ~: [set (i,i) | i : 'I_n].
{ apply/setP; move => -[i j]; rewrite !inE /=. admit. (* easy *) }
rewrite cardsCs card_prod setCK card_imset ?card_ord.
- by move => i j [].


A different strategy might be to reduce the problem to drawing 2 elements from an n-element set and use card_draws.

#### Quim (Dec 02 2020 at 16:06):

Thanks for the answer. From the code you've proposed, there is one thing that has me a bit confused. At the start of the proof we have

have -> : P n = ~: [set (i,i) | i : 'I_n].


I thought that membership to the set had to be expressed with some sort of boolean expression but here we have i : 'I_n as the "membership condition". So I am wondering if under the hood this is translated to something like i \in enum 'I_n?
Related to this, given the following expression

(i,j) \notin [set (i,i) | i : 'I_n]


I am unsure as to how to recover from the pattern matching (i,i) the fact that (i != j) [Well actually from the pattern matching you would get that i==j I would pressume]

Also I was unaware of the card_draws lemma and the binomial library. I will check it out, thanks again!

#### Christian Doczkal (Dec 02 2020 at 16:17):

Quim said:

I thought that membership to the set had to be expressed with some sort of boolean expression but here we have i : 'I_n as the "membership condition".

You should not confuse "set comprehension" [set x : T | p x] with replacement [set E | x in A] (E is an expression that may use x) which is called imset in mathcomp). And indeed, in the latter x : T stands for "x is in the full predicate over the given type.

#### Christian Doczkal (Dec 02 2020 at 16:18):

So, to answer the second half of your equestion, have a look at imsetP.

Last updated: Feb 08 2023 at 07:02 UTC