Congruenza per l'uguaglianza eterogenea

Question

Sto cercando di usare l'uguaglianza eterogeneo per dimostrare le dichiarazioni che coinvolgono questo tipo di dati indicizzati:

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

sono stato in grado di scrivere le mie prove utilizzando Relation.Binary.HeterogenousEquality.≅-Reasoning, ma solo assumendo la seguente proprietà congruenza:

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′ = {!!}

Tuttavia, non posso pattern match sul k≅k′ essere refl senza ottenere il seguente messaggio di errore dal tipo di controllo:

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

e se cerco di fare un'analisi caso su k≅k′ (vale a dire utilizzando C-c C-c dal frontend Emacs) per assicurarsi che tutti gli argomenti impliciti siano correttamente abbinati rispetto ai loro vincoli imposti dal refl, ottengo

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

(se siete interessati, qui ci sono alcuni retroscena non rilevanti: Eliminando subst per dimostrare l'uguaglianza )

Answer 1

Che cosa si può fare è prendere una prova ulteriore che i due indici sono uguali:

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

Il problema originale è che la conoscenza Counter n ≅ Counter n′ non implica n ≡ n′ perché costruttori di tipo non vengono considerati iniettiva (c'è un --injective-type-constructors bandierina per questo, che di fatto rende la partita passare attraverso, ma è noto per essere in contrasto con terzo escluso ), così mentre si può concludere che i due tipi sono uguali non riscriverà n a n′ e così si ottiene che l'errore quando si controlla se in seguito k e k′ sono unificabili.

Dal Counter n ha esattamente n elementi, in realtà è possibile dimostrare Counter è iniettiva usando qualcosa come il principio dei cassetti (e uguaglianza forse decidibile per naturali), in modo che si possa fare senza l'argomento n ≅ n′, anche se che sarebbe disordinato.

Modifica: AFAICT l'Het. comportamento uguaglianza è ancora lo stesso.