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 Exprs, 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 Names or FVarIds 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