coq - 避免 Fixpoint 的隐式参数在证明模式下变得显式

Question

有没有办法强制 Fixpoint 隐式参数在证明模式下保持隐式？

例子:

Fixpoint foo {a : Set} (l : list a) : nat :=
  match l with
  | nil => 1
  | _ :: xs => ltac:(exact (1 + foo _ xs))
                                   ^^^  
end.

但是我想写

Fixpoint foo {a : Set} (l : list a) : nat :=
  match l with
  | nil => 1
  | _ :: xs => ltac:(exact (1 + foo xs))
  end.

Answer 1

正如人们一直在说的那样，我认为它不会得到实现，但在某些情况下，我相信您可以使用部分来规避这个问题。

From Coq Require Import List.
Import ListNotations.

Section Foo.

  Context {a : Set}.

  Fixpoint foo (l : list a) : nat :=
    match l with
    | nil => 1
    | _ :: xs => ltac:(exact (1 + foo xs))
    end.

End Foo.

请注意，这等效于(因为它产生相同的定义):

Definition foo' {a : Set} :=
  fix foo' (l : list a) : nat :=
    match l with
    | nil => 1
    | _ :: xs => ltac:(exact (1 + foo' xs))
    end.

这里的技巧更明确，在执行定点之前使用参数 a : Set。

当然，这仅在所讨论的隐式参数在定义中是统一的时才有效。