Zulip Chat Archive

Stream: lean4

Topic: Importing Log breaks termination proof

Jeremy Salwen (Jan 08 2023 at 01:54):

I have been having difficulty with a termination proof. I am seeing weird behavior which seems bug-like. The following MWE works fine:

import Std.Data.List.Basic
open Lean

def examp [DecidableEq α] (delim: List α) (l:List α) (h: delim ≠ []): List α :=
  match h₀: l with
  | [] => []
  | head::tail =>
    match List.getRest l delim with
    | none => examp delim tail h
    | some rest =>
      have _: sizeOf rest < sizeOf l := by sorry
      examp delim rest h
decreasing_by decreasing_tactic

But if I add the import import Mathlib.Data.Nat.Log at the top of the file, then I get the "failed to prove termination" error message. Is this a bug, or is something else going on?

James Gallicchio (Jan 08 2023 at 04:08):

If I had to guess, it's because of the (transitively) imported mathlib simp lemmas. Could also be that mathlib extends decreasing_trivial. Investigating!

James Gallicchio (Jan 08 2023 at 04:36):

I think simp lemmas are the culprit; looks like it's actually not proving for the first recursive call, not the second

James Gallicchio (Jan 08 2023 at 04:46):

New MWE:

import Mathlib.Data.Nat.Order.Basic

example (delim : List α) (h: delim ≠ []) (head : α) (tail : List α)
  : (invImage (β := Nat) (fun (a : (_ : List α) ×' delim ≠ []) => PSigma.casesOn a fun x _ => sizeOf x) instWellFoundedRelation).1 { fst := tail, snd := h }
  { fst := head :: tail, snd := h }
  := by decreasing_with simp (config := { arith := true })

Mario Carneiro (Jan 08 2023 at 04:47):

what does set_option trace.Meta.simp.rewrite true show in each case?

James Gallicchio (Jan 08 2023 at 04:48):

Oh, a useful trace option! Let me see...

Jeremy Salwen (Jan 08 2023 at 04:49):

The weird thing is that it doesn't even present me with any unsolved goals, just that it failed. Let me try that option.

Jeremy Salwen (Jan 08 2023 at 04:49):

image.png

James Gallicchio (Jan 08 2023 at 04:50):

Oh, wait a minute

James Gallicchio (Jan 08 2023 at 04:50):

import Mathlib.Data.Nat.Order.Basic

--set_option trace.Meta.Tactic.simp.rewrite true

example (delim : List α) (h: delim ≠ []) (head : α) (tail : List α)
  : (invImage (β := Nat) (fun (a : (_ : List α) ×' delim ≠ []) => PSigma.casesOn a fun x _ => sizeOf x) instWellFoundedRelation).1 { fst := tail, snd := h }
  { fst := head :: tail, snd := h }
  := by
    simp_wf
    --simp (config := { arith := true })

James Gallicchio (Jan 08 2023 at 04:50):

so simp_wf is changing :)

James Gallicchio (Jan 08 2023 at 04:51):

Wondering if decreasing_tactic should add an alternative in its first to simply not try the given tactic...
edit: probably a bad idea

Mario Carneiro (Jan 08 2023 at 04:52):

what does it output? (lean is not in front of me)

Jeremy Salwen (Jan 08 2023 at 04:52):

Paste the whole thing here?

Jeremy Salwen (Jan 08 2023 at 04:55):

[Meta.Tactic.simp.rewrite] unfold InvImage, InvImage WellFoundedRelation.rel (fun a => PSigma.casesOn a fun x x_1 => sizeOf x)
      { fst := tail, snd := h }
      { fst := head :: tail,
        snd :=
          h } ==> WellFoundedRelation.rel ((fun a => PSigma.casesOn a fun x x_1 => sizeOf x) { fst := tail, snd := h })
      ((fun a => PSigma.casesOn a fun x x_1 => sizeOf x) { fst := head :: tail, snd := h })

[Meta.Tactic.simp.rewrite] unfold InvImage, InvImage WellFoundedRelation.rel sizeOf
      ((fun a => PSigma.casesOn a fun x x_1 => sizeOf x) { fst := tail, snd := h })
      ((fun a => PSigma.casesOn a fun x x_1 => sizeOf x)
        { fst := head :: tail,
          snd :=
            h }) ==> WellFoundedRelation.rel
      (sizeOf ((fun a => PSigma.casesOn a fun x x_1 => sizeOf x) { fst := tail, snd := h }))
      (sizeOf ((fun a => PSigma.casesOn a fun x x_1 => sizeOf x) { fst := head :: tail, snd := h }))

[Meta.Tactic.simp.rewrite] unfold Nat.lt_wfRel, Nat.lt_wfRel ==> { rel := Nat.lt, wf := Nat.lt_wfRel.proof_1 }

[Meta.Tactic.simp.rewrite] sizeOf_nat:1000, sizeOf (sizeOf tail) ==> sizeOf tail

[Meta.Tactic.simp.rewrite] @List.cons.sizeOf_spec:1000, sizeOf (head :: tail) ==> 1 + sizeOf head + sizeOf tail

[Meta.Tactic.simp.rewrite] @sizeOf_default:1000, sizeOf head ==> 0

[Meta.Tactic.simp.rewrite] @add_zero:1000, 1 + 0 ==> 1

[Meta.Tactic.simp.rewrite] sizeOf_nat:1000, sizeOf (1 + sizeOf tail) ==> 1 + sizeOf tail

[Meta.Tactic.simp.rewrite] @Nat.lt_eq:1000, Nat.lt (sizeOf tail) (1 + sizeOf tail) ==> sizeOf tail < 1 + sizeOf tail

[Meta.Tactic.simp.rewrite] @lt_add_iff_pos_left:1000, sizeOf tail < 1 + sizeOf tail ==> 0 < 1

James Gallicchio (Jan 08 2023 at 04:56):

simp_wf is declared as

macro "simp_wf" : tactic =>
  `(tactic| simp [invImage, InvImage, Prod.lex, sizeOfWFRel,
          measure, Nat.lt_wfRel, WellFoundedRelation.rel])

It's a bit odd to me that it isn't a simp only; the goal is closed by a simp lemma that can immediately be applied after the wf lemmas

Mario Carneiro (Jan 08 2023 at 04:57):

@Jeremy Salwen is that with or without the mathlib simp lemmas?

Mario Carneiro (Jan 08 2023 at 04:58):

@James Gallicchio It is intentional that it is not simp only, you should be able to mark your own functions as simp to improve the termination checker locally

Jeremy Salwen (Jan 08 2023 at 04:58):

That is with them:

import Mathlib.Data.Nat.Order.Basic
import Mathlib.Data.Nat.Log

set_option trace.Meta.Tactic.simp.rewrite true

example (delim : List α) (h: delim ≠ []) (head : α) (tail : List α)
  : (invImage (β := Nat) (fun (a : (_ : List α) ×' delim ≠ []) => PSigma.casesOn a fun x _ => sizeOf x) instWellFoundedRelation).1 { fst := tail, snd := h }
  { fst := head :: tail, snd := h }
  := by
    simp_wf
    -- simp (config := { arith := true })

Mario Carneiro (Jan 08 2023 at 04:59):

it looks like it's closing the goal, so what's the problem?

Jeremy Salwen (Jan 08 2023 at 04:59):

But actually for me James's MWE works fine.

Jeremy Salwen (Jan 08 2023 at 04:59):

Yeah ok, let me post from my original MWE

Jeremy Salwen (Jan 08 2023 at 05:01):

Here is the output from the failing original MWE:

[Meta.Tactic.simp.rewrite] unfold InvImage, InvImage WellFoundedRelation.rel fun a =>
      PSigma.casesOn a fun x snd =>
        sizeOf
          x ==> fun a₁ a₂ =>
      WellFoundedRelation.rel ((fun a => PSigma.casesOn a fun x snd => sizeOf x) a₁)
        ((fun a => PSigma.casesOn a fun x snd => sizeOf x) a₂)

[Meta.Tactic.simp.rewrite] @ne_eq:1000, delim ≠ [] ==> ¬delim = []

[Meta.Tactic.simp.rewrite] @ne_eq:1000, delim ≠ [] ==> ¬delim = []

[Meta.Tactic.simp.rewrite] unfold InvImage, InvImage WellFoundedRelation.rel sizeOf ((fun a => PSigma.casesOn a fun x snd => sizeOf x) a₁)
      ((fun a => PSigma.casesOn a fun x snd => sizeOf x)
        a₂) ==> WellFoundedRelation.rel (sizeOf ((fun a => PSigma.casesOn a fun x snd => sizeOf x) a₁))
      (sizeOf ((fun a => PSigma.casesOn a fun x snd => sizeOf x) a₂))

[Meta.Tactic.simp.rewrite] unfold Nat.lt_wfRel, Nat.lt_wfRel ==> { rel := Nat.lt, wf := Nat.lt_wfRel.proof_1 }

[Meta.Tactic.simp.rewrite] sizeOf_nat:1000, sizeOf (sizeOf a₁.fst) ==> sizeOf a₁.fst

[Meta.Tactic.simp.rewrite] sizeOf_nat:1000, sizeOf (sizeOf a₂.fst) ==> sizeOf a₂.fst

[Meta.Tactic.simp.rewrite] @Nat.lt_eq:1000, Nat.lt (sizeOf a₁.fst) (sizeOf a₂.fst) ==> sizeOf a₁.fst < sizeOf a₂.fst

[Meta.Tactic.simp.rewrite] @ne_eq:1000, delim ≠ [] ==> ¬delim = []

[Meta.Tactic.simp.rewrite] @ne_eq:1000, delim ≠ [] ==> ¬delim = []

[Meta.Tactic.simp.rewrite] @gt_iff_lt:1000, (fun a₁ a₂ => sizeOf a₁.fst < sizeOf a₂.fst) { fst := tail, snd := h }
      { fst := head :: tail,
        snd := h } ==> sizeOf { fst := tail, snd := h }.fst < sizeOf { fst := head :: tail, snd := h }.fst

[Meta.Tactic.simp.rewrite] @List.cons.sizeOf_spec:1000, sizeOf (head :: tail) ==> 1 + sizeOf head + sizeOf tail

[Meta.Tactic.simp.rewrite] @sizeOf_default:1000, sizeOf head ==> 0

[Meta.Tactic.simp.rewrite] @add_zero:1000, 1 + 0 ==> 1

[Meta.Tactic.simp.rewrite] @lt_add_iff_pos_left:1000, sizeOf tail < 1 + sizeOf tail ==> 0 < 1

[Meta.Tactic.simp.rewrite] unfold InvImage, InvImage WellFoundedRelation.rel fun a =>
      PSigma.casesOn a fun x snd =>
        sizeOf
          x ==> fun a₁ a₂ =>
      WellFoundedRelation.rel ((fun a => PSigma.casesOn a fun x snd => sizeOf x) a₁)
        ((fun a => PSigma.casesOn a fun x snd => sizeOf x) a₂)

[Meta.Tactic.simp.rewrite] @ne_eq:1000, delim ≠ [] ==> ¬delim = []

[Meta.Tactic.simp.rewrite] @ne_eq:1000, delim ≠ [] ==> ¬delim = []

[Meta.Tactic.simp.rewrite] unfold InvImage, InvImage WellFoundedRelation.rel sizeOf ((fun a => PSigma.casesOn a fun x snd => sizeOf x) a₁)
      ((fun a => PSigma.casesOn a fun x snd => sizeOf x)
        a₂) ==> WellFoundedRelation.rel (sizeOf ((fun a => PSigma.casesOn a fun x snd => sizeOf x) a₁))
      (sizeOf ((fun a => PSigma.casesOn a fun x snd => sizeOf x) a₂))

[Meta.Tactic.simp.rewrite] unfold Nat.lt_wfRel, Nat.lt_wfRel ==> { rel := Nat.lt, wf := Nat.lt_wfRel.proof_1 }

[Meta.Tactic.simp.rewrite] sizeOf_nat:1000, sizeOf (sizeOf a₁.fst) ==> sizeOf a₁.fst

[Meta.Tactic.simp.rewrite] sizeOf_nat:1000, sizeOf (sizeOf a₂.fst) ==> sizeOf a₂.fst

[Meta.Tactic.simp.rewrite] @Nat.lt_eq:1000, Nat.lt (sizeOf a₁.fst) (sizeOf a₂.fst) ==> sizeOf a₁.fst < sizeOf a₂.fst

[Meta.Tactic.simp.rewrite] @ne_eq:1000, delim ≠ [] ==> ¬delim = []

[Meta.Tactic.simp.rewrite] @ne_eq:1000, delim ≠ [] ==> ¬delim = []

[Meta.Tactic.simp.rewrite] @gt_iff_lt:1000, (fun a₁ a₂ => sizeOf a₁.fst < sizeOf a₂.fst) { fst := rest, snd := h }
      { fst := head :: tail,
        snd := h } ==> sizeOf { fst := rest, snd := h }.fst < sizeOf { fst := head :: tail, snd := h }.fst

[Meta.Tactic.simp.rewrite] @List.cons.sizeOf_spec:1000, sizeOf (head :: tail) ==> 1 + sizeOf head + sizeOf tail

[Meta.Tactic.simp.rewrite] @sizeOf_default:1000, sizeOf head ==> 0

[Meta.Tactic.simp.rewrite] @add_zero:1000, 1 + 0 ==> 1

Jeremy Salwen (Jan 08 2023 at 05:01):

As I mentioned before the orignal MWE did not display any unsolved goal, just the error message that it couldn't prove termination, as I showed in the screenshot.

Mario Carneiro (Jan 08 2023 at 05:06):

Jeremy Salwen said:

As I mentioned before the orignal MWE did not display any unsolved goal, just the error message that it couldn't prove termination, as I showed in the screenshot.

This is an error reporting issue. I believe it is leaving goals, but they aren't being reported

Mario Carneiro (Jan 08 2023 at 05:06):

one trick you can do is termination_by decreasing_tactic; trace_state (untested)

Jeremy Salwen (Jan 08 2023 at 05:07):

Hmm, trace_state seems to only output an empty message :(

James Gallicchio (Jan 08 2023 at 05:09):

aside from the error reporting, I think decreasing_tactic should probably be modified include a done alternative. if you add

macro_rules | `(tactic| decreasing_trivial) => `(tactic| done)

to the original MWE it compiles with/without mathlib :)

James Gallicchio (Jan 08 2023 at 05:10):

definitely a bug from user perspective, if simp_wf is actually intended to apply all simp lemmas

Mario Carneiro (Jan 08 2023 at 05:11):

Here's a workaround by inlining stuff:

import Std.Data.List.Basic
import Mathlib.Data.Nat.Log

open Lean

def examp [DecidableEq α] (delim: List α) (l:List α) (h: delim ≠ []): List α :=
  match h₀: l with
  | [] => []
  | head::tail =>
    match List.getRest l delim with
    | none => examp delim tail h
    | some rest =>
      have _x: sizeOf rest < sizeOf l := by sorry
      examp delim rest h
decreasing_by
  simp_wf
  repeat (first | apply Prod.Lex.right | apply Prod.Lex.left)
  repeat (first | apply PSigma.Lex.right | apply PSigma.Lex.left)

which shows an error at examp delim rest h (so it was the second goal after all):

unsolved goals
deliml: List α
h: delim ≠ []
head: α
tail: List α
h₀: l = head :: tail
rest: List α
_x: sizeOf rest < sizeOf l
⊢ sizeOf rest < 1 + sizeOf tail

James Gallicchio (Jan 08 2023 at 05:12):

the first goal is closed by simp_wf alone. the second goal is closed by decreasing_tactic.

James Gallicchio (Jan 08 2023 at 05:13):

the issue is decreasing_tactic doesn't close something that simp_wf closes by itself :)

Mario Carneiro (Jan 08 2023 at 05:13):

oh I see, adding try decreasing_tactic at the end makes it pass

James Gallicchio (Jan 08 2023 at 05:14):

i partly suspect simp_wf should be simp only, since decreasing_tactic has a simp call anyways...

(is there a reasonable way I can test changes to simp_wf? editing the lean-toolchain's file and reloading doesn't seem to do anything)

Jeremy Salwen (Jan 08 2023 at 05:14):

If I introduce have _: sizeOf rest < 1 + sizeOf tail := by sorry at the second recursion, it still fails for me.

Mario Carneiro (Jan 08 2023 at 05:15):

not for me, that works (with try decreasing_tactic)

Jeremy Salwen (Jan 08 2023 at 05:16):

import Std.Data.List.Basic
import Mathlib.Data.Nat.Log

open Lean

def examp [DecidableEq α] (delim: List α) (l:List α) (h: delim ≠ []): List α :=
  match h₀: l with
  | [] => []
  | head::tail =>
    match List.getRest l delim with
    | none => examp delim tail h
    | some rest =>
      have _: sizeOf rest < 1 + sizeOf tail := by sorry
      have _: sizeOf rest <  sizeOf l := by sorry
      examp delim rest h
decreasing_by try decreasing_tactic

is what fails for me.

James Gallicchio (Jan 08 2023 at 05:16):

Jeremy Salwen said:

If I introduce have _: sizeOf rest < 1 + sizeOf tail := by sorry at the second recursion, it still fails for me.

(I think the first recursive call fails in your MWE, not the second. decreasing_tactic should succeed on both, but there's a bug that causes it to break with poor error messages)

Jeremy Salwen (Jan 08 2023 at 05:17):

ahh ok

Jeremy Salwen (Jan 08 2023 at 05:17):

decreasing_by try simp_wf; try decreasing_tactic works

James Gallicchio (Jan 08 2023 at 05:18):

in particular, it does a simp_wf which closes the goal for rec call 1, but then does another simp which fails. there's many ways to resolve this bug, I'm not sure what is the right one...

Jeremy Salwen (Jan 08 2023 at 05:18):

Do you know what the bug is?

Mario Carneiro (Jan 08 2023 at 05:25):

I think decreasing_with should look more like

`(tactic|
   (simp_wf
    repeat (first | apply Prod.Lex.right | apply Prod.Lex.left)
    repeat (first | apply PSigma.Lex.right | apply PSigma.Lex.left)
    first
    | done
    | $ts
    | fail "failed to prove termination, possible solutions: ...")

James Gallicchio (Jan 08 2023 at 05:30):

Yeah, that's definitely an option too. I'm sorta of the mind that decreasing_with should guarantee that it applies the tactic you pass (which would imply that simp_wf shouldn't be closing goals on its own)