如何利用Coq中有关此函数类型的信息
假设我有以下类型的typ，表示bool或nat：
Inductive typ : Type := TB | TN.我还有一个函数从typ的列表中提取一个实际的函数类型，还有一个结果类型：
Fixpoint get_types (s: seq typ) (result_type: Type) : Type :=
match s with
| nil => result_type
| x :: xs => match x with
| TN => nat -> get_types xs result_type
| TB => bool -> get_types xs result_type
end
end.
Example get_types_works : get_types (TB :: TN :: nil) nat = bool -> nat -> nat.
Proof. by []. Qed.现在，我有另一个函数，它以typ的list typ和类型为get_types s的函数作为输入。
Fixpoint app (s: seq typ) (constructor: get_types s nat) : nat :=
match s with
| nil => 2 (* Not properly handling empty list case for now *)
| TB :: nil => constructor true
| TN :: nil => constructor 2
| TB :: xs => app xs (constructor true)
| TN :: xs => app xs (constructor 2)
end. 在| TB :: nil => constructor true行中定义上述函数失败的有：
Illegal application (Non-functional construction):
The expression "constructor" of type "get_types s nat" cannot be applied to the term
"true" : "bool"既然我们在这里知道get_types s nat的类型应该是bool -> nat，因为s的值是TB :: nil，我想知道是否有一种方法可以让Coq知道这一点，这样就可以定义上面的函数了？
如果不是，这是Coq的限制，还是同样适用于其他依赖类型的语言？
编辑：对于上下文来说，这不是我想要解决的最初问题；它是一个浓缩版，用来显示我在类型系统中遇到的问题。在实际版本中，而不是硬编码2和true，typ-like数据结构还包含从内存片解析的数据索引和验证函数。app的目标是一个函数，该函数获取包含此类类型的记录的typ列表、切片和构造函数，然后从要解析的类型的索引中构造该记录的实例，如果任何验证失败，则返回None。
回答 4
Stack Overflow用户
发布于 2018-02-26 13:40:35
还有另外两种定义app的方法。
第一种是使用策略，依赖于induction而不是Fixpoint。
Definition app (s: seq typ) (constructor: get_types s nat) : nat.
Proof.
induction s as [|t xs].
- exact 2.
- destruct xs.
+ destruct t.
* exact (constructor true).
* exact (constructor 2).
+ destruct t.
* exact (IHxs (constructor true)).
* exact (IHxs (constructor 2)).
Defined.第二种是加里纳和复杂的模式--比赛。
Fixpoint app (s: seq typ) : get_types s nat -> nat :=
match s return get_types s nat -> nat with
| nil => fun _ => 2
| x :: xs =>
match xs as xs0 return xs = xs0 -> get_types (x::xs0) nat -> nat with
| nil => fun _ => match x return get_types (x::nil) nat -> nat with
| TB => fun c => c true
| TN => fun c => c 2
end
| _ => fun e => match e in _ = xs1 return get_types (x::xs1) nat -> nat with
| eq_refl =>
match x return get_types (x::xs) nat -> nat with
| TB => fun c => app xs (c true)
| TN => fun c => app xs (c 2)
end
end
end eq_refl
end.在销毁xs时，我们会记住原始xs和它所销毁的内容之间的相等。我们不需要在nil分支中使用这个等式，而用fun _丢弃它。在另一个分支中，我们对等式的证明(match e)进行模式匹配，这对应于使用这个等式进行重写。在eq_refl分支中，我们可以使用原始的xs，从而进行终止检查所允许的递归调用。在模式匹配之外，我们返回xs上的模式匹配所期望的正确类型。最后要做的事情是提供xs和xs0相等的证明，但这是微不足道的eq_refl。
Stack Overflow用户
发布于 2018-02-24 06:01:06
原则上你想要的没有什么不对的。但是，至少在Coq中，有一些关于模式匹配的简单规则，这样就可以在类型中使用关于使用了哪个构造函数的信息。表层语言(在本例中是Gallina)通过帮助编译(或desugar)模式匹配来隐藏这种简单性，这样作为用户，您可以编写比底层系统所必须处理的更复杂的模式。我不太熟悉Idris，但基于依赖模式匹配的复杂性，我怀疑您在那里遇到了类似的限制，您必须将代码放入系统可以键入的检查形式中。
在这里，您将遇到模式匹配编译的两个限制。首先，基于s上的匹配，构造函数的类型不是专门化的。这很容易通过计算来自get_types s nat -> nat的函数来解决，编译器可以正确地处理这个问题。
Require Import List.
Import ListNotations.
Inductive typ : Type := TB | TN.
Fixpoint get_types (s: list typ) (result_type: Type) : Type :=
match s with
| nil => result_type
| x :: xs => match x with
| TN => nat -> get_types xs result_type
| TB => bool -> get_types xs result_type
end
end.
Fail Fixpoint app (s: list typ) : get_types s nat -> nat :=
match s with
| nil => fun constructor => 2
| TB :: nil => fun constructor => constructor true
| TN :: nil => fun constructor => constructor 2
| TB :: xs => fun constructor => app xs (constructor true)
| TN :: xs => fun constructor => app xs (constructor 2)
end.
(* fails due to limitation of termination checker with nested matches *)然后，...but会遇到终止检查器的第二个问题。请注意，您的匹配是复杂的:它分析s的结构以及它的头和尾(如果它是用cons构建的)。最后，将所有模式匹配编译为单个归纳类型上的嵌套模式匹配。如果您查看这个展开，您将s解构为t::xs，然后再将xs解构为t0::xs'，最后在xs上递归。不幸的是，Coq终止检查器只将其视为t0::xs'，而不承认它是s的一个子术语(它确实想要xs)。
我很难以一种类型检查的方式手动编写函数，但这里有一个使用功能正确的策略编写的版本。请注意，它产生的定义比任何普通的模式匹配都要复杂得多，因为它必须维护destruct_with_eqn生成的证据。但是，这一证明对于同时使用xs使终止检查器高兴和显示用于检查构造函数应用程序的类型的t0::xs'至关重要。它可能很复杂，但您仍然可以很好地运行它，如最后一行所示。
Fixpoint app (s: list typ) (constructor: get_types s nat) {struct s} : nat.
destruct s as [|t xs]; simpl in *.
exact 2.
destruct_with_eqn xs; simpl in *.
destruct t; [ exact (constructor true) | exact (constructor 2) ].
destruct t; simpl in *.
- apply (app xs).
subst.
exact (constructor true).
- apply (app xs).
subst.
exact (constructor 2).
Defined.
Eval compute in app [TB; TN] (fun x y => if x then y+2 else y).
(* = 4
: nat
*)Stack Overflow用户
发布于 2018-02-24 13:54:02
因为您用Idris标记了它，下面是它的工作方式：
data Typ = TB | TN
get_types : (args : List Typ) -> (res : Type) -> Type
get_types [] res = res
get_types (TB :: xs) res = Bool -> get_types xs res
get_types (TN :: xs) res = Nat -> get_types xs res
app : (args : List Typ) -> (con : get_types args Nat) -> Nat
app [] con = 2
app (TB :: []) con = con True
app (TN :: []) con = con 2
app (TB :: xs) con = app xs (con True)
app (TN :: xs) con = app xs (con 2)基本上，您没有问题，因为通过在args上进行匹配，编译器还可以推断出con的类型。例如，如果将最后一个案例替换为
app (TN :: xs) con = ?hole然后调查这个漏洞，您会发现编译器有关于con的新信息。
xs : List Typ
con : Nat -> get_types xs Nat
--------------------------------------
hole : Nathttps://stackoverflow.com/questions/48959586
复制相似问题
腾讯云开发者
