Proving identity for binary operator on Fin

Question

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?

You're missing the {n = Z} (FS s) f' case from your definition. Is that intended? — András Kovács
@András: if n = Z then the type Fin (S n) becomes Fin 1, and so FZ is the only legal constructor. — j11c
@Cactus: I tried this just now, but when I load the theorem prover it just gives me the goal {hole0} : (m : Nat) -> (f : Fin (S m)) -> FZ +- f = f: no mention of the value of n. And when I try to compute it does nothing. — j11c

András Kovács András Kovács · Accepted Answer · 2015-07-26T18:38:33

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')

Proving identity for binary operator on Fin

1 Answers