How can I automate counting within proofs in Coq?

Question

I have a function count that counts how many times a given predicate is provable when applied to elements of a list. It is defined as follows:

Parameter T : Type.

Parameter dec: forall (p: T -> Prop) (w: T), {p w} + {~ (p w)}.

Fixpoint count (p: T -> Prop) (l: list T) := match l with
  | nil => 0
  | (cons head tail) => if (dec p head) then (1 + (count p tail)) else (count p tail)
end.

I then use this function to state lemmas like the following:

Parameter a b c: T.
Parameter q: T -> Prop.

Axiom Aa: (q a).
Axiom Ab: (q b).
Axiom Ac: ~ (q c).

Lemma example: (count q (cons a (cons b (cons c nil)))) = 2.

My proofs of such lemmas tend to be quite tedious:

Lemma example: (count q (cons a (cons b (cons c nil)))) = 2.
Proof.
unfold count.
assert (q a); [apply Aa| auto].
assert (q b); [apply Ab| auto].
assert (~ (q c)); [apply Ac| auto].
destruct (dec q a); [auto | contradiction].
destruct (dec q b); [auto | contradiction].
destruct (dec q c); [contradiction | auto].
Qed.

What can I do to automate such tedious proofs that involve computation with my count function?

Answer 1

Let's create our custom hint database and add your axioms there:

Hint Resolve Aa : axiom_db.
Hint Resolve Ab : axiom_db.
Hint Resolve Ac : axiom_db.

Now, the firstorder tactic can make use of the hint database:

Lemma example: count q (cons a (cons b (cons c nil))) = 2.
Proof.
  unfold count.
  destruct (dec q a), (dec q b), (dec q c); firstorder with axiom_db.
Qed.

---

We can automate our solution using the following piece of Ltac:

Ltac solve_the_probem :=
  match goal with
  |- context [if dec ?q ?x then _ else _] =>
      destruct (dec q x);
      firstorder with axioms_db;
      solve_the_probem
  end.

Then, unfold count; solve_the_probem. will be able to prove the lemma.