Open fpvandoorn opened 1 week ago
https://github.com/leanprover/lean4/issues/4398 is basically the same issue, and https://github.com/leanprover/lean4/pull/4493 didn't really fix the underlying issue.
The change in #4482 is only applied to def
s whose type is a Prop
. This is not the case here.
We can easily remove the <- isProp
condition there, and eliminate the discrepancy in the def
and theorem
elaborators.
See comment at #4482 for potential impact on users.
I don't think it's feasible to generalize universe metavariables in definitions before elaborating the value. As mentioned in #4482, that will lead to huge inconveniences.
I don't think that the rule "don't have universe metavariables around" is the right solution here. Here is a (somewhat contrived) example using theorem.
theorem bar (n m : Nat) : n = m → n = m := by
have : ∀ (α : Type _) (x y : α), x = y → x = y := by
intros α x y h
simp only [id h] -- error. The proof works if you remove `id`
exact this Nat n m
I might be completely misunderstanding why the behavior here happens, but my understanding is as follows:
My understanding of this issue is that when t
is an expression (not just a name), then simp [t]
will refuse to rewrite with t
if t
still contains universe metavariables. Maybe the check can be "no universe metavariables that are introduced by this simp" (if this can be checked cheaply)?
Feel free to mark this as low priority
/wontfix
, this is a low priority issue. I was surprised when I encountered it (it was within a def
), so I opened an issue.
@fpvandoorn Note that the theorem bar
example in your message will be rejected in the future. See #4610
I don't think that the rule "don't have universe metavariables around" is the right solution here
The motivation is simplicity.
Ok, this happens only rarely in Mathlib, so I think the fallout will be limited.
After that I think the only issue is in definitions.
Prerequisites
Please put an X between the brackets as you perform the following steps:
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.Related Issues
4398 is basically the same issue, and #4493 didn't really fix the underlying issue.
Impact
Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.