<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);">
Hi Matthew, Jeremy,</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
I believe the APIs for well-founded induction from the stdlib are very difficult to use. I improved the APIs in my own project, which provides a nice and straightforward nobrainer wrapper. a running example is
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<a href="https://hustmphrrr.github.io/popl20-artifact/agda/DsubEquivSimpler.html#13825" style="" id="LPlnk160832">https://hustmphrrr.github.io/popl20-artifact/agda/DsubEquivSimpler.html#13825</a></div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
for completeness:</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<span style="font-family: "Courier New", monospace;"> <:″-trans-narrow : ∀ T → trans-on T × narrow-on T</span><span><br>
</span>
<div><span style="font-family: "Courier New", monospace;"> <:″-trans-narrow = wfRec _ aux</span><br>
</div>
<div><span style="font-family: "Courier New", monospace;"> where open Measure <-wellFounded Typ-measure</span><br>
</div>
<div><span style="font-family: "Courier New", monospace;"> aux : ∀ T → (∀ T′ → Typ-measure T′ < Typ-measure T → trans-on T′ × narrow-on T′) → trans-on T × narrow-on T</span><br>
</div>
<span style="font-family: "Courier New", monospace;"> aux T rec = -- details omitted</span><br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
As you can see, it opens up a module `Measure` which expose `wfRec` which accomplishes the well-founded induction and I only had to implement the induction body, which is the `aux` function. when I showed this code to my supervisor for the first time, he was
able to get the big picture of it so I guess it also improves readability too.<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
This example does not use lexicographically well-founded induction, but it turns out I also prepared a variant for that:</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<a href="https://hustmphrrr.github.io/popl20-artifact/agda/Utils.html#2958" style="" id="LPlnk526070">https://hustmphrrr.github.io/popl20-artifact/agda/Utils.html#2958</a></div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
APIs like this can be quite handy. probably I should see if these APIs still work in the latest stdlib and PR it this weekends.<br>
</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 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/" style="">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" style=""></a></b></span></span></font></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 Matthew Daggitt <matthewdaggitt@gmail.com><br>
<b>Sent:</b> February 29, 2020 4:07 AM<br>
<b>To:</b> Siek, Jeremy <jsiek@indiana.edu><br>
<b>Cc:</b> agda list <agda@lists.chalmers.se><br>
<b>Subject:</b> Re: [Agda] recursion, lexicographic ordering</font>
<div> </div>
</div>
<div>
<div dir="ltr">Hi Jeremy,
<div> Okay, I've written out an example of how you'd use the WellFounded part of the standard library to prove termination below. I haven't gone into the fine details of how `Acc` and `WellFounded` work as there's plenty of excellent resources out there already,
e.g. <a href="https://stackoverflow.com/questions/19642921/assisting-agdas-termination-checker">
here</a>.</div>
<div><br>
</div>
<div>Note that the latest official version of the standard library (v1.2) is missing the proof `×-wellFounded` in `Data.Product.Relation.Binary.Lex.Strict`, as I've just added it to the `<a href="https://github.com/agda/agda-stdlib/pull/1094">lexicographic-product</a>`
branch. The proof will however be available in the upcoming v1.3 release.</div>
<div><br>
</div>
<div>In the meantime I think the easiest way for you to solve this problem is to copy the updated <a href="https://raw.githubusercontent.com/agda/agda-stdlib/03209af78061fdf734521359985c9de836e063b8/src/Data/Product/Relation/Binary/Lex/Strict.agda">file</a>
into your own library and give it a new name such as `MyStrictLexProduct.agda` and import that instead of `Data.Product.Relation.Binary.Lex.Strict`. You can then delete it and switch back when v1.3 releases.</div>
<div><br>
</div>
<div>```agda</div>
<div>module Test where<br>
<br>
open import Data.Nat<br>
open import Data.Nat.Induction using (Acc; acc; <-wellFounded)<br>
open import Data.Nat.Properties using (≤-refl)<br>
open import Data.Sum using (inj₁; inj₂)<br>
open import Data.Product<br>
open import Data.Product.Relation.Binary.Lex.Strict<br>
open import Induction.WellFounded using (WellFounded)<br>
open import Relation.Binary<br>
open import Relation.Binary.PropositionalEquality using (_≡_; refl)<br>
<br>
-- Define the order over the 3-tuples using two applications of `×-Lex` from `Data.Product.Relation.Binary.Lex.Strict`:</div>
<div><br>
_<₃_ : Rel (ℕ × ℕ × ℕ) _<br>
_<₃_ = ×-Lex _≡_ _<_ (×-Lex _≡_ _<_ _<_)<br>
<br>
-- Use the new `×-wellFounded` combinator to prove that the lexicographic ordering is well-founded:</div>
<div><br>
<₃-wellFounded : WellFounded _<₃_<br>
<₃-wellFounded = ×-wellFounded <-wellFounded (×-wellFounded <-wellFounded <-wellFounded)<br>
<br>
-- The naive implementation of this function fails to pass the termination checker<br>
{-<br>
-- BAD: termination checking failure<br>
f : ℕ × ℕ × ℕ → ℕ<br>
f (x , zero , z) = z<br>
f (x , suc y , z) = f (x , y , suc z)<br>
-}<br>
<br>
-- Define a new function that takes in a decreasing Acc proof as well, and hence is acceptable to the termination checker</div>
<div><br>
f-acc : ∀ (x : ℕ) → Acc _<₃_ x → ℕ<br>
f-acc (x , zero , z) rec = z<br>
f-acc (x , suc y , z) (acc rec) = f-acc (x , y , suc z)<br>
(rec _ (inj₂ (refl , inj₁ ≤-refl))) -- proof that the tuple is decreasing lexicographically<br>
<br>
-- Use <₃-wellFounded to provide the Acc proof
<div></div>
f : ℕ × ℕ × ℕ → ℕ<br>
f xyz = f-acc xyz (<₃-wellFounded xyz)<br>
</div>
<div>```</div>
<div><br>
</div>
<div>Best,</div>
<div>Matthew</div>
</div>
<br>
<div class="x_gmail_quote">
<div dir="ltr" class="x_gmail_attr">On Sat, Feb 29, 2020 at 4:08 PM Matthew Daggitt <<a href="mailto:matthewdaggitt@gmail.com">matthewdaggitt@gmail.com</a>> wrote:<br>
</div>
<blockquote class="x_gmail_quote" style="margin:0px 0px 0px 0.8ex; border-left:1px solid rgb(204,204,204); padding-left:1ex">
<div dir="ltr">Hi Jeremy,
<div> So I've been meaning to get rid of `Induction.WellFounded.Lexicographic` for a while as it doesn't mesh with the rest of the library very well. Your question might actually provide me the impetus to do so! </div>
<div><br>
</div>
<div>Give me a few hours to upload a new branch to the standard library with some small changes and I'll get back to you with the best way to do so.</div>
<div>Best,</div>
<div>Matthew</div>
<div><br>
</div>
</div>
<br>
<div class="x_gmail_quote">
<div dir="ltr" class="x_gmail_attr">On Sat, Feb 29, 2020 at 1:05 PM Siek, Jeremy <<a href="mailto:jsiek@indiana.edu" target="_blank">jsiek@indiana.edu</a>> wrote:<br>
</div>
<blockquote class="x_gmail_quote" style="margin:0px 0px 0px 0.8ex; border-left:1px solid rgb(204,204,204); padding-left:1ex">
<div>I would like to define a function (Martello and Montanari’s unification algorithm)
<div>whose termination measure is a lexicographic ordering of three numbers.</div>
<div>I get the impression that there is support for this kind of thing in the</div>
<div>standard library, in Induction.WellFounded.Lexicographic.</div>
<div>However, I’m at a loss trying to figure out how to use it.</div>
<div>Any examples or pointers to documentation or tutorials</div>
<div>would be much appreciated.</div>
<div><br>
</div>
<div>Thank you,</div>
<div>Jeremy</div>
<div><br>
<div>
<div>
<div dir="auto" style="color:rgb(0,0,0); letter-spacing:normal; text-align:start; text-indent:0px; text-transform:none; white-space:normal; word-spacing:0px; text-decoration:none">
<div style="color:rgb(0,0,0); letter-spacing:normal; text-align:start; text-indent:0px; text-transform:none; white-space:normal; word-spacing:0px">
<div style="color:rgb(0,0,0); letter-spacing:normal; text-align:start; text-indent:0px; text-transform:none; white-space:normal; word-spacing:0px">
<div style="color:rgb(0,0,0); letter-spacing:normal; text-align:start; text-indent:0px; text-transform:none; white-space:normal; word-spacing:0px">
<div><br>
</div>
</div>
</div>
</div>
</div>
<br>
<br>
</div>
<br>
</div>
</div>
</div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote>
</div>
</blockquote>
</div>
</div>
</body>
</html>