simp unfolding let bindings

Stream: lean4

[Eric Rodriguez]

mwe:

example (a : Nat) : a + 1 - 1 = 23 := by
  let x := a + 1 - 1
  show x = _
  simp only
  sorry

I don't want Lean to unfold this let binding, and yet it is happening; I'd expect this if I did simp only [x]. Is this expected behaviour or a bug? Is there any way to work around this?

[Ruben Van de Velde]

There is a config flag, but I always forget what it's called

[Ruben Van de Velde]

Is it simp (config { zeta := false })?

[Eric Rodriguez]

having to write simp (config := ...) for every single one is pretty awful, especially as this is a "destructive" change

[Eric Rodriguez]

Usually let bindings are quite short to hide long terms, so having to write simp [my_thing] is not awful, if this is wanted behaviour

[Eric Rodriguez]

and now instead I'd have to set every single simp after initialising a let to have zeta := false?

[Ruben Van de Velde]

I didn't say I liked it :)

[Alex J. Best]

I agree that I don't much like this default, and it might be useful enough to have a mathlib tactic simp_no_zeta that shortens this

[Eric Wieser]

simp {zeta := false} would be ok IMO too

[Eric Wieser]

Or we could override the syntax of simp in mathlib to change the default

[Eric Rodriguez]

I'd be strongly in favour with overriding the default in mathlib or petitioning for it to be changed in core. Are issues still discouraged for core?

[Eric Wieser]

/poll Which default behavior of simp would you prefer in mathlib

• zeta := true (default in Lean 4), unfolds lets
• zeta := false (default in Lean 3), does not unfold lets

[Eric Wieser]

(non-binding, but to get a feel for how skewed opinion is)

[Ruben Van de Velde]

One thing to note is that lean 4 does not support let x = ...; simp [x], so it'd be good to have a short syntax for that as well

[Kyle Miller]

As of today, mathlib now has unfold_let x to do targeted zeta reduction.

[Kyle Miller]

Just so everyone knows simp (config := {zeta := false}) will preserve let expressions, so if the goal is let x := 1; x = 1 then it will remain unchanged.

[Kyle Miller]

Maybe the zeta configuration should be split into two, one that controls substitution of fvars (what the poll is about) and one that controls whether let expressions are reduced (which I presume the poll isn't about)

[Alex J. Best]

FWIW I very rarely end up with goals with lets in explicitly, but have local decls quite often. (also we wish we could could do simp {zeta := false} and not simp (config := {zeta:=False}) but currently cannot)

[Eric Rodriguez]

For those that voted for zeta being true, I'm curious as to what are your reasons, too

[Eric Rodriguez]

is it possible to at least make a quick macro so that this can be worked around for the moment? something like simpζ := simp + zeta := false

[Eric Rodriguez]

this currently makes some proofs unreadable in the tactic state...

[Bolton Bailey]

I was happy at one point to learn about set which makes it easier to control how my bindings display at various times. This discussion might be related?

[Patrick Massot]

I was discussing simp issues with Tomas over lunch and he reminded me of this thread (I voted in the poll but then forget). This allowed to write this fix which really looks like restoring sanity. Is there any progress on making that the default in Lean core? Or any explanation about why the Lean 4 behavior could be a desired default? @Sebastian Ullrich

[Patrick Massot]

And one more. simp (config := {zeta := false}) is quickly becoming my favorite tactic. It's long to type but it's really worth the trouble!

[Patrick Massot]

Lean 4 is becoming so easy it almost feels like cheating!

[Jireh Loreaux]

@Mario Carneiro and @Adam Topaz would you mind explaining why you prefer zeta := true as the default?

[Patrick Massot]

To be honest I also just pushed this commit getting rid of many unfold_let. I wrote those yesterday because let x := ... ; simp [x] didn't work so I replaced them by let x := ... ; unfold_let x; simp;. I know understand let x := ... ; simp works. But really I very much prefer to have to tell simp which definitions it should unfold since it is some much more compact and explicit. In a proving context let is used to hide complexity. Undoing this work by default seems a really wrong choice.

[James Gallicchio]

I mean, I'd probably say have hides complexity, and let just makes it more compact... other than explicit unfold_let, are the let-definitions frequently being unfolded in other parts of the proof? (maybe in defeq checks or something)

[Patrick Massot]

Sure they are also unfolded in defEq checks

[Patrick Massot]

And the difference between have and let is that one is for Prop and the other for data, so I don't understand what you mean.

[James Gallicchio]

You can have non-prop values... the difference is purely in whether the definitional equality is visible, no?

[Patrick Massot]

You can but this is never what you want to do.

[James Gallicchio]

(at least in CS-world I do use this, not frequently but not rarely...)

[Jireh Loreaux]

@James Gallicchio really? I would be interested in seeing an example. You're saying that you need to use the fact that some piece of data has a particular type without actually caring what the thing is in particular? (sorry if I sound incredulous, I'm just surprised)

[James Gallicchio]

Let me look through the archives........

[James Gallicchio]

here's an example.. The idea is I build a proof while building a value, then I want to forget the full definition and have just the generated proof as the only "fact" about the value.

[James Gallicchio]

iirc it was have instead of let specifically to prevent tactics from expanding the definition (which is unwieldy).

[James Gallicchio]

of course I could have zeta:=false'd at the callsites, but this clearly makes more sense to be thrown out at the definition site.

[Patrick Massot]

That's only supporting the idea that zeta := false should be the default.

[Patrick Massot]

And I still find this example really weird (but I can't play with it since it isn't a #mwe).

[Jireh Loreaux]

I'm also very confused about what is happening here, I think in part because your Array is not docs#Array

[James Gallicchio]

sorry, this is the first snippet grep found :big_smile: but yes, I'm not opposed to zeta:=false, I know in math-applications you frequently go between wanting to expand lets and not, whereas in CS-land I try to prove the properties I need and then close the definition permanently.

[Scott Morrison]

Perhaps someone can make a toolchain with the default changed so there is something more concrete to look at? (I think the preferred method today is to make a draft PR, and then wait an hour for the leanprover/lean4-pr-releases:pr-release-NNNN toolchain is available.)

[Patrick Massot]

Scott, I would like to try that, and I created https://github.com/PatrickMassot/lean4/tree/simp_zeta_false, but I'm reluctant to open a draft PR since it doesn't seem to comply to the contributions instructions. Do you know whether there is a way to run CI for this branch in my fork? That would be a first step.

[Matthew Ballard]

I made some notes on my experience https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/home.20cooked.20release

[Patrick Massot]

@Matthew Ballard thanks but I have no idea how to implement your list.

[Patrick Massot]

Specifically "Make sure that both the Nix-CI and CI workflows are enabled to run. The first was fine but the second was turned off by default for me. "

[Patrick Massot]

I still have no idea how to run CI in my fork but I think I built Lean locally with that change without a single error.

[Scott Morrison]

As far as I understand, none of Matthew's list is needed, except the first step.

You enable actions by visiting:
https://github.com/<username>/lean4/settings/actions

After that you just push a tag to your fork.

[Scott Morrison]

(@Patrick Massot, you should add your github username to your zulip profile, as a good example. :-)

[Patrick Massot]

Scott, the point is that I see
image.png
and that doesn't seem to be good enough.

[Matthew Ballard]

That's what I have on mine. Just nothing happens when you push a tag?

[Patrick Massot]

Oh I didn't realize I needed to push a tag to my fork! It seems to work. Sorry about taking so long.

[Matthew Ballard]

Perfectly understandable.

[Patrick Massot]

I made progress: I have https://github.com/PatrickMassot/lean4/actions saying tests are successful, but PR release failed, complaining about a missing token.

[Sebastian Ullrich]

The PR release error is confusing and should be removed, but is ultimately harmless: https://github.com/PatrickMassot/lean4/releases/tag/zeta_false2

[Matthew Ballard]

Matthew Ballard said:

• The action for releasing can require additional permission set directly in the .github/workflows/ci.yml. This seems like a known issue and can be fixed by adding

permissions:
  contents: write

after the on: node in the file

Does this fix it?

[Sebastian Ullrich]

We simply should not attempt PR releases in forks /cc @Scott Morrison

[Scott Morrison]

Yep, thank you, that is my bug! lean4#2550

[Patrick Massot]

It turns out the zeta config option isn't powerful enough to force simp to preserve let bindings. See

def f : Nat → Nat := fun x ↦ x - x

@[simp]
theorem f_zero (n : Nat) : f n = 0 := Nat.sub_self n

example (n : Nat) : False := by
  let g := f n
  have : g + n = n := by
    simp (config := {zeta := false}) [Nat.zero_add]
  sorry

which happily ignores the option and closes the goal anyway. Compare to Lean 3:

def f : nat → nat := fun x, x - x

@[simp]
lemma f_zero (n : ℕ) : f n = 0 := nat.sub_self n

example (n : nat) : false :=
begin
  let g := f n,
  have : g + n = n,
  { -- dsimp only [g],
    simp [nat.zero_add] },
  sorry
end

which does not close the goal without the dsimp line. @Heather Macbeth this is what prevents fixing the sphere instance proof, even with a patched version of field_simp.

@Sebastian Ullrich any idea how we could get back a simp that does not break through let values?

[Patrick Massot]

Of course in my example this looks like a feature, but in actual example it prevents simp from closing the goal, by sending it to a dead end.

[Eric Wieser]

I think this might happen because even if it's not unfolded, g is considered reducible?

[Eric Wieser]

simp (config := {
      contextual  := false
      memoize := false
      singlePass := true
      zeta := false
      beta := false
      eta := false
      iota := false
      proj := false
      decide := false
      arith := false
      autoUnfold := false})

also doesn't seem to help

[Tomas Skrivan]

Patrick Massot said:

any idea how we could get back a simp that does not break through let values?

I think this would require somehow ensure that this isDefEq can't see through let bindings.

When you traverse a term and there are let bindings then with zeta:=false let variables are replaced with a fresh local free variable and thus simp can't see through them anymore. Something like this needs to be done to let bindings that are in the context at the start of simp run.

I see two options:

- have an option on isDefEq not to unfold let bindings
- before running simp on an expression replace all let free variables with new fresh local free variables and after simp is done replace them back

[Tomas Skrivan]

There seems to be config setting zetaNonDep in MetaM

  /-- If zetaNonDep == false, then non dependent let-decls are not zeta expanded. -/
  zetaNonDep         : Bool := true

setting this to false might do the trick

[Kyle Miller]

That setting controls whether to zeta expand local let bindings that have nonDep set to true -- my understanding is that this value is not something you can count on unless your code is fully responsible for your local context.

[Eric Wieser]

It looks like revert g prevents simp unfolding it, which is consistent with Tomas' explanation

[Tomas Skrivan]

Kyle Miller said:

That setting controls whether to zeta expand local let bindings that have nonDep set to true -- my understanding is that this value is not something you can count on unless your code is fully responsible for your local context.

Yeah, a quick test reveals that it does not work

import Lean
import Qq

open Lean Meta Qq

#eval show MetaM Unit from do

  withLetDecl `x q(Nat) q(10) fun x => do
    let y := q(10:Nat)

    IO.println s!"with `zetaNonDep := true` is x =?= y: {← isDefEq x y}"

    let (xyEq,zetaFVars) ← withConfig (fun cfg => {cfg with zetaNonDep := false, trackZeta := true}) <| do
      pure (← isDefEq x y, ← getZetaFVarIds)

    IO.println s!"with 'zetaNonDep := false` is x =?= y: {xyEq}"

    IO.println s!"expandend let fvars {← zetaFVars.toList.mapM (fun id => ppExpr (Expr.fvar id))}"

returns

with `zetaNonDep := true` is x =?= y: true
with 'zetaNonDep := false` is x =?= y: true
expandend let fvars [x]

I hoped that it would return with 'zetaNonDep := false' is x =?= y: false

There is an option to track which fvars are zeta expanded which seems to work as expected. Not sure if it can be helpful.

[Kyle Miller]

@Tomas Skrivan You can still set nonDep := true for everything in the context

[Tomas Skrivan]

Kyle Miller said:

Tomas Skrivan You can still set nonDep := true for everything in the context

What does that do? And do you mean LocalDecl.ldecl.nonDep?

[Tomas Skrivan]

Ok, setting nonDep := true manually works, but as Kyle said it is probably not reliable

import Lean
import Qq

open Lean Meta Qq

#eval show MetaM Unit from do

  withLetDecl `x q(Nat) q(10) fun x => do

    let lctx := (← getLCtx).modifyLocalDecl x.fvarId!
      fun decl =>
        if let .ldecl i id name type val nonDep kind := decl then
          .ldecl i id name type val true kind
        else
          decl

    withLCtx lctx (← getLocalInstances) do
      let y := q(10:Nat)

      IO.println s!"with `zetaNonDep := true` is x =?= y: {← isDefEq x y}"

      let (xyEq,zetaFVars) ← withConfig (fun cfg => {cfg with zetaNonDep := false, trackZeta := true}) <| do
        pure (← isDefEq x y, ← getZetaFVarIds)

      IO.println s!"with 'zetaNonDep := false` is x =?= y: {xyEq}"

      IO.println s!"expandend let fvars {← zetaFVars.toList.mapM (fun id => ppExpr (Expr.fvar id))}"

prints

with `zetaNonDep := true` is x =?= y: true
with 'zetaNonDep := false` is x =?= y: false
expandend let fvars []

[Kyle Miller]

@Tomas Skrivan I just meant that you can't depend on it unless you were responsible for the values. Here's code that sets nonDep for all local let bindings (which I think is OK to do?), and then you get the same output as your message.

code

import Lean
import Qq

open Lean Meta Qq

def setNonDep (lctx : LocalContext) : LocalContext :=
  lctx.foldl (init := lctx) fun lctx' decl =>
    lctx'.modifyLocalDecl decl.fvarId fun decl =>
    match decl with
    | .ldecl index fvarId userName type value _nonDep kind =>
      .ldecl index fvarId userName type value true kind
    | _ => decl

#eval show MetaM Unit from do

  withLetDecl `x q(Nat) q(10) fun x => do
    let y := q(10:Nat)

    withLCtx (setNonDep (← getLCtx)) (← getLocalInstances) do

    IO.println s!"with `zetaNonDep := true` is x =?= y: {← isDefEq x y}"

    let (xyEq,zetaFVars) ← withConfig (fun cfg => {cfg with zetaNonDep := false, trackZeta := true}) <| do
      pure (← isDefEq x y, ← getZetaFVarIds)

    IO.println s!"with 'zetaNonDep := false` is x =?= y: {xyEq}"

    IO.println s!"expandend let fvars {← zetaFVars.toList.mapM (fun id => ppExpr (Expr.fvar id))}"

[Kyle Miller]

(There's also a nonDep flag in let expressions themselves, and when you intro them I believe that's what sets the nonDep flag for the ldecl. I'm not sure exactly, but isDefEq might always do zeta reduction of lets, so it doesn't matter if the let expressions could have garbage nonDep values here?)

[Tomas Skrivan]

The nonDep in let binding does not seem to affect isDefEq

    let z := Expr.letE `z q(Nat) q(10) (.bvar 0) true
    IO.println s!"with 'zetaNonDep := false` is y =?= z: {← isDefEq y z}}"

still returns true

[Kyle Miller]

Yeah, for example WHNF always zeta reduces lets

[Tomas Skrivan]

Here is demonstration that setting nonDep := true to local context can fix simp. Not sure how reliably but it might work

I had to peel bunch of layers of simp, so mysimp rather then closing the goal prints out the reduced term

code

import Lean

open Lean Elab Tactic

def f : Nat → Nat := fun x ↦ x - x

@[simp]
theorem f_zero (n : Nat) : f n = 0 := Nat.sub_self n

open Lean Parser Tactic in
syntax (name := mysimp) "mysimp" (config)? (discharger)? (&" only")?
  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*) "]")? (location)? : tactic

def setNonDep (lctx : LocalContext) : LocalContext :=
  lctx.foldl (init := lctx) fun lctx' decl =>
    lctx'.modifyLocalDecl decl.fvarId fun decl =>
    match decl with
    | .ldecl index fvarId userName type value _nonDep kind =>
      .ldecl index fvarId userName type value true kind
    | _ => decl

open Meta in
@[tactic mysimp] def mySimpTactic : Tactic := fun stx => do
  let { ctx, dischargeWrapper } ← withMainContext <| mkSimpContext stx (eraseLocal := false)

  withMainContext do
    withLCtx (setNonDep (← getLCtx)) (← getLocalInstances) do
      withConfig (fun cfg => {cfg with zetaNonDep := false, trackZeta := true}) <| do
        let mvarId ← getMainGoal
        let (r, usedSimps') ← simp (← mvarId.getType) ctx

        IO.println s!"simp reduced goal to: {← ppExpr r.expr}"


example (n : Nat) : False := by
  let g := f n
  have : g + n = n := by
    mysimp (config := {zeta := false}) [Nat.zero_add]
  sorry

with zetaNonDep := true mysimp prints out simp reduced goal to: True i.e. solves to goal
with zetaNonDep := false mysimp prints out simp reduced goal to: g + n = n i.e. leaves the goal unchanged

[Tomas Skrivan]

(How do I put the code into the collapsible box?)

[Kyle Miller]

```spoiler SomeCaption
````lean
example True := trivial
````
```

[Eric Rodriguez]

lean4#2682; I am told that :thumbs_up: on the issue mean something to the team.

[Eric Rodriguez]

Some feedback from Leo:

1. Community wants us to split the zeta flag into two new flags:

• zeta1 : Given ... x : ty := val ... |- C[x], simp reduces it to ... x : ty := val ... |- C[val]

• zeta2 : Given .... |- C[let x : ty := val; e[x]], simp reduces it to ... |- C[e[val]]

Please send suggestions to name the new flags.

2. Community wants zeta1 := false and zeta2 := true as the default setting for simp

I think this would make most people happy, yes?

[Eric Wieser]

Is there any situation in which we want zeta1 but not zeta2? If so, we could have zeta := true; zeta_ctx := true for zeta1 && zeta2, and zeta := true; zeta_ctx := false for zeta2 only.

[Scott Morrison]

@Eric Wieser, given the proposed defaults, it seems the only effect of your suggestion is making it impossible to select zeta1 := true, zeta2 := false, in the (possibly unlikely) scenario that someone wants that.

(In particular, given the proposed defaults, in the likely scenarios your proposal doesn't actually reduce the amount of configuration by the user.)

[Scott Morrison]

How about we name

• zeta2 as just zeta (i.e. so sometimes people will use zeta := false to completely turn of zeta reduction)
• zeta1 as zeta_ctx (i.e. so sometimes people will use zeta_ctx := true to additionally do zeta reduction in the context)

[Kyle Miller]

That seems reasonable to me. If someone does want to zeta reduce just local variables, there are thing like mathlib's unfold_let tactic when it's given no arguments, or core's zeta conv-mode tactic.

[Kyle Miller]

Maybe instead of zeta_ctx it could be zeta_locals?

[Eric Rodriguez]

The lean3 feature of doing simp [n] to unfold the let binding for n is back, BTW

[Kyle Miller]

Good to know, though unfold_let without arguments will unfold all local variables, so if you want the missing configuration you can do unfold_let; simp (config := {zeta := false}) ...

[Patrick Massot]

I am confused by the new behavior of simp in the presence of let bindings in the local context. It seems that config := {zeta := false} is now interpreted as: Lean shouldn't touch anything that is a let.

axiom abs : Int → Int

axiom abs_eq_self {a : Int }: abs a = a ↔ 0 ≤ a

example (x : Int) : False := by
  let y := x/2
  have h : 0 ≤ y := sorry
  have : abs y = y := by
    simp (config := {zeta := false}) only [abs_eq_self.mpr h] -- simp made no progress
  sorry

Using generalize y = z at * before the simp call make it work.

[Eric Wieser]

I assume you meant "shouldn't touch"

[Patrick Massot]

Yes, thanks Eric.

[Eric Wieser]

Isn't this what the zeta_ctx option discussed above is supposed to solve? Presumably it doesn't exist yet Nevermind, I see that this should work without unfolding

[Floris van Doorn]

The last comments on lean4#2682 are relevant. I think we'll soon get a zeta_ctx flag that does the zeta-reductions in the goals, but doesn't do the ones that are local hypotheses.

[Mario Carneiro]

There is no zeta reduction involved in this example

[Mario Carneiro]

this looks like a bug to me

[Eric Wieser]

Thanks for making the same mistake as me, Floris, to make me feel better!

[Mario Carneiro]

put another way, I would expect simp (config := {zeta := false}) to act the same as clear_value at *; simp and this isn't

[Patrick Massot]

I opened lean4#2843