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

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 Не получая следующее сообщение об ошибке от Type Checker:

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′]

(Если вам интересно, вот какой-то не связанный с собой: Устранение SUP, чтобы доказать равенство)

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′ унифицируются.

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

РЕДАКТИРОВАТЬ: AFAICT HET. Равенское поведение все же.