Library prosa.classic.util.powerset

Require Import prosa.classic.util.tactics.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop tuple.

Section PowerSet.

  (* Based on https://www.ps.uni-saarland.de/formalizations/fset/html/libs.fset.html *)
  Definition powerset {T: eqType} (l: seq T) : seq (seq T) :=
    let mT := ((size l).-tuple bool) in
      (map (fun m : mT ⇒ (mask m l)) (enum {: mT})).

  Lemma mem_powerset {T: eqType} (x: seq T) y :
    y \in (powerset x) → {subset y ≤ x}.

End PowerSet.