Устранение 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...


gadt agda
person Cactus    schedule 12.02.2012    source источник

Ответы (1)


arrow_upward
4
arrow_downward

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

person Saizan    schedule 13.02.2012
comment
HeterogenousEquality кажется правильным решением этой проблемы... Однако при попытке использовать это у меня возникает несколько похожая проблема: я не могу определить что-то вроде Counter-cong : ∀ {n n′} {A : ℕ → Set} → (f : ∀{n} → Counter n → A n) → {k : Counter n} {k′ : Counter n′} → k ≅ k′ → f k ≅ f k′, потому что тогда я получаю сообщение об ошибке Refuse to solve heterogeneous constraint k : Counter n =?= k′ : Counter n′... - person Cactus; 15.02.2012