Idris中rewrite操作失效：重写未改变目标类型问题

我正在Idris中证明一个定理，处理S_Trans分支时编写了如下代码：

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。我需要得到类型为StSubtype s (StTApp s1 s2)的hyp1'，尝试用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).

1. 使用replace函数直接构造目标值 #

Idris的replace函数专门用于通过等式转换依赖类型的实例，其类型为{a : Type} -> {x : a} -> {y : a} -> (x = y) -> P x -> P y。这里可以把P看作StSubtype s，直接用ueq把hyp1的类型从StSubtype s u转换为StSubtype s (StTApp s1 s2)：

hyp1' : StSubtype s (StTApp s1 s2)
hyp1' = replace ueq hyp1

这种方式比rewrite更直接，也更容易被Idris的类型检查器正确处理。

2. 调整rewrite的使用方式 #

如果一定要用rewrite，需要确保等式方向与类型改写需求匹配，并且显式引导类型推导。可以尝试显式标注类型后直接改写：

hyp1' : StSubtype s (StTApp s1 s2)
hyp1' = rewrite ueq in hyp1

如果还是不生效，可通过sym函数调整等式方向后再改写（虽然等式方向本身正确，但显式操作能帮助类型检查器识别）：

hyp1' : StSubtype s (StTApp s1 s2)
hyp1' = rewrite sym (sym ueq) in hyp1

不过这种方式不如replace直观可靠。

3. 检查StSubtype的定义 #

如果上述方法都无效，需要确认StSubtype是否是合法的依赖参数化类型。比如StSubtype的定义应该是类似StSubtype : (a : StType) -> (b : StType) -> Type的形式，确保第二个参数是可通过等式替换的参数。如果StSubtype的定义包含特殊索引约束，可能需要额外证明引理来支持类型转换。

内容的提问来源于stack exchange，提问作者Henrique Guerra