Congruence pour l'égalité hétérogène

Question

Je suis en train d'utiliser pour prouver l'égalité des déclarations hétérogènes impliquant ce type de données indexées:

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

j'ai pu écrire mes preuves en utilisant Relation.Binary.HeterogenousEquality.≅-Reasoning, mais seulement en assumant la propriété congruence suivante:

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

Cependant, je ne peux pas match de motif sur k≅k′ être refl sans faire passer le message d'erreur suivant du contrôleur de type:

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

et si je tente de faire une analyse de cas sur k≅k′ (à savoir en utilisant C-c C-c du frontend Emacs) pour vous assurer que tous les arguments implicites sont correctement adaptés par rapport à leurs contraintes imposées par le refl, je reçois

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

(si vous êtes intéressé, voici quelques informations non pertinentes: L'élimination de prouver Subst d'égalité)

Answer 1

Ce que vous pouvez faire est de prendre une preuve supplémentaire que les deux indices sont égaux:

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

Le problème initial est que la connaissance Counter n ≅ Counter n′ ne signifie pas n ≡ n′ parce que les constructeurs de type ne sont pas supposés être injective (il y a un --injective-type-constructors de drapeau pour ce qui en fait fait le match aller à travers, mais il est connu pour être incompatible avec milieu exclu ), si bien qu'il peut conclure que les deux types sont égaux, il ne sera pas réécrire n à n′ et

ainsi vous obtenez cette erreur quand il vérifie si plus tard k et k′ sont unifiable.

Depuis Counter n a exactement n éléments, il est en fait possible de prouver Counter est injective en utilisant quelque chose comme le principe de pigeonhole (et l'égalité peut-être décidable pour Naturals), de sorte que vous pouvez faire sans l'argument n ≅ n′, bien que ce serait désordre.

Edit: AFAICT Het. le comportement de l'égalité est toujours le même.