[Agda] termination checking & with

[Robby Findler]

Hi all:

I've noticed that termination checking has trouble "seeing" through `with`
and I'm wondering if there might be some improvements coming down the pike
that might help.

As a simple example, compare these two definitions of `merge` from merge
sort; the first one is okay and the second one isn't.

merge : 𝕃 ℕ -> 𝕃 ℕ -> 𝕃 ℕ
merge [] l = l
merge (x :: l) [] = x :: l
merge (x₁ :: l1) (x₂ :: l2) =
  if (x₁ < x₂)
  then x₁ :: merge l1 (x₂ :: l2)
  else x₂ :: merge (x₁ :: l1) l2


merge : 𝕃 ℕ -> 𝕃 ℕ -> 𝕃 ℕ
merge [] m = m
merge (x :: l) [] = x :: l
merge (x :: l) (y :: m) with x < y
... | tt = merge l (y :: m)
... | ff = merge (x :: l) m

This also comes up in proofs where the inductive hypothesis has to be bound
to a variable before doing a case split (with a `with`).

Robby

;; --------

The code above is using the IAL; here's a complete agda file without any
dependencies in case that's helpful.

module _ where

data 𝔹 : Set where
 tt : 𝔹
 ff : 𝔹

infix  4 if_then_else_

if_then_else_ : ∀ {ℓ} {A : Set ℓ} → 𝔹 → A → A → A
if tt then y else z = y
if ff then y else z = z

data 𝕃 {ℓ} (A : Set ℓ) : Set ℓ where
  [] : 𝕃 A
  _::_ : (x : A) (xs : 𝕃 A) → 𝕃 A

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

_<_ : ℕ → ℕ → 𝔹
zero < zero = ff
zero < (suc y) = tt
(suc x) < (suc y) = x < y
(suc x) < zero = ff

merge : 𝕃 ℕ -> 𝕃 ℕ -> 𝕃 ℕ
merge [] l = l
merge (x :: l) [] = x :: l
merge (x₁ :: l1) (x₂ :: l2) =
  if (x₁ < x₂)
  then x₁ :: merge l1 (x₂ :: l2)
  else x₂ :: merge (x₁ :: l1) l2

merge' : 𝕃 ℕ -> 𝕃 ℕ -> 𝕃 ℕ
merge' [] m = m
merge' (x :: l) [] = x :: l
merge' (x :: l) (y :: m) with x < y
... | tt = merge' l (y :: m)
... | ff = merge' (x :: l) m
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20211228/ad5bbd74/attachment-0001.html>