The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

On Mon, Jul 15, 2013 at 2:02 PM, Arnaud Spiwack
<aspiwack AT lix.polytechnique.fr>
 wrote:

> The last two propositions are equivalent <...>. The T + { a = remove } is
> different though. In particular it allows you to return a T even if 
> a=remove.

But I can do that with all three:

Fixpoint f (n: nat) : n <> 0 -> nat.
  intro; exact 42. Defined.

Fixpoint f' (n: {m: nat | m <> 0}) : nat.
  exact 42. Defined.

Fixpoint f'' (n: nat) : nat + {n = 0}.
  exact (inleft 42). Defined.

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

I've started using this idiom. Let's see how that goes. :-)

--
www.mhelvens.net