coq - 最大与非最大隐式参数的目的

Question

我刚刚发现了最大和非最大参数的存在(见 documentation)。
但是是否有动机使用其中一种？一个比另一个更新吗？最大隐式参数只需要 {}要创建，而必须使用 Arguments或 Implicit Arguments指定非最大值。这是否意味着应该首选最大隐式参数？

Answer 1

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

是的，但是(像往常一样)“这取决于”。让我们首先讨论一下它们之间的区别。

最大插入隐式 (MII) 参数为语言添加了下一级的“隐式”。
仅当函数应用于至少一个参数时，才会插入普通(非 MII)参数。此外，Coq 仅插入这些参数 之前 一些提供了明确的论据。

MII 参数更“急切”:Coq 认为它们已插入 之后 一些提供了明确的论点。一个极端情况:如果一个函数的签名以 MII 参数开头，那么只需提及函数名称(即使没有应用程序)，Coq 就可以将其转换为部分应用的函数(非 MII 参数不会发生这种情况)。有时这种急切的行为有助于编写简洁的代码，有时它有点令人讨厌，因为它迫使我们插入其他多余的 @禁止插入隐式参数的符号。

让我展示一些简单的示例，这些示例主要来自引用手册或标准库。

前言:

Require Import Coq.Lists.List. Import ListNotations.

Section Length.
  Variable A:Type.

length函数具有非 MII 第一个参数:

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

这就是以下简单代码失败的原因(它失败是因为 length 没有部分应用，所以 A 没有插入):

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

必须写这样的东西才能使它工作:

  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 _) :

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

但有时，当一个人想要以最通用的形式(未部分应用)使用某个函数或构造函数时，最大程度地插入参数会妨碍您。 Coq.Lists.List 中带有非 MII 参数的工作示例模块:

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.

但是 exact Forall2_nil在 MII 参数的情况下不起作用。 constructor不过会帮助我们:

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 参数:

Declare Left Step eq_stepl.

但是，在这里我们必须添加'@':

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

有时采用 <tactic-name> ... with (_ := _). 形式的策略在存在 MII 参数的情况下将失败。这是来自 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 的争论阻碍了我们的进步:

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 ?

我不知道我希望有人能对此有所了解。

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 参数，插入 {}在适当情况下。