[Agda] recursion, lexicographic ordering

[Matthew Daggitt]

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>
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> 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
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200229/86fdf6cd/attachment.html>