Coq：证明归纳关系（相对于 Fixpoint）

Question

是否可以为 count 函数“转换”Fixpoint 定义：

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.

到 Inductive 谓词（我第一次尝试如下，但我不确定它是否正确）？（这个谓词应该描述函数的输入和输出之间的关系）

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.

为了确定它是否正确，我定义了这个定理（弱规范）：

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

但是我不知道怎么完成...有人可以帮忙吗？

Answer 1

您的关系不正确，因为当列表的头部不是您要查找的 Z 时，它缺少大小写。例如。没有 Count 0 [0] 1 类型的术语，尽管 count 1 [0] = 0。添加它，当你这样做时，使类型更自然（以相同的方式对参数进行排序，并使 z 成为参数）。

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.

至于正确性定理，好吧，count 在 l 上是归纳的，所以关于它的任何定理可能也是如此。

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.

请注意，有一种自动机制可以根据 count:

定义 Count 和 count_correct

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 *)

Coq：证明归纳关系（相对于 Fixpoint）

Coq: Prove Inductive relation (vs Fixpoint)

coq

coqide