将临时列表转换为 Coq 中的依赖类型列表
Transform casual list into dependently typed list in Coq
我在 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)
.
它描述了"list of elements of type A
where at least n
of them fulfill predicate 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 知道这个真相。
如何正确定义这个函数?甚至可以这样做吗?
您可以使用依赖模式匹配,因为结果类型 plist (pcount (h :: t))
取决于 P_dec h
是 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.
替换p := P_dec h
时,类型plist (if p then _ else _)
必须等于plist (pcount (h :: t))
。然后在每个分支中,比如说left proof
,你需要产生plist (if left proof then _ else _)
(减少到左边的分支)。
Coq 可以推断出这里下划线中的内容,这有点神奇,但为了安全起见,您始终可以拼写出来:if p then S (pcount t) else pcount t
(这意味着与 [=26= 的定义完全匹配) ]).
我在 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)
.
它描述了"list of elements of type A
where at least n
of them fulfill predicate 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 知道这个真相。
如何正确定义这个函数?甚至可以这样做吗?
您可以使用依赖模式匹配,因为结果类型 plist (pcount (h :: t))
取决于 P_dec h
是 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.
替换p := P_dec h
时,类型plist (if p then _ else _)
必须等于plist (pcount (h :: t))
。然后在每个分支中,比如说left proof
,你需要产生plist (if left proof then _ else _)
(减少到左边的分支)。
Coq 可以推断出这里下划线中的内容,这有点神奇,但为了安全起见,您始终可以拼写出来:if p then S (pcount t) else pcount t
(这意味着与 [=26= 的定义完全匹配) ]).