[Agda] Noetherian vs WellFounded

[Jason Hu]

how do you write down Noetherian in Agda? I'd imagine an infinite sequence is a function from Nat to A (your type comparable by _<_)? so Noetherian is something like "given an infinite sequence f,  not (for all Nat n, f (1 + n) < f n)"?

Thanks,
Jason Hu
https://hustmphrrr.github.io/
________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of mechvel at scico.botik.ru <mechvel at scico.botik.ru>
Sent: October 5, 2021 9:29 AM
To: agda at lists.chalmers.se <agda at lists.chalmers.se>
Subject: [Agda] Noetherian vs WellFounded

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20211005/0d600b08/attachment.html>