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

fix: improvements to change tactic #6022

Merged
merged 11 commits into from
Nov 16, 2024
Merged

fix: improvements to change tactic #6022

merged 11 commits into from
Nov 16, 2024

Conversation

kmill
Copy link
Collaborator

@kmill kmill commented Nov 10, 2024 •
edited
Loading

This PR makes the change tactic and conv tactic use the same elaboration strategy. It works uniformly for both the target and local hypotheses. Now change can assign metavariables, for example:

example (x y z : Nat) : x + y = z := by
  change ?a = _
  let w := ?a
  -- now `w : Nat := x + y`

@kmill kmill added the changelog-language Language features, tactics, and metaprograms label Nov 10, 2024
@kmill kmill requested a review from kim-em as a code owner November 10, 2024 00:35
@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 Nov 10, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 10, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6022
50916fc
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 10, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6022
1ac5838
@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Nov 10, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 10, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6022
2b44f5f
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 10, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6022
ca54d60
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 10, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6022
fc5eab7
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 10, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6022
1a7ba50
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 10, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6022
19aa3ac
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 10, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6022
79eca06
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Nov 13, 2024 •
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 256b49bda95591e5d0ad0274523149025e25ae90 --onto 5e01e628b2ef90d8881a5ba10340032eeeabc5d4. (2024-11-13 19:10:17)
  • 💥 Mathlib branch lean-pr-testing-6022 build failed against this PR. (2024-11-15 18:29:09) View Log
  • 💥 Mathlib branch lean-pr-testing-6022 build failed against this PR. (2024-11-15 19:40:50) View Log
  • 💥 Mathlib branch lean-pr-testing-6022 build failed against this PR. (2024-11-16 06:41:50) View Log
  • ✅ Mathlib branch lean-pr-testing-6022 has successfully built against this PR. (2024-11-16 07:17:44) View Log

kmill added 9 commits November 15, 2024 09:13
@kmill
fix: improvements to change tactic
93a07b6 
This PR makes the `change` tactic and conv tactic use the same new elaboration strategy that works uniformly for both the target and local hypotheses. Fixes an issue where the following example would fail due to `a` being defined after `h`:
```lean
example (x y z w : Nat) (h : x + y = z + w) : True := by
  let a := x + y
  change a = _ at h
  trivial
```
Breaking change: `change` no longer creates goals if there are unassigned metavariables. Instead it throws "don't know how to synthesize placeholder" errors.
@kmill
allow creating new goals
f89f13a
@kmill
revert line reordering
9466bad
@kmill
use Term version of elabTermEnsuringType
28e5bec
@kmill
add .defEqHint synthetic mvar kind
62e24ec
@kmill
revert change to a test
d7e3879
@kmill
tests
07f7965
@kmill
update test
65eb47a
@kmill
remove defeqhint
b58b1d8
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 15, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6022
9f761d6
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 15, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6022
f1c3bee
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 15, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6022
9c03a98
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 15, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6022
21a7252
@kmill
fix: use Expr.equal instead of == in MVarId.replaceTargetDefEq …
cc3676f 
…and `MVarId.replaceLocalDeclDefEq` (leanprover#6098)

This PR modifies `Lean.MVarId.replaceTargetDefEq` and
`Lean.MVarId.replaceLocalDeclDefEq` to use `Expr.equal` instead of
`Expr.eqv` when determining whether the expression has changed. This is
justified on the grounds that binder names and binder infos are
user-visible and affect elaboration.
@kmill kmill requested a review from leodemoura as a code owner November 16, 2024 05:47
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 16, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6022
c562526
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 16, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6022
7dbc30d
@kmill kmill added this pull request to the merge queue Nov 16, 2024
@leanprover-community-bot leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Nov 16, 2024
Merged via the queue into leanprover:master with commit 7643867 Nov 16, 2024
19 checks passed
JovanGerb pushed a commit to JovanGerb/lean4 that referenced this pull request Jan 21, 2025
@kmill @JovanGerb
fix: improvements to change tactic (leanprover#6022)
7d3a2e8 
This PR makes the `change` tactic and conv tactic use the same
elaboration strategy. It works uniformly for both the target and local
hypotheses. Now `change` can assign metavariables, for example:
```lean
example (x y z : Nat) : x + y = z := by
  change ?a = _
  let w := ?a
  -- now `w : Nat := x + y`
```
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR 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
@kmill @leanprover-community-bot