## Stream: Coq users

### Topic: how termination is proved in Coq?

#### 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.
"

• note this last line.

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?

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

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

#### Alexander Gryzlov (Nov 24 2021 at 22:46):

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

#### 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".

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

#### 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` ?

#### Alexander Gryzlov (Nov 25 2021 at 11:57):

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

#### Alexander Gryzlov (Nov 25 2021 at 11:58):

Equations is newer and more powerful

#### Karl Palmskog (Nov 25 2021 at 11:58):

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

#### Paolo Giarrusso (Nov 25 2021 at 12:30):

Is this structural recursion?

Yes.

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

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

#### 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 _<_` ?

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

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

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

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

#### 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?

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.

#### 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".
?

#### Li-yao (Nov 25 2021 at 14:08):

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

#### Paolo Giarrusso (Nov 25 2021 at 14:15):

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

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

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

#### 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?

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

#### Paolo Giarrusso (Nov 25 2021 at 14:20):

maybe I see what's going on

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

#### 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".

#### Paolo Giarrusso (Nov 25 2021 at 14:22):

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

#### Paolo Giarrusso (Nov 25 2021 at 14:23):

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

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

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

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

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

#### 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!

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

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

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

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

#### 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".

#### 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` ?

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

#### Gaëtan Gilbert (Nov 25 2021 at 14:55):

the real question is what do you mean by `terminating`?

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

#### Gaëtan Gilbert (Nov 25 2021 at 15:04):

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

#### Li-yao (Nov 25 2021 at 15:06):

Postulate `descending_halt _<_ -> well_founded _<_`

#### 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 _<_`.
?

#### Sergei Meshveliani (Nov 25 2021 at 15:25):

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

Then it will be probably possible to prove a contradiction.

#### 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

#### 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.
``````

(deleted)

(deleted)

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

#### 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 `.

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

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

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

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

#### Pierre-Marie Pédrot (Nov 25 2021 at 19:33):

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

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

#### 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

#### 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

#### 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 _≤_` ?

#### 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?

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

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

#### 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 _≤'_`.
?

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

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

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

#### 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 _<_`.

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

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

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

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.

#### 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"

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

#### 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

#### 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

#### Pierre-Marie Pédrot (Nov 26 2021 at 14:08):

induction is fairly powerful in type theory

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

#### 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

#### 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?

#### Pierre-Marie Pédrot (Nov 26 2021 at 14:13):

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

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

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

#### 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?

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

#### Paolo Giarrusso (Nov 26 2021 at 17:17):

and there seems to be some subtlety indeed.

#### Paolo Giarrusso (Nov 26 2021 at 17:18):

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

#### 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 :-|

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

#### 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 :-)

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

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

#### 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
(?).

#### 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

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

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

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

#### 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 `?

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

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

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

#### Paolo Giarrusso (Nov 27 2021 at 23:42):

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

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

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

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

#### 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 `<`.

#### 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)?

#### Sergei Meshveliani (Nov 30 2021 at 21:16):

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

But this `plus`does 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 ...
?

#### 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

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

#### YAMAMOTO Mitsuharu (Dec 01 2021 at 08:55):

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

Alternatively, `af_strengthen`to 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)).
``````

#### 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?

#### 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`?

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

#### 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.
?

#### 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.`

#### 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: May 18 2024 at 10:02 UTC