Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] a simple question about "sigT".

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] a simple question about "sigT".


Chronological Thread 
  • From: Jonathan Leivent <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] a simple question about "sigT".
  • Date: Thu, 19 Feb 2015 14:47:24 -0500


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




Archive powered by MHonArc 2.6.18.

Top of Page