We have

eq_ind =
λ (A : Type) (x : A) (P : A → Prop) (f : P x) (a : A) (e : x = a),
  match e in (_ = a0) return (P a0) with
  | erefl _ _ => f
     : ∀ (A : Type) (x : A) (P : A → Prop),
         P x → ∀ a : A, x = a → P a
Arguments eq_ind [A]%type_scope x P%function_scope f y e
  (where some original arguments have been renamed)

Here only the first argument is implicit. Indeed, in the standard Coq library Coq.Init.Logic, there is:

Arguments eq_ind [A] x P _ y _ : rename.

We could make x and y (initially a) implicit and have instead:

Arguments eq_ind [A] [x] P _ [y] _ : rename.

The advantages seem to me obvious: instead of providing five arguments it would be enough to provide only three arguments. Since the standard library does not make x and y implicit, I thought that there are probably good reasons for that. So, my question is: is there any drawback in making x and y implicit?

More generally, when some arguments can be made implicit because they can be deduced from the other arguments, are there sometimes good reasons to avoid making them implicit?

  • 1
    $\begingroup$ It is possible to make Coq set implicit arguments automatically. Check out the flags starting here in the refman. I don't know why they are off by default, but my guess would be (new) user-friendliness. MathComp has the oposite default. $\endgroup$
    – Ana Borges
    Jan 14 at 20:03

1 Answer 1


One potential reason is partial application: if you often want to apply eq_ind to all its arguments except the proof of equality (getting something of type x = y -> P y), then making x and y implicit is annoying, because you have to write @eq_ind _ x P f y instead of eq_ind x P f y, since without the last argument Coq cannot infer x or y.

Although, in this particular case, I am not sure this is really the reason…


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.