Ssreflect Users Discussion List

[Assia Mahboubi <>]

Hello Florent,

sorry for this late follow-up to your questions.

Le 12/02/2016 00:43, Florent Hivert a écrit :

> 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 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 ?

One basic pattern you can use for this purpose the subType interface:

https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/eqtype.v#L12

and more precisely the insub construction:

https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/eqtype.v#L53

or its transparent version:

https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/eqtype.v#L65

The subType interface provides support to work with types "isomorphic" to
boolean sigma-types, like {x : T | P x = true} (with P : T -> bool).

True boolean sigma types{x : T | P x = true}   are canonical instances of
subtypes of T. Thus for instance they inherit all the "combinatorial" 
structures
(eqtype, fintype, ...) available on T. But an other interesting tool is this
insub constant : it implements a partial projection from T to a subType of T,
using an option type: if (x : T), (insub x) is either Some y if P x = true or
None if P x = false. In the first case, you get a term y that lives in the
subType (the one specified by the  type constraints of your context). And you
can use y to compute your "counter-example".

In order to make this discourse clearer, I attach an example based on your
initial question and which implements the function you asked for. I hope it is
commented enough to illustrate that once you have proved that:
~~ trivIset P -> exists ...
the rest of the job can be done by generic constructions.

Hope this helps,

assia


> 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.
>

Attachment: florent_trivIset.v
Description: application/save-to-disk