Destructing on the result of applying a predicate function

Question

I'm new to Coq and have a quick question about the destruct tactic. 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 h v with
        | true => 1 + count v xs
        | false => count v xs
      end
  end.

I'd like to prove the following theorem:

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

If I were proving the analogous theorem for n = 0, I could simply destruct y to 0 or S y'. For the general case, what I'd like to do is destruct (beq_nat n y) to true or false, but I can't seem to get that to work--I'm missing some piece of Coq syntax.

Any ideas?

Answer 1

Your code is broken

Fixpoint count (v : nat) (xs : natlist) : nat :=
 match xs with
  | nil => 0
  | h :: t =>
  match beq_nat h v 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 h v with
    | true => 1 + count v t
    | false => count v t
  end
end.

Using destruct is then a perfectly good way to get your solution. But, you need to keep a few things in mind

• destruct is syntactic, that is it replaces terms that are expressed in your goal/assumptions. So, you normally need something like simpl (works here) or unfold first.
• the order of terms matters. destruct (beq_nat n y) is not the same thing as destruct (beq_nat y n). In this case you want the second of those

Generally the problem is destruct is dumb, so you have to do the smarts yourself.

Anyways, start your proof

intros n y xs. simpl. destruct (beq_nat y n).

And all will be good.