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.

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.
- admit. (* aritmetic *)
- 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`

.

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!

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.

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

.

Last updated: Jul 23 2024 at 21:01 UTC