Конгруэнтность для гетерогенного равенства

Question

Я пытаюсь использовать гетерогенное равенство, чтобы доказать утверждения, включающие этот индексированный тип данных:

data Counter : ℕ → Set where
  cut : (i j : ℕ) → Counter (suc i + j)

Я смог написать свои доказательства, используя Relation.Binary.HeterogenousEquality.≅-Reasoning, но только предполагаяследующее свойство конгруэнтности:

Counter-cong : ∀ {n n′} {k : Counter n} {k′ : Counter n′} →
               {A : ℕ → Set} → (f : ∀{n} → Counter n → A n) →
               k ≅ k′ → f k ≅ f k′
Counter-cong f k≅k′ = {!!}

Однако я не могу сопоставить шаблон с k≅k′, являющимся refl, без получения следующего сообщения об ошибке из проверки типов:

Refuse to solve heterogeneous constraint 
    k : Counter n =?= k′ : Counter n′

и если я попытаюсь выполнить анализ кейса на k≅k′ (то есть, используя C-c C-c из внешнего интерфейса Emacs), чтобы убедиться, что все неявные аргументы правильно сопоставлены с их ограничениями, наложенными refl, я получу

Cannot decide whether there should be a case for the constructor
refl, since the unification gets stuck on unifying the 
inferred indices 
    [{.Level.zero}, {Counter n}, k] 
with the expected indices 
    [{.Level.zero}, {Counter n′}, k′]

(если вам интересно, вот несколько не относящихся к делу фонов: Устранение саба для доказательства равенства )

Answer 1

Что вы можете сделать, это получить дополнительное доказательство того, что два индекса равны:

Counter-cong : ∀ {n n′} {k : Counter n} {k′ : Counter n′} →
               {A : ℕ → Set} → (f : ∀{n} → Counter n → A n) →
               n ≅ n′ → k ≅ k′ → f k ≅ f k′
Counter-cong f refl refl = refl

Первоначальная проблема заключается в том, что знание Counter n ≅ Counter n′ не подразумевает n ≡ n′, потому что конструкторы типов не предполагаются инъективными (для этого есть флаг --injective-type-constructors, который фактически делает совпадение проходным, но известно быть несовместимым с исключенным средним), поэтому, хотя он может заключить, что два типа равны, он не будет перезаписывать n в n′, и поэтому вы получите эту ошибку, когда позже проверите, если k и k′ unifiable.

Так как Counter n имеет ровно n элементов, фактически можно доказать, что Counter инъективен, используя что-то вроде принципа голубиного отверстия (и, возможно, разрешимого равенства для натуральных чисел), так что вы можете обойтись без n ≅ n′ аргумент, хотя это было бы грязно.

Редактировать: AFAICT Het. Поведение равноправия остается прежним.