如何在 coq 中编写一个“安全”的头？

如何解决如何在 coq 中编写一个“安全”的头？

我试图在 Coq 中做一些类似于 this liquid Haskell trick 的事情，它定义了一个部分函数，​​但证明它实际上是完整的：

{-@ head :: {xs:[a] | len xs > 0} -> a @-}
head (x:xs) = x

这是我的第一次尝试，但 Coq 不喜欢它（“这里不支持强制转换 模式。”）：

Definition safeHead {A : Type} (xs : list A) (nonempty : xs <> nil) : A.
Proof.
  refine (fun {A : type} (xs : list A) (pf : xs <> nil) =>
            match xs with
            | x : xs => x
            | nil => _
            end).
  (* Some tactic here to prove the hole from nonempty *)
Defined.

我也尝试从 this blog post 中调整选项 1，但失败并出现相同的错误：

Definition safeHead {A : Type} (xs : list A) (not_nil : xs <> nil) : A
  match xs return _ with
  | x : xs => fun _ => x
  | nil => fun is_nil => False_rect _ (not_nil is_nil)
  end eq_refl.

有没有办法让它在 coq 中工作？我也很想了解错误信息；什么是“演员表”，它以哪种模式失败？

解决方法

正如@kyo dralliam 所指出的，对于列表的 cons 操作，您应该使用 :: 而不是 :。

你的定义的主要问题是当你匹配它时，你会丢失 xs 不为空的信息。要保留该信息，您必须明确说明。像这样：

From Coq Require Import Utf8 List.
Import ListNotations.

Definition safeHead {A : Type} (xs : list A) (nonempty : xs ≠ []) : A :=
  match xs as l return l ≠ [] → A with
  | [] => ltac:(contradiction)
  | x :: xs => λ _,x
  end nonempty.

使用 return 的 match 信息，我说我构造了 l ≠ [] → A 的证明，其中 l 是我给 xs 使用的本地名称as 子句。

这意味着在 [] 的情况下，我们必须居住在 [] ≠ [] → A 中，因此我得出结论使用 contradiction 策略，在术语中使用策略。

在 cons 情况 x :: xs 中，我们并不真正关心非空假设，因此我忽略参数并根据需要返回头部 x。

最后，整个 match 表达式现在具有 xs ≠ [] → A 类型，因此要获得 A，我们必须给它 nonempty 证明。

,

实现这一目标的一种方法是使用策略来编写定义的主体

Definition safeHead' {A : Type} (xs : list A) (not_nil : xs <> nil) : A.
  destruct xs.
  - exfalso; apply not_nil; reflexivity.
  - apply a.
Defined.

Let xs := cons 1 nil.
Definition xs_not_nil : xs <> nil.
  unfold xs; intro; discriminate.
Defined.

Eval compute in safeHead' xs xs_not_nil.

实现类似行为的另一种非常简单的方法是为非空列表定义归纳数据类型。

Inductive nlist {A : Type} : Type :=
  ncons (x : A) (xs : list A) : nlist.

Let nxs := ncons 1 nil.

Definition safeHead {A : Type} (nxs : nlist) : A :=
  match nxs with
  | ncons x xs => x
  end.

Eval compute in safeHead nxs. (* 1 : nat *)