<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
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)"?
<br>
</div>
<div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div id="Signature">
<div>
<div></div>
<div id="divtagdefaultwrapper" dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif;">
<font size="3"><b>Thanks,</b></font></div>
<div dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif;">
<font size="3"><b>Jason Hu</b></font></div>
<div dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif;">
<font size="3"><b><a href="https://hustmphrrr.github.io/">https://hustmphrrr.github.io/</a></b></font><br>
<font size="3"><b></b></font><font style="font-size:12pt" size="3"><span style="color: rgb(69, 129, 142);"><span style="font-family:trebuchet ms,sans-serif"><b><a target="_blank"></a></b></span></span></font></div>
</div>
</div>
</div>
<div id="appendonsend"></div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Agda <agda-bounces@lists.chalmers.se> on behalf of mechvel@scico.botik.ru <mechvel@scico.botik.ru><br>
<b>Sent:</b> October 5, 2021 9:29 AM<br>
<b>To:</b> agda@lists.chalmers.se <agda@lists.chalmers.se><br>
<b>Subject:</b> [Agda] Noetherian vs WellFounded</font>
<div> </div>
</div>
<div class="BodyFragment"><font size="2"><span style="font-size:11pt;">
<div class="PlainText">Can people, please, explain:<br>
<br>
how can Agda treat the relation between the Noetherian property of an <br>
ordering _<_<br>
and its property of WellFounded<br>
(of Induction.WellFounded of Standard library) ?<br>
<br>
A relation _<_ is called Noetherian iff there does not exist any <br>
infinite sequence descending by _<_.<br>
<br>
The matter is that many proofs in mathematics look like this:<br>
"This process terminates because it includes forming a descending <br>
sequence a₁ > a₂ > ...,<br>
while the relation _>_ is Noetherian<br>
".<br>
<br>
For example, I have to prove a certain termination, while having<br>
* a proof for Noetherian _<_,<br>
* a proof for DecTotalOrder for _<_,<br>
* a certain proved bijection algorithm Carrier <--> ℕ<br>
(whithout preserving the ordering).<br>
<br>
And I wonder of how to prove this termination in Agda.<br>
<br>
<br>
* Is it possible to prove in Agda (Noetherian ==> Wellfounded)<br>
for any partial ordering _<_ ?<br>
<br>
* What additional condition (the more generic the better) can be <br>
sufficient for this proof?<br>
For example:<br>
a) a bijection algorithm Carrier <--> ℕ<br>
(whithout a given proof for preserving the ordering),<br>
or/and<br>
b) DecTotalOrder for _<_.<br>
<br>
* Is there a counter-example for (Noetherian ==> Wellfounded) ?<br>
<br>
* What can be the consequences of using, say,<br>
postulate<br>
Noetherian⇒WellFounded :<br>
∀ (_<_ : of DecTotalOrder) → Noetherian _<_ → WellFounded _<_<br>
<br>
all through an applied library?<br>
<br>
<br>
Thank you for possible explanation.<br>
<br>
Regards,<br>
_______________________________________________<br>
Agda mailing list<br>
Agda@lists.chalmers.se<br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div>
</span></font></div>
</body>
</html>