2

假设我们有：

Require Import ZArith Program.

Program Fixpoint range (from to : Z) {measure f R} : list  :=
  if from <? to
  then from :: range (from + 1) to
  else [].

我想说服 Coq 这将终止 - 我尝试通过将范围的大小测量为abs (to - from). 但是，这并不完全有效，因为一旦范围为空（即from >= to），它就会再次开始增加。

我也尝试过测量：

Definition get_range (from to : Z) : option nat :=
  let range := (to - from) in 
    if (range <? 0)
    then None
    else Some (Z_to_nat (Z.abs range) (Z.abs_nonneg range)).

使用我的自定义：

Definition preceeds_eq (l r : option nat) : Prop :=
  match l, r with
    | None, None         => False
    | None, (Some _)     => True
    | (Some _), None     => False
    | (Some x), (Some y) => x < y
  end.

和演员：

Definition Z_to_nat (z : Z) (p : 0 <= z) : nat.
Proof.
  dependent destruction z.
    - exact (0%nat).
    - exact (Pos.to_nat p).
    - assert (Z.neg p < 0) by apply Zlt_neg_0.
      contradiction.
Defined.

但它遇到了我无法证明这一点的问题，None < None并且使用反身preceeds_eq使关系没有很好的基础，这让我回到了同样的问题。

有没有办法说服 Coqrange终止？我的方法完全被打破了吗？

4

1 回答 1

3

如果您将间隔的长度映射到natusingZ.abs_nat或Z.to_nat函数，并使用一个函数来确定范围是否为非空，并使用更多信息的结果类型 ( Z_lt_dec)，那么解决方案将变得非常简单：

Require Import ZArith Program.

Program Fixpoint range (from to : Z) {measure (Z.abs_nat (to - from))} : list Z :=
  if Z_lt_dec from to
  then from :: range (from + 1) to
  else [].
Next Obligation. apply Zabs_nat_lt; auto with zarith. Qed.

使用Z_lt_dec而不是其布尔对应部分可以让您将证明传播from < to到上下文中，这使您能够轻松处理证明义务。

于 2018-01-05T22:44:43.107 回答