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: Mar 28 2024 at 23:01 UTC