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: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
- To: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?
- Date: Sun, 14 Jul 2013 18:54:32 +0200
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
- [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.