Zulip Chat Archive

Stream: mathlib4

Topic: zify


Moritz Doll (Oct 04 2022 at 16:32):

How do I create a SimpTheorem from some declaration? My goal is to create a custom list of simp-lemmas for the lift_to_z step in zify. I did not find a definition in Mathlib4 that constructs the whole Simp.Context, but I found most of the ingredients to do that

Jannis Limperg (Oct 04 2022 at 16:38):

Check SimpTheorems.addConst.

Alex J. Best (Oct 04 2022 at 18:08):

BTW if you are working on zify, the analogous qify just got added to mathlib 3 today (see #rss). Might be worth considering if the internals can be merged somehow for mathlib4 or at least just writing qify when zify is done!

Moritz Doll (Oct 04 2022 at 18:20):

Yeah, I saw that. I'll first have to figure out how to do zify with just one lemma and then I would try to see whether it is possible to factor out the general stuff in a way that both zify and qify are very simple (and that it becomes trivial to write extensions for the reals and the complex numbers).

Moritz Doll (Oct 04 2022 at 18:22):

at the moment I am mainly trying to figure out how simp is working, which seems to be way more complicated than I've expected it to be

Moritz Doll (Oct 08 2022 at 08:23):

I've tried to imitate what zify is doing in Lean 3, but I don't understand how SimpTheorem and SimpTheorems work. It seemed to me that there are several places where you could put a lemma in: SimpTheorems seems to be a list (tree) of SimpTheorems with some additional stuff (pre and post) that I don't understand, but the simplifyer takes an array of SimpTheorems..
Is there a function that I can call for creating a SimpContext that behaves as a simp only? This sounds rather useful, but I could not find it.
I also wondered whether zify could be largely implemented in a macro (one needs a function to create the list of simp only lemmas, but apart from that the macro system might be able to do everything zify needs.
Finally, how do you debug meta code? I came up with the bad code below, it does not work and I have no idea how to find out what I am doing wrong.

import Mathlib.Tactic.Basic
import Mathlib.Tactic.NormCast
import Mathlib.Tactic.ZifyAttr

namespace Mathlib.Tactic

open Lean
open Lean.Meta
open Lean.Elab
open Lean.Elab.Command
open Lean.Elab.Tactic
open Lean.Parser.Tactic
open Std


syntax (name := zify') "zify'" : tactic

open Lean in
def hasZifyAttr (declName : Name) : CoreM Bool :=
  return zifyAttr.hasTag ( getEnv) declName

open Lean in
def getZifyAttr : CoreM (List Name) :=
  return (zifyAttr.ext.getState ( getEnv)).toList

@[zify] lemma eq_iff_coe (a b : ) : (a : ) = (b : )  a = b := sorry

def liftToZ : TacticM Unit := do
    let s : SimpTheorems := default
    let zifyList  getZifyAttr
    let s  s.addConst zifyList[0]!
    let simpThmsArray : SimpTheoremsArray := Array.mkEmpty 1
    let simpCtx : Simp.Context := {simpTheorems := simpThmsArray.push s}
    match ( simpAll ( getMainGoal) simpCtx) with
    | none => replaceMainGoal []
    | some mvarId => replaceMainGoal [mvarId]

@[tactic zify'] def evalZify' : Tactic := fun
  | `(tactic| zify') =>
  withMainContext do
    liftToZ
  | _ => throwUnsupportedSyntax

variable (a b : )

example (a b : ) : a = b := by
  zify'
  simp

and the contents of ZifyAttr.lean are

import Lean

open Lean

initialize zifyAttr : TagAttribute  registerTagAttribute `zify "simple user defined attribute"

Mario Carneiro (Oct 08 2022 at 08:32):

Is there a function that I can call for creating a SimpContext that behaves as a simp only? This sounds rather useful, but I could not find it.

Yes, see the mkSimpContext function. Depending on what you are doing you may either want to call that function directly or do something similar to its implementation

Moritz Doll (Oct 08 2022 at 09:46):

this is almost what I am looking for, but I was searching for a version without the elaboration parts. I don't think it is the correct way to write the syntax and then elaborate it. To me it seems there has to be version of mkSimpContext, which takes an inductive datatype that carries all the information that is in the syntax variable (minus the config) and the SimpContext created by elabSimpArgs.

Moritz Doll (Oct 08 2022 at 09:48):

I am probably overcomplicating things, because I don't understand the logic behind the code, but my feeling is that mkSimpContext should not mix up the elaboration with the creation of the SimpContext

Jireh Loreaux (Oct 08 2022 at 15:07):

Moritz, I think the code for PushNeg should be a relatively simple example of the kind of thing you want to do.

Moritz Doll (Oct 23 2022 at 10:33):

I finally have time again to work on this and I actually managed to get my initial attempt to work, but now I am stuck with the push_cast step.
In Lean 3 this works fine:

example (a b : ) : (((a + 1) : ) : ) = a + 1 :=
begin
  push_cast,
end

whereas the analogue in Lean 4 does not:

example (a b : ) : (((a + 1) : ) : ) = a + 1 := by
  push_cast

This is probably just a matter of the corresponding lemma not existing yet in mathlib4 with the norm_cast attribute, but this really hinders me in testing the tactic. Should I PR the tactic for now as it is and we add the more serious tests once the corresponding lemmas are available or should I just sit on it for now? I don't really have the time to get into the porting business.

Mario Carneiro (Oct 23 2022 at 10:41):

it seems to work fine for me, although you have to use rfl at the end if you want it to actually close the goal

Moritz Doll (Oct 23 2022 at 10:47):

ah this also works:

example (a b : ) (h : (a : ) + 1 = b): a + 1 = b := by
  zify'
  assumption

(and my zify' does not have the push_cast step in yet)

Moritz Doll (Oct 23 2022 at 10:48):

this seems to be a difference between mathlib3 and 3 for some automatic coercions with + 1

Moritz Doll (Oct 23 2022 at 10:51):

maybe my example was really bad since refl/rfl closes the goal anyways

Mario Carneiro (Oct 23 2022 at 11:32):

well, with_reducible rfl fails before and succeeds after so clearly it did something

Mario Carneiro (Oct 23 2022 at 11:32):

I don't actually know what issue you are hitting

Moritz Doll (Oct 28 2022 at 06:00):

I've looked up what Rob wrote for the differences between simp only zify push_cast and zify:

`zify` is very nearly just `simp only with zify push_cast`. There are a few minor differences:
* `zify` lemmas are used in the opposite order of the standard simp form.
  E.g. we will rewrite with `int.coe_nat_le_coe_nat_iff` from right to left.
* `zify` should fail if no `zify` lemma applies (i.e. it was unable to shift any proposition to ).
  However, once this succeeds, it does not necessarily need to rewrite with any `push_cast` rules.

(from https://github.com/leanprover-community/mathlib/blob/master/src/tactic/zify.lean )

As discussed yesterday night, the first point is a complete non-issue (actually the lemmas are in the correct form in mathlib4). For the second point I think this is not too important and if it is at all addressed then maybe as an extension to simp, i.e., introduce a modifier to a simp_attribute such that simp fails if no lemma corresponding to that attribute gets applied; something along the lines of simp only zify! push_cast fail if no zify-tagged lemmas gets applied, but does not care whether push_cast-lemmas get used.

For now are there any objections to PR zify as a macro for simp only zify push_cast?

Moritz Doll (Oct 28 2022 at 08:38):

Ok, I've run into another problem: the additional simpArgs and I have no idea how to combine them with [zifyArgs, push_cast] in a macro.
This does obviously not work

import Mathlib.Tactic.Basic
import Mathlib.Tactic.NormCast
import Mathlib.Tactic.ZifyAttr

namespace Mathlib.Tactic

open Lean
open Lean.Parser.Tactic

/-- tbw-/

syntax (name := zify) "zify" (simpArgs)? (ppSpace location)? : tactic

macro_rules
| `(tactic| zify $[at $location]?) =>
  `(tactic| simp only [zifyAttr, push_cast] $[at $location]?)
| `(tactic| zify $simpArgs $[at $location]?) =>
  `(tactic| simp only [zifyAttr, push_cast].append $simpArgs $[at $location]?)

Moritz Doll (Oct 28 2022 at 08:40):

I've looked into mathlib and this feature is never used (zify itself is not used that often), so there is also the question whether to port it at all

Mario Carneiro (Oct 28 2022 at 09:04):

macro_rules
| `(tactic| zify $[[$simpArgs,*]]? $[at $location]?) =>
  let args := simpArgs.map (·.getElems) |>.getD #[]
  `(tactic| simp only [zifyAttr, push_cast, $args,*] $[at $location]?)

Moritz Doll (Nov 17 2022 at 04:20):

As per request by Scott, I have had a look at plumbing zify to linarith. My plan is to create a custom Simp.Context and then use simpLocation to do the simplifying and later worry about how that gets put into linarith's GlobalPreprocessor. If this is the wrong approach for any reasons please let me know.
I have started with the Simp.Context and this is what I came up with. I want to get rid of the syntax altogether, but I have no idea how to put "[zify_simps, push_cast]" there instead. I vague remember that there was a cheatsheet for that, but I could not find it.

import Mathlib.Tactic.Zify


namespace Mathlib.Tactic.Zify

open Lean
open Lean.Meta
open Lean.Parser.Tactic
open Lean.Elab.Tactic
open Lean.Elab.Tactic.Simp

def mkZifyContext (stx : Syntax) : TacticM Simp.Context := do
  let simpTheorems  simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems)
  let congrTheorems  getSimpCongrTheorems
  let r  elabSimpArgs stx[4] (eraseLocal := false) (kind := SimpKind.simp) {
    config      := {}--(← elabSimpConfigCore stx[1])
    simpTheorems := #[simpTheorems], congrTheorems
  }
  let ctx := r.ctx
  let mut simpTheorems := ctx.simpTheorems
  let hs  getPropHyps
  for h in hs do
    unless simpTheorems.isErased (.fvar h) do
      simpTheorems  simpTheorems.addTheorem (.fvar h) ( h.getDecl).toExpr
  let ctx := { ctx with simpTheorems }
  return ctx

Moritz Doll (Nov 17 2022 at 04:22):

and in the unlikely case that this is the correct approach, should I factor out the later part of that function to not duplicate code from mkSimpContext?

Mario Carneiro (Nov 17 2022 at 04:28):

what is stx here?

Moritz Doll (Nov 17 2022 at 04:28):

it came from mkSimpContext, but this is the part I want to get rid of

Mario Carneiro (Nov 17 2022 at 04:28):

okay but what is it?

Mario Carneiro (Nov 17 2022 at 04:29):

this code has no entry point

Mario Carneiro (Nov 17 2022 at 04:30):

I'm not clear on why you can't just call mkSimpContext with the simp syntax from before

Moritz Doll (Nov 17 2022 at 04:31):

yes that would work as well

Moritz Doll (Nov 17 2022 at 04:32):

and it is probably better

Moritz Doll (Nov 17 2022 at 04:32):

but then I still have the same question on how to get the syntax

Mario Carneiro (Nov 17 2022 at 04:59):

Mario Carneiro said:

macro_rules
| `(tactic| zify $[[$simpArgs,*]]? $[at $location]?) =>
  let args := simpArgs.map (·.getElems) |>.getD #[]
  `(tactic| simp only [zifyAttr, push_cast, $args,*] $[at $location]?)

?

Moritz Doll (Nov 17 2022 at 05:08):

I only want to get the Simp.Context not the full tactic. If it is possible to somehow use the tactic directly in linarith I would be happy, but I don't know that could work

Mario Carneiro (Nov 17 2022 at 05:08):

If you call mkSimpContext with <- `(tactic| simp only [zifyAttr, push_cast, $args,*] $[at $location]?) as argument, simp will not be run


Last updated: Dec 20 2023 at 11:08 UTC