Ssreflect Users Discussion List

[Christian Doczkal <>]

Thanks, this is about the proof length I had expected. I missed cardsT
and its interaction with powersetT. -- Cheers Christian.

On 01/13/2016 07:20 PM, Maxime Dénès wrote:
> Lemma card_set (T:finType) : #|{set T}| = 2^#|T|.
> by rewrite -!cardsT -powersetT -card_powerset.
> Qed.
> 
> Cheers,
> 
> Maxime.
> 
> On 01/13/16 18:42, Christian Doczkal wrote:
>> Hello
>>
>> Today I needed the following lemma with, surprisingly, I could not find
>> in the ssreflect component:
>>
>> Lemma card_set (T:finType) : #|{set T}| = 2^#|T|.
>>
>> I have a proof (see below), but the proof seems overly complicated.
>> Specifically, I did not manage to exploit that {set T} is defined in
>> terms of finite function types for which a cardinality lemma exists.
>>
>> Can someone show me a simpler proof that exploits the definition of
>> set_type?
>>
>> Cheers
>> Christian
>>
>> ------------------------------------------------------------------------
>>
>> Require Import mathcomp.ssreflect.ssreflect.
>>  From mathcomp Require Import all_ssreflect.
>>
>> Set Implicit Arguments.
>> Unset Strict Implicit.
>> Unset Printing Implicit Defensive.
>>
>> Lemma inj_leq_card (T T' : finType) (f : T -> T') :
>>    injective f -> #|T| <= #|T'|.
>> Proof. move => inj_f. by rewrite -(card_imset predT inj_f) max_card. Qed.
>>
>> Lemma bij_card {X Y : finType} (f : X->Y): bijective f -> #|X| = #|Y|.
>> Proof.
>>    case => g /can_inj Hf /can_inj Hg. apply/eqP.
>>    by rewrite eqn_leq (inj_leq_card Hf) (inj_leq_card Hg).
>> Qed.
>>
>> Lemma card_set (T:finType) : #|{set T}| = 2^#|T|.
>> Proof.
>>    suff H: #|{set T}| = #|{ffun pred T}|
>>      by rewrite H card_ffun card_bool.
>>    pose f (X:{set T}) := [ffun x => x \in X].
>>    pose g (F:{ffun pred T}) := [set x | F x].
>>    apply : (bij_card (f := f)). apply: (Bijective (g := g)).
>>    - move => X. rewrite /f /g. apply/setP => x. by rewrite inE ffunE.
>>    - move => F. rewrite /f /g. apply/ffunP => x. by rewrite ffunE inE.
>> Qed.
>