[Agda] Noetherian vs WellFounded

[mechvel at scico.botik.ru]

On 2021-10-05 16:40, Jason Hu wrote:
> 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)"?


  Noetherian _<_ =  ∀ (f : ℕ → A) → ∃ (\n →  ¬ (f n > f (suc n)))


Here  _>_ = flip _<_,
and the existence ∃ is constructive:   Σ A (\n →  ¬ (f n > f (suc n))

--
SM



>  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