The Coq mailing list

[Michiel Helvensteijn <mhelvens AT gmail.com>]

On Wed, Jul 17, 2013 at 9:42 AM, Hendrik Tews 
<tews AT os.inf.tu-dresden.de>
 wrote:

>    Thanks! You do make the sumor idiom seem very attractive. :-)
>
> Well, I should have added to my summary, that the sumor idiom may
> become a nuisance in expressing properties. I did not elaborate
> on that, because it is mostly obvious. With sumor, your function
> does not easily compose any more and therefore many of your
> theorems need a case distinction.

Yes, I understand.

I'm trying something new now. I develop the subtype version `st`. Then
I also implement the sumor version `so`, in terms of `st`, and prove a
companion lemma about the output of `so`:

Definition st (a: {o: Op | o <> remove}) : nat := 42.

Program Definition so (a: Op) : nat + {a = remove} :=
  match a with
  |  remove => inright eq_refl
  |  _      => inleft (st a)
  end.
Solve All Obligations using (congruence || discriminate).

Lemma so_st: forall a, (a = remove) -> (exists P, so a = inright P).
  intros a H; destruct a;
    (contradict H; discriminate) || (unfold so; eauto with *).
Qed.

The idea is that I can choose which to go with on a case by case
basis. Not sure yet if it works in practice.

--
www.mhelvens.net