Idris 重写不会发生

Question

import Data.Vect
import Data.Vect.Quantifiers

sameKeys : Vect n (lbl, Type) -> Vect n (lbl, Type) -> Type
sameKeys xs ys = All (uncurry (=)) (zip (map fst xs) (map fst ys))

g : {xs,ys : Vect n (lbl, Type)} -> sameKeys xs ys -> map (\b => fst b) xs = map (\b => fst b) ys
g {xs = []} {ys = []} [] = Refl
g {xs = x::xs} {ys = y::ys} (p::ps) = rewrite g ps in ?q

这是我看到的错误：

*main> :load main.idr
Type checking ./main.idr
main.idr:57:3:When checking right hand side of g with expected type
        map (\b => fst b) (x :: xs) = map (\b6 => fst b6) (y :: ys)

rewriting
    Data.Vect.Vect n implementation of Prelude.Functor.Functor, method map (\b => fst b) xs
to
    Data.Vect.Vect n implementation of Prelude.Functor.Functor, method map (\b6 => fst b6) ys
did not change type
    fst x :: Data.Vect.Vect n implementation of Prelude.Functor.Functor, method map (\b => fst b) xs = fst y :: Data.Vect.Vect n implementation of Prelude.Functor.Functor, method map (\b6 => fst b6) ys
Holes: Main.g

为什么不重写呢？

Answer 1

发生这种情况是因为 Idris 以某种方式无法推断 g 的正确隐式参数，而是在上下文中引入了新的向量。

作为解决方法，我建议按如下方式证明它。首先，我们需要一个双参数函数的同余引理：

total
cong2 : {f : a -> b -> c} -> (a1 = a2) -> (b1 = b2) -> f a1 b1 = f a2 b2
cong2 Refl Refl = Refl

现在原引理的证明很简单了：

total
g : sameKeys xs ys -> map (\b => fst b) xs = map (\b => fst b) ys
g {xs = []} {ys = []} x = Refl
g {xs = x :: xs} {ys = y :: ys} (p :: ps) = cong2 p $ g ps

Idris 重写不会发生

Idris rewrite does not happen

idris