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: 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: Tue, 16 Jul 2013 09:50:31 +0200



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.
 

Of course, but you misunderstood the sense of my remark. Your first question was whether all three form were equivalent, and they aren't (as long as we understand equivalent to mean isomorphic). In the case of  forall n:nat, n<>0 -> nat  the function cannot even be called if n=0. When the type is forall n:nat, nat + { n=0 } then not only can it be called but it can return a natural number. Under the hypothesis that the side condition is decidable (which is the case for your examples), then forall n:nat, n<>0 -> nat is indeed isomorphic to something like forall n:nat, { _:nat | n<>0 } + { n = 0 }.

Not that there is anything wrong with your proposal, but it is a looser type, accepting more functions (for instance, despite appearances of the contrary, your f'' is a different function from f and f').



Archive powered by MHonArc 2.6.18.

Top of Page