gadt - 消除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 :Bx...

Answer 1

如果您使用 stdlib 中的 Relation.Binary.HeterogeneousEquality，则可以指定 subst-elim 的类型。然而，我可能只是在 with 或 rewrite 子句中对 x ≠ x′ 的最终证明进行模式匹配，因此您不必制作显式的消除器，因此不会出现打字问题。