Fixpoint 中的列表决策者

Question

我对 coq 比较陌生，我不知道如何继续。

我想为列表库的 In Fixpoint 编写一个可判定性函数，如下所示：

Program Fixpoint InDec (s : K) (l : list K) : {In s l} + {~ In s l} :=
  match l with
  | nil => ~ In s l
  | head :: tail => 
    if eq_dec s head
    then In s l
    else InDec s tail
  end.

在这个部分中，K 是一个类型并且具有以下属性：

Context `{EqDec K}.

哪里

Class EqDec A : Type := {
  eq_dec: forall a1 a2 : A, {a1 = a2} + {a1 <> a2}
  }.

我是如何理解的， {In s l} + {~ In s l} 是一个类型，而 In s l 是一个 Prop，这导致它不起作用，但我不确定到底为什么。 我需要更改什么，以便我可以在 if 表达式中使用 InDec 以及为什么 In s l 不是以下成员 {In s l} + {~ In s l}？

我认为 {In s l} + {~ In s l} 会创建一个居民为 In s l 和 ~ In s l 的类型。

Answer 1

你的“函数定义”没有任何意义。就好像您想这样定义加法：

Fixpoint add (n:nat) (m:nat) : nat := 
match n, m with
  0,   m => nat (* instead of [m] *)
| S n, m => nat (* instead of [S (add n m)] *)
end

这实际上并没有定义函数。您需要指定要返回哪个数字，但您只是告诉 Coq 要返回一个数字。这没有道理。 相反，你应该像这样定义你的函数：

Obligation Tactic := idtac. (* for didactic reasons *)
Program Fixpoint InDec (s : K) (l : list K) : {In s l} + {~ In s l} :=
  match l with
  | nil => right _
  | head :: tail => 
    if eq_dec s head
    then left _
    else match InDec s tail with
      left Hl => left _
    | right Hr => right _ end
  end.
(* prove that if l = Nil, the element is not in the list *)
Next Obligation. intros s l _ []. Qed.
(* prove that if s = head, the element is in the list *)
Next Obligation. intros s l head tail _ Heq. left. symmetry. apply Heq. Qed.
(* prove that the recusion steps work *)
Next Obligation.
  intros InDex s l head tail _ Hne rr Hl _.
  right. apply Hl.
Qed.
Next Obligation.
  intros InDex s l head tail _ Hne rr Hr _.
  intros [H1|H2].
    + apply Hne. symmetry. apply H1.
    + apply Hr, H2.
Qed.

请注意，不要写例如

~In s l

在第一种情况下（列表为空），这是一个

类型

，我们实际上必须给出一个证明（即具有该类型的术语）。另请注意，我们需要证明的是

{In s nil} + {~In s nil}

，第一步是确定我们处于正确的情况，因此我们使用构造函数right。实际上，证明

~In s nil

是一项带有下划线的义务（因为我们使用的是

Program

），以便之后可以使用策略来解决这个目标。具体来说，这是首要义务。请记住，在 Coq 中，您需要证明一些事情。仅仅为您的决策者“返回 true”是不够的，您需要返回一个证明您做出了正确选择的证据。这还需要证明递归调用的结果在这里适用。