I've defined an operator, +- (ignore the terrible name), as follows:
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')
The intention is that it behaves exactly like + as defined on Fin, but the upper bound of the result is tighter by 1. As far as I can tell, it works correctly.
The problem I'm having is in trying to prove that (FZ +- f) = f for any f : Fin n. I'm not expecting this to be true in general, because it will usually be the case that FZ +- f has a looser bound than f on account of the call to weakenN. However, in the particular case where the FZ has type Fin 1, then the types (and the values) ought to match up.
Is there any way of indicating to Idris that I only want to assert the equality in that particular case, rather than for all possible types of FZ? Or is there a completely different approach that I ought to be taking?
If we reshuffle the definition for (+-) a bit, 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 checks out because the rewrite on the right hand side of the (+-) definition happens to normalize to concrete values instead of substitutions/coercions.
On the other hand, if we'd like to stick with the original definition for (+-), then the rewrite doesn't go away, and we're in for a whole world of pain, because now we have to work with heterogeneous equalities. I did a proof with heterogeneous equalities in Agda, however I couldn't get it to work in Idris on short notice, and I believe making it work would be a rather painful experience. Here it is in Agda.
Note though that we would have to add one more case to the original definition in order to make proving properties about it feasible in the first place. That's because it doesn't pass the coverage checker as it is. It's evident to us that Fin 1 only has FZ as constructor, but this has to be also 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')