Proof involving unfolding two recursive functions in COQ

Question

I've began learning Coq, and am trying to prove something that seems fairly simple: if a list contains x, then the number of instances of x in that list will be > 0.

I've defined the contains and count functions as follows:

Fixpoint contains (n: nat) (l: list nat) : Prop :=
  match l with
  | nil => False
  | h :: t => if beq_nat h n then True else contains n t
  end.

Fixpoint count (n acc: nat) (l: list nat) : nat :=
  match l with
  | nil => acc
  | h :: t => if beq_nat h n then count n (acc + 1) t else count n acc t
  end.

I'm trying to prove:

Lemma contains_count_ge1 : forall (n: nat) (l: list nat), contains n l -> (count n 0 l > 0).

I understand the proof will involve unfolding the definitions of count and contains, but then I'd like to say "the list cannot be nil, as contains is true, so there must be an element x in l such that beq_nat h x is true", and I've played around a bit but can't figure out how to use tactics to do this. Any guidance would be greatly appreciated.

Answer 1

Well, you pose many questions about basic Coq beyond what is IMO possible to address here. For this particular problem, I would proceed this way (in reality I would use the already provided lemmas in MathComp):

From Coq Require Import PeanoNat Bool List.

Fixpoint contains (n: nat) (l: list nat) : bool :=
  match l with
  | nil    => false
  | h :: t => if Nat.eqb h n then true else contains n t
  end.

Fixpoint count (n : nat) (l: list nat) : nat :=
  match l with
  | nil => 0
  | h :: t => if Nat.eqb h n then S (count n t) else count n t
  end.

Lemma contains_count_ge1 n l : contains n l = true -> count n l > 0.
Proof.
induction l as [|x l IHl]; simpl; [now congruence|].
now destruct (Nat.eqb_spec x n); auto with arith.
Qed.

My "standard" solution:

Lemma test n (l : list nat) : n \in l -> 0 < count_mem n l.
Proof. by rewrite lt0n => /count_memPn/eqP. Qed.

and different definitions of count and contains that may prove useful:

Fixpoint contains (n: nat) (l: list nat) : bool :=
  match l with
  | nil    => false
  | h :: t => Nat.eqb h n || contains n t
  end.

Fixpoint count (n : nat) (l: list nat) : nat :=
  match l with
  | nil    => 0
  | h :: t => Nat.b2n (Nat.eqb h n) + (count n t)
  end.