The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Mon, 25 Jul 2011 15:38:43 +0800,
Jean-Francois Monin 
<jean-francois.monin AT imag.fr>
 a écrit :

> Because A <-> B, by definition, is A -> B /\ B-> A.
> f : A -> B can be applied to an argument x:A,
> g: A <-> B cannot, only (fst g) can.

By the way it is (proj1 g) not (fst g)

Note that you can try to use Coercion to solve it.
Or also use fancy notations if you think that "fst" and "proj1" should
be unified or at ugly to read:

Notation "x '₁'" := (let (x, _) := x in x) (at level 0).
Notation "x '₂'" := (let (_, x) := x in x) (at level 0).

(There may be some error as I didn't tried it now, but I already
defined such a thing and it did work; for instance I am not sure for
the single quotes.)

Then after you can use "(bcoef_pos_ok n p) ₁" instead of
"(proj1 (bcoef_pos_ok n p))";

and it will also work for pairs.

Print ((1, 8) ₁).
====
1

and even for the witness of an existential (although it should not be
used for such a thing, as the notation is quite strange to be used in
a dependant sum, and may be misleading)

X : exists n, n>0
----
Check (X ₁).
====
X₁: nat


Of course, you can replace it with any ascii character (or sequence)
but '_1' won't be that pretty.

> 
> Hope this helps,
> JF
> 
> On Mon, Jul 25, 2011 at 10:27:21AM +0800, Ly Kim Quyen (Gwenhael)
> wrote:
> > Lemma bcoef_pos_ok : forall n (p : poly n), bcoef_pos n p = true <->
> > coef_pos n p.
> > 
> > Lemma bcoef_pos_ok_2 : forall n (p : poly n), bcoef_pos n p = true
> > -> coef_pos n p.
> > [...]
> > 
> > My question is: Why I cannot apply the lemma *bcoef_pos_ok* in this
> > definition?
> > I got the error saying that: "*The expression "bcoef_pos_ok n p" of
> > type "bcoef_pos n p = true <-> coef_pos n p"
> > cannot be applied to the term  "h0" : "bcoef_pos n p = true"* "
> > But if I am using the lemma *bcoef_pos_ok_2* it works.
> > 
> > Thank you very much,
> > Gwen