1

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

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.
  - ...

但我不知道如何完成它......有人可以帮忙吗？

4

1 回答 1

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_correct来自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 *)
于 2021-05-24T15:54:41.730 回答