Stream: Coq users

Topic: how termination is proved in Coq?


view this post on Zulip Sergei Meshveliani (Nov 24 2021 at 20:52):

Can anybody, please, explain me in simple words:
what are the tools in Coq (in the Gallina language?) for proving the program termination?

For example, I program computer algebra in Agda.
And a certain program of reduction of a polynomial f produces a sequence f = f(1) >e f(2) >e ...
of polynomials descending according to a certain order >e.
And it is proved constructively that that the >e order is constructively Noetherian (descending-halting):
there is known an algorithm that for any sequence S(i) finds k such that S(k) <=e S(k+1).

It is natural to expect that seeing this proof the compiler (its type checker part) must decide that the above function (program) terminates.

But the descending-halt condition is not enough for Agda,
it needs a proof for <e to be a
WellFounded order

-- see its nice definition in the Agda Standard library (src/Induction/WellFounded.agda).

In many cases WellFounded can be proved constructively as easy as Noetherianity.
But I tend to think that this is not in all cases.

On the other hand, people write the things of the following kind.

https://ncatlab.org/nlab/show/well-founded+relation
:
"
In constructive mathematics, we may prove that a well-founded relation has no infinite descent
(see Proposition 2.3), but not the converse
...
Remark 2.2.
We note that classical well-foundedness is really too strong for constructive (i.e., intuitionistic) mathematics, due to Proposition 2.1.

On the other hand, the infinite descent condition is too weak to be of much use in constructive mathematics.
It is the inductive notion of well-foundedness that is just right.
"

Now: what is the Coq approach to all this?

For example, for the Groebner basis method, various papers write that the normalization procedure for a polynomial produces a certain descending chain, and the corresponding order relation is constructively proved as decsending-halt, hence the procedure terminates.

And I guess that there is somewhere known the Groebner basis function in the Coq library which termination is based on this descending-halt property of <e.

Is this so?

view this post on Zulip Li-yao (Nov 24 2021 at 21:34):

Since you seem to be familiar with Agda, the short answer is "the same as in Agda".

How do you define "noetherian"? Wikipedia says it's the same thing as well_founded, the Coq standard library has a definition https://coq.inria.fr/stdlib/Coq.Sets.Relations_3.html#Noetherian which is also the same as well_founded, which is the same in Coq and Agda.

view this post on Zulip Sergei Meshveliani (Nov 24 2021 at 22:39):

Thank you.
For clarity, let us forget of the word Noetherian, and use instead a more concrete notion of descending-halting:
there is given an algorithm that for any sequence S(i) finds k such that not S(k) >e S(k+1).
This is a constructive expression of
"for each sequence S(i), its descending part is broken at some point k".

I asked: whether Coq (Gallina) can take a descending-halting proof to verify termination of a function (a program written in Gallina (in Coq?)).

Another point: looking into
https://ncatlab.org/nlab/show/well-founded+relation

I see that it calls Noetherian the same thing which is called WellFounded in the Agda Standard library !

According to the mathematical tradition, it is more correct to call Noetherian either the property of ascending-halt or or the property of descending-halt sequence.
So it is in textbooks on algebra (and E. Noether was an algebraist).

The matter is that constructively, WellFounded is not equivalent to the descending-halt condition.

Anyway, the second question remains as above.
Probably Coq has in its libraries (applied or standard) the Groebner basis function. And it needs a termination proof.
In the papers, the authors base this proof on the descending-halt (or maybe ascending-halt) condition.
As WellFounded is not equivalent to the descending-halt condition, then how it is proved in Coq the termination of the Groebner basis function?
References?
I think this must know the people, who deal with the multivariate polynomial algebra in Coq.

view this post on Zulip Alexander Gryzlov (Nov 24 2021 at 22:46):

The most convenient way is probably to use the Equations plugin or the Program mode.

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 01:12):

Li-yao said:

Since you seem to be familiar with Agda, the short answer is "the same as in Agda".

As a side note, while that's essentially correct, Agda has various kinds of cleverness on top of "structural recursion".

view this post on Zulip Sergei Meshveliani (Nov 25 2021 at 11:42):

As a side note, while that's essentially correct, Agda has various kinds of cleverness on top of "structural recursion".

I do not know just all of Agda. Probably you mean the following feature:

f (x  xs) = ... (g x (f xs))             -- (I)
....
h (suc n) = ... (foo n (h n))        -- (II)

In (I), f is called at a list (x ∷ xs), and its recursive call (f xs) in the right-hand part is syntactically smaller. So that Adga decides automatically on termination. Similarly it is for other data constructors, not only for lists.
Is this structural recursion?

The above structural thing is not of the library, it is of the language , the ability is built-in to the type checker.
This indeed often works. Also it often works introducing counter : Natural as an additional argument.
But this is not for all cases.
For example, consider f x = f (g x x) when it is proved (g x x) << x for a certain ordering << specified abstractly by its properties.
This cannot be held by structural recursion (if this is the word).
But if this << is proved as satisfying the descending-halt property, then the function f terminates. It is so in mathematics.

For difficult cases, there is _termination by a proved property of_ WellFounded _<_ for the relation _<_ introduced by the programmer.
The WellFounded data is defined in Agda in the Standard library, together with several theorem proofs for its properties.
The thing is nice and useful.
But in mathematics , it is often used the termination proof by proving the descending-halt property for some _<_ introduced.
Sometimes descending-halt is proved, and I do not know how to constructively prove
descending-halt ==> WellFounded.
Probably this cannot be proved as general.

view this post on Zulip Sergei Meshveliani (Nov 25 2021 at 11:51):

Alexander Gryzlov writes

The most convenient way is probably to use the Equations plugin or the Program mode.

Can you, please, explain in simple words, what is Equations plugin, Program mode ?

view this post on Zulip Alexander Gryzlov (Nov 25 2021 at 11:57):

Basically convenient ways to write functions using well-founded recursion.

view this post on Zulip Alexander Gryzlov (Nov 25 2021 at 11:57):

https://coq.inria.fr/refman/addendum/program.html
https://mattam82.github.io/Coq-Equations/

view this post on Zulip Alexander Gryzlov (Nov 25 2021 at 11:58):

Equations is newer and more powerful

view this post on Zulip Karl Palmskog (Nov 25 2021 at 11:58):

I think the usual terminology is structural vs. general recursion, right?

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 12:30):

Is this structural recursion?

Yes.

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 12:34):

Sometimes descending-halt is proved, and I do not know how to constructively prove descending-halt ==> WellFounded.
Probably this cannot be proved as general.

I suspect not, but in practice these matters only affect the theory of well-founded recursion, not (in essence) the concrete uses.

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 12:46):

However, https://eprints.whiterose.ac.uk/76642/7/schusterp1.pdf suggests this specific example is probably trickier, and surveys the details.

view this post on Zulip Sergei Meshveliani (Nov 25 2021 at 13:00):

Sometimes descending-halt is proved, and I do not know how to constructively prove descending-halt ==> WellFounded.
Probably this cannot be proved as general.

Paolo> I suspect not, but in practice these matters only affect the theory of well-founded recursion, not (in essence) the concrete uses.

I kept this in mind. Unfortunately this is not only the effect in theory.
Because for each concrete instance of descending-halt the programmer needs to individually invent a proof for
descending-halt + a thing ==> WellFounded.
And if language + standard do understand termination by descending-halt, then much of the programmer effort is saved.
1) I do not understand: what can be a fundamental reason for which the dependent type functional programming languages can handle WellFounded for termination and cannot handle descending-halt for this.
2) Can Standard library include constructive proofs for several theorems like
descending-halt + something reasonable ==> WellFounded ?
For example, is this possible for something reasonable being DecidableTotalOrder _<_ ?

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 13:03):

Because for each concrete instance of descending-halt the programmer needs to individually invent a proof for
descending-halt + a thing ==> WellFounded.

I've never seen proofs of that theorem. We just write recursive algorithms foo x (other args), and prove that recursive calls to foo x' are only done when x' <R x, when <R is a well-founded relation.

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 13:04):

In some complex cases, one can use derived principles (some examples appear in https://github.com/coq-community/almost-full and the linked paper, but it's not trivial).

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 13:07):

but a priori, descending-halt seems strictly weaker, since it just says that a specific sequence, ordered according to <=, is finite, not that no infinite sequences exist.

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 13:28):

in fact, one can surely prove descending-halt for non-well-founded relations — a stupid example is to pick a relation over Z, but then prove descending-halt because all elements of the sequence f(i) are positive, but other examples are probably possible.

view this post on Zulip Sergei Meshveliani (Nov 25 2021 at 13:47):

but a priori, descending-halt seems strictly weaker, since it just says that a specific sequence, ordered according to <=,
is finite, not that no infinite sequences exist.

It is good that it is weaker and also is constructive-mathematically sufficient for termination.
Why the DT programming systems avoid relying on it?

https://eprints.whiterose.ac.uk/76642/7/schusterp1.pdf

Great! Thank you. It also has references to inspect. One of these is by Lombardy & Perdry, in which have looked in.
I have an impression that all of them prove that many complex methods are constructive. But they rely in the end either on ascending-halt (say increаsing chain of ideals in a ring ) or descending-halt, and this is not accepted by Agda nor by Coq.
This is not for sure, this is by impression. Because these papers avoid simple problems. They start with cosmic problems in algebra, so that it is difficult to reduce the discourse to a simple special case that can be understood.

For example, I have a proof in Agda for termination of the algorithm NF for reducing a polynomial to the normal form as it is in the Groebner basis method. The proof bases strictly of WellFounded, without using any descending-halt. This was not easy to compose the proof.
But further, a more complex construct will follow in this method, with ordering among the _finite sets_ of monomials.
And there the ascendig(descending)-halt intrudes with more power, and one has a problem of how to eliminate this.

view this post on Zulip Sergei Meshveliani (Nov 25 2021 at 13:58):

in fact, one can surely prove descending-halt for non-well-founded relations — a stupid example is to pick a relation over Z,
but then prove descending-halt because all elements of the sequence f(i) are positive, but other examples are probably
possible.

This gives more reason for the approach "WellFounded is not enough, let the DT programming systems implement the rule
descending-halt + something reasonable ==> terminating".
?

view this post on Zulip Li-yao (Nov 25 2021 at 14:08):

It's also feasible to postulate excluded middle and just reason classically.

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 14:15):

@Li-yao It's not clear to me how exactly that would apply here...

view this post on Zulip Li-yao (Nov 25 2021 at 14:16):

Or if you want to keep the proofs constructive, you can also accept descending-halt as a good enough condition (if a well-foundedness claim is really that much harder to prove). It doesn't allow you to close the loop in Coq but you can defer the burden to the real world (e.g., extract the loop body and iterate it in OCaml).

view this post on Zulip Sergei Meshveliani (Nov 25 2021 at 14:16):

It's also feasible to postulate excluded middle and just reason classically.

This is only for the case when nobody is able to provide a constructive proof. This case is different.
A constructive proof gives more notion than non-constructive.

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 14:17):

A constructive proof gives more notion than non-constructive.

But then why are you complaining that the constructive proofs require stronger conditions?

view this post on Zulip Li-yao (Nov 25 2021 at 14:20):

I think not wanting to worry about constructivism is a perfectly acceptable and pragmatic stance, where introducing classical principles is not an admission of failure.

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 14:20):

maybe I see what's going on

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 14:21):

@Sergei 1. Just to clarify, it's _not_ the case that well-founded recursion is part of the kernel of these systems. It's a construction in libraries, that reduces wf-recursion to structural recursion.

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 14:21):

  1. Part of the reason is that you _can't_ just postulate "descending-halt + something reasonable ==> terminating".

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 14:22):

Once you find "something reasonable", you need to define how such fixpoints compute exactly.

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 14:23):

Adding a library construction is easier. If you can provide one, that's great!

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 14:24):

For extensions to the kernel, a proper study of the metatheory is necessary (and often not sufficient). That can take a PhD.

view this post on Zulip Sergei Meshveliani (Nov 25 2021 at 14:25):

But then why are you complaining that the constructive proofs require stronger conditions?

Because descending-halt ==> terminating is a constructive way to prove things, and I complain that it is not implemented in the DT programing systems. This tool will be more powerful than WellFounded.

view this post on Zulip Karl Palmskog (Nov 25 2021 at 14:25):

these days, I guess one could formalize extensions to kernel in MetaCoq? Not at all trivial, but soundness could conceptually be reduced to existing soundness of Coq.

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 14:26):

@Sergei is it constructive tho? You just said "It is natural to expect that seeing this proof the compiler (its type checker part) must decide that the above function (program) terminates.", which is plausible but not obvious to me.

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 14:27):

Even intuitively, I agree that, under descendin-halting, the sequence cannot be infinite. And if we had double-negation elimination (DNE), then the sequence would be finite. But DNE is classical!

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 14:31):

I'm not an expert here, but a few principles exist which let you prove termination using semi-classical means (https://ncatlab.org/nlab/show/principle+of+omniscience is a somewhat famous one). In such cases, your actual algorithm will terminate, but the termination proof requires some limited amount of classical reasoning. _Some_ schools of constructive mathematics accept such principles.

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 14:34):

For this example, nLab also mentions that this "obvious principle" fails in a certain topos; that might even be a model of type theory/CIC/Coq? If so, this principle should not be hard-coded in Coq.

view this post on Zulip Sergei Meshveliani (Nov 25 2021 at 14:37):

Well, somehow build in to the implementation kernel (to the type checker):
"accept: relied of descending-halt ==> terminating".
Similar as it is now "relied of WellFounded ==> terminating".
?
I proposed this to Agda, with certain more details. But the experts wrote that this is somehow inconsistent with the dependent types principles. I did not understand their explanation, and the proposal is just hanging. Probably they are right, but I do not understand: a specific domain, a terminology ...
This is in the Adga e-mail archive somewhat of last two years.

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 14:41):

Feel free to provide a link, but Agda's usually more open to extensions than Coq for a bunch of reasons, so if your idea is inconsistent in Agda, it's likely inconsistent in Coq as well.

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 14:43):

But again, this is only an heuristic argument — and maybe you don't even mean "inconsistent" in the technical sense of "allows proving false".

view this post on Zulip Sergei Meshveliani (Nov 25 2021 at 14:51):

Well: define descending-halt _<_ on A as

forall (f : Natural  -> A) ->  exists (i : Natural)  such that   (not (f  (1+i) < f i))

That is the function (algorithm) returns a pair (i , any needed proof for the inequality negation).
What evil could happen to the type checker if it accepts this rule of descending-halt ==> terminating ?

view this post on Zulip Li-yao (Nov 25 2021 at 14:53):

You can already postulate stuff in Agda and Coq, there is no reason for adding it to the kernel, especially when there is no computational interpretation for it.

view this post on Zulip Gaëtan Gilbert (Nov 25 2021 at 14:55):

the real question is what do you mean by terminating?

view this post on Zulip Sergei Meshveliani (Nov 25 2021 at 15:03):

You can already postulate stuff in Agda and Coq, there is no reason for adding it to the kernel, especially when there is no
computational interpretation for it.

descending-halt is not a postulate, it is a definition. And it is formulated easily in Agda.
As to descending-halt ==> terminating, I suggest it to be treated as a postulate.
But it cannot be formulated in Agda. Because the property of terminating cannot be expressed in Agda, this notion is built in to the type checker.
For example, the programmer can express in Agda "the function f(x, y) is commutative" as a type declaration.
But one cannot express "the function f terminates" as a type declaration.

view this post on Zulip Gaëtan Gilbert (Nov 25 2021 at 15:04):

but what function is terminating when you have the descending-halt?

view this post on Zulip Li-yao (Nov 25 2021 at 15:06):

Postulate descending_halt _<_ -> well_founded _<_

view this post on Zulip Sergei Meshveliani (Nov 25 2021 at 15:11):

but what function is terminating when you have the descending-halt?

The same function which is terminating when the program uses WellFounded.
For using WellFounded _< _ there is a way to write a function f which termination is by referring to the proof for WellFounded _<_.
And the type checker understands this.
Similarly, the function body for f will have to refer to the proof for descending-halt _<_.
?

view this post on Zulip Sergei Meshveliani (Nov 25 2021 at 15:25):

Postulate descending_halt _<_ -> well_founded _<_.

Then it will be probably possible to prove a contradiction.

view this post on Zulip Gaëtan Gilbert (Nov 25 2021 at 15:34):

I don't think there's a contradiction
it's probably provable up to axiom of choice and/or excluded middle

view this post on Zulip Gaëtan Gilbert (Nov 25 2021 at 16:11):

the proof:

Axiom choice : forall {A B}, (forall a:A, inhabited (B a)) -> inhabited (forall a, B a).
Axiom DNE : forall {A}, ~ ~ A -> A.

Lemma not_forall_exists {A} {P:A->Prop} : ~ (forall x, P x) -> inhabited (sigT (fun x => ~ P x)).
Proof.
  intros nF.
  apply DNE.
  intros nE.
  apply nF;intros x.
  apply DNE;intros nP.
  apply nE. constructor;exists x;assumption.
Qed.

Section S.

  Variables (A:Type) (R:A -> A -> Prop).
  Infix "<" := R.

  Lemma not_acc_exists0 (a:A) : ~ Acc R a -> inhabited (sigT (fun b => R b a /\ ~ Acc R b)).
  Proof.
    intros nAcc.
    assert (nAcc':~ (forall b, R b a -> Acc R b)) by (intros nB;apply nAcc;constructor;exact nB);
      clear nAcc;rename nAcc' into nAcc.
    apply not_forall_exists in nAcc.
    destruct nAcc as [[x nX]].
    apply not_forall_exists in nX.
    destruct nX as [[Hx nX]].
    constructor;now exists x.
  Qed.

  Definition not_acc_exists : inhabited (forall a, ~ Acc R a -> sigT (fun b => R b a /\ ~ Acc R b))
    := choice (fun a => choice (not_acc_exists0  a)).

  Definition not_acc_F :
    sigT (fun a : A => ~ Acc R a) -> (forall a, ~ Acc R a -> sigT (fun b => R b a /\ ~ Acc R b)) ->
    nat -> {a : A & ~ Acc R a}.
  Proof.
    intros v0 F.
    fix not_acc_F 1; intros [|n].
    - exact v0.
    - destruct (not_acc_F n) as [vn nHn].
      apply F in nHn.
      destruct nHn as [vSn [_ nHSn]].
      exists vSn;assumption.
  Defined.

  Lemma not_acc_F_spec v0 F n : projT1 (not_acc_F v0 F (S n)) < projT1 (not_acc_F v0 F n).
  Proof.
    simpl.
    destruct (not_acc_F v0 F n) as [vn nHN];clear.
    destruct (F vn nHN) as [? [? ?]].
    simpl;assumption.
  Qed.

  Definition halt := forall f, inhabited (sigT (fun i => not (f (S i) < f i))).

  Theorem wf (H:halt) : well_founded R.
  Proof.
    apply choice in H.
    destruct H as [H].
    destruct not_acc_exists as [F].
    intros a;apply DNE;intros nHa.
    pose proof (existT (fun a => ~ Acc R a) a nHa) as v0;clear a nHa.
    pose (f := fun n => projT1 (not_acc_F v0 F n)).
    destruct (H f) as [i nH].
    apply nH.
    apply not_acc_F_spec.
  Qed.

End S.

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 16:54):

(deleted)

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 16:55):

(deleted)

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 17:00):

Nevermind; that proof makes sense to me. It'll just mean that one can't necessarily compute using wf, but Acc_intro_generator/stdpp's wf_guard should help with that in many cases.

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2021 at 17:28):

There is quite a bit of literature on the constructive formulation of noetherianness. There are various non-equivalent formulations, but it's generally agreed upon that the most natural one to consider in MLTT is indeed the well-founded predicated based on Acc .

view this post on Zulip Sergei Meshveliani (Nov 25 2021 at 18:43):

I don't think there's a contradiction
it's probably provable up to axiom of choice and/or excluded middle

May be, not a contradiction. But probably something from which excluded middle is derived.
Right?
If so, then this is not the point.

view this post on Zulip Sergei Meshveliani (Nov 25 2021 at 19:19):

Paolo writes

Feel free to provide a link, but Agda's usually more open to extensions than Coq for a bunch of reasons,
so if your idea is inconsistent in Agda, it's likely inconsistent in Coq as well.

The reason for asking the Coq cafe is another.
So far, I like Agda, for a certain reasons.
And in Agda, I do not not see any other computer algebra program than mine.
And this year I come up to multivariate polynomials, to Groebner bases.
This meets the question of providing termination, when Agda requires WellFounded
while the known to me theory is satisfied with the descending-(ascending)-halt condition .
In Agda, I do not know any programs for Groebner basis, I am going to try such, with the Agda proofs.
And in Coq, there must be such. I do not know, may be, by L.Pottier.
If so, then I wonder of a small point: of how does it provide termination, in detail.
And I discover now that Coq also always relies on WellFounded, only it calls it Noetherian !
(which word is misleading, to my mind, even despite of what Wikipedia could write).
The papers write about constructive Groebner basis in general, but always avoid this concrete question about possible implementation in a system of the certified programming.

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2021 at 19:32):

What I don't understand in @Sergei 's question is why this matter for practical uses. Obviously you can't prove internally that classical noetherian implies well-foundedness, but by some meta-theoretical argument you can probably argue that any closed instance of the first implies the second.

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2021 at 19:33):

(You might have to refine a bit this statement to make it literally true, but this is the spirit.)

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2021 at 19:33):

So there is no point in taking the weaker statement as a hypothesis.

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2021 at 19:34):

It's like argueing that funext is critical for some development. Obviously it's easier to prove stuff when you have it as an axiom, but any practical instance of it can be removed by explicit setoid manipulation.

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2021 at 19:36):

Do you have an example of some ring construction you're interested in that preserves classical noetherianness but breaks ideal well-foundedness

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2021 at 19:38):

(which word is misleading, to my mind, even despite of what Wikipedia could write).

btw, it's a common phenomenon that constructive logic is finer than classical logic and the precise phrasing of a property becomes important, and I don't think it precludes reusing the name from the classical world into the intuitionistic world

view this post on Zulip Sergei Meshveliani (Nov 25 2021 at 20:13):

Paolo writes

Part of the reason is that you _can't_ just postulate "descending-halt + something reasonable ==> terminating".
One you find "something reasonable", you need to define how such fixpoints compute exactly.

For example, "something reasonable" can be IsDecTotalOrder _ ≤_ (is decidable total ordering)
Is it possible to constructively prove descending-halt _≤_, IsDecTotalOrder _≤_ ==> WellFounded _≤_ ?

view this post on Zulip Sergei Meshveliani (Nov 25 2021 at 20:47):

Pierre-Marie Pedrot writes

Do you have an example of some ring construction you're interested in that preserves classical noetherianness but breaks ideal well-
foundedness

1) The word Noetherian is ambiguous here, due to the definition in the Coq library, so let us avoid it.

2) I have an example of an ordering _<'_and a function (algorithm) for which termination the papers give proofs based on the descending-halt condition or on ascending-halt condition, but both of them are not supported neither by Agda nor by Coq.
This is so-called admissible ordering on NN = Natural × Natural
(the dimension 2 is sufficient for the example).
This is any total decidable ordering _<'_ on NN which satisfies the axioms
(1) (0,0) is minimal
(2) \forall (e e' d : NN) (e <' e' ==> e +' d <' e' +' d) , where +' the the coordinatewise addition.

A very strong conditions, in fact.
There is a list gs : List NN by which each given e : NN is being reduced.
The function NF: NN -> NN is programmed so that it produces e₁ >' e₂ >' ... and stops when no one in gs
can reduce the current eᵢ. And it is solved in the program when any g from gs can reduce any given e : NN and to what
t : NN is it reduced by this step.

How do you write this NF in Coq, in Agda?

view this post on Zulip Pierre-Marie Pédrot (Nov 25 2021 at 22:03):

First, prove that any admissible R is well-founded. I believe this should be the case since everything here is decidable so you don't have to invoke neither choice nor classical logic, so if you have a paper proof using ascending / descending chain you should be able to mimick the argument in Coq. That's the hard part. Then you do an induction over the wf predicate, as mentioned in a post above. This is the easy part.

view this post on Zulip Guillaume Melquiond (Nov 26 2021 at 09:23):

I did not follow all the details, but I think people are making it more complicated than it needs to be. Consider the following predicate over lists:

Inductive Q (R : T -> T -> bool) : list T -> Prop :=
  Qrec l : (forall h, increasing R (h :: l) = true -> Q R (h :: l)) -> Q R l.

Now consider Lemma foo R : Q R nil. Its proof is the same as the proof of decreasing_halt R. (You might need the excluded middle and the axiom of choice if you want to prove this equivalence in the logic rather than the metalogic. But does it really matter?)
And that is it. foo is your wellfounded term upon which you can define whichever recursive function you need.

view this post on Zulip Sergei Meshveliani (Nov 26 2021 at 10:17):

Pierre-Marie-Pedrot writes

First, prove that any admissible R is well-founded. I believe this should be the case since everything here is decidable so you
don't have to invoke neither choice nor classical logic,

If so, then can you prove in Coq (Agda) (DecTotalOrder _≤'_, Descending-halt _≤'_) ==> WellFounded _≤'_
in general?

so if you have a paper proof using ascending / descending chain you should be able to mimick the argument in Coq.
That's the hard part. Then you do an induction over the wf predicate, as mentioned in a post above.
This is the easy part.

Mimicing this paper I shall obtain an Agda proof for Ascending(Descending)-halt _≤'_.
And for the Agda (Coq) program it is needed WellFounded _≤'_.
?

view this post on Zulip Paolo Giarrusso (Nov 26 2021 at 10:39):

@Sergei "mimicking" here means "reusing the same ideas to prove WellFounded". No idea if that's easy here, but it is in most cases.

view this post on Zulip Paolo Giarrusso (Nov 26 2021 at 10:45):

BTW, probably a typo but just to confirm: you mention WellFounded _<=_, but a non-strict order <= is never going to be well-founded, only its strict relative _<_ can be.

view this post on Zulip Sergei Meshveliani (Nov 26 2021 at 11:10):

Paolo writes

"mimicking" here means "reusing the same ideas to prove WellFounded". No idea if that's easy here, but it is in most cases.

This is a very creative kind of mimicing. May need invention.
And the rule Descending-halt _<_ ==> terminating is proposed for the system exactly in order to free the programmers of this creative mimicing.

On the Guillaume suggestion with the Inductive type: I do not understand it, so far.
I guess that in this Coq declaration Inductive ... the word Inductive probably means in Agda any data type definition done in the recursive (inductive) style. Right?
I imagine something like this for Agda:

data Q  (R : Rel T _) (List T) :   Set _
   where
   Q :   {xs : List T}    (∀ h (Decreasing R (h :: xs)   Q R (h :: xs)))   Q R xs

-- may be it needs improvement.
I often define recursive types. But I never did this for the aim of proving termination for somewhat a problem function.
How does this help to program a concrete function f which produces a sequence of the values decreasing by _<'_ ?
And the words about "excluded middle" sound frightening, the goal is exactly to avoid a generic excluding middle.
Probably I do not undesrtand the context.

view this post on Zulip Sergei Meshveliani (Nov 26 2021 at 11:17):

Paolo writes

BTW, probably a typo but just to confirm: you mention WellFounded _<=_, but a non-strict order <= is never going to be well-founded, only its
strict relative _<_ can be.

Yes, I meant WellFounded _<_.
But then I need to write for the additional properties IsStrictTotalOrder _<_ instead of
DecTotalOrder _≤_, and to add that IsStrictTotalOrder implies Decidable _<_.

view this post on Zulip Sergei Meshveliani (Nov 26 2021 at 11:33):

"mimicking" here means "reusing the same ideas to prove WellFounded". No idea if that's easy here, but it is in most cases.

I have managed to prove WellFounded _<'_ for this particular example -- without mimicing, and without using descending-halt.
But this was difficult to compose.
And I doubt greatly that mimicking can help making it easier.

view this post on Zulip Guillaume Melquiond (Nov 26 2021 at 12:35):

Sergei said:

How does this help to program a concrete function f which produces a sequence of the values decreasing by _<'_ ?

The function f takes as arguments a list l of the previously encountered values and a proof p : Q l. It computes a new value h and can then perform the recursive call f (h::l) (p' h refl) with p == Qrec l p'.
As for the excluded middle, it is only useful if you need to prove the general equivalence for an arbitrary R. (That is Gaetan's proof.) You do not need it for a specific relation R, unless the proof of decreasing_halt R needed it too.

view this post on Zulip Sergei Meshveliani (Nov 26 2021 at 13:30):

Finally I see what it was needed:
LAURENT THÉRY. "A Machine-Checked Implementation of Buchberger’s Algorithm"
Journal of Automated Reasoning 26: 107–137, 2001.
© 2001 Kluwer Academic Publishers. Printed in the Netherlands.

The program is in the _library package_ list in Coq.
The paper looks clear enough. Many things can be understood from it about programming Groebner basis in Coq (and in Agda too).
And it comes close to my small concrete question about termination:
"
Hypothesis <wf : wellFounded(<).
...
The hypothesis <wf is a consequence of a weak version of Dickson’s lemma. This lemma states that in every infinite sequence of monomials, there exists at least one monomial M_i that divides another monomial M_j such that
i < j.
If < were not well founded, there would be an infinite sequence (L i) i∈N such that (L i+1) < (L i).
As (L i) ⊂ (L i+1), we could build an infinite sequence of terms that would contradict Dickson’s lemma.
"
The word "divides" means here (for monomials in two variables) that
(i, j) ≤p (i', j') in the pointwise ordering ≤p on the pairs of natural numbers.

You see: this discourse part is very non-constructive.
On the other hand: there is accessible the corresponding program in Coq, and there this WellFounded _<_ must be proved constructively.
I fear to look into any program's code, such are difficult to understand.
First one needs to read about a _constructive_ proof of Dickson's lemma (in its simplest version!).
I expect that this constructive proof is complex enough.
Second , it is needed to _constructively_ derive WellFounded from Dickson's lemma for this particular example.
I wonder of whether I can see these details in this paper.

view this post on Zulip Gaëtan Gilbert (Nov 26 2021 at 13:37):

the constructive version doesn't need to be more complex
sometimes classical mathematicians will use negative definitions when a positive one would work fine
eg they say "there is no infinite descending sequence" where a constructive mathematician would say "every descending sequence is finite"

view this post on Zulip Sergei Meshveliani (Nov 26 2021 at 14:01):

The thing is reduced to the two concrete questions.
(1) Denote ≤p the coordinate-wise ordering on the domain NN of pairs of natural numbers:
(x, y) ≤p (x', y' ) = x ≤ x' and y ≤ y'.
Provide an algorithm that for each sequence f : Natural -> NN returns a pair i < j such that
(f i ) ≤p (f j).

(2) Derive from the above algorithm that <e' is WellFounded on NN. Here <e on NN is different from <p`, but it holds ≤p ==> ≤e, and also
<p ==> <e.
≤e is total, while ≤p is partial.

I expect that (1) is diificult, and probably (2) is not so simple.
For example, if <e' is defined as lexicographic, then ``WellFounded <e`` is proved directly and simply. But it is needed the abstract case when <e` is preserved under summing pairs in NN.

view this post on Zulip Pierre-Marie Pédrot (Nov 26 2021 at 14:07):

(1) is easy, you just have to look at most fst (f 0) × snd (f 0) values

view this post on Zulip Pierre-Marie Pédrot (Nov 26 2021 at 14:08):

but I am quite sure that if you only want to prove well-foundedness you don't have to explicitly exhibit such functions

view this post on Zulip Pierre-Marie Pédrot (Nov 26 2021 at 14:08):

induction is fairly powerful in type theory

view this post on Zulip Pierre-Marie Pédrot (Nov 26 2021 at 14:10):

mathematicians were taught to only recognize induction over natural numbers (except for set theorists / logicians who are happy to do arbitrary transfinite inductions)

view this post on Zulip Pierre-Marie Pédrot (Nov 26 2021 at 14:10):

but in practice there is a lot of stuff that is expressed naturally as a trivial induction in CIC

view this post on Zulip Paolo Giarrusso (Nov 26 2021 at 14:12):

For this concrete ordering, I think well-foundedness is easier to prove directly, and the algorithm is a complication... Is this in the stdlib, next to lexicographic orders?

view this post on Zulip Pierre-Marie Pédrot (Nov 26 2021 at 14:13):

well I wouldn't even prove wf with this, just do a nested induction

view this post on Zulip Sergei Meshveliani (Nov 26 2021 at 14:22):

Pierre writes

(1) is easy, you just have to look at most fst (f 0) × snd (f 0) values

Probably, not. Because f i and f (1+i) can be incomparable in ≤p. One coordinate gets smaller while another may increase.
So that such single step does not discover the needed pair i < j. One needs a subtler proof. I am sure, it is described in some paper.

view this post on Zulip Sergei Meshveliani (Nov 26 2021 at 14:44):

Paolo writes

For this concrete ordering, I think well-foundedness is easier to prove directly,

Do you mean the ≤p coordinate-wise (partial) ordering?
It is easy to prove WellFounded <p. But then, how to prove WellFounded <e ?
The idea of the paper is that the Dickson's lemma has to be proved first.
I expect that the Coq program does this.

and the algorithm is a complication... Is this in the stdlib, next to lexicographic orders?

I am not sure I understand the question. If it is about the Agda standard library, then it proves
WellFounded <l for A = B × C, for <l being the lexicogrpaphic construct over <b and <c which are WellFounded
on A and B respectively.
For any occasion: the coordinate-wise order ≤p on NN is not lexicographic.

view this post on Zulip Sergei Meshveliani (Nov 26 2021 at 15:01):

(1) is easy, you just have to look at most fst (f 0) × snd (f 0) values
but I am quite sure that if you only want to prove well-foundedness you don't have to explicitly exhibit such functions
induction is fairly powerful in type theory

Note, that in (1) the goal is not wellfoundedness.
It is just Dickson's lemma, which is as follows.
Denote ≤p the coordinate-wise ordering on the domain NN of pairs of natural numbers:
(x, y) ≤p (x', y' ) = x ≤ x' and y ≤ y'.
Prove constructively that for each sequence f : Natural -> NN there exists a index pair i < j such that
(f i ) ≤p (f j).

induction is fairly powerful in type theory

If it is powerful, then can you write in Coq a simple proof for this simple lemma?

view this post on Zulip Paolo Giarrusso (Nov 26 2021 at 17:16):

https://www-sop.inria.fr/marelle/Laurent.Thery/coq.html claims indeed a proof of Dickson's lemma "due to Henrik Persson", and https://www.math.lmu.de/~petrakis/Dickson.pdf has details...

view this post on Zulip Paolo Giarrusso (Nov 26 2021 at 17:17):

and there seems to be some subtlety indeed.

view this post on Zulip Paolo Giarrusso (Nov 26 2021 at 17:18):

also, @Laurent Théry has an account here, and certainly has more insight than me.

view this post on Zulip Paolo Giarrusso (Nov 26 2021 at 17:25):

But as a meta-point, this thread seems to be progressing weirdly...

  1. There's a proposal to extend Coq, but IMHO it seems too premature to be seriously considered. Extending the Coq kernel takes lots of work.
  2. There seems to be an argument that this extension is important, and this part of the debate seems very ill-defined and unproductive... in part because @Sergei's example seems potentially tricky, it seems to have a published constructive proof acceptable to Coq but none of the participants (until now, and me included) seem to understand all the details :-|

view this post on Zulip Paolo Giarrusso (Nov 26 2021 at 17:38):

I guess the truth is that, even if some proof is hard in Coq without axioms (which seems @Sergei's point), it doesn't mean Coq's kernel need be extended. It might just mean the proof is intrinsically hard, or hard to do constructively/intuitionistically.

view this post on Zulip Paolo Giarrusso (Nov 26 2021 at 17:46):

Last link: while Théry's cited paper had non-constructive steps, both https://github.com/coq-community/buchberger and https://github.com/thery/grobner seem free of classical axioms. make validate on the first only reports axiom K (Coq.Logic.Eqdep.Eq_rect_eq.eq_rect_eq), which is pretty constructive :-)

view this post on Zulip Laurent Théry (Nov 26 2021 at 18:26):

Paolo Giarrusso said:

https://www-sop.inria.fr/marelle/Laurent.Thery/coq.html claims indeed a proof of Dickson's lemma "due to Henrik Persson", and https://www.math.lmu.de/~petrakis/Dickson.pdf has details...

Yep my initial proof was not constructive, thanks to Henrik Persson (see his paper in Types 98 Grobner Basis in Type Theory) we can prove constructively DIckson lemma using bar induction. This is what is done here .

view this post on Zulip Karl Palmskog (Nov 26 2021 at 20:16):

I think this is the paper by Henrik: https://rd.springer.com/chapter/10.1007/3-540-48167-2_3

Hopefully this paper is talking about the Dickson lemma proof that is in https://github.com/coq-community/buchberger/blob/master/theories/Dickson.v (whose SSReflect/MathComp variant Laurent referenced)

view this post on Zulip Sergei Meshveliani (Nov 26 2021 at 20:30):

Laurent Thery wites

Yep my initial proof was not constructive, thanks to Henrik Persson (see his paper in Types 98 Grobner Basis in Type Theory) > we can prove constructively DIckson lemma using bar induction. This is what is done here .

Laurent,
I am trying to understand: how is it programmed in Coq the normal form function NF for a polynomial in the Groebner basis method.
Namely how is it based its termination.

I do not know Coq, and use Agda instead.
I am looking into "Groebner Bases in Type Theory" by T. Coquand and Henrik Persson
and trying to guess of the whole construct idea of this termination base.
My guess is as follows.

1) NF is programmed recursively, and the leading monomial of the polynomial being reduced becomes smaller in a certain <m ordering after each reduction step.
2) Coq will accept the NF function only if this function refers to some proof for the property WellFounded _<m_.
Right?
By WellFounded I mean this thing defined in the Agda library (I simplify it a bit):

-- The accessibility predicate: x is accessible if everything which is
-- smaller than x is also accessible (inductively).
--
data Acc {A : Set _} (_<_ : Rel A _) (x : A) :  Set _
  where
  acc : (∀ y  y < x  Acc _<_ y)  Acc _<_ x

WellFounded : Rel A _  Set _             -- "everything in A is accessible"
WellFounded _<_ =  x  Acc _<_ x

3) In order to prove WellFounded _<m_, it is first proved the Dickson's lemma in its certain simple version:
"For any sequence a(i) it is possible to constructively find i < j such that a(i) ≤p a(j)",
where ≤p is the coordinate-wise (partial) ordering of the n-tuples of natural numbers.
Right?

4) Then WellFounded <m is somehow derived constructively from the proof of the Dickson's lemma.

Do I understand correct the idea?

And there is a certain danger of confusion here:
as I see, what I and Agda call WellFounded, in the Coq library is called Notherian
(?).

view this post on Zulip Alexander Gryzlov (Nov 26 2021 at 21:08):

Not really, in Coq it's also well_founded: https://coq.inria.fr/library/Coq.Init.Wf.html

view this post on Zulip Laurent Théry (Nov 27 2021 at 14:15):

Sergei said:

Laurent Thery wites

Yep my initial proof was not constructive, thanks to Henrik Persson (see his paper in Types 98 Grobner Basis in Type Theory) > we can prove constructively DIckson lemma using bar induction. This is what is done here .

Laurent,
I am trying to understand: how is it programmed in Coq the normal form function NF for a polynomial in the Groebner basis method.
Namely how is it based its termination.

I do not know Coq, and use Agda instead.
I am looking into "Groebner Bases in Type Theory" by T. Coquand and Henrik Persson
and trying to guess of the whole construct idea of this termination base.
My guess is as follows.

1) NF is programmed recursively, and the leading monomial of the polynomial being reduced becomes smaller in a certain <m ordering after each reduction step.
2) Coq will accept the NF function only if this function refers to some proof for the property WellFounded _<m_.
Right?
By WellFounded I mean this thing defined in the Agda library (I simplify it a bit):

-- The accessibility predicate: x is accessible if everything which is
-- smaller than x is also accessible (inductively).
--
data Acc {A : Set _} (_<_ : Rel A _) (x : A) :  Set _
  where
  acc : (∀ y  y < x  Acc _<_ y)  Acc _<_ x

WellFounded : Rel A _  Set _             -- "everything in A is accessible"
WellFounded _<_ =  x  Acc _<_ x

3) In order to prove WellFounded _<m_, it is first proved the Dickson's lemma in its certain simple version:
"For any sequence a(i) it is possible to constructively find i < j such that a(i) ≤p a(j)",
where ≤p is the coordinate-wise (partial) ordering of the n-tuples of natural numbers.
Right?

4) Then WellFounded <m is somehow derived constructively from the proof of the Dickson's lemma.

Do I understand correct the idea?

And there is a certain danger of confusion here:
as I see, what I and Agda call WellFounded, in the Coq library is called Notherian
(?).

yep, this is the idea but the key part is in proving the accessibility of an element using the bar induction.

view this post on Zulip Sergei Meshveliani (Nov 27 2021 at 18:11):

Alexander Gryzlov wrote

Not really, in Coq it's also well_founded: https://coq.inria.fr/library/Coq.Init.Wf.html

But it looks like in https://coq.inria.fr/stdlib/Coq.Sets.Relations_3.html#Noetherian
the same thing is defined, and called Noetherian.
?
I do not know, your reference is on the applied library, and the reference with "Noetherian" is of stdlib (of Standard).

view this post on Zulip Gaëtan Gilbert (Nov 27 2021 at 18:17):

having both library/ and stdlib/ seems like a website bug, they're the same thing (probably one got incompletely renamed to the other at some point in the past)
that noetherian definition is indeed the same as Acc, I have no idea why we have it
I don't think anyone has seriously looked at that Relations_3 file for over a decade
maybe even over 2 decades, git log doesn't show any real change for its whole existence (there are only trivial adaptions and copyright date updates)

view this post on Zulip Sergei Meshveliani (Nov 27 2021 at 18:54):

Guillaume Melquiond wrote

Consider the following predicate over lists:

Inductive Q (R : T -> T -> bool) : list T -> Prop :=
  Qrec l : (forall h, increasing R (h :: l) = true -> Q R (h :: l)) -> Q R l.

Now consider Lemma foo R : Q R nil.
Its proof is the same as the proof of decreasing_halt R.
[..]
The function f takes as arguments a list l of the previously encountered values and a proof p : Q l
[..]

This thing is not clear to me. The example is as follows.
T = ℕ × ℕ -- the domain of pairs of natural numbers .
_<'_ is some StrictTotal order on T, and it is decidable, so that it is also given
_<'?_ : Decidable _<'_.
The function step : T → T takes e : T and either returns e Or some e' <' e - this is a reduction attempt.
The normal form function nf takes e : T and computes in its body recursively the sequence e(i): as
e(i+1) = step e(i).
It stops when it holds step e(i) == e(i), with returning the current e(i).
Also we suppose that we have a Coq/Agda proof decr-halt-<' : DecreasingHalt _<'_.

How to make Coq/Agda to take the function nf as terminating?
decr-halt-<' is not sufficient for this.

First, you declare

Inductive Q (R : T -> T -> bool) : list T -> Prop :=
   Qrec l : (forall h, increasing R (h :: l) = true -> Q R (h :: l)) -> Q R l.

As I understand, your suggested type Q presents kind of tracing for the function nf (?).
Your arbitrary relation (_<_ Rel T _) is in my example fixed as <',, so the argument can be removed.
And I translate this to Agda as

data Q (List T) :  Set _   where
   Qrec :   {l : List T}  (∀ h (Increasing (h :: l)  Q (h :: l)))  Q l

I understand Qrec l : ... as Qrec : \forall l .. , Qrec being a constructor for the type Q.
Right?
Increasing needs to be defined as the property on List T expressing that the elements of the argument list are ordered increasingly by <'.
Right?

Now consider Lemma foo R : Q R nil. Its proof is the same as the proof of decreasing_halt R

Here I need to program the function

foo :   Q nil
foo =   ?

which returns a proof for Q nil. What implementation has one to set after this = ?
The value after = has to be obtained only by applying Qrec to something ... (?)
How can nf be programmed with using the type Q ?

view this post on Zulip Sergei Meshveliani (Nov 27 2021 at 19:03):

Laurent Thery wrote

yep, this is the idea but the key part is in proving the accessibility of an element using the bar induction.

Thank you. I shall see.

view this post on Zulip Sergei Meshveliani (Nov 27 2021 at 21:09):

Gaetan Gilbert writes

having both library/ and stdlib/ seems like a website bug, they're the same thing (probably one got incompletely renamed to the other at
some point in the past) that noetherian definition is indeed the same as Acc, I have no idea why we have it

Traditionally, Noetherian comes from algebra, and it means something close to what is (probably) currently called AscendingChain-halt (Asscending-halt) in this community.
In 1960, 70 ... it was also used for the ordering relations, with the meaning close to what it is (probably) called DescendingChain-halt ( Descending-halt) in this community.
To confuse it with WellFounded is greatly misleading.

view this post on Zulip Paolo Giarrusso (Nov 27 2021 at 23:42):

It's not misleading. Noetherian relation is used by classical mathematicians to mean either of a few equivalent things (e.g. https://en.wikipedia.org/w/index.php?title=Noetherian_relation&redirect=no)

view this post on Zulip Paolo Giarrusso (Nov 27 2021 at 23:42):

Since Coq does constructive math, it picks the definition which is most useful, as for everything.

view this post on Zulip Paolo Giarrusso (Nov 27 2021 at 23:46):

(strictly speaking, "noetherian" = converse well-founded, according to Wikipedia, but the Coq stdlib definition expects indeed a "flipped" relation, relative to well-foundedness, so it gets this point right).

view this post on Zulip Sergei Meshveliani (Nov 30 2021 at 19:11):

The main question remains:
what bad may happen if a Dependent Types system incorporates into the kernel the rule
"Descending-halt ==> Terminating" ?
What is a fundamental obstacle to this?
For example, if it is possible to derive a general excluded third from it, then indeed this is a reason.

Why is it needed?
Because many constructively provable methods are easier to write, if this termination rule is accepted.
For example, the algorithm NF that I described above that produces the chain e_1 >' e2 >' ... of k-tuples of Natural
descending by any admissible ordering (StrictTotalOrder, with preserving <' under the vector addition).

The situation is as follows.
The papers say that they give a constructive proof for the Dickson's lemma.
And it is easy to derive Descending-halt <' from this.
But Descending-halt is not sufficient for implementing the above NF function as terminating (in Coq/Agda)
It is needed WellFounded <'.
And so far I do not see how to derive WellFounded <' in this situation.

Then I look into the papers on the Coq implementation of the Groebner basis method.
And they do not show of how WellFounded <' is derived.
Instead they prove termination by implementing the function in rather a particular and complicated way,
by defining a certain complicated inductive type.
It is similar to what Guillaume Melquiond writes above on this topic:

Inductive Q (R : T -> T -> bool) : list T -> Prop :=
   Qrec l : (forall h, increasing R (h :: l) = true -> Q R (h :: l)) -> Q R l
...

The program terminates, because in its involved types is somehow incorporated a proof for Descending-halt <'.
So that the cost of avoiding a proof for WellFounded <' is a considerable complication of the source code for the
NF function (in the papers they do this for GroebnerBasis, and NF is its small part).

I think it is much better to prove WellFounded <', and this will allow one to write more clear functions that are based
on <'.
I do not now, may be it is possible to prove it in a similar way as Descending-halt <'. But I do not find it, so far.

view this post on Zulip Gaëtan Gilbert (Nov 30 2021 at 19:23):

what bad may happen if a Dependent Types system incorporates into the kernel the rule
"Descending-halt ==> Terminating" ?

It's not enough to say it's terminating, you also need to provide reduction rules
I have no idea what that would look like (it's not even clear to me what you would tell the kernel to provide it with the descending-halt proof)
alternatively you can axiomatize descending-halt -> well-founded outside the kernel (then reduction will block since it's an axiom)

view this post on Zulip Sergei Meshveliani (Nov 30 2021 at 20:27):

It's not enough to say it's terminating, you also need to provide reduction rules

What are reduction rules? Is it the general rules for normalization of a term in the Coq/Agda program?

alternatively you can axiomatize descending-halt -> well-founded outside the kernel (then reduction will block since it's an axiom)

Do you mean to add to my program

postulate   forall _<_ -> Descending-halt  _<_ -> Well-founded _<_

?
I do not know, will it be possible to derive the general excluded third from it?

I would add that in classical logic it is easy to derive WellFounded from Descending-halt.
Because if < is not well founded, then there exist a(1) and a(2) < a(1) where a(2) is not accessible. Hence there exists
a(3) < a(2) where a(3) is not accessible, and so on, with bringing a contradiction to Descending-halt <.

view this post on Zulip Gaëtan Gilbert (Nov 30 2021 at 20:37):

I do not know, will it be possible to derive the general excluded third from it?

no idea, but it's probably a theorem if you add descending-halt to the kernel

What are reduction rules? Is it the general rules for normalization of a term in the Coq/Agda program?

yes
for instance if you have

plus : nat -> nat -> nat
plus 0 n = n
plus (S k) n = S (plus k n)

you have the reductions given by the = rules
this satisfies that recursive calls in the reduced term are only on subterms of the arguments of the original call (otherwise the definition is rejected)
meanwhile plus applied to arguments where the 1st one reduces to neither 0 or S of something is blocked, ie doesn't further reduce

how would you define plus using descending-halt (using pseudocode)?

view this post on Zulip Sergei Meshveliani (Nov 30 2021 at 21:16):

how would you define plus using descending-halt (using pseudocode)?

But this plusdoes work in presence of the system rule of WellFounded ==> terminating.
Similarly it would work in presence of the system rule of Descending-halt ==> terminating. (?)
For example, I program in Agda the gcd function for binary represented natural numbers:

gcd : (a b : Bin)  GCD a b
gcd a b =    gc a b <-acc
  where
  gc :  (x y : Bin)  (Acc _<_ x)  GCD x y
  gc x y (acc wf)
         with x  0#
   ... | yes _ = ...
  ...

It relies on wf-Bin : WellFounded _<_, proved earlier, where < is on Bin.
And the auxiliary function gc takes as an additional argument a proof for that x is accessible.
I do not know, may be with Descending-halt, it would take as an argument a proof for that everything descending starting with x is halting ...
?

view this post on Zulip Gaëtan Gilbert (Nov 30 2021 at 21:29):

Similarly it would work in presence of the system rule of Descending-halt ==> terminating. (?)

I don't really understand how it works so I'm asking for a fully detailed example

view this post on Zulip YAMAMOTO Mitsuharu (Dec 01 2021 at 05:16):

Sergei Meshveliani said:

The thing is reduced to the two concrete questions.
(1) Denote ≤p the coordinate-wise ordering on the domain NN of pairs of natural numbers:
(x, y) ≤p (x', y' ) = x ≤ x' and y ≤ y'.
Provide an algorithm that for each sequence f : Natural -> NN returns a pair i < j such that
(f i ) ≤p (f j).

(2) Derive from the above algorithm that <e' is WellFounded on NN. Here <e on NN is different from <p`, but it holds ≤p ==> ≤e, and also
<p ==> <e.
≤e is total, while ≤p is partial.

I expect that (1) is diificult, and probably (2) is not so simple.

For this problem, you can use https://github.com/coq-community/almost-full mentioned in an earlier post, but not via an algorithm finding (i, j).
You can show almost_full ≤p from leq_af and af_product in AFConstructions.v.
Then (2) can be derived from the lemma below in AlmostFull.v, by taking T := <e and R := ≤p

Lemma wf_from_af :
 forall (X:Type) (R : X -> X -> Prop) (T : X -> X -> Prop),
  (forall x y, clos_trans_1n X T x y /\ R y x -> False) ->
  almost_full R -> well_founded T.

where clos_trans_1n X T means the transitive closure of the relation T on X.
Note that almost_full is defined inductively and stronger than the condition on infinite sequences (though they are equivalent classically):

Corollary af_inf_chain (X : Type) (R : X -> X -> Prop):
 almost_full R -> forall (f : nat -> X), exists n, exists m, (n > m) /\ R (f m) (f n).

view this post on Zulip YAMAMOTO Mitsuharu (Dec 01 2021 at 08:55):

Then (2) can be derived from the lemma below in AlmostFull.v

Alternatively, af_strengthento get almost_full ≤e from almost_full ≤p, and wf_from_wqo to conclude well_founded (fun x y => x ≤e y /\ not (y ≤e x)):

Lemma af_strengthen:
 forall (X:Type) (A : X -> X -> Prop), almost_full A ->
 forall (B : X -> X -> Prop), (forall x y, A x y -> B x y) -> almost_full B.
Lemma wf_from_wqo :
  forall (X:Type) (R : X -> X -> Prop), transitive X R -> almost_full R ->
  well_founded (fun x y => R x y /\ not (R y x)).

view this post on Zulip Sergei Meshveliani (Dec 01 2021 at 22:01):

Gaetan Gilbert

writes I don't really understand how it works so I'm asking for a fully detailed example.

Let me try. First, program plus : ℕ → ℕ → ℕ by relying on <-wellFounded for ℕ = Natural instead of relying on structural recursion. This is to compare to plus' which is shown further and relies on DescendingHalt.
It is in Agda.
Please see the attached code (because the code is shown badly in this screen).
tt.agda

Then there is defined what are DecreasingHalt and AllDAccessible for any relation _<_ on any Set.
Then it is proved allDAccessible-<ₙ : AllDAccessible _<ₙ_ for natural numbers.

Then it is programmed plus' that relies on allDAccessible-<ₙ.
It has one line of pseudocode:

  r = terminates allDAccessible-< m-1<m (aux m-1)

The prefix of terminates allDAccessible-<ₙ m-1<m explains why does the further (aux m-1) terminate.
It refers to m, m-1 and to the proofs allDAccessible-<ₙ, m-1<m .
Can this be translated into something correct?

view this post on Zulip Gaëtan Gilbert (Dec 01 2021 at 22:08):

DAcc x = ∀ {seq : Sequence A} → seq 0 ≡ x → DecreasingHalt seq

this looks like a weird thing to define, why do we care about this concept? why don't we have AllDAccessible = forall seq, DecreasingHalt seq?

view this post on Zulip Gaëtan Gilbert (Dec 01 2021 at 22:13):

it seems to boil down to having a combinator like

recurse : forall (A : Type) (_<_ : A -> A -> Type) -> AllDAccessible _<_ -> forall (T : A -> Type) -> (forall (x : A) -> (forall (y : A) -> y < x -> T y) -> T x) -> forall (x : A) -> T x

but then you get AllDAccessible -> WellFounded
and it's unclear what reduction rules you could have with AllDAccessible so you may as well axiomatize, then recurse is a theorem and you can also prove recurse A _<_ H T F x = F x (\y H -> recurse A _<_ H T F y) (up to a bit of funext possibly)

view this post on Zulip Sergei Meshveliani (Dec 01 2021 at 22:36):

this looks like a weird thing to define, why do we care about this concept? why don't we have
AllDAccessible = forall seq, DecreasingHalt seq ?

All right, let it be AllDAccessible = forall seq, DecreasingHalt seq.

it seems to boil down to having a combinator like [..]
but then you get AllDAccessible -> WellFounded

?
I do not understand such a complex thing as this combinator.
AllDAccessible = ... is a definition, it is not a proof for anything. And I wonder how can it be proved AllDAccessible -> WellFounded.
Sounds strangely.
Your statement looks contradictory. AllDAccessible -> WellFounded cannot be proved constructively.
Therefore either the above combinator cannot be derived from AllDAccessible or this combinator is wrongly used in the further inference.
?

view this post on Zulip Sergei Meshveliani (Dec 02 2021 at 16:30):

YAMAMOTO Mitsuharu writes

For this problem, you can use https://github.com/coq-community/almost-full mentioned in an earlier post, but not via an
algorithm finding (i, j).
You can show almost_full ≤p from leq_af and af_product in AFConstructions.v.
[..]

Thank you.
This looks interesting.
From the start, the conditions are as follows.

(1) p  is a (partial) coordinatwise order on  NN =  ×  :   (x, y) p (x', y') =   x  x'  And  y  y'.
(2) <e   is any total strict (decidable) order on NN;
     and it has its induced   e   - which is a decidable total order.
     And it holds  p ==> e.

It is needed to derive WellFounded _<e_.
(And in reality, I have the k-tuples: NN = ℕ^k).

With setting T := <e, R := ≤p, your lemma

forall (X:Type) (R : X -> X -> Prop) (T : X -> X -> Prop),
  (forall x y, clos_trans_1n X T x y /\ R y x -> False) ->  almost_full R -> well_founded T.

reduces to

lemma-II :  (forall x y, not (x <e y /\ y p x))  ->  almost_full p -> well_founded <e

because <e is already transitive. You say, this lemma is proved in AlmostFull.v.
The condition forall x y, not (x <e y /\ y ≤p x) is satisfied trivially in my example, because
y ≤p x implies y ≤e x,
and also not (x <e y) -- due to that ≤e is a decidable total order.

So, it remains to apply AlmostFull.v.
And I have to inspect https://github.com/coq-community/almost-full, AlmostFull.v.

view this post on Zulip YAMAMOTO Mitsuharu (Dec 03 2021 at 11:07):

I don't think decidability is necessary. In particular, if you define <e as fun x y => x ≤e y /\ not (y ≤e x) (or show equivalence between them), then you can show well_founded <e using af_strengthen and wf_from_wqo straightforwardly.


Last updated: Feb 08 2023 at 23:03 UTC