coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?
Chronological Thread
- From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
- To: Michiel Helvensteijn <mhelvens AT gmail.com>
- Cc: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>, coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?
- Date: Mon, 15 Jul 2013 14:02:13 +0200
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.
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édrotI have two questions about this idiom:
<pierre-marie.pedrot AT inria.fr> wrote:
> For efficiency reasons, I would personally favor the
>
> T + { a = remove }
(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.
Ah, indeed. I understand the alternatives you suggest. In this case,
> 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 :
however, my work is more about proofs than programs. The programs I'm
writing are only examples.
Thanks!
--
www.mhelvens.net
- [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Michiel Helvensteijn, 07/14/2013
- Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Pierre-Marie Pédrot, 07/14/2013
- Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Michiel Helvensteijn, 07/14/2013
- Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Arnaud Spiwack, 07/15/2013
- Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Michiel Helvensteijn, 07/16/2013
- Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Arnaud Spiwack, 07/16/2013
- Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Michiel Helvensteijn, 07/16/2013
- Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Arnaud Spiwack, 07/16/2013
- Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Michiel Helvensteijn, 07/16/2013
- Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Arnaud Spiwack, 07/15/2013
- Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Michiel Helvensteijn, 07/14/2013
- Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Hendrik Tews, 07/16/2013
- Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Michiel Helvensteijn, 07/16/2013
- Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Hendrik Tews, 07/17/2013
- Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Michiel Helvensteijn, 07/17/2013
- Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Hendrik Tews, 07/17/2013
- Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Michiel Helvensteijn, 07/16/2013
- Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?, Pierre-Marie Pédrot, 07/14/2013
Archive powered by MHonArc 2.6.18.