Destroying the result of applying a predicate function

Question

I am new to Coq and am asking a quick question about destruction tactics. Suppose I have a count function that counts the number of occurrences of a given natural number in a list of natural numbers:

 Fixpoint count (v : nat) (xs : natlist) : nat := match xs with | nil => 0 | h :: t => match beq_nat hv with | true => 1 + count v xs | false => count v xs end end. 

I would like to prove the following theorem:

 Theorem count_cons : forall (ny : nat) (xs : natlist), count n (y :: xs) = count n xs + count n [y]. 

If I proved a similar theorem for n = 0, I could simply destroy y to 0 or S y '. In the general case, what I would like to do is destruct (beq_nat ny) is true or false, but I cannot make it work - I do not see any part of the Coq syntax.

Any ideas?

Answer 1

Your code is corrupted

 Fixpoint count (v : nat) (xs : natlist) : nat := match xs with | nil => 0 | h :: t => match beq_nat hv with | true => 1 + count v xs (*will not compile since "count v xs" is not simply recursive*) | false => count v xs end end. 

you probably meant

 Fixpoint count (v : nat) (xs : natlist) : nat := match xs with | nil => 0 | h :: t => match beq_nat hv with | true => 1 + count vt | false => count vt end end. 

Using destruct is a great way to get your solution. But you need to remember a few things

• destruct is syntactic, that is, it replaces the terms expressed in your goal / assumptions. So you usually need something like simpl (works here) or unfold .
• the order of the terms matters. destruct (beq_nat ny) is not the same as destruct (beq_nat yn) . In this case, you want the second one

As a rule, the destruct problem is not indicated, so you must do smarts yourself.

Anyway, start your proof

 intros ny xs. simpl. destruct (beq_nat yn). 

And all will be well.