Zulip Chat Archive
Stream: mathlib4
Topic: simp
Yury G. Kudryashov (Nov 26 2022 at 21:15):
How do I call simp
from meta code? I have a name of a local hypothesis and I want to run simp only [h] at *
.
Yury G. Kudryashov (Nov 26 2022 at 21:15):
(do I need to explicitly remove h
from *
?)
Scott Morrison (Nov 27 2022 at 17:42):
Sorry @Yury G. Kudryashov, I should have posted this snippet before, which may be helpful:
open Meta
open Lean.Meta
open Lean.Elab.Tactic
def simpTheoremsOfNames (lemmas : List Name) : MetaM SimpTheorems := do
lemmas.foldlM (·.addConst ·) (← simpOnlyBuiltins.foldlM (·.addConst ·) {})
def simpOnlyNames (lemmas : List Name) (e : Expr) : MetaM Simp.Result := do
(·.1) <$> simp e { simpTheorems := #[← simpTheoremsOfNames lemmas], congrTheorems := ← getSimpCongrTheorems }
def categorySimp (e : Expr) : MetaM Simp.Result :=
simpOnlyNames [``Category.comp_id, ``Category.id_comp, ``Category.assoc] e
Yury G. Kudryashov (Nov 27 2022 at 20:40):
Can you PR it?
Scott Morrison (Nov 27 2022 at 20:59):
These are coming as part of https://github.com/leanprover-community/mathlib4/pull/749. Once I have a green tick there I can slice it up.
Patrick Massot (Nov 27 2022 at 21:36):
I see a green tick there
Scott Morrison (Nov 27 2022 at 22:05):
Okay mathlib4#755 has just the meta code.
Yury G. Kudryashov (Nov 27 2022 at 23:15):
Can you add location
parameter?
Scott Morrison (Nov 27 2022 at 23:20):
I mean, those functions are intended to operate purely on Expr
s, not interacting with a local context or goals.
Moritz Doll (Nov 27 2022 at 23:38):
Yury you might want to have a look at simpLocation
in core and https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/Zify.lean#L68 for creating a Simp.Context
Moritz Doll (Nov 27 2022 at 23:42):
so it should be something along the lines of
let ctx ← mkSimpContext (← `(tactic| simp only [foo])) false
simpLocation ctx location
Scott Morrison (Nov 27 2022 at 23:54):
The problem here is when you have to interpolate Name
s or FVarId
s that you have on hand back into that `(tactic| ...)
.
Yury G. Kudryashov (Nov 29 2022 at 16:37):
@Scott Morrison Could you please help with mathlib4#723? The missing bit is simp only [← ${eqName}] at *
after the first replaceMainGoal
if eqName ≠ `rfl
.
Yury G. Kudryashov (Nov 29 2022 at 16:38):
Also, the tactic code probably needs a thorough review.
Scott Morrison (Nov 29 2022 at 19:47):
Is there a test file? How am I meant to tell if I do it right? :-)
Scott Morrison (Nov 29 2022 at 19:47):
Here's a guess:
if eqName ≠ `rfl then
-- We want to run `simp only [← $eqName] at *`,
-- but `eqName` is just a user facing name, and we need to resolve it first.
-- This feels like we swimming against the current, but we convert it from
-- `Name` to `LocalDecl` to `FVarId` to `Expr` to `Syntax`...
let eq : Term ← (Expr.fvar (← getLocalDeclFromUserName eqName).fvarId).toSyntax
evalTactic (← `(tactic| simp only [← $eq] at *))
Scott Morrison (Nov 29 2022 at 19:48):
I'm happy to have a go at refactoring this, but some tests (whether passing or failing!) would be nice.
Last updated: Dec 20 2023 at 11:08 UTC