测试一个“简单”的身份类型示例,mod等同,但是传递性证明不会进行类型检查,即使是从模板中也是如此。不仅仅是修复,我想知道为什么?
这是最小问题的片段
data ModEq : (n:Nat) -> (x:Nat) -> (y:Nat) -> Type where
{- 3 constructors
reflexive: x == x (mod n),
left-induct: x == y (mod n) => (x+n) == y (mod n)
right-induct: x == y (mod n) => x == (y+n) (mod n)
-}
Reflex : (x:Nat) -> ModEq n x x --- Needs syntatic sugar, for now prefix
LInd : (ModEq n x y) -> ModEq n (x+n) y
RInd : (ModEq n x y) -> ModEq n x (y+n)
{----- Proof of transitive property. -----}
total
isTrans : (ModEq n x y) -> (ModEq n y z) -> (ModEq n x z)
{- x=x & x=y => x=y -}
isTrans (Reflex x) v = v
isTrans u (Reflex y) = u
{- ((x=y=>(x+n)=y) & y=z) => x=y & y=z => x=z (induct) => (x+n)=z -}
isTrans (LInd u) v = LInd (isTrans u v)
isTrans u (RInd v) = RInd (isTrans u v)
{- (x=y=>x=(y+n)) & (y=z=>(y+n)=z) => x=y & y=z => x=z (induct) -}
isTrans (RInd u) (LInd v) = isTrans u v
类型不匹配是在最后一行,即使从评论行我真的不知道为什么逻辑上错了。这是错误:
48 | isTrans (RInd u) (LInd v) = isTrans u v
| ~~~~~~~
When checking left hand side of isTrans:
When checking an application of Main.isTrans:
Type mismatch between
ModEq n (x + n) z (Type of LInd v)
and
ModEq n (y + n) z (Expected type)
Specifically:
Type mismatch between
plus x n
and
plus y n
我不仅对LInd v
如何被赋予(错误的看似)类型ModEq n(x + n)z感到困惑,而且我指出当我只是尝试使用内置模板的“type-define-refine”方法时,我得到了:
isTrans : (ModEq n x y) -> (ModEq n y z) -> (ModEq n x z)
isTrans (RInd _) (LInd _) = ?isTrans_rhs_1
它甚至不会打字,它会抱怨:
40 | isTrans (RInd _) (LInd _) = ?isTrans_rhs_1
| ~~~~~~~
When checking left hand side of isTrans:
When checking an application of Main.isTrans:
Type mismatch between
ModEq n (x + n) z (Type of LInd _)
and
ModEq n (y + n) z (Expected type)
Specifically:
Type mismatch between
plus x n
and
plus y n
问题是编译器无法在你的上一个案例中推断出y = {x + n}
。不过你可以给它一个提示:
isTrans : (ModEq n x y) -> (ModEq n y z) -> (ModEq n x z)
isTrans (Reflex _) v = v
isTrans u (Reflex _) = u
isTrans (LInd u) v = LInd $ isTrans u v
isTrans u (RInd v) = RInd $ isTrans u v
isTrans (RInd u) (LInd v) {n} {x} {y = x + n} = ?isTrans_rhs
这为isTrans_rhs
提供了以下目标:
x : Nat
n : Nat
u : ModEq n x x
z : Nat
v : ModEq n x z
--------------------------------------
isTrans_rhs : ModEq n x z
因此,你可以用isTrans (RInd u) (LInd v) {n} {x} {y = x + n} = v
结束