The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

The last two propositions are equivalent (trivially so, even, so it makes little difference which one you use, the one using "subtype" plays better with the Program keyword, and the one without subtype is better with the apply tactic, but it's small differences really). The T + { a = remove } is different though. In particular it allows you to return a T even if a=remove. The only thing you know is that if you fail then a=remove. Besides any kind of correspondence between this form and the other two, relies on the decidability of the proposition a=remove.

If we are willing to make the hypothesis that your index type Op is indeed an inductive type, there is an alternative idiom which may be even better for your uses:

Definition do_stuff (a: Op) : match a with remove => True | _ -> T end.

Here you never have to provide a proof yourself. However, you'll exchange this for more annotations on pattern matchings over Op.

In practice, you pretty much have to experiment with various options to figure which one you are most comfortable with.

On 14 July 2013 19:16, Michiel Helvensteijn <mhelvens AT gmail.com> wrote:

On Sun, Jul 14, 2013 at 6:54 PM, Pierre-Marie Pédrot
<pierre-marie.pedrot AT inria.fr> wrote:

> For efficiency reasons, I would personally favor the
>
> T + { a = remove }

I have two questions about this idiom:

(1)  In what sense is it more efficient?
(2)  If I know that (a <> remove), how do I extract a return value of
type T? It's probably simple, but I've so far been unable to do this.

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

Ah, indeed. I understand the alternatives you suggest. In this case,
however, my work is more about proofs than programs. The programs I'm
writing are only examples.

Thanks!

--
www.mhelvens.net