Proof of the identity for the binary operator on Fin
I have defined the operator +-
(ignore the dreadful name) like this:
infixr 10 +-
(+-) : Fin (S n) -> Fin (S m) -> Fin (S (n + m))
(+-) {n} {m} FZ f' = rewrite plusCommutative n m in weakenN n f'
(+-) {n = S n} (FS f) f' = FS (f +- f')
It is supposed to behave exactly +
as defined on Fin
, but the upper bound on the result is tighter by 1. As far as I can tell, it works correctly.
The problem I am facing is trying to prove that (FZ +- f) = f
to anyone f : Fin n
. I do not expect this to be true in general, because it will usually FZ +- f
have a looser border than it f
is due to the challenge weakenN
. However, in the specific case where it FZ
has a type Fin 1
, then the types (and values) must match.
Is there a way to tell Idris that I only want to assert equality in this particular case and not for all possible types FZ
? Or is there a completely different approach I should be taking?
source to share
If we change the definition for a little (+-)
, the proof becomes easy:
import Data.Fin
infixr 10 +-
total
(+-) : Fin (S n) -> Fin (S m) -> Fin (S (n + m))
(+-) {n = Z} {m = m} a b = b
(+-) {n = (S n)}{m = m} FZ b = rewrite plusCommutative (S n) m in weakenN (S n) b
(+-) {n = (S n)}{m = m} (FS a) b = FS (a +- b)
lem : (f : Fin (S n)) -> the (Fin 1) FZ +- f = f
lem FZ = Refl
lem (FS x) = Refl
This is checked because the rewrite
right side of the definition (+-)
happens with normalization to specific values instead of substitutions / coercions.
On the other hand, if we want to stick to the original definition for (+-)
, then rewrite
it will not disappear, and we are in a larger world, because now we have to work with heterogeneous equalities. I did a heterogeneous equality proof in Agda, however, I couldn't get it to work in Idris in a short time, and I find getting it to work would be quite a painful experience. Here he is in Agda.
Note that we would have to add another case to the original definition to make the evidential properties in the first place. This is because it does not pass coverage testing as is. It is clear to us that Fin 1
it only has a construct FZ
, but this must also be explained to the compiler:
(+-) : Fin (S n) -> Fin (S m) -> Fin (S (n + m))
(+-) {n} {m} FZ f' = rewrite plusCommutative n m in weakenN n f'
(+-) {n = Z} (FS FZ) f' impossible
(+-) {n = S n} (FS f) f' = FS (f +- f')
source to share