dst*_*fel 5 casting typechecking coq dependent-type
我有一个关于 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)) ;
}.
newSig所以里面有这个词。因此，替代定义
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')".，同样，应该从前提中清除。
如果有人能帮助我，我会很高兴。Coq 的类型检查机制有时有点不方便……;)
提前致谢！
/编辑（2018-09-27）：尽管我在下面给了自己一个安抚类型检查器的答案，但在尝试解决谓词逻辑领域的一些定理和定义问题时，我仍然遇到了很多问题。例如，由于类型检查，我完全无法定义一个令人满意的保守性定理版本（如果一个公式在结构中有效，那么它在所有扩展中也有效），即使添加了一个疯狂的约束（扩展共享相同的签名，所以它不是真正的扩展）并添加（工作）演员，我无法证明这一点！
这次，我想我给出了一个完整的例子。我隔离了该问题并将其作为GitHub Gist放入单个文件“firstorder.v”中（https://gist.github.com/rindPHI/9c55346965418bd5db26bfa8404aa7fe）。文档中有一些评论解释了我自己发现的挑战。如果有人找到其中一两个“主要挑战”的答案，我会很高兴了解它们（并且会接受这里作为问题的答案）。再次感谢！我希望这些问题的解决方案不仅可以帮助我，还可以帮助其他因依赖问题而变得绝望的人;)
感谢安东的评论，我设法以某种方式解决了这个问题。Anton 引用的第一个问题的答案让我考虑编写一个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 中转换表达式（假设有证据表明转换没问题——我可以接受）！
/编辑：我现在找到了一个用于此类转换的库：Heq 库。有了这个，myLemma看起来像
Lemma myLemma :
forall t1 t2 : Type,
forall (l1 : list t1) (l2 : list t2),
forall (H : t2 = t1),
l1 = << list # H >> l2.
所以你不必编写自己的转换函数。
不幸的是，我无法真正消除证明中的演员表（无论我使用自己的演员表还是 Heq 的演员表）；看来您需要成为一名真正有经验的依赖类型黑客才能做到这一点。或者我的引理是错误的，但我不这么认为。对于那些真正想深入了解这个主题的人，Adam Chlipala 的伟大的CPDT 书中有一章关于平等的内容；就我而言，我个人只是“ admit”一些简化这些表达式的证明并在此基础上进行构建。至少它会进行类型检查......