Purpose of maximal vs non-maximal implicit argumen

Question

I have just discovered the existence of maximal and non-maximal arguments (see https://coq.inria.fr/refman/Reference-Manual004.html#sec109).

But is there some motivation to use one over the other? Is one more recent than the other? Maximal implicit arguments simply need {} to be created, whereas one has to use Arguments or Implicit Arguments to specify non-maximal ones. Does it mean that maximal implicit arguments should be preferred?

Answer 1

... is there some motivation to use one over the other ?

Yes there is, but (as usual) "it depends". Let's first discuss a little bit the difference between them.

Maximally-inserted implicit (MII) arguments add the next level of "implicitness" to the language. Ordinary (non-MII) arguments get inserted only when a function is applied to at least one argument. Furthermore, Coq inserts those arguments only before some provided explicit argument.

MII arguments are more "eager": Coq considers them inserted after some supplied explicit argument. A corner case: if a function's signature starts with an MII argument, it suffices to mention the function name (even without application) for Coq to turn it into a partially applied function (it doesn't happen with non-MII arguments). Sometimes this eager behavior helps to write succinct code and sometimes its a bit of a nuisance, because it forces us to insert otherwise redundant @ symbols to suppress insertion of implicit arguments.

Let me show some simple examples, drawn mostly from the reference manual or the standard library.

Preamble:

Require Import Coq.Lists.List. Import ListNotations.

Section Length.
  Variable A:Type.

The length function has non-MII first argument:

  Print Implicit length.
  (*
  Output:
  length : forall A : Type, list A -> nat
  Argument A is implicit
  *)

That's why the following simple code fails (it fails because length is not partially applied, so A is not inserted):

  Fail Check (fun l:list (list A) => map length l).

One have to write something like this to make it work:

  Check (fun l:list (list A) => map (@length _) l).
  (* or *)
  Check (fun l:list (list A) => map (length (A := _)) l).
  (* or *)
  Check (fun l:list (list A) => map (fun xs => length xs) l).

Another way would be to use MII arguments. Intuitively, in this case Coq replaces length with (@length _):

  Arguments length {A} _.
  Check (fun l:list (list A) => map length l).
End Length.

---

But sometimes maximally inserted arguments are getting into the way, when one wants to use some function or a constructor in its most general form (not partially applied). A working example with non-MII arguments from the Coq.Lists.List module:

Set Implicit Arguments.  (* non-MII arguments is the default behavior *)
Inductive Forall2 A B (R:A->B->Prop) : list A -> list B -> Prop :=
 | Forall2_nil : Forall2 R [] []
 | Forall2_cons : forall x y l l',
    R x y -> Forall2 R l l' -> Forall2 R (x::l) (y::l').

Theorem Forall2_refl : forall A B (R:A->B->Prop), Forall2 R [] [].
Proof. exact Forall2_nil. Qed.

But exact Forall2_nil won't work in the case of MII arguments. The constructor will help us, though:

Arguments Forall2_nil {A B} _.
Theorem Forall2_refl' : forall A B (R:A->B->Prop), Forall2 R [] [].
Proof. Fail (exact Forall2_nil). constructor. Qed.

---

One more instance of premature implicit argument insertion (from Coq.Init.Logic). This works with non-MII arguments:

Declare Left Step eq_stepl.

But, here we have to add '@':

Arguments eq_stepl {A} _ _ _ _ _.
Fail Declare Left Step eq_stepl.
Declare Left Step @eq_stepl.

---

Sometimes tactics of the form <tactic-name> ... with (_ := _). will fail in the presence of MII arguments. Here is another (working) example from Coq.Init.Logic:

Definition eq_ind_r :
  forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y.
  intros A x P H y H0; elim eq_sym with (1 := H0); assumption.
Defined.

But MII arguments impede our progress:

Arguments eq_sym {A x y} _.
Definition eq_ind_r' :
  forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y.
  intros A x P H y H0.
  Fail elim eq_sym with (1 := H0); assumption.
  (* this works *)
  elim @eq_sym with (1 := H0); assumption.
  (* or this: *)
  elim (eq_sym H0); assumption.
Defined.

---

Is one more recent than the other ?

I don't know I hope someone could shed some light on it.

Maximal implicit arguments simply need {} to be created, whereas one has to use Arguments or Implicit Arguments to specify non-maximal ones. Does it mean that maximal implicit arguments should be preferred ?

By default, the directive Set Implicit Arguments. declares non-maximally inserted implicit arguments. So Coq is conservative (but not too much) about the level of implicitness. I'd stick to non-MII arguments by default, inserting {} where appropriate.