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

Question

我在Coq中具有以下list的定义：

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)等于证明了这一点。我不能让Coq知道这个事实。pcount (h :: t)P h

如何正确定义此功能？甚至有可能这样做吗？

Answer 1

您可以使用相关的模式匹配，因为结果类型plist (pcount (h :: t))取决于P_dec his left或right。

在下面，关键字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 hleft proofplist (if left proof then _ else _)

Coq可以推断出下划线的含义，这有点神奇，但是为了安全起见，您可以随时将其拼写出来：（if p then S (pcount t) else pcount t这与的定义完全匹配pcount）。