CoQ：对定义中的术语进行类型检查时使用类型相等 [英] Coq: Use equality of types for type checking a term in a definition
问题描述
我有一个关于Coq中类型检查定义的问题。我遇到了一种情况，我有两个T1和T2类型的项，从定义上我知道T1和T2是相等的(T1=T2)。但是，我不能同时使用这两个术语，因为类型检查器认为这两个类型不相等。我试图分离出一个模拟情况的最小示例(是的，我知道这是一个愚蠢的属性，但我只想检查它的类型；)：
Require Import Coq.Lists.List.
Lemma myLemma :
forall t1 t2 : Type,
forall (l1 : list t1) (l2 : list t2),
t1 = t2 ->
l1 = l2.
假设我不能直接写(l2 : list t1)，因为它来自另一个定义。
我尝试使用Program，因为我希望能够以某种方式推迟任务以证明类型匹配，但这无济于事(得到相同的类型检查错误)。
如果上面的例子不足以清楚地说明问题，下面是我的实际问题的摘录：
Definition taclet_sound_new (t : taclet) :=
forall K st seSt, let S := (sig K) in
[(K, st)] |= (pathC seSt) ->
(forall K', let S' := (sig K') in
S' = (newSig t S) ->
exists (seSt' : (@sestatesc (newSig t S))),
List.In seSt' (apply t S seSt) ->
[(K', st)] |= (conv S' (pathC seSt'))).
系统报告The term "pathC seSt'" has type "@pathCond (newSig t S)" while it is expected to have type "@pathCond S'".；但是，从前提S' = (newSig t S)我预计应该可以以某种方式检查该定义类型。
(备注：conv是一个微不足道的定义，我添加它只是为了改善Coq的输出--Definition conv (S : signature) (pc : (@pathCond S)) : list (@formulas S) := pc.--否则，它会说The term "pathC seSt'" has type "pathCond" while it is expected to have type "list formulas".掩盖了实际问题。)
为完整起见：记录taclet定义为
Record taclet : Type := {
defined (prog : P) : Prop;
newSig (S1 : signature) : signature ;
apply : forall (S1 : signature),
(@sestatesc S1) -> list (@sestatesc (newSig S1)) ;
}.
Definition taclet_sound_new (t : taclet) :=
forall K st seSt, let S := (sig K) in
[(K, st)] |= (pathC seSt) ->
(forall K', let S' := (sig K') in
exists (seSt' : (@sestatesc S')),
S' = (newSig t S) ->
List.In seSt' (apply t S seSt) ->
[(K', st)] |= (pathC seSt')).
也不进行类型检查，出现类似的错误The term "apply t S seSt" has type "list (sestatesc P (newSig t S))" while it is expected to have type "list (sestatesc P S')".，这也应该从前提中清除。
提前谢谢！
/EDIT(2018-09-27)：尽管我在下面给了自己一个安抚类型检查器的答案，但在尝试围绕谓词逻辑领域中的一些定理和定义来解决问题时，我仍然遇到了许多问题。例如，由于类型检查，我完全无法定义一个令人满意的保守性定理版本(如果一个公式在结构中有效，它在所有扩展中也是有效的)，即使添加一个疯狂的约束(扩展共享相同的签名，所以它不是真正的扩展)并添加(工作的)强制转换，我也无法证明！
这一次，我想我给出了一个完整的示例。我隔离了问题并将其作为GitHub Gist(https://gist.github.com/rindPHI/9c55346965418bd5db26bfa8404aa7fe)放入单个文件"firstorder.v"中。这份文件中有一些评论解释了我自己发现的挑战。如果有人在其中找到了一个或两个"主要挑战"的答案，我将非常非常了解它们(并接受这一点作为这里问题的答案)。再次感谢！我希望这些问题的解决方案不仅能帮助我，也能帮助其他因依赖问题而变得绝望的人。)
推荐答案
多亏了Anton的评论，我设法在某种程度上解决了这个问题。This answerAnton引用的第一个问题让我考虑编写一个cast函数(我也尝试使用另一个替代方法jmeq，但它无济于事--可能我并不真正理解它)。我想我会分享这个解决方案，以防它对某人有帮助。
首先，我编写了以下cast函数并通过两个包装器使用它(我不会发布，因为它们通常并不有趣：
Definition simple_cast {T1 T2 : Type} (H : T1 = T2) (x : T1) : T2 :=
eq_rect T1 (fun T3 : Type => T3) x T2 H.
(备注：我没有直接想出eq_rect这个术语，因为我不是一个足够专业的用户；但是，在Coq中可以做以下事情，我觉得这很有趣：Definition simple_cast {T1 T2 : Type} (H : T1 = T2) (x : T1) : T2. rewrite -> H in x. assumption. Defined.如果您当时Print simple_cast，您可以简化一个术语，并直接将其发布到定义中以使其更加明确。以这种方式构建术语要容易得多，因为您可以使用简单的策略)。
接下来，我想出了以下定义，省去了包装器：
Definition cast {T : Type} {T1 T2 : T} (H : T1 = T2) (f : T -> Type) (x : f T1) :=
eq_rect T1 (fun T3 : T => f T3) x T2 H.
关于简单列表示例，以下代码类型检查：
Lemma myLemma :
forall t1 t2 : Type,
forall (l1 : list t1) (l2 : list t2),
forall (H : t2 = t1),
l1 = cast H (list) l2.
我的实际代码片段还输入检查：
Definition taclet_sound_new (t : taclet) :=
forall K st seSt, let S := (sig K) in
[(K, st)] |= (pathC seSt) ->
(forall K', let S' := (sig K') in
forall (H : (newSig t S) = S'),
exists (seSt' : (@sestatesc (newSig t S))),
List.In seSt' (apply t S seSt) ->
[(K', st)] |= (cast H (@pathCond) (pathC seSt'))).
最后，我可以在Coq中强制转换表达式(假设有命名证据表明强制转换是正确的--我可以接受)！
/EDIT：我现在找到了一个用于此类强制转换的库：Heq library。这样，myLemma看起来就像
Lemma myLemma :
forall t1 t2 : Type,
forall (l1 : list t1) (l2 : list t2),
forall (H : t2 = t1),
l1 = << list # H >> l2.
这样您就不必编写自己的CAST函数。
不幸的是，我不能真正消除校样中的强制转换(不管我使用自己的强制转换还是HEQ的强制转换)；看起来您需要是一个真正有经验的依赖类型黑客才能做到这一点。或者我的词汇表是错的，但我并不这么认为。对于那些真正想要进入这个主题的人，在Adam Chlipala的伟大的CPDT book中有一个关于等式的章节；在我的例子中，我个人只会"admit"一些简化这些表达式的证明，并以此为基础。至少它会进行类型检查...
这篇关于CoQ：对定义中的术语进行类型检查时使用类型相等的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
