zify

Stream: mathlib4

[Moritz Doll]

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]

Check SimpTheorems.addConst.

[Alex J. Best]

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]

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]

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]

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]

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]

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]

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]

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

[Moritz Doll]

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]

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]

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]

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

[Moritz Doll]

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

[Mario Carneiro]

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

[Mario Carneiro]

I don't actually know what issue you are hitting

[Moritz Doll]

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]

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]

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]

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

[Moritz Doll]

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]

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]

what is stx here?

[Moritz Doll]

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

[Mario Carneiro]

okay but what is it?

[Mario Carneiro]

this code has no entry point

[Mario Carneiro]

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

[Moritz Doll]

yes that would work as well

[Moritz Doll]

and it is probably better

[Moritz Doll]

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

[Mario Carneiro]

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]

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]

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