避免Fixpoint的隐式参数在证明模式下显式

如何解决避免Fixpoint的隐式参数在证明模式下显式？

有没有一种方法可以强制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.

解决方法

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

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。

当然，只有当所讨论的隐式参数在定义中统一时，该方法才起作用。

简化Wilterhalter的响应，我们可以简单地添加一个let定义而无需隐式参数

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

[db:链接]

声明：本站所有文章，如无特殊说明或标注，均为本站原创发布。任何个人或组织，在未征得本站同意时，禁止复制、盗用、采集、发布本站内容到任何网站、书籍等各类媒体平台。如若本站内容侵犯了原著者的合法权益，可联系我们进行处理。