消除subst以证明相等

Question

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

data Counter : ℕ → Set where
  cut : (i j : ℕ) → Counter (suc (i + j))

使用这一点，定义两个关键操作非常简单(为简洁起见，省略了一些证明)：

_+1 : ∀ {n} → Counter n → Counter n
cut i zero    +1 = subst Counter {!!} (cut zero i)
cut i (suc j) +1 = subst Counter {!!} (cut (suc i) j)

_-1 : ∀ {n} → Counter n → Counter n
cut zero    j -1 = subst Counter {!!} (cut j zero)
cut (suc i) j -1 = subst Counter {!!} (cut i (suc j))

当试图证明+1和-1是相反的时候，问题就来了。我总是遇到这样的情况，即我需要为引入的这些subst创建一个消除器，比如

subst-elim : {A : Set} → {B : A → Set} → {x x′ : A} → {x=x′ : x ≡ x′} → {y : B x} → subst B x=x′ y ≡ y
subst-elim {A} {B} {x} {.x} {refl} = refl

但事实证明这是一个问题:它不被类型检查器接受，因为subst B x=x' y : B x'和y : B x……

Answer 1

如果您在stdlib中使用Relation.Binary.HeterogeneousEquality，则可以声明subst-elim的类型。然而，我可能只是在with或rewrite子句中对x≡x‘的最终证明进行模式匹配，所以您不必显式地创建消除符，也就没有输入问题。