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?
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