Устранение субстрата для доказательства равенства

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

вы можете указать тип вашего sub-elim, если вы используете Relation.Binary.HeterogeneEquality из stdlib.Однако я, вероятно, просто сопоставлю шаблон с возможным доказательством x ≡ x ′ в предложении with или rewrite, так что вам не нужно создавать явный элиминатор и, таким образом, не возникнет проблем с печатанием.