为什么 Idris 中特定形式的 cong 无法进行类型检查？

如何解决为什么 Idris 中特定形式的 cong 无法进行类型检查？

Idris 具有非常简单的 cong 函数。

cong : {f : t -> u} -> a = b -> f a = f b
cong Refl = Refl

如果我创建一个特殊形式的 cong 来添加超过零，它无法进行类型检查。

cong0 : {f : Nat -> Nat} -> a + Z = a -> f (a + Z) = f a
cong0 Refl = Refl

在 Idris 1 中我得到

When checking left hand side of cong0:
When checking an application of Main.cong0:
        Type mismatch between
                a = a (Type of Refl)
        and
                a + 0 = a (Expected type)
        
        Specifically:
                Type mismatch between
                        a
                and
                        plus a 0

在 Idris 2 中我得到

Can't solve constraint between:
        ?_ [no locals in scope]
and
        plus ?_ 0
at:
2       cong0 Refl = Refl
              ^^^^

但是，如果我只是用 cong0 替换 cong 的定义，一切都可以正常编译：

cong0 : {f : Nat -> Nat} -> a + Z = a -> f (a + Z) = f a
cong0 = cong

如果我也只是不在等式两边重复 a，一切似乎都很好。

cong0 : {f : Nat -> Nat} -> a + Z = b -> f (a + Z) = f b
cong0 Refl = Refl

这是怎么回事？为什么我可以直接证明 cong0 的广义版本而不是它的特殊版本？

这是否与抽象变量 a 以不同的句法形式出现在 = 的两侧有关？如果是这样，为什么 Idris 不允许这样的事情与 Refl 模式统一，但完全满足于允许 a = b？

解决方法

这与依赖类型理论的微妙之处有关。考虑模式匹配的最佳方式是作为“归纳规则”应用的语法糖。对于平等，规则是

eq_ind : (a : Type) -> 
         (x : a) ->
         (P : (y : a) -> x = y -> Type) ->
         P x Refl ->
         (y : a) ->
         (q : x = y) ->
         P y q
eq_ind a x P reflCase x Refl = reflCase

类型 x = y 上的所有模式匹配都必须简化为 eq_ind 的“明显”应用。

在这种情况下，我们看到我们可以写

cong : {f : t -> u} -> x = y -> f x = f y
cong {t} {u} {f} {x} {y} q = eq_ind t x (\y,_ => f x = f y) Refl y q

这是对 cong 定义中模式匹配的非常直接的解释，作为应用 eq_ind 的特殊情况。

其实我们也可以写

cong1 : {f : Nat -> Nat} -> a + Z = b -> f (a + Z) = f b
cong1 {f} {a} {b} q = eq_ind Nat (a + Z) (\b,_ => f (a + Z) = f b) Refl b q

请注意，我们只能在尝试证明形式为 eq_ind 的事物时使用 (y : a) -> (q : x = y) -> P y q。换句话说，相等类型的右边必须是一个变量 y，它不会在 x 中自由出现。

我们不能直接用eq_ind来证明语句{f : Nat -> Nat} -> a + Z = a -> f (a + Z) = f a，因为在表达式a + Z = a中，右边的变量也出现在左边。类型只是不工作。由于从您的模式匹配到 eq_ind 的使用没有明显的转换，因此 Idris 不能让您使用模式匹配。

然而，我们绝对可以使用 cong 作为辅助函数来证明 a + Z = a -> f (a + Z) = f a。事实上，这是证明这个说法的最好方法。

请注意，我们也不能“明显地”使用 eq_ind 来证明对 cond1 的对称陈述，即 {f : t -> u} -> b = (a + Z) -> f b = f (a + Z)。因此，我们也不能在这里使用模式匹配。尽管我们可以使用模式匹配来证明 a + Z = b -> f (a + Z) = b，但我们不能用等号反过来做。

如果你想了解更多关于它是如何工作的细节，你应该研究“路径归纳”，最好阅读同伦类型理论书的前两章。