[Agda] Noetherian vs WellFounded

[mechvel at scico.botik.ru]

On 2021-10-05 18:18, Martin Escardo wrote:
> You may wish to look here:
> 
> https://mathoverflow.net/questions/239560/noetherian-rings-in-constructive-mathematics
> 


No, my subject is much simpler than ascending ideals in rings.
Ideals are infinite sets, and I have only integer points on the plane.

This relates to a normal form algorithm NF for multivariate polynomials.
There is only
              Carrier = PP = ℕ × ℕ   -- "power product"

Generally there are n components, but  n = 2  is sufficient to test the 
approach.
And there are
     _<_  : Rel PP _,
     _+'_ : PP → PP → PP
            defined as the pointwise addition.

Axioms of _admissible ordering_ on PP:
   (A1) _<_ is of DecTotalOrder,
   (A2) ∀ e → Nonzero e → (0 , 0) < e,
   (A3) ∀ (e e' d) → e < e' → e +' d < e' +' d

Let _<_ be admissible.
This is not so easy, but it can be proved in Agda that _<_ is 
Noetherian.
First one needs to prove the Dickson's lemma.
After this, it is easy to prove  Noetherian _<_.
The NF algorithm includes forming a sequence in PP recursively from  e  
to  e',  where  e > e'.
It is evident that  Noetherian _<_  is a nice and regular base for the 
termination proof for NF.
But I do not see how to derive  WellFounded  in this case.

There is a certain nice classification for the admissible orderings.
One may hope to use this classification to prove WellFounded.
But
a) to prove this classification is Agda will be extremely difficult, if 
ever possible,
b) to prove in Agda WellFounded from this classification will also be 
difficult, if possible.

And using    Dickson => (Noetherian _<_) => terminating
is nice and surely gives the result.

-- 
SM




> On 05/10/2021 14:29, mechvel at scico.botik.ru wrote:
>> Can people, please, explain:
>> 
>> how can Agda treat the relation between the Noetherian property of an
>> ordering _<_
>> and its property of WellFounded
>> (of Induction.WellFounded of Standard library) ?
>> 
>> A relation _<_ is called Noetherian iff there does not exist any
>> infinite sequence descending by _<_.
>> 
>> The matter is that many proofs in mathematics look like this:
>> "This process terminates because it includes forming a descending
>> sequence  a₁ > a₂ > ...,
>> while the relation _>_ is Noetherian
>> ".
>> 
>> For example, I have to prove a certain termination, while having
>> * a proof for Noetherian _<_,
>> * a proof for DecTotalOrder for _<_,
>> * a certain proved bijection algorithm Carrier <--> ℕ
>>   (whithout preserving the ordering).
>> 
>> And I wonder of how to prove this termination in Agda.
>> 
>> 
>> * Is it possible to prove in Agda  (Noetherian ==> Wellfounded)
>>   for any partial ordering _<_ ?
>> 
>> * What additional condition (the more generic the better) can be
>> sufficient for this proof?
>>   For example:
>>   a) a bijection algorithm Carrier <--> ℕ
>>      (whithout a given proof for preserving the ordering),
>>   or/and
>>   b) DecTotalOrder for _<_.
>> 
>> * Is there a counter-example for (Noetherian ==> Wellfounded) ?
>> 
>> * What can be the consequences of using, say,
>>   postulate
>>     Noetherian⇒WellFounded :
>>       ∀ (_<_ : of DecTotalOrder) → Noetherian _<_ → WellFounded _<_
>> 
>>   all through an applied library?
>> 
>> 
>> Thank you for possible explanation.
>> 
>> Regards,
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda