Hi all,
I am perplexed by this piece of Coq code, which defines the bijectivity of a function:
Definition injective {A B} (f : A -> B) := forall x y : A, f x = f y -> x = y.
Definition surjective {A B} (f : A -> B) := forall y : B, exists x, f x = y.
Definition bijective {A B} (f : A -> B) := injective f /\ surjective f.
Definition idf {A} (x : A) := x.
Lemma id_bij {A : Type} : bijective idf.
Admitted.
Coq dismisses this because it cannot find an instance for the B : Type in bijective. However, the identity function has type A -> A, i.e. I want Coq to understand that in this case, A = B. Is there any way to avoid explicit argument passing using @ ?
I am not sure it is really about understanding that A = B. I think both A and B are unknown: nothing tells us which A has to be considered as implicit argument of idf in the statement of id_bij.
Why do you think Coq should be able to infer it? Lemma id_bij {A : Type} : bijective (@idf nat). is accepted. Lemma id_bij {A} : bijective (@idf A). is accepted.
There does not seem to be a reason why Coq should choose one rather than the other.
I think the confusion in the original question comes from the fact that two bound variables seemingly have the same name A. Therefore, a human user might believe that they are somehow related, but they are really different. The definition Definition idf {A} (x : A) := x. really has the same meaning has Definition idf {C} (x : C) := x. and in this case one is less drawn to think that the A in id_bij should be the same as the C in idf.