避免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。

当然，只有当所讨论的隐含论点在定义中是一致的时，这才有效。