Hello Agda users, recently I have encountered a strange problem.<br><br>See code below.<br><br>While defining equality between elements of Fin n, the two definitions<br>fineq and fineq&#39; below behave differently when type checking. The fist<br>
definition defined by using equality on ℕ where the second is defined<br>directly.<br><br>At the end of the program, where giving an element of Result, the final <br>proof that Fineq (suc zero) (negate zero) fails with fineq but succeeds with<br>
fineq&#39;. Agda allows for the trivial proof to be refined but then when type<br>checked fails with the error:<br><br>zero != (suc 0) of type ℕ<br>when checking that the expression tt has type<br>Fineq 2 (suc zero) (negate _56)<br>
<br>From the error message it looks like that there are holes in the term, this<br>should not be the case as all terms are grounded.<br><br>Could someone explain why these two definitions provide different behavior?<br>To me they appear that they should be the same. I have tried using refl and<br>
it worked with no problems, but am interested why this occurs.<br><br>I have tested using the latest development version of both Agda and the standard<br>library.<br><br>Karim Kanso<br>Swansea University<br><br>module oddprob where<br>
<br>open import Data.Nat<br>open import Data.Fin<br>open import Data.Bool<br>open import Data.Unit<br><br>_==_ : ℕ → ℕ → Bool<br>zero == zero = true<br>(suc n) == (suc m) = n == m<br>_ == _ = false<br><br>fineq : (n : ℕ) → Fin n → Fin n → Bool<br>
fineq k n m = toℕ n == toℕ m<br><br>fineq&#39; : (n : ℕ) → Fin n → Fin n → Bool<br>fineq&#39; .(suc n) (zero {n}) zero = true<br>fineq&#39; .(suc n) (zero {n}) (suc i) = false<br>fineq&#39; .(suc n) (suc {n} i) zero = false<br>
fineq&#39; .(suc n) (suc {n} i) (suc i&#39;) = fineq&#39; n i i&#39;<br><br>Fineq : (n : ℕ) → Fin n → Fin n → Set<br>Fineq k n m = T (fineq k n m)<br><br>negate : (s : Fin 2) → Fin 2<br>negate zero = suc zero<br>negate (suc zero) = zero<br>
negate (suc (suc ()))<br><br>data Result (a : Fin 2) : Fin 2 → Set where<br>  res : (b : Fin 2) → Fineq 2 b (negate a) → Result a b<br><br>r : Result zero (suc zero)<br>r = res (suc zero) tt<br>