[Merged by Bors] - fix(library/tactic): improve out_param support in simp #659
Conversation
|
This certainly needs a ready-to-synthesize check, otherwise everything is treated as an out_param†: class A (α β : Type) -- no out_param!
instance : A ℕ ℤ := ⟨⟩
def p (_ : Type) : Prop := false
@[simp] lemma l {α β} [A α β] : p α ↔ p β := iff.rfl
example : p ℕ := by simp --> p ℤ† albeit with reducible transparency instead of semireducible, of course Can you also mention where this turned up in mathlib? This will make it easier to sell as a Lean 4 change. |
|
as far as I know, this patch was because lemmas like |
This ensures non-`out_param`s are not accidentally filled through unification with the temporary metavariables. `out_param`s are still allowed to contain metavariables that will be unified (see also #657). I moved the `ready_to_synthesize` check from the elaborator to the type context in order to access it from the simplifier. Co-Authored-By: Gabriel Ebner <gebner@gebner.org>
src/library/tactic/simp_util.h
Outdated
| tout() << "unable to assign instance for: " << mvar_type << "\n";); | ||
| failed = true; | ||
| tout() << "unable to synthesize instance for: " << mvar_type << "\n";); | ||
| done = false; |
There was a problem hiding this comment.
I think we can do an early return here now. If it fails once, then it's not going to succeed in a future iteration (because of the ready-to-synthesize check). The same goes for the auto-param/discharging code below, if it fails we shouldn't try to fill in the other parameters. (I'm a bit concerned about performance here. Ideally we'd only try to synthesize each argument once, and fail immediately without futilely solving the rest if it doesn't succeed.)
There was a problem hiding this comment.
I wanted to retry the instances to avoid having cases like {α : Type*} [some_class_with_out_param α] [some_class_with_in_param α] work and {α : Type*} [some_class_with_in_param α] [some_class_with_out_param α] fail. As long as it's guarded by the metavariable check, I agree that this should work.
Indeed this was one of the cases, although this was mostly worked around as a side effect of adding the For the |
|
LGTM. Thanks! bors r+ |
When a `simp` lemma matches with the goal, all remaining arguments, occurring as temporary metavariables, were inferred left-to-right by `instantiate_emetas`, stopping at the first metavariable that can't be inferred through matching with the goal, instance synthesis, or using the prover argument to `simp`. This meant a `simp` lemma with a parameter corresponding to the `out_param` of a typeclass will be rejected, unless that class occurs in the goal. I modified `instantiate_emetas` to instead repeat until either all metavariables are inferred, or no progress is made on instantiating. I had to use a temporary type context to infer instances, in order to correctly unify the `out_param`s with the temporary metavariables occurring earlier in the `simp` lemma. If I understand the comments about temporary type contexts correctly, this is the same as `rw` does, so this should not cause any regressions.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
This PR introduces morphism classes corresponding to `mul_action_hom`, `distrib_mul_action_hom`, `mul_semiring_action_hom` and `linear_map`. Most of the new generic results work smoothly, only `simp` seems to have trouble applying `map_smulₛₗ`. I expect this requires another fix in the elaborator along the lines of [lean#659](leanprover-community/lean#659). For now we can just keep around the specialized `simp` lemmas `linear_map.map_smulₛₗ` and `linear_equiv.map_smulₛₗ`. The other changes are either making `map_smul` protected where it conflicts, or helping the elaborator unfold some definitions that previously were helped by the specific `map_smul` lemma suggesting the type. Thanks to @dupuisf for updating and making this branch compile! Co-Authored-By: Frédéric Dupuis <dupuisf@iro.umontreal.ca> Co-authored-by: Frédéric Dupuis <dupuisf@iro.umontreal.ca> Co-authored-by: Anne Baanen <t.baanen@vu.nl>
When a
simplemma matches with the goal, all remaining arguments, occurring as temporary metavariables, were inferred left-to-right byinstantiate_emetas, stopping at the first metavariable that can't be inferred through matching with the goal, instance synthesis, or using the prover argument tosimp. This meant asimplemma with a parameter corresponding to theout_paramof a typeclass will be rejected, unless that class occurs in the goal.I modified
instantiate_emetasto instead repeat until either all metavariables are inferred, or no progress is made on instantiating. I had to use a temporary type context to infer instances, in order to correctly unify theout_params with the temporary metavariables occurring earlier in thesimplemma. If I understand the comments about temporary type contexts correctly, this is the same asrwdoes, so this should not cause any regressions.