The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

Thank you Jonathan,

On 18/02/15 17:15, Jonathan Leivent wrote:
>
> You would use the existT and exist constructors.  An example instance is:
> 
> (existT (fun n : nat => {m : nat & n < m}) 1 (exist (fun m : nat => 1 < m) 
> 2 (le_n 2)))
> 
> which Coq can infer from this much easier to read version:
> 
> (existT _ 1 (exist _ 2 (le_n 2)))

The above term seems absolutely lovely!

Although it does not seem to work in practise.

I have tried something simpler.

This works:

        Check exist (fun n => n < 10) 5 lt_5_10.

        (* where lt_5_10 : 5 < 10 *)

But here:

        Check exist _ 5 lt_5_10.

Coq complains:

        Error: Unable to unify "6 <= 10" with "?P 5" (cannot unify "?P 5" and 
"6 <= 10").

Similarly; this works:

        Check existT (fun n => {m | n < m}) 5 (exist (fun m => 5 < m) 10 
lt_5_10).

Also this works:

        Check existT (fun n => {m | n < m}) 5 (exist _ 10 lt_5_10).

But this:

        Check existT _ 5 (exist _ 10 lt_5_10).

unfortunatelly does not work. I am getting again:

        Error: Unable to unify "{x : nat | 5 < x}" with "?T 5" (cannot unify 
"?T 5" and "{x : nat | 5 < x}").

I am curious, is this supposed to work?
(I guess not, but now I am curious)

Thanks in advance!