Докажите, что powerset конечного множества конечен, используя Coq

Question

Пытаясь доказать некоторые вещи, я столкнулся с невинно выглядящим утверждением, которое мне не удалось доказать в Coq. Утверждение состоит в том, что для данного конечного ансамбля powerset также конечен. Заявление приведено в коде Coq ниже.

Я просмотрел документацию Coq о конечных наборах и фактах о конечных наборах и наборах мощности, но я не смог найти что-то, что деконструирует набор питания в объединение подмножеств (такое, чтобы можно было использовать конструктор Union_is_finite). Другой подход может состоять в том, чтобы показать, что кардинальный номер блока питания равен 2 ^ | S | но здесь я, конечно, понятия не имею, как подойти к доказательству.

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.

Answer 1

Я не решил ее полностью, потому что сам много боролся с этим доказательством. Я просто перенес это по вашей линии мысли. Теперь суть проблемы в том, что мощность множества наборов из n элементов равна 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.