casting - Coq:使用类型相等对定义中的术语进行类型检查

Question

我有一个关于 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 的那种类型检查机制有时有点不方便……;)

提前致谢!

/edit (2018-09-27): 虽然我在下面给了自己一个安抚类型检查器的答案，但在试图解决我在谓词逻辑领域的一些定理和定义的问题时，我仍然遇到了很多问题。例如， 我完全没有定义一个令人满意的保守性定理 (如果公式在结构中有效，则它在所有扩展中也有效)由于类型检查，以及 即使添加一个疯狂的约束 (扩展共享相同的签名，所以它不是真正的扩展)并添加一个(工作)类型转换， 我无法证明 !

这一次，我以为我给了 完整示例 .我隔离了问题并将其作为 放入单个文件“firstorder.v”中。 GitHub 要点 ( https://gist.github.com/rindPHI/9c55346965418bd5db26bfa8404aa7fe )。文档中有一些评论解释了我为自己发现的挑战。如果有人在那里找到一两个“主要挑战”的答案，我会很高兴知道他们(并且会接受这里作为问题的答案)。再次感谢!我希望这些问题的解决方案不仅可以帮助我，也可以帮助其他因依赖问题而绝望的人;)

Answer 1

感谢 Anton 的评论，我设法以某种方式解决了这个问题。 This answer 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 中转换表达式(假设有命名的证据表明转换没问题——我可以接受)!

/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.

所以你不必编写自己的强制转换函数。

不幸的是，我无法真正消除证明中的类型转换(无论我是使用自己的类型转换还是 Heq 的类型转换)；看来你需要成为一个真正有经验的依赖型黑客才能做到这一点。或者我的引理是错误的，但我不这么认为。对于那些真正想进入该主题的人，Adam Chlipala 的伟大著作 CPDT book 中有一个关于平等的章节。 ;就我而言，我个人只是“ admit ”一些简化这些表达式并以此为基础的证明。至少它类型检查......