Hi all, I am trying to define a fixpoint whose measure relation isn't the standard < on nat, but rather an "eventually less than" on sequences of nats, as follows:

```
Program Fixpoint eventually_lt {f : nat -> nat} (a b : nat * nat) {measure (max ((snd b) - (snd a)) ((snd a) - (snd b)))}: Prop :=
let '(n,N) := a in
let '(m,M) := b in
match N =? M with
| true => n < m
| false =>
match (n,N), (m,M) with
(* step thru 2nd coord till N == M*)
| (n', N'), (m', M') => match N' <? M' with
| true => eventually_lt (f:=f) (f(S N'), S N') (m', M')
| false => eventually_lt (f:=f) (n', N') (f(S M'), S M')
end
```

Please forgive the confusion here, the 2nd coordinate N/M is the input (index) to the sequence as function

```
nat -> nat
```

This relation is all well and good, but it has an implicit argument that is the sequence itself. I am trying to define another Fixpoint which is my sequence, but its measure relation takes as argument this sequence itself which is circular. Coq does not allow me to provide this as argument to the relation. Is there a way around this circularity?

Can't the second `match`

there be simplified?

This function doesn't really make use of the first component of the tuple, but that business with the second `match`

makes me wonder if there isn't a typo somewhere.

Li-yao said:

This function doesn't really make use of the first component of the tuple, but that business with the second

`match`

makes me wonder if there isn't a typo somewhere. But I think you can simplify/refactor this definition to get rid of the dependency on`f`

.

The second match is redundant and came from a prior implementation and lazy editing, apologies on that I missed it when posting. You could rewrite as

```
Program Fixpoint eventually_lt {f : nat -> nat} (a b : nat * nat) {measure (max ((snd b) - (snd a)) ((snd a) - (snd b)))}: Prop :=
let '(n,N) := a in
let '(m,M) := b in
match N =? M with
| true => n < m
| false =>
match N <? M with
| true => eventually_lt (f:=f) (f(S N), S N) (m, M)
| false => eventually_lt (f:=f) (n, N) (f(S M), S M)
end
```

I don't see how you could get rid of f though.

this seems equivalent to

```
Program Fixpoint eventually_lt_aux (N M : nat) {measure (max (b - a) (a - b))} :=
match N =? M with
| true => (N, M)
| false => match N <? M with
| true => eventually_lt_aux (S N) M
| false => eventually_lt_aux N (S M)
end
end.
Definition eventually_lt f N M :=
let '(N, M) := eventuall_lt_aux N M in
f N < f M.
```

(unless the initial `fst a`

and `fst b`

aren't always `f (snd a)`

and `f (snd b)`

, in which case we can still write a eventually_lt_aux returning a pair of (bool * nat) where the bool says whether the nat changed)

And the loop must end at either `N`

or `M`

. It boils down to `max N M`

.

Gaëtan Gilbert said:

this seems equivalent to

`Program Fixpoint eventually_lt_aux (N M : nat) {measure (max (b - a) (a - b))} := match N =? M with | true => (N, M) | false => match N <? M with | true => eventually_lt_aux (S N) M | false => eventually_lt_aux N (S M) end end. Definition eventually_lt f N M := let '(N, M) := eventuall_lt_aux N M in f N < f M.`

(unless the initial

`fst a`

and`fst b`

aren't always`f (snd a)`

and`f (snd b)`

, in which case we can still write a eventually_lt_aux returning a pair of (bool * nat) where the bool says whether the nat changed)

I see, I agree this is a good rephrasing of the function. Thank you

But my concern in the original post is the following: Suppose I have a fixpoint later on which will use this relation. The fixpoint itself will be defining the sequence given here by `f`

. This is circular, no? My general question is, how do I define a function on `nat`

/ a sequence via fixpoint which satisfies `eventually_lt`

? Here, `f`

will not satisfy the usual `<`

used in fixpoint measures so it unfortunately cannot be defined this way (using the usual `<`

) and then later proved to satisfy `eventually_lt`

in a separate lemma.

What does "satisfies `eventually_lt`

" mean? With `eventually_lt`

defined as above, `eventually_lt f N M`

is always false, because `eventually_lt_aux`

always returns a pair of equal elements.

The general advice is "don't do cyclic definitions". Even in conventional mathematics circular definitions have to be justified by somehow breaking the cycle.

Sorry, when I said "satisfies" I meant that it can be used as the relation on a measure which could be used to define that sequence `f`

as a fixpoint. I see your point though, in my original definition I did not mean to increment the index N (w.l.o.g.) which was the lesser, I meant to increment the index M (w.l.o.g.) that was the greater of the two. But mistakenly I reversed that, incrementing the smaller index until the two were equal and leading to a function that would always return false. My intent was that a sequence `f : nat -> nat`

satisfies this "eventually less than" property, iff

$\forall N,M \in \mathbb{N}, \exists k \in \mathbb{N}: f(N) < f(M+k)$

Here assuming that `N < M`

WLOG. More and more I get the feeling fixpoint is not the way to express this in Coq, because of the circularity and how much this measure differs from the simple `<`

. Is there another way to define this property (and sequences that have this property) or does this math not fit into Coq?

```
Definitions eventually_lt (f : nat -> nat) : Prop :=
forall n m : nat, exists k : nat, f n < f (m + k).
```

Yes, I got to a definition something like this after you pointed out my error. My question though, as I said in the second half of my last reply, is how do I define a sequence which will actually have this property without also simply being a decreasing sequence? I suppose for decreasing we change it to

```
Definition eventually_lt (f : nat -> nat) : Prop :=
forall n m : nat, exists k : nat, f n > f (m + k).
```

Now the question is for an example of such a sequence which isn't simply decreasing. Here I am referencing the Coq documentation on Fixpoints that specify measures: https://coq.inria.fr/doc/V8.9.1/refman/addendum/program.html

In particular:

measure f ( R ) where f is a value of type X computed on any subset of the arguments and the optional (parenthesised) term (R) is a relation on X. By default X defaults to nat and R to lt.

And I am wanting to replace `R`

with `eventually_lt`

. But as I said before, it seems a Fixpoint isn't a good way to define such a sequence that has the property `eventually_lt`

but not the property `lt`

, because it would be circular as the Fixpoint itself would be the definition for `f`

. So, is there another way to define such an `f`

in Coq that has this property?

Indeed you don't need fixpoint to answer this question. You can do much simpler. The definition of such a sequence also won't need to mention `eventually_lt`

.

Before doing it in Coq, do you know how to answer it in normal math?

Sure, I think any periodic sequence would be a good start but the sequence would need some modification to the local minimum value of `f`

within a period, so that you could always find a lower value in a later period if your `N`

were at the local minimum of one of the periods. Something like a sine curve like

$f(n) = \lfloor 20 \frac{|\sin n|+1}{n} \rfloor$

But this relies on asymptotic behavior and the floor function (or any integer rounding) ruins the fact that it is actually having its local minima decrease after you get below a certain value. But for the purposes of using as a fixpoint's measure, this is probably fine.

another way to oscillate is $(-1)^n$. add 2 if you want it to be positive. And you get $2 + (-1)^n/n$. But since we're using `nat`

this is not expressible, but you can use the same idea to find an example for the version of the property with "<" instead of ">".

What do you think of this:

```
Definition f (n : nat) : nat :=
if Nat.even n then 0 else n.
```

That's great too! Definitely works for `<`

and was one of my first thoughts, but I realized that if I'm trying to mirror the relation `R`

for a Fixpoint, I need `>`

instead.

All of this work is for the purpose of defining a very specific function via fixpoint which now seems impossible to define, and it would rely on such a relation where the sequence is only decreasing in this loose eventual sense. The function in question finds references to `Sorts`

in Inductives, all via MetaCoq. Since these can be recursive (i.e. an inductive with another inductive as a parameter) we need a recursive function to find them, but we also know that the number of `Sorts`

in the next recursion may not be strictly less than the current number, only that eventually we will get to the end and have fewer of them.

(deleted)

Okay now it makes sense. The sequence you want to rely on is the number of reference to `Sorts`

at the nth iteration of your function, which satisfies that eventually lt property, so that it must be finite (and it couldn't be a function `nat -> nat`

).

If you're recursing through inductives, isn't a simpler measure the number of inductives you haven't seen yet? But in any case you can only make a fixpoint out of this if you have all of the inductives as a pure value, not hidden in MetaCoq's state.

Yes, it would be finite but of unknown bound so I thought it easier to think of as a function `nat -> nat`

which is eventually 0 after reaching the last recursion/parameter.

On your second point, I don't have a way to count how many inductives there are total. In fact, a simpler version of the function I'd like to construct simply counts those `Sorts`

instead of returning, say, a list of them. This is similar to counting how many inductives there are as parameters or fields, though it also includes counting `Sorts`

that occur bare in the fields/parameters and not inside an inductive in those locations. I have no way (that I know of) of knowing that count *a priori*, unless there is some MetaCoq functionality that I haven't found. But I have been looking for a while.

Last updated: Jun 23 2024 at 04:03 UTC