Define NoDup_dec with Defined instead of Qed

[olympichek]

This pull request will close issue #125

[proux01]

@rocq-prover/stdlib-maintainers could anyone have a look please (I'm not qualified myself about those transparencies questions, their impact in terms of performances,...)

[ppedrot]

I think this is a very bad idea. It exposes bits of proofs constructed via tactics and that's a big no-no. Furthermore it's probably not usable in practice due to these huge proof terms creeping in.

Across the decades we've been taking nonsense design decisions in the stdlib out of inertia, but the proper way to do this is to write a decision function returning a boolean and prove that indeed it reflects the predicate.

[Villetaneuse]

Following @ppedrot's remark, I have just played around with adding memb and nodupb boolean operations, together with reflection lemmas (and weaker lemmas, more usable in vanilla).
Here is the result, I don't know if it goes in the right direction. This is
#132
But TBH, I'm not so sure it should make it, it's mostly to discuss about the future of List.
@olympichek what it proposes is to use a boolean function directly, named nodupb (can be changed) in definitions, and lemmas relating it to NoDup for proving

[olympichek]

I agree with @ppedrot that defining a boolean function and a lemma of equivalence is a better way to go.
Thank you for your work, @Villetaneuse

[ppedrot]

Relatedly, I think that the time is more than ripe for a general guideline about what should be Defined and what should be Qed in the stdlib. The not-so-recent introduction of SProp is also a great guiding principle for this.

[Villetaneuse]

@olympichek given recent discussions about the Stdlib (and my own feelings, TBH), I really don't think the linked PR will make it in the near future, it would require many changes in the general organization of the Stdlib and very important design choices to be made.
In the meantime, do not hesitate to use this work if it's useful for you.

[Villetaneuse]

Relatedly, I think that the time is more than ripe for a general guideline about what should be Defined and what should be Qed in the stdlib. The not-so-recent introduction of SProp is also a great guiding principle for this.

What you seem to suggest is never to use Defined and use boolean functions instead with reflection principles.
That's fine by me, if we get some of the machinery of ssreflect to work with reflections.
I don't understand the part about SProp, but maybe we can discuss it after I have played a bit with it.

[andres-erbsen]

I've created a design issue about the open questions here: #165 I'm closing this PR for now -- if the design does end up including something like this, we can always revive it.