Zulip Chat Archive

Stream: lean4

Topic: No goal to be solved error


Alice Laroche (Jan 24 2022 at 23:40):

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 (Jan 24 2022 at 23:48):

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 (Jan 24 2022 at 23:51):

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

Alice Laroche (Jan 24 2022 at 23:53):

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 (Jan 24 2022 at 23:53):

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

Alice Laroche (Jan 24 2022 at 23:54):

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

Chris B (Jan 24 2022 at 23:55):

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 (Jan 24 2022 at 23:56):

@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 (Jan 24 2022 at 23:56):

(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 (Jan 25 2022 at 00:01):

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 (Jan 25 2022 at 00:05):

@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 (Jan 25 2022 at 00:07):

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

Chris B (Jan 25 2022 at 00:20):

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.


Last updated: Dec 20 2023 at 11:08 UTC