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

Question

Я пытаюсь использовать разнородное равенство доказать заявления с участием индексированного типа данных:

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

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

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

(если вы заинтересованы, вот некоторые несвойственных фон: Eliminating subst to prove equality)

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′ сделать esn't подразумевает n ≡ n′, потому что конструкторы типов не предполагаются инъективными (для этого есть флаг --injective-type-constructors, что фактически делает совпадение пройденным, но оно, как известно, несовместимо с исключенным средним), поэтому, хотя можно сделать вывод, что два типы равны, он не будет переписывать n в n′, и поэтому вы получите эту ошибку, когда она позже проверит, являются ли возможности k и k′.

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

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