Нахождение обоснованного отношения, чтобы доказать завершение функции, которая в какой-то момент перестает убывать

Question

Предположим, у нас есть:

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 делает связь недостаточно обоснованной, что возвращает меня к той же проблеме.

Есть ли способ убедить Coq, что range заканчивается? Мой подход полностью сломан?

Answer 1

Если вы сопоставите длину вашего интервала с nat с помощью Z.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 в контекст, который дает вам возможность легко справиться с обязательством доказательства.