The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 14/07/2013 13:59, Michiel Helvensteijn wrote:
> I'm trying to decide which to go ahead with. In your experience, what
> are the advantages and disadvantages of each of these choices in
> practice? Which do you prefer?

For efficiency reasons, I would personally favor the

T + { a = remove }

idiom. Actually, if you plan on writing programs rather than proofs, I 
would even get rid of the dependency and write it in two parts, as a 
partial function and a specification lemma :

Definition bla (a : Op) : option T.

Lemma bla_spec : forall a, a <> remove -> bla <> None.

This is more efficient when you're going to compute with your proofs, as 
you won't be manipulating ugly terms representing (morally irrelevant) 
proofs.

Introducing even more type dependency, there is also a presentation you 
forgot, which works in your particular case :

Definition bla (a : Op) : match a with remove => unit | Some _ => T end.

This is isomorphic to the option presentation, and at the same time you 
get the specification lemma for free.

PMP