Ssreflect Users Discussion List

[(Emilio Jesús Gallego Arias)]

Hi Florent,

This is my try at your problem. I think it should be possible to prove
some properties of function "gen_not_triv" building the set you mentioned.

Best regards,
Emilio

From mathcomp
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.

From mathcomp
Require Import fintype bigop finset.

Section Florent.

Variable T : finType.
Implicit Types (A B : {set T}) (AB : {set T} * {set T}) (P : {set {set T}}).

Definition set00 : {set T} * {set T} := (set0, set0).
Definition cond_triv AB := (AB.1 != AB.2) && (AB.1 :&: AB.2 != set0).

Definition replace_byU A B P := (A :&: B) |: P :\: [set A; B].

Lemma ax P : exists AB, ~~ trivIset P ==> cond_triv AB.
Proof.
have [|/=] := @trivIsetP _ P => ht; first by exists set00.
suff: ~ forall AB, (AB.1 == AB.2) || (AB.1 :&: AB.2 == set0).
  move/forallP; rewrite negb_forall; case/existsP=> ab.
  by rewrite negb_or => /andP[h1 h2]; exists ab; rewrite /cond_triv h1 h2.
move=> ht'; apply: ht => a b _ _ /eqP ab_neq; have := ht' (a, b).
by rewrite -setI_eq0; case/orP => //= /eqP.
Qed.

Lemma axC P : { AB | ~~ trivIset P ==> cond_triv AB }.
Proof. exact : sigW (ax _). Qed.

Definition choose_sets P :=
  if trivIset P then set00
  else choose cond_triv (projT1 (axC P)).

Definition choose_setsP P : ~~ trivIset P ->
  cond_triv (choose_sets P).
Proof.
rewrite /choose_sets; case: ifP => // /negbT tsn _.
by apply: chooseP; case: (axC P) => //= x; rewrite tsn.
Qed.

Definition gen_not_triv P :=
  if trivIset P then P
  else let: (A, B) := choose_sets P in
       replace_byU A B P.

End Florent.