Coq: Prove Inductive relation (vs Fixpoint)

Question

Is it possible to "convert" a Fixpoint definition for the count function:

Fixpoint count (z: Z) (l: list Z) {struct l} : nat :=
  match l with
  | nil => 0%nat
  | (z' :: l') => if (Z.eq_dec z z')
                  then S (count z l')
                  else count z l'
  end.

To an Inductive predicate (I have my first attempt bellow, but I'm not sure if it is correct)? (This predicate is supposed to describe the relation between the function's input and output)

Inductive Count : nat -> list Z -> Z -> Prop :=
  | CountNil : forall (z: Z), Count 0 nil z
  | CountCons: forall (n: nat) (l0: list Z) (z: Z), Count n l0 z -> Count (S n) (cons z l0) z.

To find out if it's correct, I defined this Theorem (weak specification):

Theorem count_correct : forall (n: nat) (z: Z) (l: list Z), Count (count z l) l z.
Proof.
  intros.
  destruct l.
  - constructor.
  - ...

But I don't know how to complete it... Anyone can help?

Answer 1

Your relation is incorrect because it is missing the case for when the head of your list is not the Z you're looking for. E.g. there is no term of type Count 0 [0] 1 even though count 1 [0] = 0. Add that, and while you're at it make the type more natural (order the arguments in the same way and also make z a parameter).

Inductive Count (z : Z) : list Z -> nat -> Prop :=
  | CountNil : Count z nil 0
  | CountYes : forall l n, Count z l n -> Count z (z :: l) (S n)
  | CountNo  : forall z' l n, z <> z' -> Count z l n -> Count z (z' :: l) n.

As for the correctness theorem, well, count is inductive on l, so probably so should be any theorem about it.

Theorem count_correct (z : Z) (n : N) (l : list Z) : Count z l (count z l).
Proof.
  intros.
  induction l as [ | z' l rec].
  - constructor.
  - cbn [count].
    destruct (Z.eq_dec z z') as [<- | no]; constructor; assumption.
Qed.

Do note that there's an automated mechanism to define Count and count_correct from count:

Require Import FunInd.

Function count (z : Z) (l : list Z) {struct l} : nat :=
  match l with
  | nil => 0
  | z' :: l =>
    if Z.eq_dec z z'
    then S (count z l)
    else count z l
  end.
  
Print R_count. (* Like Count *)
(* Inductive R_count (z : Z) : list Z -> nat -> Set :=
     R_count_0 : forall l : list Z, l = nil -> R_count z nil 0
  | R_count_1 : forall (l : list Z) (z' : Z) (l' : list Z),
    l = z' :: l' ->
    forall _x : z = z',
    Z.eq_dec z z' = left _x ->
    forall _res : nat,
    R_count z l' _res -> R_count z (z' :: l') (S _res)
  | R_count_2 : forall (l : list Z) (z' : Z) (l' : list Z),
    l = z' :: l' ->
    forall _x : z <> z',
    Z.eq_dec z z' = right _x ->
    forall _res : nat,
    R_count z l' _res -> R_count z (z' :: l') _res. *)
Check R_count_correct. (* : forall z l _res, _res = count z l -> R_count z l _res *)
Check R_count_complete. (* : forall z l _res, R_count z l _res -> _res = count z l *)