Idris：重写不起作用（重写者...没有改变）

Question

我正在证明 Idris 中的一个定理，在第二种情况下：

theorem1 t1 t2 s (S_Trans u hyp1 hyp2) = let 
    (s1 ** (s2 ** (ueq, st1, st2))) = theorem1 t1 t2 u 
    hyp1' = rewrite ueq in hyp1
    in case theorem1 s1 s2 s hyp1' of
        (s1' ** (s2' ** (ueq', st1', st2'))) => (s1' ** (s2' ** (ueq', S_Trans s1 st1 st1', S_Trans s2 st2' st2)))`

hyp1

具有类型

StSubtype s u

，并且

ueq

具有类型

u = StTApp s1 s2

。我想要一个学期

hyp1'

类型为

StSubtype s (StTApp s1 s2)

。

为此，我尝试了

rewrite ueq in hyp1

，这给出了错误：

Error: While processing right hand side of theorem1. Rewriting
by u = StTApp s1 s2 did not change
type ?_ [locals in scope: u, t2, t1, hyp2, s, hyp1, s1, s2, ueq, st1, st2].

如果我为

hyp1'

、

hyp1' : StSubtype s (StTApp s1 s2)

编写类型注释，它会给出类似的错误：

Error: While processing right hand side of theorem1. While processing right hand
side of $resolved2797,hyp1'. Rewriting by u = StTApp s1 s2 did not change
type StSubtype s (StTApp s1 s2).```

Answer 1

使用

rewrite cong (StSubtype s) in hyp1

。

rewrite a = b in c

将

c

的整个类型从

b

更改为

a

（或将

a

更改为

b

，我永远不记得了）。你想要的是将

StSubtype s u

变成

StSubtype s (StTApp s1 s2)

，但你只有

u = StTApp s1 s2

。与

cong : (0 f : t -> u) -> (0 p : a = b) -> f a = f b

您可以添加

StSubtype s

以获得

StSubtype s u = StSubtype s (StTApp s1 s2)

。