how termination is proved in Coq? · Coq users

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.

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

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.

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

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

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

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

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

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

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

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

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

Paolo Giarrusso (Nov 25 2021 at 12:34):

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

Sergei Meshveliani (Nov 25 2021 at 13:00):

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.

Paolo Giarrusso (Nov 25 2021 at 16:54):

Paolo Giarrusso (Nov 25 2021 at 16:55):

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

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

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

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

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

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

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.

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

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

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

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

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

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

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

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

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

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

Sergei Meshveliani (Nov 26 2021 at 14:22):

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

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.

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

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

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

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

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

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

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

Sergei Meshveliani (Nov 26 2021 at 20:30):

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.

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

Laurent Théry (Nov 27 2021 at 14:15):

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

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

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.

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.

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?

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

Sergei Meshveliani (Nov 27 2021 at 21:09):

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

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

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

What are reduction rules? Is it the general rules for normalization of a term in the Coq/Agda 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):

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

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

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

Gaëtan Gilbert (Nov 30 2021 at 21:29):

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

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

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

Sergei Meshveliani (Dec 01 2021 at 22:01):

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

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

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

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

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

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.

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.

Stream: Coq users

Topic: how termination is proved in Coq?

Sergei Meshveliani (Nov 24 2021 at 20:52):

Li-yao (Nov 24 2021 at 21:34):

Sergei Meshveliani (Nov 24 2021 at 22:39):

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

Paolo Giarrusso (Nov 25 2021 at 01:12):

Sergei Meshveliani (Nov 25 2021 at 11:42):

Sergei Meshveliani (Nov 25 2021 at 11:51):

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

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

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

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

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

Paolo Giarrusso (Nov 25 2021 at 12:34):

Paolo Giarrusso (Nov 25 2021 at 12:46):

Sergei Meshveliani (Nov 25 2021 at 13:00):

Paolo Giarrusso (Nov 25 2021 at 13:03):

Paolo Giarrusso (Nov 25 2021 at 13:04):

Paolo Giarrusso (Nov 25 2021 at 13:07):

Paolo Giarrusso (Nov 25 2021 at 13:28):

Sergei Meshveliani (Nov 25 2021 at 13:47):

Sergei Meshveliani (Nov 25 2021 at 13:58):

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

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

Li-yao (Nov 25 2021 at 14:16):

Sergei Meshveliani (Nov 25 2021 at 14:16):

Paolo Giarrusso (Nov 25 2021 at 14:17):

Li-yao (Nov 25 2021 at 14:20):

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

Paolo Giarrusso (Nov 25 2021 at 14:21):

Paolo Giarrusso (Nov 25 2021 at 14:21):

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

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

Paolo Giarrusso (Nov 25 2021 at 14:24):

Sergei Meshveliani (Nov 25 2021 at 14:25):

Karl Palmskog (Nov 25 2021 at 14:25):

Paolo Giarrusso (Nov 25 2021 at 14:26):

Paolo Giarrusso (Nov 25 2021 at 14:27):

Paolo Giarrusso (Nov 25 2021 at 14:31):

Paolo Giarrusso (Nov 25 2021 at 14:34):

Sergei Meshveliani (Nov 25 2021 at 14:37):

Paolo Giarrusso (Nov 25 2021 at 14:41):

Paolo Giarrusso (Nov 25 2021 at 14:43):

Sergei Meshveliani (Nov 25 2021 at 14:51):

Li-yao (Nov 25 2021 at 14:53):

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

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

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

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

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

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

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

Gaëtan Gilbert (Nov 25 2021 at 16:11):

Paolo Giarrusso (Nov 25 2021 at 16:54):

Paolo Giarrusso (Nov 25 2021 at 16:55):

Paolo Giarrusso (Nov 25 2021 at 17:00):

Pierre-Marie Pédrot (Nov 25 2021 at 17:28):

Sergei Meshveliani (Nov 25 2021 at 18:43):

Sergei Meshveliani (Nov 25 2021 at 19:19):

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

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

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

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

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

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

Sergei Meshveliani (Nov 25 2021 at 20:13):

Sergei Meshveliani (Nov 25 2021 at 20:47):

Pierre-Marie Pédrot (Nov 25 2021 at 22:03):

Guillaume Melquiond (Nov 26 2021 at 09:23):

Sergei Meshveliani (Nov 26 2021 at 10:17):

Paolo Giarrusso (Nov 26 2021 at 10:39):

Paolo Giarrusso (Nov 26 2021 at 10:45):

Sergei Meshveliani (Nov 26 2021 at 11:10):

Sergei Meshveliani (Nov 26 2021 at 11:17):

Sergei Meshveliani (Nov 26 2021 at 11:33):

Guillaume Melquiond (Nov 26 2021 at 12:35):

Sergei Meshveliani (Nov 26 2021 at 13:30):

Gaëtan Gilbert (Nov 26 2021 at 13:37):

Sergei Meshveliani (Nov 26 2021 at 14:01):