Suppose we have:
Require Import ZArith Program.
Program Fixpoint range (from to : Z) {measure f R} : list :=
if from <? to
then from :: range (from + 1) to
else [].
I'd like to convince Coq that this terminates - I tried by measuring the size of the range as abs (to - from). However, this doesn't quite work because once the range is empty (that is, from >= to), it simply starts increasing once again.
I've also tried measuring with:
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)).
using my custom:
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.
and the cast:
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.
But it runs into the issue that I cannot show that None < None and using reflexive preceeds_eq makes the relation not well founded, which brings me back to the same problem.
Is there a way to convince Coq that range terminates? Is my approach completely broken?
If you map the length of you interval to nat using Z.abs_nat or Z.to_nat functions, and use a function deciding if the range is not-empty with a more informative result type (Z_lt_dec) then the solution becomes very simple:
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.
Using Z_lt_dec instead of its boolean counter-part gives you the benefit of propagating the proof of from < to into the context, which gives you the ability to deal with the proof obligation easily.