[Agda] recursion, lexicographic ordering

[Jason -Zhong Sheng- Hu]

Hi Matthew, Jeremy,

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

https://hustmphrrr.github.io/popl20-artifact/agda/DsubEquivSimpler.html#13825

for completeness:

  <:″-trans-narrow : ∀ T → trans-on T × narrow-on T
  <:″-trans-narrow = wfRec _ aux
    where open Measure <-wellFounded Typ-measure
          aux : ∀ T → (∀ T′ → Typ-measure T′ < Typ-measure T → trans-on T′ × narrow-on T′) → trans-on T × narrow-on T
          aux T rec = -- details omitted

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.

This example does not use lexicographically well-founded induction, but it turns out I also prepared a variant for that:

https://hustmphrrr.github.io/popl20-artifact/agda/Utils.html#2958

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.

Thanks,
Jason Hu
https://hustmphrrr.github.io/
________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of Matthew Daggitt <matthewdaggitt at gmail.com>
Sent: February 29, 2020 4:07 AM
To: Siek, Jeremy <jsiek at indiana.edu>
Cc: agda list <agda at lists.chalmers.se>
Subject: Re: [Agda] recursion, lexicographic ordering

Hi Jeremy,
 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. here<https://stackoverflow.com/questions/19642921/assisting-agdas-termination-checker>.

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 `lexicographic-product<https://github.com/agda/agda-stdlib/pull/1094>` branch. The proof will however be available in the upcoming v1.3 release.

In the meantime I think the easiest way for you to solve this problem is to copy the updated file<https://raw.githubusercontent.com/agda/agda-stdlib/03209af78061fdf734521359985c9de836e063b8/src/Data/Product/Relation/Binary/Lex/Strict.agda> 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.

```agda
module Test where

open import Data.Nat
open import Data.Nat.Induction using (Acc; acc; <-wellFounded)
open import Data.Nat.Properties using (≤-refl)
open import Data.Sum using (inj₁; inj₂)
open import Data.Product
open import Data.Product.Relation.Binary.Lex.Strict
open import Induction.WellFounded using (WellFounded)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

-- Define the order over the 3-tuples using two applications of `×-Lex` from `Data.Product.Relation.Binary.Lex.Strict`:

_<₃_ : Rel (ℕ × ℕ × ℕ) _
_<₃_ = ×-Lex _≡_ _<_ (×-Lex _≡_ _<_ _<_)

-- Use the new `×-wellFounded` combinator to prove that the lexicographic ordering is well-founded:

<₃-wellFounded : WellFounded _<₃_
<₃-wellFounded = ×-wellFounded <-wellFounded (×-wellFounded <-wellFounded <-wellFounded)

-- The naive implementation of this function fails to pass the termination checker
{-
-- BAD: termination checking failure
f : ℕ × ℕ × ℕ → ℕ
f (x , zero  , z) = z
f (x , suc y , z) = f (x , y , suc z)
-}

-- Define a new function that takes in a decreasing Acc proof as well, and hence is acceptable to the termination checker

f-acc : ∀ (x : ℕ) → Acc _<₃_ x → ℕ
f-acc (x , zero  , z) rec       = z
f-acc (x , suc y , z) (acc rec) = f-acc (x , y , suc z)
  (rec _ (inj₂ (refl , inj₁ ≤-refl)))  -- proof that the tuple is decreasing lexicographically

-- Use <₃-wellFounded to provide the Acc proof
f : ℕ × ℕ × ℕ → ℕ
f xyz = f-acc xyz (<₃-wellFounded xyz)
```

Best,
Matthew

On Sat, Feb 29, 2020 at 4:08 PM Matthew Daggitt <matthewdaggitt at gmail.com<mailto:matthewdaggitt at gmail.com>> wrote:
Hi Jeremy,
 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!

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.
Best,
Matthew


On Sat, Feb 29, 2020 at 1:05 PM Siek, Jeremy <jsiek at indiana.edu<mailto:jsiek at indiana.edu>> wrote:
I would like to define a function (Martello and Montanari’s unification algorithm)
whose termination measure is a lexicographic ordering of three numbers.
I get the impression that there is support for this kind of thing in the
standard library, in Induction.WellFounded.Lexicographic.
However, I’m at a loss trying to figure out how to use it.
Any examples or pointers to documentation or tutorials
would be much appreciated.

Thank you,
Jeremy





_______________________________________________
Agda mailing list
Agda at lists.chalmers.se<mailto: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/20200229/c05e92fa/attachment.html>