I have just discovered the existence of maximal and non-maximal arguments (see documentation).
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?
... 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 useArguments
orImplicit 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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With