"Not bound variables at all" but also can't find and instance

Using Coq
1

Hello, I’m struggling a bit with the standard library.

I implemented a Module of type OrderedTypeFull' and from it got a TotalTransitiveLeBool by using OTF_to_TTLB. So I have a module X with the lemma “leb_trans”.
My problem is that I have something like this:

H1: X.leb a b = true 
H2: X.leb b c = true

and I would like to get that X.leb a c = true, by applying leb_trans.

If I try to just apply X.leb_trans in H I get: " Unable to find an instance for the variable z."

Makes sense, so I try : apply X.leb_trans with (z:=c) in H1. and I get: " No such bound variable z (no bound variables at all in the expression)."

This confuses me because clearly leb_trans is defined by this Transitive definition so I have “x” “y” and “z” and I want to provide “c” as the “z”. The same happens when I try to provide the 3 arguments.

Is something wrong on how I want to use the transitive lemma?

2

Presumably, the declaration of X.leb_trans does not have the signature you point out. (Even if a lemma satisfies a given class signature, that does not necessarily mean that it names the arguments in the exact same way as the class.) Could you try About X.leb_trans to see what the actual argument names are?

3

I do get arguments x y z:

X.leb_trans : Transitive (fun x y : timePoint => is_true (X.leb x y))

X.leb_trans is not universe polymorphic
Expanded type for implicit arguments
X.leb_trans : forall [x y z : timePoint], 
(fun x0 y0 : timePoint => is_true (X.leb x0 y0)) x y -> 
(fun x0 y0 : timePoint => is_true (X.leb x0 y0)) y z -> X.leb x z = true
4

The fact that About does not display the following line

Arguments X.leb_trans x y z _ _

seems to indicate that Coq did not recognize that there were some named arguments.

5

Actually, I think the issue comes from the fact that the arguments are declared as implicit (i.e., the square brackets in forall [x y z : timePoint], ...). I am not quite sure whether this is a bug or a feature.