simp doesn't rewrite because of unassigned metavariables #4398
Labels
bug
Something isn't working
Comments
leodemoura
added a commit
that referenced
this issue
Jun 17, 2024
When the type of a definition or example is a proposition,
we should elaborate on them as we elaborate on theorems.
This is particularly important for examples that are often
used in educational material.
Recall that when elaborating theorem headers, we convert unassigned
universe metavariables into universe parameters. The motivation is
that the proof of a theorem should not influence its statement.
However, before this commit, this was not the case for definitions and
examples when their type was a proposition. This discrepancy often confused users.
Additionally, we considered extending the above behavior whenever
the type of a definition is provided. That is, we would keep the
current behavior only if `: <type>` was omitted in a definition.
However, this proved to be too restrictive.
For example, the following instance in `Core.lean` would fail:
```
instance {α : Sort u} [Setoid α] : HasEquiv α :=
⟨Setoid.r⟩
```
and we would have to write instead:
```
instance {α : Sort u} [Setoid α] : HasEquiv.{u, 0} α :=
⟨Setoid.r⟩
```
There are other failures like this in the core, and we assume many more in Mathlib.
closes #4398
This was referenced Jun 17, 2024
github-merge-queue bot
pushed a commit
that referenced
this issue
Jun 24, 2024
When the type of an `example` is a proposition,
we should elaborate on them as we elaborate on theorems.
This is particularly important for examples that are often
used in educational material.
Recall that when elaborating theorem headers, we convert unassigned
universe metavariables into universe parameters. The motivation is
that the proof of a theorem should not influence its statement.
However, before this commit, this was not the case for examples when
their type was a proposition.
This discrepancy often confused users.
Additionally, we considered extending the above behavior to definitions
when
1- When their type is a proposition. However, it still caused disruption
in Mathlib.
2- When their type is provided. That is, we would keep the current
behavior only if `: <type>` was omitted. This would make the elaborator
for `def` much closer to the one for `theorem`, but it proved to be too
restrictive.
For example, the following instance in `Core.lean` would fail:
```
instance {α : Sort u} [Setoid α] : HasEquiv α :=
⟨Setoid.r⟩
```
and we would have to write instead:
```
instance {α : Sort u} [Setoid α] : HasEquiv.{u, 0} α :=
⟨Setoid.r⟩
```
There are other failures like this in the core, and we assume many more
in Mathlib.
closes #4398
closes #4482 Remark: PR #4482 implements option 1 above. We may consider
it again in the future.
leodemoura
added a commit
that referenced
this issue
Jun 27, 2024
When the type of a definition or example is a proposition,
we should elaborate on them as we elaborate on theorems.
This is particularly important for examples that are often
used in educational material.
Recall that when elaborating theorem headers, we convert unassigned
universe metavariables into universe parameters. The motivation is
that the proof of a theorem should not influence its statement.
However, before this commit, this was not the case for definitions and
examples when their type was a proposition. This discrepancy often confused users.
Additionally, we considered extending the above behavior whenever
the type of a definition is provided. That is, we would keep the
current behavior only if `: <type>` was omitted in a definition.
However, this proved to be too restrictive.
For example, the following instance in `Core.lean` would fail:
```
instance {α : Sort u} [Setoid α] : HasEquiv α :=
⟨Setoid.r⟩
```
and we would have to write instead:
```
instance {α : Sort u} [Setoid α] : HasEquiv.{u, 0} α :=
⟨Setoid.r⟩
```
There are other failures like this in the core, and we assume many more in Mathlib.
closes #4398
github-merge-queue bot
pushed a commit
that referenced
this issue
Jun 27, 2024
…e` (#4482) When the type of a definition or example is a proposition, we should elaborate on them as we elaborate on theorems. This is particularly important for examples that are often used in educational material. Recall that when elaborating theorem headers, we convert unassigned universe metavariables into universe parameters. The motivation is that the proof of a theorem should not influence its statement. However, before this commit, this was not the case for definitions and examples when their type was a proposition. This discrepancy often confused users. Additionally, we considered extending the above behavior whenever the type of a definition is provided. That is, we would keep the current behavior only if `: <type>` was omitted in a definition. However, this proved to be too restrictive. For example, the following instance in `Core.lean` would fail: ``` instance {α : Sort u} [Setoid α] : HasEquiv α := ⟨Setoid.r⟩ ``` and we would have to write instead: ``` instance {α : Sort u} [Setoid α] : HasEquiv.{u, 0} α := ⟨Setoid.r⟩ ``` There are other failures like this in the core, and we assume many more in Mathlib. closes #4398 @semorrison @jcommelin: what do you think?
|
While I think this was a good fix, I don't think my underlying issue was actually solved by this fix. set_option trace.Meta.Tactic.simp true
def foo {ι : Type _} (n m : ι) (h h' : n = m) : ℕ := by
simp only [id h] at h' -- no progress
simp only [h] at h' -- worksThis is an artificial example, but it frequently happens that as part of a definition you have to prove some proposition, so there can be (universe) metavariables around. Note: this is a low priority issue. It only rarely affects me. Can you reopen this, or do you prefer that I create a new issue? (I edited the first post, in case you reopen this.) |
3 tasks
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Prerequisites
Please put an X between the brackets as you perform the following steps:
https://github.com/leanprover/lean4/issues
Avoid dependencies to Mathlib or Batteries.
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
The following code fails:
The trace message is
Note that the unassigned metavariable is the universe metavariable of
ιExpected behavior:
simp only [id h]should succeed, just likesimp only [h]already does.Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
The text was updated successfully, but these errors were encountered: