Ssreflect Users Discussion List

[Florent Hivert <>]

      Dear Emilio,

Thanks a lot for your code. It is indeed shorter than mine. After, rereading
it and reworking it I'm not sure to understand why ? Is there a specific trick
you can pinpoint that made it shorter or simpler and that I can remember and
reuse ? Or do you think, is it just that you know how to use ssreflect tactics
better than me.

Thank for your time,

Regards,

Florent


For the sake of completeness, you missed the Hypothesis that the two
intersecting block are in P in your cond_triv definition.

Definition cond_triv P AB :=
  [&& (AB.1 \in P), (AB.2 \in P), (AB.1 != AB.2) & (AB.1 :&: AB.2 != set0)].

It makes the proof of the ax lemma a little longer:

Lemma ax P : exists AB, ~~ trivIset P ==> cond_triv P AB.
Proof.
  suff: ~~ trivIset P -> [exists AB, cond_triv P AB].
    by case: (trivIset _) / boolP => /= _; [exists set00|move/(_ 
erefl)/existsP].
  apply contraR; rewrite negb_exists_in => /forallP hdis.
  apply/trivIsetP => A B HA HB AB_neq; have := hdis (A,B).
  by rewrite HA HB AB_neq /= setI_eq0 negbK.
Qed.