[Agda] Noetherian vs WellFounded

[Martin Escardo]

You may wish to look here:

https://mathoverflow.net/questions/239560/noetherian-rings-in-constructive-mathematics

Martin

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

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe