termination by

Stream: lean4

[Joseph O]

i need a termination by but i dont really know how they work. i need it for this function:

def allPairsAux (xs : List α) (ys : List β) (accum : List (α × β)) : List (α × β) :=
  match xs, ys with
  | [], [] => accum
  | _::xss, [] => allPairsAux xss ys accum
  | [], _::yss => allPairsAux xs yss accum
  | x::xs, y::ys =>
    allPairsAux (x::xs) ys ((x, y)::accum)

[Chris B]

I think this is actually kind of an advanced example because it's not on one argument:

def allPairsAux (xs : List α) (ys : List β) (accum : List (α × β)) : List (α × β) :=
  match hx:xs, hy:ys with
  | [], [] => accum
  | _::xss, [] =>
    have h0 : xss.length + ys.length < xss.length + 1 := by simp [hy, Nat.lt_succ_self]
    allPairsAux xss ys accum
  | [], _::yss =>
    have h0 : xs.length + yss.length < yss.length + 1 := by simp [hx, Nat.lt_succ_self]
    allPairsAux xs yss accum
  | x::xs, y::ys => allPairsAux (x::xs) ys ((x, y)::accum)
  termination_by _ _ xs ys _ => xs.length + ys.length

[Joseph O]

Chris B said:

I think this is actually kind of an advanced example because it's not on one argument:

def allPairsAux (xs : List α) (ys : List β) (accum : List (α × β)) : List (α × β) :=
  match hx:xs, hy:ys with
  | [], [] => accum
  | _::xss, [] =>
    have h0 : xss.length + ys.length < xss.length + 1 := by simp [hy, Nat.lt_succ_self]
    allPairsAux xss ys accum
  | [], _::yss =>
    have h0 : xs.length + yss.length < yss.length + 1 := by simp [hx, Nat.lt_succ_self]
    allPairsAux xs yss accum
  | x::xs, y::ys => allPairsAux (x::xs) ys ((x, y)::accum)
  termination_by _ _ xs ys _ => xs.length + ys.length

how is the termination by working there? and why are the haves nessacery?

[Chris B]

They're not strictly necessary, the syntax for termination hints allows for a decreasing_by <tactic proof>clause to discharge the proof obligations, but I think decreasing_by has issues when more than one branch produces a unique obligation. But in any case you have to show that something being passed as an argument is strictly decreasing with each recursive call, where decreasing is defined in terms of some instance of WellFoundedRelation.

[Chris B]

For each branch I think it looks in the local assumptions for a proof first, which is why the have thing works.

[Joseph O]

ah yes

[Joseph O]

how does the by simp thing work?

[Joseph O]

also, what is hx:xs and hy:ys?

[Chris B]

hx and hy are hypotheses. The by simp parts are tactic proofs, simp is a tactic that applies lemmas; it's applying the stuff in the brackets.

[Chris B]

Well I guess more accurately it's like syntax for a match that preserves the hypotheses in the match arms. So like in the first case you need a witness that hy = [].

[Joseph O]

how can i debug print values in the middle of a function?

[Joseph O]

Nevermind, i found it

[Joseph O]

i do have a question about my function:

def allPairsAux (xs : List α) (ys : List β) (accum : List (α × β)) : List (α × β) :=
  match hx:xs, hy:ys with
  | [], [] => accum.reverse
  | _::xs, [] =>
    have h0 : xs.length + ys.length < xs.length + 1 := by simp [hy, Nat.lt_succ_self]
    allPairsAux xs ys accum
  | [], _::ys =>
    have h0 : xs.length + ys.length < ys.length + 1 := by simp [hx, Nat.lt_succ_self]
    allPairsAux xs ys accum
  | x::xs, y::ys =>
    allPairsAux (x::xs) ys ((x, y)::accum)

lets say i input ['a', 'b'] [1, 2, 3] []. Here is how the iterations should go:

['a', 'b'] [1, 2, 3] []
['a', 'b'] [2, 3] [('a', 1)]
['a', 'b'] [3] [('a', 2), ('a', 1)]
['a', 'b'] [] [('a', 3), ('a', 2), ('a', 1)]
['b'] [1, 2, 3] [('a', 3), ('a', 2), ('a', 1)] -- this is what it should turn into, because it matches at the second case, but for some reason this is not happening
-- same process

this is the output: [("a", 1), ("a", 2), ("a", 3)]

i wish there was a way i could debug and print the values

[Joseph O]

do you have an idea why this could be happening @Chris B ?

[Chris B]

Because the version you just posted is now explicitly reversing the list in the nil/nil case.

[Reid Barton]

What do you expect allPairsAux ['a', 'b'] [] [('a', 3), ('a', 2), ('a', 1)] to be?

[Joseph O]

well it shouldn't return accum.reverse since it doesnt match the [] [] case

[Joseph O]

why is it matching on that then @Chris B

[Reid Barton]

It isn't matching the [] [] case.

[Chris B]

def allPairsAux (xs : List α) (ys : List β) (accum : List (α × β)) : List (α × β) :=
  match hx:xs, hy:ys with
  | [], [] => accum
  | _::xss, [] =>
    have h0 : xss.length + ys.length < xss.length + 1 := by simp [hy, Nat.lt_succ_self]
    allPairsAux xss ys accum
  | [], _::yss =>
    have h0 : xs.length + yss.length < yss.length + 1 := by simp [hx, Nat.lt_succ_self]
    allPairsAux xs yss accum
  | x::xs, y::ys => allPairsAux (x::xs) ys ((x, y)::accum)
  termination_by _ _ xs ys _ => xs.length + ys.length

-- [('a', 3), ('a', 2), ('a', 1)]
#eval allPairsAux ['a', 'b'] [1, 2, 3] []

def allPairsAux (xs : List α) (ys : List β) (accum : List (α × β)) : List (α × β) :=
  match hx:xs, hy:ys with
  | [], [] => accum.reverse
  | _::xss, [] =>
    have h0 : xss.length + ys.length < xss.length + 1 := by simp [hy, Nat.lt_succ_self]
    allPairsAux xss ys accum
  | [], _::yss =>
    have h0 : xs.length + yss.length < yss.length + 1 := by simp [hx, Nat.lt_succ_self]
    allPairsAux xs yss accum
  | x::xs, y::ys => allPairsAux (x::xs) ys ((x, y)::accum)
  termination_by _ _ xs ys _ => xs.length + ys.length

-- [('a', 1), ('a', 2), ('a', 3)]
#eval allPairsAux ['a', 'b'] [1, 2, 3] []

[Chris B]

The only thing I changed is the accum.reverse in the nil/nil case.

[Joseph O]

Yes, but that is not the output i am looking for

[Joseph O]

What i meant here:

['a', 'b'] [1, 2, 3] []
['a', 'b'] [2, 3] [('a', 1)]
['a', 'b'] [3] [('a', 2), ('a', 1)]
['a', 'b'] [] [('a', 3), ('a', 2), ('a', 1)]
['b'] [1, 2, 3] [('a', 3), ('a', 2), ('a', 1)] -- this is what it should turn into, because it matches at the second case, but for some reason this is not happening
-- same process

Is not the output, but it what allPairsAux should be taking as its arguments on its next iteration

[Joseph O]

The output should actually be

[(“a”, 1), (“a”,  2), (“a”, 3),  (“b”, 1), (“b”, 2), (“b”, 3)]

Sorry for not making myself clear

[Chris B]

That's just not the function you wrote, I don't know what to tell you. In the case that ys is empty and xs is not, you're calling the function recursively with the tail of xs and the empty list.

[Chris B]

But you seem to expect ys to become [1, 2, 3] again.

[Arthur Paulino]

I think it's easier if you write an auxiliary function that receives a : α and l : List β and then returns something of type List (α × β). Such that the return of 2 and ["a", "b", "c"] is [(2, "a"), (2, "b"), (2, "c")].

Then you can do a foldl on a List α using your function

[Arthur Paulino]

Unless, of course, you want to go through the exercise of building a standalone function. Then you can ignore my idea

[Joseph O]

Arthur Paulino said:

I think it's easier if you write an auxiliary function that receives a : α and l : List β and then returns something of type List (α × β). Such that the return of 2 and ["a", "b", "c"] is [(2, "a"), (2, "b"), (2, "c")].

Then you can do a foldl on a List α using your function

An auxiliary function for my auxiliary function?

[Joseph O]

Chris B said:

That's just not the function you wrote, I don't know what to tell you. In the case that ys is empty and xs is not, you're calling the function recursively with the tail of xs and the empty list.

I wanted it to reset to the original ys

[Joseph O]

that would solve the whole problem

[Joseph O]

Arthur Paulino said:

I think it's easier if you write an auxiliary function that receives a : α and l : List β and then returns something of type List (α × β). Such that the return of 2 and ["a", "b", "c"] is [(2, "a"), (2, "b"), (2, "c")].

Then you can do a foldl on a List α using your function

Why would I want to use fold? Doesn’t fold turn a sequence into a value

[Joseph O]

if I could hold the original values somewhere

[Yakov Pechersky]

That "value" can be another sequence.

[Joseph O]

Yakov Pechersky said:

That "value" can be another sequence.

And that sequence holds the original two lists?

[Yakov Pechersky]

You can build up a tuple as an aux function, and use prod.snd to get your final value. Check out accumulators in Haskell too.

[Joseph O]

i tried using a Product,

def allPairsAux (xs : List α) (ys : List β) (accum : List (α × β)) (origs: (List α × List β)) : List (α × β) :=
  match hx:xs, hy:ys with
  | [], [] => accum
  | _::xs, [] =>
    have h0 : xs.length + ys.length < xs.length + 1 := by simp [hy, Nat.lt_succ_self]
    allPairsAux xs (origs.2) accum origs
  | [], _::ys =>
    have h0 : xs.length + ys.length < ys.length + 1 := by simp [hx, Nat.lt_succ_self]
    allPairsAux (origs.1) ys accum origs
  | x::xs, y::ys =>
    allPairsAux (x::xs) ys ((x, y)::accum) origs

but i get the error

tactic 'assumption' failed,
α : Type u_1
β : Type u_2
xs✝ : List α
ys : List β
accum : List (α × β)
origs : List α × List β
x✝ : α
xs : List α
hx : xs✝ = x✝ :: xs
hy : ys = []
h0 : List.length xs + List.length ys < List.length xs + 1
⊢ List.length origs.snd + List.length accum < List.length accum

its pretty weird in my opinion

[Joseph O]

What could have cuased the assumption to fail?

[Reid Barton]

well, it's definitely not true that List.length origs.snd + List.length accum < List.length accum, right?

[Reid Barton]

I suggest you start out with a partial def so you can make sure the definition is correct first without worrying about termination

[Joseph O]

I have to prove that too?

[Joseph O]

Reid Barton said:

I suggest you start out with a partial def so you can make sure the definition is correct first without worrying about termination

ok

[Joseph O]

Reid Barton said:

well, it's definitely not true that List.length origs.snd + List.length accum < List.length accum, right?

where can i use that?

[Joseph O]

Any ideas???

[Alexander Bentkamp]

The last version you posted does not terminate:

partial def allPairsAux (xs : List α) (ys : List β) (accum : List (α × β)) (origs: (List α × List β)) : List (α × β) :=
  match hx:xs, hy:ys with
  | [], [] => accum
  | _::xs, [] =>
    have h0 : xs.length + ys.length < xs.length + 1 := by simp [hy, Nat.lt_succ_self]
    allPairsAux xs (origs.2) accum origs
  | [], _::ys =>
    have h0 : xs.length + ys.length < ys.length + 1 := by simp [hx, Nat.lt_succ_self]
    allPairsAux (origs.1) ys accum origs
  | x::xs, y::ys =>
    allPairsAux (x::xs) ys ((x, y)::accum) origs

#eval allPairsAux [1] [] [] ([1],[1])  -- Does not terminate.

Reid is right. Try to add partial like I did here and test the function using #eval until it does what you want it to do. Then you can attempt to prove termination.

[Joseph O]

i tried this but its the same thign

def allPairsAux (xs : List α) (ys : List β) (accum : List (α × β)) (origs: (List α × List β)) : List (α × β) :=
  match hx:xs, hy:ys with
  | [], [] => accum
  | _::xs, [] =>
    have h0 : xs.length + ys.length < xs.length + 1 := by simp [hy, Nat.lt_succ_self]
    allPairsAux xs (origs.snd) accum origs
  | [], _::ys =>
    have h0 : xs.length + ys.length < ys.length + 1 := by simp [hx, Nat.lt_succ_self]
    allPairsAux (origs.fst) ys accum origs
  | x::xs, y::ys =>
    allPairsAux (x::xs) ys ((x, y)::accum) origs

termination_by _ _ xs ys accum origs => (origs.snd).length + accum.length < accum.length

[Joseph O]

EDIT: fixed

[Arthur Paulino]

Isn't your server dead? CTRL+SHIFT+X sometimes brings it back to life

[Joseph O]

It was because I was evalutating a function that didnt terminate

[Joseph O]

something keeps crashing vscode though

[Joseph O]

and I really dont know how to fix the termination. Im going to admit it

[Alexander Bentkamp]

Here's my attempt at it (at least of what I think you are trying to define):

def allPairs (xs : List α) (ys : List β) : List (α × β) := xs.bind (fun x => ys.map (fun y => (x, y)))

[Joseph O]

Ah you used map. My goal was ultimately to use functions like map and fold as little as possible. But you know, its much esier. Also, what does xs.bind do?

[Joseph O]

I have no idea how the code you wrote works

[Mario Carneiro]

l.bind f is (l.map f).join, where join flattens a list of lists

[Mario Carneiro]

that is, you apply the function to each element of the list, and then concatenate all the resulting lists (the function returns a list for each element)

[Alexander Bentkamp]

Maybe it's easier to understand if I write it using two auxiliary definitions:

def attach (x : α) (ys : List β) : List (α × β) := ys.map (fun y => (x, y))

#eval attach 2 ["a","b","c"]
-- [(2, "a"), (2, "b"), (2, "c")]

def allPairsAux (xs : List α) (ys : List β) : List (List (α × β)) := xs.map (fun x => attach x ys)

#eval allPairsAux [1,2,3] ["a","b","c"]
-- [[(1, "a"), (1, "b"), (1, "c")], [(2, "a"), (2, "b"), (2, "c")], [(3, "a"), (3, "b"), (3, "c")]]

def allPairs (xs : List α) (ys : List β) : List (α × β) := (allPairsAux xs ys).join

#eval allPairs [1,2,3] ["a","b","c"]
-- [(1, "a"), (1, "b"), (1, "c"), (2, "a"), (2, "b"), (2, "c"), (3, "a"), (3, "b"), (3, "c")]

[Mario Carneiro]

Here's a version using only primitive operations on list:

def allPairs (xs : List α) (ys : List β) : List (α × β) :=
  let rec aux
  | [], ys, r => r
  | x::xs, ys, r =>
    let rec aux₂
    | [], r => r
    | y::ys, r => (x, y) :: r
    aux₂ ys (aux xs ys r)
  aux xs ys []

[Mario Carneiro]

Here's another version that should work but causes a kernel type check error (cc: @Leonardo de Moura)

def allPairs (xs : List α) (ys : List β) : List (α × β) :=
  let rec aux
  | [], r => r
  | x::xs, r =>
    let rec aux₂
    | [], r => r
    | y::ys, r => (x, y) :: r
    aux₂ ys (aux xs r)
  aux xs []

  (kernel) declaration has free variables 'allPairs.aux'

[Leonardo de Moura]

Mario Carneiro said:

Here's another version that should work but causes a kernel type check error (cc: Leonardo de Moura)

def allPairs (xs : List α) (ys : List β) : List (α × β) :=
  let rec aux
  | [], r => r
  | x::xs, r =>
    let rec aux₂
    | [], r => r
    | y::ys, r => (x, y) :: r
    aux₂ ys (aux xs r)
  aux xs []

  (kernel) declaration has free variables 'allPairs.aux'

Thanks for reporting the issue. I will take a look.

[Arthur Paulino]

I love it when bugs are found by casually playing with a system

[Mario Carneiro]

I think they call it "monkey testing"

[Leonardo de Moura]

https://github.com/leanprover/lean4/issues/1020

[Arthur Paulino]

Mario Carneiro said:

I think they call it "monkey testing"

I knew that terminology for random tests equipped with brutally fast inputs (easily applicable for testing apps with GUIs). Which makes me wonder if it's possible to apply this technique to attack the Lean kernel in various ways in search for bugs like this

[Mario Carneiro]

that sounds more like fuzz testing (which would probably work fairly well against the lean kernel)

[Joseph O]

Thanks everyone