Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Subtype argument, precondition or sumor return type? Which to choose?

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



Archive powered by MHonArc 2.6.18.

Top of Page