Skip to content

feat: let get_elem_tactic_trivial handle [a]'h.2#3132

Merged
nomeata merged 4 commits intomasterfrom
joachim/mem_upper_element
Jan 8, 2024
Merged

feat: let get_elem_tactic_trivial handle [a]'h.2#3132
nomeata merged 4 commits intomasterfrom
joachim/mem_upper_element

Conversation

@nomeata
Copy link
Copy Markdown
Collaborator

@nomeata nomeata commented Jan 3, 2024

The pattern

    for h : i in [:xs.size] do
      let x := xs[i]'h.2

is occassionally useful to iterate over an array with the index in
hand. This PR extends the get_elem_tactic_trivial so that one can
simply write

    for h : i in [:xs.size] do
      let x := xs[i]

fixes #3032.

@nomeata
feat: let get_elem_tactic_trivial handle [a]'h.2
7bb9446 
The pattern
```
    for h : i in [:xs.size] do
      let x := xs[i]'h.2
```
is occassionally useful to iterate over an array with the index in
hand. This PR extends the `get_elem_tactic_trivial` so that one can
simply write
```
    for h : i in [:xs.size] do
      let x := xs[i]
```

fixes #3032.
@nomeata nomeata requested review from Kha and leodemoura as code owners January 3, 2024 12:04
@nomeata nomeata marked this pull request as draft January 3, 2024 12:09
@nomeata
Copy link
Copy Markdown
Collaborator Author

nomeata commented Jan 3, 2024

Hmm, the tactic

exact Membership.mem.upper (by assumption)

I wrote doesn’t work as well as I thought; the by assumption can pick the wrong one. #mwe:

macro_rules
  | `(tactic| get_elem_tactic_trivial) => `(tactic| exact Membership.mem.upper (by assumption))


def withTwoRanges (xs : Array Nat) : Option Nat := Id.run do
  for h1 : i in [:xs.size] do
    for h2 : j in [i + 1:xs.size] do
      if xs[i] == xs[j] then
        return i
  return none

Is it possible to say “apply Membership.mem.upper with the assumption that fits”? Or does that need something like solveByElim?

NB: Simply apply fails with

tactic 'apply' failed, failed to unify
  ?i < ?r.stop
with
  i < size a

@leodemoura
Copy link
Copy Markdown
Member

leodemoura commented Jan 3, 2024 •
edited
Loading

@nomeata What about the following?

theorem helper {r : Std.Range} (h₁ : i ∈ r) (h₂ : r.stop = n) : i < n := by
  have := h₁.2
  rw [h₂] at this
  assumption

macro_rules
  | `(tactic| get_elem_tactic_trivial) => `(tactic| apply helper; assumption; rfl)

def withTwoRanges (xs : Array Nat) : Option Nat := Id.run do
  for h1 : i in [:xs.size] do
    for h2 : j in [i + 1:xs.size] do
      if xs[i] == xs[j] then
        return i
  return none

BTW, we will be working on better automation this year.

@nomeata
Copy link
Copy Markdown
Collaborator Author

nomeata commented Jan 3, 2024

I thought about something in that direction, good to know that it was a reasonable direction :-)

@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 Jan 3, 2024
@ghost
Copy link
Copy Markdown

ghost commented Jan 3, 2024

  • ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-12-31' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2024-01-03 13:04:14)

@nomeata nomeata marked this pull request as ready for review January 3, 2024 13:53
@nomeata nomeata added the will-merge-soon …unless someone speaks up label Jan 3, 2024
@nomeata nomeata added this pull request to the merge queue Jan 8, 2024
Merged via the queue into master with commit 684f32f Jan 8, 2024
@kim-em kim-em mentioned this pull request Jan 9, 2024
Merged
digama0 pushed a commit to leanprover-community/batteries that referenced this pull request Jan 9, 2024
@kim-em
chore: remove unnecessary have (#516)
d5b9a30 
After leanprover/lean4#3132 the linter will complain about this.
kim-em added a commit to leanprover-community/batteries that referenced this pull request Feb 1, 2024
@kim-em @digama0
@leodemoura @nomeata @kmill @madvorak @fgdorais
chore: move to v4.6.0-rc1, merging adaptations (#576)
276953b 
* feat: hover info for `rcases h : ...` (#486)

* feat: hover info for `rcases h : ...`

* fix

* chore: adaptations for leanprover/lean4#3123 (#502)

* chore: adaptations for leanprover/lean4#3123

* update toolchain

* chore: remove unnecessary `have` (#516)

After leanprover/lean4#3132 the linter will complain about this.

* chore: simproc PR changes (#496)

See leanprover/lean4#3124

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

* chore: adaptions for nightly-2023-01-11 (#524)

* advance toolchain to nightly-2024-01-12, no updates required

* chore: updates to DiscrTree for changes in nightly (#536)

* doc: extend docstrings for `ext` and `ext1` (#525)

Makes sure to mention that the patterns are processed using `rintro`, and makes sure `ext` mentions `ext1`.

* docs(Data/List): typo (#529)

* feat: Eq.rec lemma (#385)

* chore: Add empty collection instance to BinomialHeap (#532)

* Incremental Library Search (#421)

This ports library_search from Mathlib to Std.  It preserves the ability to do caching, but is designed to support a cacheless mode.  The exact and apply tactics are named `std_exact?` and `std_apply?`, but will eventually be renamed.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

* fix termination_by clauses in LazyDiscrTree

fix LibrarySearch

* bump toolchain

---------

Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Martin Dvořák <martin.dvorak@matfyz.cz>
Co-authored-by: François G. Dorais <fgdorais@gmail.com>
Co-authored-by: Joe Hendrix <joe@lean-fro.org>

* feat: adaptations for leanprover/lean4#3159 (#557)

* merge origin/main

* chore: fixes for `simp` refactor (#571)

* move to v4.6.0-rc1

* fix proofs

---------

Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: Leonardo de Moura <leonardo@microsoft.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Martin Dvořák <martin.dvorak@matfyz.cz>
Co-authored-by: François G. Dorais <fgdorais@gmail.com>
Co-authored-by: Joe Hendrix <joe@lean-fro.org>
fgdorais added a commit to fgdorais/batteries that referenced this pull request Feb 18, 2024
@kim-em @digama0
@leodemoura @nomeata @kmill @madvorak @fgdorais
chore: move to v4.6.0-rc1, merging adaptations (leanprover-community#576
e8eb209 
)

* feat: hover info for `rcases h : ...` (leanprover-community#486)

* feat: hover info for `rcases h : ...`

* fix

* chore: adaptations for leanprover/lean4#3123 (leanprover-community#502)

* chore: adaptations for leanprover/lean4#3123

* update toolchain

* chore: remove unnecessary `have` (leanprover-community#516)

After leanprover/lean4#3132 the linter will complain about this.

* chore: simproc PR changes (leanprover-community#496)

See leanprover/lean4#3124

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

* chore: adaptions for nightly-2023-01-11 (leanprover-community#524)

* advance toolchain to nightly-2024-01-12, no updates required

* chore: updates to DiscrTree for changes in nightly (leanprover-community#536)

* doc: extend docstrings for `ext` and `ext1` (leanprover-community#525)

Makes sure to mention that the patterns are processed using `rintro`, and makes sure `ext` mentions `ext1`.

* docs(Data/List): typo (leanprover-community#529)

* feat: Eq.rec lemma (leanprover-community#385)

* chore: Add empty collection instance to BinomialHeap (leanprover-community#532)

* Incremental Library Search (leanprover-community#421)

This ports library_search from Mathlib to Std.  It preserves the ability to do caching, but is designed to support a cacheless mode.  The exact and apply tactics are named `std_exact?` and `std_apply?`, but will eventually be renamed.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

* fix termination_by clauses in LazyDiscrTree

fix LibrarySearch

* bump toolchain

---------

Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Martin Dvořák <martin.dvorak@matfyz.cz>
Co-authored-by: François G. Dorais <fgdorais@gmail.com>
Co-authored-by: Joe Hendrix <joe@lean-fro.org>

* feat: adaptations for leanprover/lean4#3159 (leanprover-community#557)

* merge origin/main

* chore: fixes for `simp` refactor (leanprover-community#571)

* move to v4.6.0-rc1

* fix proofs

---------

Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: Leonardo de Moura <leonardo@microsoft.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Martin Dvořák <martin.dvorak@matfyz.cz>
Co-authored-by: François G. Dorais <fgdorais@gmail.com>
Co-authored-by: Joe Hendrix <joe@lean-fro.org>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@leodemoura leodemoura leodemoura approved these changes

@Kha Kha Awaiting requested review from Kha

Assignees

No one assigned

Labels

toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN will-merge-soon …unless someone speaks up

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

RFC: Extend get_elem_tactic_trivial to handle [a]'h.2

2 participants

@nomeata @leodemoura