Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Bug: GuessLex prints “Unexpected expression while unpacking n-ary argument” #3175

Closed
nomeata opened this issue Jan 13, 2024 · 0 comments · Fixed by #3176
Closed

Bug: GuessLex prints “Unexpected expression while unpacking n-ary argument” #3175

nomeata opened this issue Jan 13, 2024 · 0 comments · Fixed by #3176
Labels
bug Something isn't working

Comments

@nomeata
Copy link
Collaborator

nomeata commented Jan 13, 2024

Description

GuessLex is confused by

def foo {n : Nat} (i : Fin n) : Bool := foo ⟨0, Nat.zero_lt_one⟩
decreasing_by decreasing_tactic

and prints

Unexpected expression while unpacking n-ary argument

No such error with

def foo {n : Nat} (i : Fin n) : Bool := foo ⟨0, Nat.zero_lt_one⟩
termination_by foo => sizeOf i
decreasing_by decreasing_tactic

Versions

4.5.0-rc1

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
@nomeata nomeata added the bug Something isn't working label Jan 13, 2024
@nomeata nomeata mentioned this issue Jan 13, 2024
Merged
github-merge-queue bot pushed a commit that referenced this issue Jan 13, 2024
@nomeata
fix: Fix/GuessLex: refine through more casesOnApp/matcherApp (#3176)
53af5ea 
there was a check

if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then

that would avoid going through `.refineThrough`/`.addArg` for
matcher/casesOn applications. It seems it tries to detect when refining
the motive/param is pointless, but it was too eager, and cause confusion
with, for example, this reasonably reasonable function:

    def foo : (n : Nat) → (i : Fin n) → Bool
      | 0, _ => false
      | 1, _ => false
      | _+2, _ => foo 1 ⟨0, Nat.zero_lt_one⟩
    decreasing_by simp_wf; simp_arith

In particular, the `GuessLex` code later expects that the (implict)
`PProd.casesOn` in the implementation of `foo._unary` will refine the
paramter, because else the (rather picky) `unpackArg` fails. But it also
prevents this from being provable.

So let's try without this shortcut.

Fixing this also revealed that `withRecApps` wasn’t looking in all
corners
of a matcherApp/casesOnApp.

Fixes #3175
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Something isn't working
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: Fix/GuessLex: refine through more casesOnApp/matcherApp leanprover/lean4
1 participant
@nomeata