8000 feat: bv_decide support for simple pattern matching on enum inductives by hargoniX · Pull Request #7329 · leanprover/lean4 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

feat: bv_decide support for simple pattern matching on enum inductives #7329

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
Merged
merged 20 commits into from
Mar 7, 2025
Merged

feat: bv_decide support for simple pattern matching on enum inductives #7329

merged 20 commits into from
Mar 7, 2025

Conversation

hargoniX
Copy link
Contributor
@hargoniX hargoniX commented Mar 4, 2025 •
edited
Loading

This PR adds support to bv_decide for simple pattern matching on enum inductives. By simple we mean non dependent match statements with all arms written out.

This PR enables use cases such as:

namespace PingPong

inductive Direction where
  | goingDown
  | goingUp

structure State where
  val : BitVec 16
  low : BitVec 16
  high : BitVec 16
  direction : Direction

def State.step (s : State) : State :=
  match s.direction with
  | .goingDown =>
    if s.val = s.low then
      { s with direction := .goingUp }
    else
      { s with val := s.val - 1 }
  | .goingUp =>
    if s.val = s.high then
      { s with direction := .goingDown }
    else
      { s with val := s.val + 1 }

def State.steps (s : State) (n : Nat) : State :=
  match n with
  | 0 => s
  | n + 1 => (State.steps s n).step

def Inv (s : State) : Prop := s.low ≤ s.val ∧ s.val ≤ s.high ∧ s.low < s.high

example (s : State) (h : Inv s) (n : Nat) : Inv (State.steps s n) := by
  induction n with
  | zero => simp only [State.steps, Inv] at *; bv_decide
  | succ n ih =>
    simp only [State.steps, State.step, Inv] at *
    bv_decide

There is an important thing to consider in this implementation. As the enums pass can now deal with control flow there is a tension between the structures and enums pass at play:

  1. Enums should run before structures as it could convert matches on enums into cond
    chains. This in turn can be used by the structures pass to float projections into control
    flow which might be necessary.
  2. Structures should run before enums as it could reveal new facts about enums that we might
    need to handle. For example a structure might contain a field that contains a fact about
    some enum. This fact needs to be processed properly by the enums pass

To resolve this tension we do the following:

  1. Run the structures pass (if enabled)
  2. Run the enums pass (if enabled)
  3. Within the enums pass we rerun the part of the structures pass (if enabled) that could profit from the
    enums pass as described above. This comes down to adding a few more lemmas to a simp
    invocation that is going to happen in the enums pass anyway and should thus be cheap.

8000
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 4, 2025 14:33 Inactive
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Mar 4, 2025
@leanprover-community-bot
Copy link
Collaborator
leanprover-community-bot commented Mar 4, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 45806017e570fc17d3182c907a6ffe6c146025c6 --onto e3c6909ad593e5a966a449df5e92abb1f0dbc317. (2025-03-04 14:51:37)
  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-03-07 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-07 09:28:17)

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 4, 2025 16:41 Inactive
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 4, 2025 17:17 Inactive
@hargoniX hargoniX added the changelog-language Language features, tactics, and metaprograms label Mar 4, 2025
@hargoniX hargoniX marked this pull request as ready for review March 4, 2025 22:35
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 4, 2025 22:39 Inactive
@hargoniX hargoniX force-pushed the hbv/bv_decide_enum_match branch from 31c4eac to b8be79a Compare March 7, 2025 09:02
@hargoniX hargoniX enabled auto-merge March 7, 2025 09:03
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 7, 2025 09:08 Inactive
@hargoniX hargoniX added this pull request to the merge queue Mar 7, 2025
Merged via the queue into master with commit 20571a9 Mar 7, 2025
15 checks passed
@hargoniX hargoniX deleted the hbv/bv_decide_enum_match branch March 7, 2025 09:58
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@hargoniX @leanprover-community-bot
0