Stream: Coq users

Topic: Defining Fixpoint with new Relation on Sequences


view this post on Zulip Angelo Taranto (Mar 28 2024 at 17:38):

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?

view this post on Zulip Li-yao (Mar 28 2024 at 19:54):

Can't the second match there be simplified?

view this post on Zulip Li-yao (Mar 28 2024 at 19:57):

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.

view this post on Zulip Angelo Taranto (Mar 28 2024 at 21:20):

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.

view this post on Zulip Gaëtan Gilbert (Mar 28 2024 at 22:09):

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)

view this post on Zulip Li-yao (Mar 29 2024 at 15:11):

And the loop must end at either N or M. It boils down to max N M.

view this post on Zulip Angelo Taranto (Apr 04 2024 at 17:14):

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.

view this post on Zulip Li-yao (Apr 04 2024 at 17:19):

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.

view this post on Zulip Li-yao (Apr 04 2024 at 17:22):

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

view this post on Zulip Angelo Taranto (Apr 04 2024 at 17:55):

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

N,MN,kN:f(N)<f(M+k)\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?

view this post on Zulip Li-yao (Apr 04 2024 at 18:47):

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

view this post on Zulip Angelo Taranto (Apr 04 2024 at 20:25):

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?

view this post on Zulip Li-yao (Apr 04 2024 at 20:33):

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.

view this post on Zulip Li-yao (Apr 04 2024 at 20:35):

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

view this post on Zulip Angelo Taranto (Apr 04 2024 at 20:58):

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)=20sinn+1nf(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.

view this post on Zulip Li-yao (Apr 04 2024 at 21:09):

another way to oscillate is (1)n(-1)^n. add 2 if you want it to be positive. And you get 2+(1)n/n2 + (-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 ">".

view this post on Zulip Li-yao (Apr 04 2024 at 21:14):

What do you think of this:

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

view this post on Zulip Angelo Taranto (Apr 04 2024 at 21:34):

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.

view this post on Zulip Li-yao (Apr 04 2024 at 21:37):

(deleted)

view this post on Zulip Li-yao (Apr 04 2024 at 21:47):

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

view this post on Zulip Li-yao (Apr 04 2024 at 21:51):

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.

view this post on Zulip Angelo Taranto (Apr 05 2024 at 15:56):

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