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

unknown constant in mutually recursive definition #2883

Closed
nomeata opened this issue Nov 15, 2023 · 0 comments · Fixed by #2892
Closed

unknown constant in mutually recursive definition #2883

nomeata opened this issue Nov 15, 2023 · 0 comments · Fixed by #2892
Assignees
@nomeata
Labels
bug Something isn't working

Comments

@nomeata
Copy link
Collaborator

nomeata commented Nov 15, 2023 •
edited
Loading

Description

In some mutually recursive definitions, we get unknown constant

Context

This was reported on Zulip.

Steps to Reproduce

mutual
  inductive A : Type
  | baseA  : A
  | fromB : B → A

  inductive B : Type
  | fromA  : A → B
end

mutual
  def foo : B → Prop    -- unknown constant 'bar'
  | .fromA a => bar a 0

  def bar : A → Nat → Prop
  | .baseA   => (fun _ => True)
  | .fromB b => (fun (c : Nat) => ∃ (t : Nat), foo b)
end
termination_by
  foo x => sizeOf x
  bar x => sizeOf x

Versions

4.3.0-rc1 on https://live.lean-lang.org/

Additional Information

This may or may not be the same or related to #2628.

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 Nov 15, 2023
@nomeata nomeata mentioned this issue Nov 16, 2023
Merged
nomeata added a commit that referenced this issue Nov 16, 2023
@nomeata
fix: PackMutual: Deal with extra arguments
6418a03 
previously, it would ignore a recursive call that has extra arguments,
which can happen when the recursive functions return something of
function type. Therefore just leave them extra arguments in place.

Fixes #2883.
nomeata added a commit that referenced this issue Nov 16, 2023
@nomeata
fix: PackMutual: Deal with extra arguments
cafff2a 
previously, it would ignore a recursive call that has extra arguments,
which can happen when the recursive functions return something of
function type. Therefore just leave them extra arguments in place.

Fixes #2883.
@nomeata nomeata self-assigned this Nov 16, 2023
nomeata added a commit that referenced this issue Nov 17, 2023
@nomeata
fix: PackMutual: Eta-Expand as needed
8ecf2e1 
The `packMutual` code ought to reliably replace all recursive calls to
the functions in `preDefs`, even when they are under- or over-applied.
Therefore eta-expand if need rsp. keep extra arguments around.

Needs a tweak to `Meta.transform` to avoid mistaking the `f` in
`f x1 x2` as a zero-arity application.

Includes a test case.

This fixes #2628 and #2883.
@nomeata nomeata mentioned this issue Nov 17, 2023
Merged
nomeata added a commit that referenced this issue Nov 17, 2023
@nomeata
fix: PackMutual: Eta-Expand as needed
7355af4 
The `packMutual` code ought to reliably replace all recursive calls to
the functions in `preDefs`, even when they are under- or over-applied.
Therefore eta-expand if need rsp. keep extra arguments around.

Needs a tweak to `Meta.transform` to avoid mistaking the `f` in
`f x1 x2` as a zero-arity application.

Includes a test case.

This fixes #2628 and #2883.
nomeata added a commit that referenced this issue Nov 20, 2023
@nomeata
fix: PackMutual: Deal with extra arguments (#2892)
9800e06 
previously, it would ignore a recursive call that has extra arguments,
which can happen when the recursive functions return something of
function type. Therefore just leave them extra arguments in place.

Fixes #2883.
github-merge-queue bot pushed a commit that referenced this issue Nov 22, 2023
@nomeata
fix: PackMutual: Eta-Expand as needed (#2902)
260eaeb 
The `packMutual` code ought to reliably replace all recursive calls to
the functions in `preDefs`, even when they are under- or over-applied.
Therefore eta-expand if need rsp. keep extra arguments around.

Needs a tweak to `Meta.transform` to avoid mistaking the `f` in
`f x1 x2` as a zero-arity application.

Includes a test case.

This fixes #2628 and #2883.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@nomeata nomeata

Labels
bug Something isn't working
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: PackMutual: Deal with extra arguments leanprover/lean4
1 participant
@nomeata