The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

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