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


I wrote about the example where the Noetherian property (the descending 
chain property) for _<_
can be proved in Agda, but it is problematic to prove WellFounded _<_:

   Carrier = PP = ℕ × ℕ

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

   Prove WellFounded _<_.


But now I see that WellFounded _<_ can be proved directly in Agda for 
this example.


Still I believe that there are many examples when the descending chain 
property is easy to prove
(so that termination of the related function should be derived from 
this),
but proving WellFounded is difficult or problematic.

May be Standard library needs to include a proof for a theorem of kind

"If _<_ has the descending chain property and Condition-II,
  then WellFounded _<_
"
?

Condition-II could be, say, IsStrictTotalOrder,
or something reasonable and usable that allows to derive WellFounded.

By the descending chain property I mean

    (f : Nat -> A) -> exists (\i -> not (f i) > (f (suc i)))

--
SM