The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 02/19/2015 01:33 PM, Matej Kosik wrote:
> 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  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.

The simpler term will work, but only where Coq is expecting the type you 
gave.  Hence the following does work:

Check (existT _ 1 (exist _ 2 (le_n 2))) : {n : nat & {m : nat | n < m}}.

Without the type, the type checker (invoked through Check) doesn't have 
the necessary info to fill in the holes ("_"'s).

Similarly if you had a goal, then the type checker would have the 
necessary info to fill in the holes:

Goal {n : nat & {m : nat | n < m}}.
Proof.
  exact (existT _ 1 (exist _ 2 (le_n 2))).
Qed.


If you want Coq to find an appropriate proof term in place of [le_n 2] 
above, you can do something like this:

Require Import Arith.
Goal {n : nat & {m : nat | n < m}}.
Proof.
  refine (existT _ 1 (exist _ 2 _)).
  auto with arith.
Qed.

If the predicate is more complex, you might need [omega] or something 
like it ([lia], for example) instead of [auto with arith].

-- Jonathan