The Coq mailing list

[Christian Doczkal <christian.doczkal AT inria.fr>]

Hi,

I can't say much about the reason for having this in the first place,
but I can point you to a library where it is used extensively: the
mathematical components library. A quick fgrep yields 222 occurrences.

I guess the main difference is that is saves a "destruct" whenever
eliminating an exisist2-hypothesis and a "split" whenever proving one.

Indeed mathcomp also introduces n-ary conjunctions and disjunctions so
one rarely nests multiple and/or operations.

Best,
Christian

On 4/17/20 7:51 PM, Maximilian Wuttke wrote:
> Hi Club,
> 
> I wondered for some time for what reason there is `ex2` in Coq's stdlib.
> In particular, it is trivial to prove the following:
> 
> ```
> Goal forall {X:Type} (P1 P2 : X -> Prop),
>     (exists2 x, P1 x & P2 x) <->
>     exists x, P1 x /\ P2 x.
> Proof. firstorder. Qed.
> ```
> 
> Are there any practical use cases were `ex2` would be any better than
> `ex`? Do you know Coq libraries where it is used?
> 
> To the country, I would argue that `ex` is more 'extensible': If you
> have to add one more proposition for `x`, you would have to use `/\` anyway.
> 
> --
> Maximilian
>