Something that doesn't reduce, again

Stream: new members

[Ilmārs Cīrulis]

"Stole" the function merge from Init.Data.List.Sort.Basic and tried to use it for my purposes, but it doesn't reduce. Is there a way to modify it and make it reducible?

import Mathlib

def merge (xs ys : List Nat) : List Nat :=
  match xs, ys with
  | [], ys => ys
  | xs, [] => xs
  | x :: xs, y :: ys =>
    if Nat.ble x y then
      x :: merge xs (y :: ys)
    else
      y :: merge (x :: xs) ys

#reduce merge [1, 2, 3, 4] [2, 3, 4, 5]
#eval merge [1, 2, 3, 4] [2, 3, 4, 5]

[Ilmārs Cīrulis]

The original function is with @[irreducible] tag here, and I thought that maybe I can use it after copypasting the definition.

[Aaron Liu]

It's well founded recursion

[Aaron Liu]

which is always irreducible by default

[Ilmārs Cīrulis]

Ok, I will remember. Thank you!

[Aaron Liu]

You can see in src#List.merge that it isn't explicitly marked irreducible

[Aaron Liu]

There is probably a way to implement it in a way that it will reduce

[Ilmārs Cīrulis]

Yes, indeed.

I will try to find that way.

[Aaron Liu]

I can show you once I'm back at a keyboard

[Aaron Liu]

This is what I usually do to convert these termination by product lex kind of functions from well founded recursion into structural recursion

def merge (xs ys : List Nat) : List Nat :=
  match xs with
  | [] => ys
  | x :: xs => go x xs ys fun ys => merge xs ys
where
  go (x : Nat) (xs ys : List Nat) (k : List Nat → List Nat) :=
    match ys with
    | [] => x :: xs
    | y :: ys =>
      if x ≤ y then
        x :: k (y :: ys)
      else
        y :: go x xs ys k

[Ilmārs Cīrulis]

Oh, interesting, thank you!

This is my try, which I clumsily threw together before looking at your solution.

import Mathlib

def merge_aux (W : Nat) : ∀ (L1 L2 : List Nat) (_ : L1.length + L2.length = W), List Nat :=
  match W with
  | 0 => fun _ _ _ => []
  | w + 1 =>
    fun L1 L2 H =>
    match L1, L2 with
    | [], _ => L2
    | _, [] => L1
    | x1 :: t1, x2 :: t2 =>
      match Nat.ble x1 x2 with
      | true => x1 :: merge_aux w t1 (x2 :: t2) (by simp at H; grind)
      | false => x2 :: merge_aux w (x1 :: t1) t2 (by simp at H; grind)

def merge L1 L2 := merge_aux (L1.length + L2.length) L1 L2 rfl

#reduce merge [1, 2, 3, 4] [2, 3, 4, 5]
#eval merge [1, 2, 3, 4] [2, 3, 4, 5]

[Aaron Liu]

fuel?

[Aaron Liu]

I guess it's not really fuel

[Aaron Liu]

but in this case we have something better than fuel

[Aaron Liu]

since it's lexographic structural recursion we can split it up like this

[Ilmārs Cīrulis]

I will take your solution and use it, thank you!

[Ilmārs Cīrulis]

(and will study it, too, to be able to replicate it in similar situation next time)