coq - 将临时列表转换为 Coq 中的依赖类型列表

Question

我在 Coq 中有以下列表定义:

Variable A : Set.
Variable P : A -> Prop.
Hypothesis P_dec : forall x, {P x}+{~(P x)}.

Inductive plist : nat -> Set :=
   pnil : plist O
  | pcons : A -> forall n, plist n -> plist n
  | pconsp : forall (a:A) n, plist n -> P a -> plist (S n)
  .

它描述了“A 类型的元素列表，其中至少有 n 满足谓词 P”。

我的任务是创建将临时列表转换为 plist(具有最大可能的 n)的函数。我的尝试是先统计所有匹配P的元素，然后根据结果设置输出类型:

Fixpoint pcount (l : list A) : nat :=
  match l with
  | nil => O
  | h::t => if P_dec h then S(pcount t) else pcount t
  end.

Fixpoint plistIn (l : list A) : (plist (pcount l)) :=
  match l with
  | nil => pnil
  | h::t => match P_dec h with
          | left proof => pconsp h _ (plistIn t) proof
          | right _ => pcons h _ (plistIn t) 
          end
  end.

但是，我在 left proof 行中遇到错误:

Error:
In environment
A : Set
P : A -> Prop
P_dec : forall x : A, {P x} + {~ P x}
plistIn : forall l : list A, plist (pcount l)
l : list A
h : A
t : list A
proof : P h
The term "pconsp h (pcount t) (plistIn t) proof" has type
 "plist (S (pcount t))" while it is expected to have type
 "plist (pcount (h :: t))".

问题是 Coq 看不到 S (pcount t) 等于 pcount (h::t) 知道 P h，这已经被证明了。我不能让 Coq 知道这个真相。

如何正确定义这个函数？甚至可以这样做吗？

Answer 1

您可以使用依赖模式匹配，因为结果类型 plist (pcount (h::t)) 取决于 P_dec h 是否为 left 或 对。

下面关键字as引入了一个新的变量p，return告诉了整个match的类型> 表达式，由 p 参数化。

Fixpoint plistIn (l : list A) : (plist (pcount l)) :=
  match l with
  | nil => pnil
  | h::t => match P_dec h as p return plist (if p then _ else _) with
          | left proof => pconsp h (pcount t) (plistIn t) proof
          | right _ => pcons h _ (plistIn t) 
          end
  end.

类型 plist (if p then _ else _) 必须等于 plist (pcount (h::t)) 替换 p := P_dec h.然后在每个分支中，比如 left proof，您需要生成 plist(if left proof then _ else _)(减少到左分支)。

Coq 可以推断出这里下划线中的内容，这有点神奇，但为了安全起见，您始终可以拼写出来:if p then S (pcount t) else pcount t(这是意味着完全匹配 pcount 的定义)。