I'm currently following the Software Foundations book, I am currently on the Lists chapter. However, I'm having a hard time wrapping my head around a specific case of pattern matching and, due to being a beginner in Coq, I'm not sure about how to find the answer of this question.
So, the exercise was to create a Fixpoint to calculate how many nat v we have in a list s (a bag, more specifically).
I decided to use pattern matching for this, but if I tried to define a function like this:
Fixpoint count' (v: nat) (s: bag) : nat :=
match s with
| nil => O
| h :: t => match h with
| v => S (count' v t)
end
end.
and tried to apply this function to, let's say,
Example test_count1: count' 1 [1;2;3;1;4;1] = 3.
I would end up with 6 = 3. My understanding is that matching h with v is always "true", so it ends up counting every element of the list.
But why does it happen? How could we compare, using pattern matching, the values of both h and v?
PS: I have already solved this exercise using an auxiliary function that compares if h and v are equal, but I'm wondering if this can be achieved only using built-in pattern matching.
The pattern
match h with
| v => S (count' v t)
end
introduces a new variable v bound to h, shadowing the existing v. It is equivalent to a let expression:
let v := h in S (count' v t)
(* or, without shadowing *)
let v1 := h in S (count' v1 t)
Instead, to compare h and v, use a comparison function:
if h =? v then ... else ...