最大与非最大隐式参数的目的 [英] Purpose of maximal vs non-maximal implicit arguments

问题描述

我刚刚发现存在最大和非最大参数（请参见 https://coq.inria.fr/refman/Reference-Manual004.html#sec109 ）。

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

但是是否有一些动机可以在其中使用一个其他？一个比另一个最近吗？最大的隐式参数只需要创建 {} ，而必须使用 Arguments 或隐式参数指定非最大参数。

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.

最大插入的隐式（MII）参数为该语言增加了下一层的隐式性。
普通（非MII）参数仅在将函数应用于至少一个参数时才插入。此外，Coq仅在之前插入某些提供的显式自变量的那些自变量。

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自变量更渴望： Coq认为在后面后面提供了一些显式自变量。一个极端的例子：如果函数的签名以MII参数开头，则只需提及函数名称（即使没有应用），也可以让Coq将其转换为部分应用的函数（非MII参数则不会发生）。有时候这种急切的行为有助于编写简洁的代码，有时又有点麻烦，因为它迫使我们插入其他多余的 @ 符号来抑制隐式参数的插入。

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.

序言：

Require Import Coq.Lists.List. Import ListNotations.

Section Length.
  Variable A:Type.

length 函数的开头不是MII参数：

The length function has non-MII first argument:

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

这就是以下简单代码失败的原因（它失败是因为 length 应用，因此未插入 A ）：

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).

另一种方法是使用MII参数。直观地讲，在这种情况下，Coq用（@ length _）替换 length ：

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.

---

但有时插入的最大参数正在进入，当您想使用某种函数或最一般形式的构造函数（未部分应用）时。一个来自 Coq.Lists.List 模块的非MII参数的工作示例：

---

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.

但是确切的Forall2_nil 无效MII论证的情况。 构造函数将为我们提供帮助，

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.

---

还有一个过早的隐式参数插入实例（来自 Coq.Init.Logic ）。这适用于非MII参数：

---

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.

---

有时的格式为<战术名称> ...与（_：= _）。在存在MII参数的情况下将失败。这是来自 Coq.Init.Logic 的另一个（有效的）示例：

---

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.

但是MII的论点阻碍了我们的进步：

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.

最大的隐式参数只需要创建 {} ，而必须使用 Arguments 或隐式参数来指定非最大值。

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 ?

默认情况下，指令 Set Implicit Arguments。声明非最大插入的隐式参数。因此，Coq对于隐含性的级别是保守的（但不是太多）。默认情况下，我会坚持使用非MII参数，并在适当的地方插入 {} 。

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.

这篇关于最大与非最大隐式参数的目的的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！