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').
- [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.