消除subst来证明平等
我试图将 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...
I'm trying to representat mod-n counters as a cut of the interval [0, ..., n-1] into two parts:
data Counter : ℕ → Set where
cut : (i j : ℕ) → Counter (suc (i + j))
Using this, defining the two crucial operations is straightforward (some proofs omitted for brevity):
_+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))
The problem comes when trying to prove that +1 and -1 are inverses. I keep running into situations where I need an eliminator for these substs introduced, i.e. something like
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
but this turns out to be (somewhat) begging the question: it isn't accepted by the type checker, because subst B x=x' y : B x' and y : B x...
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
如果您使用 stdlib 中的 Relation.Binary.HeterogeneousEquality，则可以指定 subst-elim 的类型。
然而，我可能只是在 with 或 rewrite 子句中对 x ≠ x′ 的最终证明进行模式匹配，因此您不必制作显式的消除器，因此没有打字问题。
you can state the type of your subst-elim if you use Relation.Binary.HeterogeneousEquality from the stdlib.
However i'd probably just pattern match on the eventual proof of x ≡ x′ in a with or rewrite clause, so you don't have to make an explicit eliminator and so no typing problem.