Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
Require Import finfun bigop finset.

Lemma tuto_iffP :
  forall (P Q : Prop) (b : bool),
       reflect P b -> (P -> Q) -> (Q -> P) -> reflect Q b.
move => P Q [ | ].
  move => pt pq qp; apply: ReflectT (pq _).
  by move: {1 3}true pt (refl_equal true) => b; case.
move => pf pq qp; apply ReflectF; move/qp. 
by move: {1 3} false pf (refl_equal false) => b; case.
Qed.

(* We plan to use any finite type as the type of vertices.  It has an inherent
  order, given by the order of appearance in the finite type's enumeration.
  I still don't know how to recover this order, but I am not sure this is
  needed, because the order was only used to establish a direct correspondance
  between lists and sets of vertices. *)

Module Type context.

Variable V : finType.

End context.

Module first_try (CTXT : context).
Import CTXT.

Definition simplex := {set V}.

(* The reunion of all sets of parts of simplexes in s. This takes care
  of removing duplicates.  To describe the powerset, I take all parts
  of the whole set intersected with x. *)

Definition powerset (x : simplex) : {set simplex} := setT ::&: x.

Lemma powersetE :
  forall (x : simplex) (y : simplex), y \in powerset x -> y \subset x.
(*   forall z, z \in y -> z \in x. *)
Proof.
rewrite /powerset.  rewrite /ssetI; move => x y.
rewrite [y \in _]inE. 
by move/andP => [_].
Qed.

Lemma in_powerset : forall (x y : simplex), y \subset x -> y \in powerset x.
Proof.
move => x y xy; rewrite inE.
rewrite xy andbT.
by [].
Qed.

(* utiliser bigcup_sup *)

Definition create_sc (s : seq simplex) : {set simplex} :=
  \bigcup_(sp <- s) powerset sp.

Definition good_sc (c : {set simplex}) :=
    forall x, x \in c -> forall y : simplex, y \subset x ->  y \in c.

Lemma create_sc_good : forall (s : seq simplex), good_sc (create_sc s).
(*   forall x, x \in create_sc s -> forall y : {set V}, y \subset x ->
  y \in create_sc s. *)
move => s. set c := create_sc s. 
rewrite /good_sc.
move => x xc y yx; rewrite /c /create_sc.
rewrite bigcup_seq; apply/bigcupP.
move: xc.
rewrite /c /create_sc.
rewrite bigcup_seq; move/bigcupP => [si sis xsi].
exists si; first by [].
apply: in_powerset.
apply: subset_trans yx _.
by apply: powersetE.
Qed.

Definition facet (c : {set simplex}) (x : simplex) :=
   [set y : simplex | (x \subset y) && (y \in c)] == [set x].

Definition facets (c : {set simplex}) := [set x : simplex | facet c x].

Lemma in_facets :
  forall c : {set simplex}, forall x : simplex, x \in facets c ->
      (x \in c) /\ (forall y, (y \in c) -> (x \subset y) -> (x == y)).
move => c x; rewrite /facets /facet.
rewrite inE.
rewrite eqEsubset. case/andP.
move/subsetP => inx; move/subsetP => xin.
split.
  have xx : x \in [set x] by apply/set1P.
  by move: (xin x xx); rewrite inE; case/andP.
move => y yc xy; apply/eqP; symmetry; apply/set1P.
by apply: inx; rewrite inE yc xy.
Qed.

Lemma facet_in : forall c x, facet c x -> x \in c.
Proof.
move => c x fcx;  move: (in_facets c x).
rewrite /facets inE.
by move => h; move: (h fcx) => {h}; case.
Qed.

Lemma facet_in_csc : forall (s : seq simplex) (x : simplex),
   facet (create_sc s) x -> x \in s.
elim.
  move => x fx; have fx': x \in facets (create_sc [::]) by rewrite in_set.
  case: (in_facets _ _ fx').
  by rewrite /create_sc; rewrite big_nil; rewrite in_set0.
rewrite /facet => si s Hs x; rewrite eqEsubset; case/andP => inx xin.
case insi : (si \in create_sc s).
  rewrite /= inE; apply/orP; right.
  apply: Hs.
  rewrite eqEsubset; apply/andP; split.
    apply: subset_trans inx.
    apply/subsetP => z; rewrite !inE.
    case/andP => ->  h' /=.
    by rewrite /create_sc big_cons inE h' orbT. 
  rewrite sub1set inE;apply/andP; split; first by [].
  move: xin; rewrite sub1set inE.
  case/andP => _; rewrite /create_sc big_cons.
  move/setUP => [xsi | xs]; last by [].
  apply: (create_sc_good s _ insi).
  by apply: powersetE.
move: xin; rewrite sub1set inE.
case/andP => _; rewrite /create_sc big_cons.
move/setUP => [xsi | xs].
  have : x == si.
    rewrite eq_sym -in_set1.
    move/subsetP: inx => inx; apply: (inx si).
    rewrite inE powersetE //=.
    rewrite /create_sc big_cons.
    rewrite inE; apply/orP; left.
    by apply in_powerset.
  by rewrite inE => ->.
move: xs; rewrite -[\bigcup_(j<-s) _]/(create_sc s) => xs.
apply/orP; right; apply: Hs.
rewrite eqEsubset sub1set; apply/andP; split.
  apply: subset_trans inx.
  apply/subsetP => z; rewrite !inE; case/andP => -> zs /=.
  by rewrite /create_sc big_cons; apply/setUP; right.
by rewrite inE; apply/andP.
Qed.

(*
Lemma facets_preserve :
  forall s : seq simplex, facets [set x | x \in s ] = facets (create_sc s).

*)
End first_try.

Module second_try (CTXT : context).

Import CTXT.

Definition simplex := {set V}.

(* This time, I use the provided notion of powerset. *)

Definition powerset (x : simplex) : {set simplex} :=
   [set y | powerset (mem x) (finfun_of_set y)].

(*
Lemma powersetE :
  forall (x : simplex) (y : simplex), y \in powerset x -> y \subset x.
move => x y.
rewrite /powerset inE /finfun.powerset /=.
move/pffun_onP => [ A _ ]; rewrite subsetE.
apply/pred0P => z /=.
case h: (z\in y); last by rewrite andbF.
move: (A z); rewrite /support /= => Az; rewrite Az /= {Az}; first by [].
move: h.
case y => yf.
*)
End second_try.

Module third_try (CTXT : context).
Import CTXT.

Definition simplex := {set V}.

(* The reunion of all sets of parts of simplexes in s. This takes care
  of removing duplicates.  To describe the powerset, I take all parts
  of the whole set intersected with x. *)

Definition powerset (x : simplex) : {set simplex} := setT ::&: x.

Lemma powersetE :
  forall (x : simplex) (y : simplex), y \in powerset x -> y \subset x.
(*   forall z, z \in y -> z \in x. *)
Proof.
rewrite /powerset.  rewrite /ssetI; move => x y.
rewrite [y \in _]inE. 
by move/andP => [_].
Qed.

Lemma in_powerset : forall (x y : simplex), y \subset x -> y \in powerset x.
Proof.
move => x y xy; rewrite inE.
rewrite xy andbT.
by [].
Qed.

(* utiliser bigcup_sup *)

Definition create_sc (s : {set simplex}) : {set simplex} :=
  \bigcup_(sp \in s) powerset sp.

Definition good_sc (c : {set simplex}) :=
    forall x, x \in c -> forall y : simplex, y \subset x ->  y \in c.

Lemma create_sc_good : forall s, good_sc (create_sc s).
move => s x xc y yx.
rewrite /create_sc.
apply/bigcupP.
move: xc.
rewrite /create_sc.
move/bigcupP  => [si sis xsi].
exists si; first by [].
apply: in_powerset.
apply: subset_trans yx _.
by apply: powersetE.
Qed.

Definition facet (c : {set simplex}) (x : simplex) :=
   [set y : simplex | (x \subset y) && (y \in c)] == [set x].

Definition facets (c : {set simplex}) := [set x : simplex | facet c x].

Lemma in_facets :
  forall c : {set simplex}, forall x : simplex, x \in facets c ->
      (x \in c) /\ (forall y, (y \in c) -> (x \subset y) -> (x == y)).
move => c x; rewrite /facets /facet.
rewrite inE.
rewrite eqEsubset. case/andP.
move/subsetP => inx; move/subsetP => xin.
split.
  have xx : x \in [set x] by apply/set1P.
  by move: (xin x xx); rewrite inE; case/andP.
move => y yc xy; apply/eqP; symmetry; apply/set1P.
by apply: inx; rewrite inE yc xy.
Qed.

Lemma facet_in : forall c x, facet c x -> x \in c.
Proof.
move => c x fcx;  move: (in_facets c x).
rewrite /facets inE.
by move => h; move: (h fcx) => {h}; case.
Qed.

Lemma facet_in_csc : forall (s : {set simplex}) (x : simplex),
   facet (create_sc s) x -> x \in s.
move => s; move: {2}#|s| (refl_equal #|s|) => n; elim: n s.
  move => s s0 x fx; have fx': x \in facets (create_sc s) by rewrite in_set.
  case: (in_facets _ _ fx').
  move/eqP: s0; rewrite cards_eq0; move/eqP => ->.
  by rewrite /create_sc big_set0 in_set0.
rewrite /facet => n Hn s' cards' x; rewrite eqEsubset; case/andP => inx xin.
have : (s' != set0) by rewrite -card_gt0 cards'.
move/set0Pn => [si sis].
have s'dec : s' = si |: (s' :\ si) by rewrite setD1K.
have cards'2 :  #|s' :\ si| = (si \in s') + #|s' :\ si| - 1 by
  rewrite sis subSS subn0.
case insi : (si \in create_sc (s' :\ si)).
  rewrite -(setD1K sis) /= inE; apply/orP; right.
  apply: Hn; first by rewrite cards'2 -cardsD1 cards' subSS subn0.
  rewrite eqEsubset; apply/andP; split.
    apply: subset_trans inx.
    apply/subsetP => z; rewrite !inE.
    case/andP => ->  h' /=.
    by rewrite /create_sc (big_setD1 _ sis) inE h' orbT. 
  rewrite sub1set inE;apply/andP; split; first by [].
  move: xin; rewrite sub1set inE.
  case/andP => _; rewrite /create_sc (big_setD1 _ sis).
  move/setUP => [xsi | xs]; last by [].
  apply: (create_sc_good (s' :\ si) _ insi).
  by apply: powersetE.
move: xin; rewrite sub1set inE.
case/andP => _; rewrite /create_sc (big_setD1 _ sis).
move/setUP => [xsi | xs].
  have : x == si.
    rewrite eq_sym -in_set1.
    move/subsetP: inx => inx; apply: (inx si).
    rewrite inE powersetE //=.
    rewrite /create_sc (big_setD1 _ sis).
    rewrite inE; apply/orP; left.
    by apply in_powerset.
  by move/eqP => ->.
move: xs; rewrite -[\big[_/_]_( i \in _) _]/(create_sc (s' :\ si)) => xs.
rewrite s'dec inE; apply/orP; right; apply: Hn.
  by rewrite cards'2 -cardsD1 cards' subSS subn0.
rewrite eqEsubset sub1set; apply/andP; split.
  apply: subset_trans inx.
  apply/subsetP => z; rewrite !inE; case/andP => -> zs /=.
  by rewrite /create_sc (big_setD1 _ sis); apply/setUP; right.
by rewrite inE; apply/andP.
Qed.

End third_try.