Proving `weaken` doesn't change the value of a number

Question

Let's say we want to prove that weakening the upper bound of a Data.Fin doesn't change the value of the number. The intuitive way to state this is:

weakenEq : (num : Fin n) -> num = weaken num

Let's now generate the defini... Hold on! Let's think a bit about that statement. num and weaken num have different types. Can we state the equality in this case?

The documentation on = suggests we can try to, but we might want to use ~=~ instead. Well, anyway, let's go ahead and generate the definition and case-split, resulting in

weakenEq : (num : Fin n) -> num = weaken num
weakenEq FZ = ?weakenEq_rhs_1
weakenEq (FS x) = ?weakenEq_rhs_2

The goal in the weakenEq_rhs_1 hole is FZ = FZ, which still makes sense from the value point of view. So we optimistically replace the hole with Refl, but only to fail:

When checking right hand side of weakenEq with expected type
        FZ = weaken FZ

Unifying k and S k would lead to infinite value

A somewhat cryptic error message, so we wonder if that's really related to the types being different.

Anyway, let's try again, but now with ~=~ instead of =. Unfortunately, the error is still the same.

So, how one would state and prove that weaken x doesn't change the value of x? Does it really make sense to? What should I do if that's a part of a larger proof where I might want to rewrite a Vect n (Fin k) with Vect n (Fin (S k)) that's obtained by mapping weaken over the original vector?

Answer 1

If you really want to prove that the value of the Fin n does not change after applying the weaken function, you would need to prove the equality of these values:

weakenEq: (num: Fin n) -> finToNat num = finToNat $ weaken num
weakenEq FZ     = Refl
weakenEq (FS x) = cong $ weakenEq x

Answer 2

To your second problem/Markus' comment about map (Data.Fin.finToNat) v = map (Data.Fin.finToNat . Data.Fin.weaken) v:

vectorWeakenEq : (v: Vect n (Fin k)) -> 
                 map Fin.finToNat v = map (Fin.finToNat . Fin.weaken) v
vectorWeakenEq [] = Refl
vectorWeakenEq (x :: xs) =
  rewrite sym $ weakenEq x in
  cong {f=(::) (finToNat x)} (vectorWeakenEq xs)

And to see why num = weaken num won't work, let's take a look at a counterexample:

getSize : Fin n -> Nat
getSize _ {n} = n

Now with x : Fin n, getSize x = n != (n + 1) = getSize (weaken x). This won't happen with functions which only depend on the constructors, like finToNat. So you have to constrain yourself to those and prove that they behave like that.