simp error "unknown metavariable"

[digama0]

@[simp] theorem liftOn_mk (a : α) (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :
    Quot.liftOn (Quot.mk r a) f h = f a := rfl

theorem eq_iff_true_of_subsingleton [Subsingleton α] (x y : α) : x = y ↔ True :=
  iff_true _ ▸ Subsingleton.elim ..

section attribute [simp] eq_iff_true_of_subsingleton end

@[simp] theorem PUnit.default_eq_unit : (default : PUnit) = PUnit.unit := rfl

example : (default : PUnit) = x := by simp
-- unknown metavariable '?_uniq.827'

Reported on Zulip.

[leodemoura]

Is liftOn_mk an actual [simp] theorem in Mathlib?
It is tried everywhere since we index things modulo reducibility.

[semorrison]

It is, and was just ported to mathlib4, in leanprover-community/mathlib4#559. I'll go have a look at where it is actually used in mathlib3.

[semorrison]

I haven't finished recompiling, but it looks like it's an easy fix to remove the @[simp] in mathlib. We'll need to write a new linter to catch these, however!

[semorrison]

Sorry, actually, I don't understand why this lemma would be a problem. The LHS still has head Quot.lift.

[leodemoura]

Sorry, actually, I don't understand why this lemma would be a problem. The LHS still has head Quot.lift.

@semorrison Lean 4 is computing the whnf modulo reducible constants. The term reduces to f a.
It seems this is going to be a big issue for the Mathlib port. We should probably change Lean 4, and only reduce nested terms when creating the index.

cc @digama0

[digama0]

Unfolding reducibles is indeed a change from lean 3, but I'm not yet convinced we can't just adapt to it as long as the new behavior is strictly better. One area where it is problematic is that simp is very unwilling to unfold reducible constants when asked to, because it sees right through them and hence doesn't see anything that needs unfolding. For the most part, if the LHS and RHS are equal up to reducible unfolding then I think we can just safely remove the @[simp] attribute on them. It would be nice to get a warning about this but I think a mathlib linter can do the job, but it does seem to be a regression that

@[simp] theorem liftOn_mk (a : α) (f : α → γ) : f a = f a := rfl

(which is how lean sees this lemma) is not an error, like it would be in lean 3 because the lemma trivially loops and also starts with a metavariable. (EDIT: actually this isn't an error in lean 3 either. It probably should be...)

[leodemoura]

I'm not yet convinced we can't just adapt to it as long as the new behavior is strictly better.

Not sure it is better. It seems to make it harder for users to control which [simp] theorems are applied. For example, suppose we have a reducible constant f ... := g ..., any simp theorem we add for f will also be applied to g applications. It seems we should disable reduction at least for the head symbol.

I will tag this issue with dev meeting.

[digama0]

Not sure it is better. It seems to make it harder for users to control which [simp] theorems are applied. For example, suppose we have a reducible constant f ... := g ..., any simp theorem we add for f will also be applied to g applications.

At least as far as near term advice for mathlib porting, I will be telling people not to tag simp theorems which have reducible definitions in them, and checking this in the simpNF linter. It just doesn't have the desired behavior - either firing on the wrong things or not firing on the right things - and this is because reducible definitions are supposed to be transparent to tactics like simp and rw, or at least that's what I tell people.