消除subst来证明平等

Question

我试图将 mod-n 计数器表示为将间隔[0, ..., n-1]分为两部分：

\n\n

data Counter : \xe2\x84\x95 \xe2\x86\x92 Set where\n  cut : (i j : \xe2\x84\x95) \xe2\x86\x92 Counter (suc (i + j))\n

\n\n

使用它，定义两个关键操作很简单（为简洁起见，省略了一些证明）：

\n\n

_+1 : \xe2\x88\x80 {n} \xe2\x86\x92 Counter n \xe2\x86\x92 Counter n\ncut i zero    +1 = subst Counter {!!} (cut zero i)\ncut i (suc j) +1 = subst Counter {!!} (cut (suc i) j)\n\n_-1 : \xe2\x88\x80 {n} \xe2\x86\x92 Counter n \xe2\x86\x92 Counter n\ncut zero    j -1 = subst Counter {!!} (cut j zero)\ncut (suc i) j -1 = subst Counter {!!} (cut i (suc j))\n

\n\n

当试图证明+1和-1是逆时，问题就出现了。我不断遇到需要为这些subst引入的消除器的情况，即类似的情况

\n\n

subst-elim : {A : Set} \xe2\x86\x92 {B : A \xe2\x86\x92 Set} \xe2\x86\x92 {x x\xe2\x80\xb2 : A} \xe2\x86\x92 {x=x\xe2\x80\xb2 : x \xe2\x89\xa1 x\xe2\x80\xb2} \xe2\x86\x92 {y : B x} \xe2\x86\x92 subst B x=x\xe2\x80\xb2 y \xe2\x89\xa1 y\nsubst-elim {A} {B} {x} {.x} {refl} = refl\n

\n\n

但这结果（在某种程度上）回避了这个问题：类型检查器不接受它，因为subst B x=x' y : B x'并且y : B x......

\n

Answer 1

如果您使用 stdlib 中的 Relation.Binary.HeterogeneousEquality，您可以声明 subst-elim 的类型。\n但是，我可能只是对 x \xe2\x89\xa1 x\xe2\x80\xb2 的最终证明进行模式匹配在 with 或 rewrite 子句中，因此您不必创建显式消除器，因此不会出现打字问题。

\n