我试图将 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
and -1
是倒数。我不断遇到需要消除器的情况subst
s 介绍,即类似的东西
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'
and y : B x
...
如果您使用 stdlib 中的 Relation.Binary.HeterogeneousEquality,则可以指定 subst-elim 的类型。
然而,我可能只是在 with 或 rewrite 子句中对 x ≠ x′ 的最终证明进行模式匹配,因此您不必制作显式的消除器,因此没有打字问题。
本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)