The Coq mailing list

[Arnaud Spiwack <arnaud.spiwack AT gmail.com>]

Right. I did (plus a lambda). Your point is well taken indeed :) .

On Jan 27, 2014 4:32 PM, "Guillaume Melquiond" <guillaume.melquiond AT inria.fr> wrote:

On 27/01/2014 16:13, Arnaud Spiwack wrote:

 >> Definition extension2 f x y := exists a, exists b, x a -> x b -> f a b
 >
 >
 > Unfortunately no.
 > In Why3, we display a warning whenever the user writes this kind of
predicate ; it has been helpful to debug some broken specifications
early. It might be worth having the same warning message in Coq.

I'm confused. Apart from the fact that I forgot an obvious lambda (f is
supposed to be of type A->B->(X->Prop)), this definition is a correct
binary extension for the powerset monad. Could you elaborate on the
issue you have with it?

My issue is that this kind of predicate is (almost) always a tautology, which makes it pointless. So I doubt it is what you intended to write in the first place. Didn't you mean the following instead?

Definition extension2 f x y := exists a, exists b, x a /\ x b /\ f a b.

Best regards,

Guillaume