I'm trying to use heterogenous equality to prove statements involving this indexed datatype:
data Counter : ℕ → Set where
cut : (i j : ℕ) → Counter (suc i + j)
I was able to write my proofs using Relation.Binary.HeterogenousEquality.≅-Reasoning
, but only by assuming the following congruence property:
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′ = {!!}
However, I can't pattern match on k≅k′
being refl
without getting the following error message from the type checker:
Refuse to solve heterogeneous constraint
k : Counter n =?= k′ : Counter n′
and if I try to do a case analysis on k≅k′
(i.e. by using C-c C-c
from the Emacs frontend) to make sure all the implicit arguments are properly matched with respect to their constraints imposed by the refl
, I get
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′]
(if you're interested, here are some non-relevant background: Eliminating subst to prove equality)
data Counter (n : ℕ) : Set where cut : (i j : ℕ) → (i+j+1=n : suc (i + j) ≡ n) → Counter n
– Cactus Feb 17 '12 at 13:43