Prove that the powerset of a finite set is finite using Coq
Asked Answered
K

1

7

While trying to prove some things, I encountered an innocent looking claim that I failed to prove in Coq. The claim is that for a given Finite Ensemble, the powerset is also finite. The statement is given in the Coq code below.

I looked through the Coq documentation on finite sets and facts about finite sets and powersets, but I could not find something that deconstructs the powerset into a union of subsets (such that the Union_is_finite constructor can be used). Another approach may be to show that the cardinal number of the powerset is 2^|S| but here I certainly have no idea how to approach the proof.

From Coq Require Export Sets.Ensembles.
From Coq Require Export Sets.Powerset.
From Coq Require Export Sets.Finite_sets.

Lemma powerset_finite {T} (S : Ensemble T) :
  Finite T S -> Finite (Ensemble T) (Power_set T S).
Proof.
  (* I don't know how to proceed. *)
Admitted.
Klecka answered 21/5, 2019 at 14:30 Comment(5)
I have a related result here, showing that the powerset of a finite set is also a finite set. But it relies on a different representation of finite sets, namely as ordered lists. Your result will certainly need the extensionality axiom for ensembles (Extensionality_Ensembles), and maybe also classical logic.Hemangioma
Don't know if it is relevant, but it is impossible to prove that exponentiation is total in bounded arithmetic (I don't have a good link for that claim, but see Edward Nelson's book "Predicative Arithmetic"). This suggests that any such proof will need to use some relatively powerful principles.Homicide
@ArthurAzevedoDeAmorim that is a good point. This is just part of some learning and I wouldn't mind introducing an axiom if I can then manage to proceed the proof. In general I found it interesting so far how even reasoning that other fields may consider strict or formal (such as proofs about automata) are pretty hard to translate to Coq.Klecka
Learning Coq does take time. But a lot of things become easier once you get used to it. For instance, working with finite automata wouldn't be too difficult with a library of finite types and sets, along the lines of the link that I sent you.Hemangioma
@JohnColeman Coq's theory is quite powerful, going beyond constructive arithmetic. The issue here has more to do with the lack of extensionality for predicates, which is a pretty basic reasoning principle to add.Hemangioma
M
2

I did not solve it completely because I myself struggled a lot with this proof. I merely transferred it along your line of thought. Now the crux of problem is, proving the cardinality of power set of a set of n elements is 2^n.

From Coq Require Export Sets.Ensembles.
From Coq Require Export Sets.Powerset.
From Coq Require Export Sets.Finite_sets.
From Coq Require Export Sets.Finite_sets_facts.

Fixpoint exp (n m : nat) : nat :=
  match m with
    | 0 => 1
    | S m' => n * (exp n m')
  end.

Theorem power_set_empty :
  forall (U : Type), Power_set _ (Empty_set U) = Singleton _ (Empty_set _).
Proof with auto with sets.
  intros U.
  apply Extensionality_Ensembles.
  unfold Same_set. split. 
  + unfold Included. intros x Hin.
    inversion Hin; subst. 
    apply Singleton_intro.
    symmetry. apply less_than_empty; auto.

  + unfold Included. intros x Hin.
    constructor. inversion Hin; subst.
    unfold Included; intros; assumption.
Qed.

Lemma cardinality_power_set :
  forall (U : Type) (A : Ensemble U) (n : nat),
    cardinal U A n -> cardinal _ (Power_set _ A) (exp 2 n).
Proof.
  intros U A n. revert A.
  induction n; cbn; intros He Hc.
  + inversion Hc; subst. rewrite power_set_empty.
    Search Singleton.
    rewrite <- Empty_set_zero'.
    constructor; repeat auto with sets. 
  + inversion Hc; subst; clear Hc.
Admitted.



Lemma powerset_finite {T} (S : Ensemble T) :
  Finite T S -> Finite (Ensemble T) (Power_set T S).
Proof.
  intros Hf.
  destruct (finite_cardinal _ S Hf) as [n Hc].
  eapply cardinal_finite with (n := exp 2 n).
  apply cardinality_power_set; auto.
Qed.
Myiasis answered 30/5, 2019 at 13:53 Comment(0)

© 2022 - 2024 — McMap. All rights reserved.