No goal to be solved error

Stream: lean4

[Alice Laroche]

I have a problem, and a minimal working (kinda) example.
I have an intricate function where lean is unable to prove termination, so i provide termination_by
Then i have some things to prove, so i write theorems and tag them @[simp]
And then i get No goal to be solved where i previously got tactic 'assumption' failed

In this MWE lean is able to prove termination, but if i use the termination_by modifier the same problem appear, so i hope it will be enough

open List

inductive Foo : Type where
| baz : Foo
| bar : Char -> Foo -> Foo
open Foo

@[simp] -- comment this for seeing the `tactic 'assumption' failed` error
def tmp (c' : Char) (cs' : List Char) : sizeOf cs' < 1 + sizeOf c' + sizeOf cs' :=
by rw [Nat.add_comm, Nat.add_comm 1, Nat.add_one, Nat.add_succ]
   apply Nat.succ_le_succ
   apply Nat.le_add_right

def toLst (f : Foo) (l : List Char) : List Char :=
match f, l with
| baz     , l => l
| bar c cs, nil=> []
| bar c cs, cons c' cs' => toLst cs (toLst cs cs')
termination_by _ => (sizeOf l) -- lean can work without this but it's not the point

[Arthur Paulino]

Lean is able to figure out termination on my machine here:

open List

inductive Foo : Type where
| baz : Foo
| bar : Char -> Foo -> Foo
open Foo

def toLst (f : Foo) (l : List Char) : List Char :=
match f, l with
| baz     , l => l
| bar c cs, nil=> []
| bar c cs, cons c' cs' => toLst cs (toLst cs cs')

Version: leanprover/lean4:nightly-2022-01-15

[Arthur Paulino]

(maybe I wasn't able to understand the issue you're facing)

[Alice Laroche]

It's a simplification of a function where lean can't figure out termination and where i'm forced to add the termination_by
and then i get No goal to be solved

[Alice Laroche]

like in this example if you don't remove the last line

[Alice Laroche]

(i will search a simple function where lean can't figure out the termination tomorrow, but now i need to sleep)

[Chris B]

If you leave the last line in, I assume it's just complaining because you don't need to manually show that toLst is decreasing. If you're saying toLst is different than the function you're actually working with, you may have to post the whole thing to get useful feedback.

[Kyle Miller]

@Alice Laroche Here you go, an example where you can neither include nor not include the last line:

open List

inductive Foo : Type where
| baz : Foo
| bar : Char × Foo -> Foo
open Foo

@[simp] -- comment this for seeing the `tactic 'assumption' failed` error
def tmp (c' : Char) (cs' : List Char) : sizeOf cs' < 1 + sizeOf c' + sizeOf cs' :=
by rw [Nat.add_comm, Nat.add_comm 1, Nat.add_one, Nat.add_succ]
   apply Nat.succ_le_succ
   apply Nat.le_add_right

def toLst (f : Foo) (l : List Char) : List Char :=
match f, l with
| baz     , l => l
| bar (c, cs), nil=> []
| bar (c, cs), cons c' cs' => toLst cs (toLst cs cs')
termination_by _ => (sizeOf l) -- lean can work without this but it's not the point

[Kyle Miller]

(I'm having the same kind of problem: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/structural.20recursion.20cannot.20be.20used/near/269063033)

[Chris B]

That seems like a less than perfect error message for needing a decreasing_by clause. This works for me.

inductive Foo : Type where
| baz : Foo
| bar : Char × Foo -> Foo
open Foo

@[simp] -- comment this for seeing the `tactic 'assumption' failed` error
def tmp (c' : Char) (cs' : List Char) : sizeOf cs' < 1 + sizeOf c' + sizeOf cs' :=
by rw [Nat.add_comm, Nat.add_comm 1, Nat.add_one, Nat.add_succ]
   apply Nat.succ_le_succ
   apply Nat.le_add_right

def toLst (f : Foo) (l : List Char) : List Char :=
match f, l with
| baz     , l => l
| bar (c, cs), nil=> []
| bar (c, cs), cons c' cs' => toLst cs (toLst cs cs')
termination_by _ => (sizeOf l) -- lean can work without this but it's not the point
decreasing_by sorry

[Alice Laroche]

@Kyle Miller
Oh, so this was the product type which messed up
I have a product in my original function, it was what was missing, thank you

[Alice Laroche]

@Chris B Well, using sorry is not really a solution

[Chris B]

By "this works for me", I meant "this quiets the error message you mentioned". You still need to provide a proof that it's decreasing.