k :=0
for i ←1 to n
c←a[i]
k←k+1
this is the algorithim to know the number of elements
Technically, yes, k <= i is an invariant but not a very useful one. The reason we use invariants is that we can use them to prove the state after the loop. With your invariant you can prove that k <= n holds after the loop. Although very true, that doesn't really help you trying to prove what the loop really does.
So what kind of invariant would be useful? We want to prove that k is equal to the number of elements that are both in a and b. Since we are looping over the elements in a, a good choice would be: k equals the number of elements up to a[i] that are also in b.
We now need to prove that this invariant holds. I'll keep it a bit sketchy so it's still up to you to formalize this.
Initially, we need to show that k = 0 is the number of elements before a[1] that are also in b. There are no such elements, so k = 0 is correct.
Now, given that ki is the number of elements up to a[i] that are also in b, we need to prove that the invariant holds for i+1. There are two options: either a[i+1] is in b, or not.
a[i+1] in b, then the number of elements up to a[i + 1] that are in b is one greater than the number of elements up to a[i] that are in b. Using our invariant, we thus need to show that ki+1 = ki + 1.a[i+1] not in b, then the number of elements up to a[i + 1] that are in b is equal to the number of elements up to a[i] that are in b. Using our invariant, we thus need to show that ki+1 = ki.I'll leave it up to you to prove those.