Ssreflect Users Discussion List

[Florent Hivert <>]

      Dear All,

Thanks to Georges, I managed to get something...

Here is my Goal: I'd like to write a function that given a P : {set {set t}}
- either returns P if trivIset P holds, that is the elements of P have trivial
  intersection;
- or finds two distinct intersecting sets A and B in P
  and replace them in P by their union
The actual return value is not important here, the question is more about
handling the counter example to trivIset P.

I got that in three steps:


Lemma trivIsetEn (T : finType) (P : {set {set T}}) :
  ~~ trivIset P =
  [exists A in P, [exists B in P, (A != B) && (A :&: B != set0)]].

Lemma trivIset_VpairI (T : finType) (P : {set {set T}}) :
  ( trivIset P ) +
  { AB : {set T} * {set T} |
    [/\ AB.1 \in P, AB.2 \in P, AB.1 != AB.2 & AB.1 :&: AB.2 != set0] }.

Definition join_inter (T : finType) (P : {set {set T}}) : {set {set T}}.
  case: (trivIset_VpairI P) => [_ | [[A B] _]].
  - exact P.
  - exact ((A :&: B) |: P :\: [set A; B]). (* replace A and B by their union 
*)
Defined.

I'd like to know if there is a more simpler or natural way. Here are some
comments:

- in trivIsetEn I only need the implication.

- trivIset_VpairI is merely a rephrasing of trivIsetEn; Still, I need it.
Indeed, I tried to merge the proof of trivIset_VpairI into the definition of
join_inter. I managed to get a working function join_inter_fail, where 
instead of
writing

  case: (trivIset_VpairI P)

in the definition of I wrote

  case: (boolP (trivIset P))
  - ...
  - rewrite trivIsetEn

However, with this second version, I can't manage to prove anything
useful. Indeed, having trivIsetEn (with a call to eq_rect) into the definition
leads to dependent type error if I try to make the same case analysis (case:
(boolP (trivIset P))) in a proof about join_inter_fail.

I think that, more generally, my question is the following. Is there some
basic pattern to write function which does something if a certain boolean is
true and otherwise compute something from a counter example ?

Thanks for any suggestion.

Best,

Florent



By the way, here is the complete code:

Lemma trivIsetEn (T : finType) (P : {set {set T}}) :
  ~~ trivIset P =
  [exists A in P, [exists B in P, (A != B) && (A :&: B != set0)]].
Proof.
  apply/idP/idP.
  - apply contraR; rewrite negb_exists_in => /forall_inP Hall.
    apply/trivIsetP => A B /Hall {Hall}.
    rewrite negb_exists_in => /forall_inP Hall/Hall{Hall} H Hneq.
    move: H; rewrite Hneq /= negbK => /eqP H.
    by rewrite -setI_eq0 H.
  - move=> /existsP [] A /andP [] HA /existsP [] B /andP [] HB /andP [] HAB 
Hn0.
    apply (introN idP) => /trivIsetP/(_ A B HA HB HAB) /disjoint_setI0 H.
    by move: Hn0; rewrite H eq_refl.
Qed.

Lemma trivIset_VpairI (T : finType) (P : {set {set T}}) :
  ( trivIset P ) +
  { AB : {set T} * {set T} |
    [/\ AB.1 \in P, AB.2 \in P, AB.1 != AB.2 & AB.1 :&: AB.2 != set0] }.
Proof.
  case: (boolP (trivIset P)) => H; [by left | right].
  move: H; rewrite trivIsetEn.
  move=> /existsP/sigW [] A /andP [] HA /existsP/sigW [] B /and3P [] HB Hneq 
H0.
  by exists (A, B).
Qed.

Definition join_inter (T : finType) (P : {set {set T}}) : {set {set T}}.
  case: (trivIset_VpairI P) => [_ | [[A B] _]].
  - exact P.
  - exact ((A :&: B) |: P :\: [set A; B]).
Defined.

(* Due to dependant type error, I can't prove anything about this function *)
Definition join_inter_fail (P : {set {set T}}) : {set {set T}}.
  case: (boolP (trivIset P)) => [_ |].
    exact: P.
  rewrite trivIsetEn => /existsP/sigW [] A /andP [] _ /existsP/sigW [] B _.
  apply ((A :&: B) |: P :\: [set A; B]).
Defined.