coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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:The above term seems absolutely lovely!
(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)))
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
- [Coq-Club] a simple question about "sigT"., Matej Kosik, 02/18/2015
- Re: [Coq-Club] a simple question about "sigT"., Jonathan Leivent, 02/18/2015
- Re: [Coq-Club] a simple question about "sigT"., Matej Kosik, 02/19/2015
- Re: [Coq-Club] a simple question about "sigT"., Jonathan Leivent, 02/19/2015
- Re: [Coq-Club] a simple question about "sigT"., Matej Kosik, 02/19/2015
- Re: [Coq-Club] a simple question about "sigT"., Jonathan Leivent, 02/18/2015
Archive powered by MHonArc 2.6.18.