memb and nodupb in ListDec.v

[Villetaneuse]

Still a draft, request for comments

• reflect_iff_false in Bool/Bool.v to help work with reflect in vanilla
• memb and nodupb in List.dec with reflection principles (some weaker, again to help with vanilla apply) : membP, memb_In, memb_nIn, nodupbP, nodupb_NoDup, nodupb_nNoDup

What I'm not so sure about :

• the whole thing is parameterized by a proof named dec of strong decidability of equality (in sumbool), instead of eqb together with a reflection principle of eqb (maybe bundled in an eqType, as in mathcomp)
• I know, these are equivalent, via bool_of_sumbool and sumbool_of_bool, but still it encourages to use a, maybe strange and changing, proof of decidability in definitions, instead of a nice boolean function

But, if we change things this way :

• Maybe take eqType and most of seq from mathcomp in StdLib ? Or part of them ? In different files ? And keep ListDec (at least serveral versions) frozen for compatibility before removal ?

Fixes / closes #????

• Added changelog.
• Added / updated documentation.

• Opened overlay pull requests.

[ppedrot]

I think that this goes the right direction. The boolean decider should probably be made fully boolean, i.e. depend on a boolean function rather than a predicate decider. The full boolean version is a strict subtype of the other, so it's more expressive, and it furthermore ensures a strict stratification between ugly tactic-generated proofs and computational parts.