fixes to simp regressions

Stream: mathlib4

[Scott Morrison]

Leo has put up lean4#2734, which proposes to fix:

• lean4#2669: simp unfolding let even with zeta := false option
• lean4#2281: simp (with beta/zeta disabled) and discrimination trees
• lean4#2682: RFC: simp should not reduce tactic-defined lets.

[Scott Morrison]

I've got this more or less working (std4#316, https://github.com/leanprover-community/aesop/pull/79) at #7847, but there are a number of broken proofs, and I'd be happy to have help with these.

[Scott Morrison]

Likely these are "expert mode" requests, as we don't just want to get the proofs working again, but to understand why the tactic behaviours have changed, and decided what we want to do.

[Scott Morrison]

Current problems are in:

• Mathlib.Topology.DenseEmbedding, where a unfold_let is not firing: @Kyle Miller or @Patrick Massot?
• Mathlib.CategoryTheory.Functor.Flat, where there is complicated porting note about simp expanding let, and separately failing to use a lemma!
• Mathlib.NumberTheory.PythagoreanTriples, where a proof by norm_cast; apply Rat.den_nz q is no longer working.

[Patrick Massot]

Thanks a lot. I'll wait to get oleans before investigating the topology issue (unless Kyle is faster).

[Patrick Massot]

I handled the topology issue. It was all good. The issue was not at all about that unfold_let. The discrepancy was created by a filter_upwards a couple of lines above. filter_upwards calls dsimp (config := {zeta := false}) but the config used to be ignored. So the proof in master was using that filter_upwards unfolded a let.

[Jireh Loreaux]

@Scott Morrison just a quick question about usage: let's say I have the following situation.

example : ∃ n, n + n = 2 := by
  let a := 1
  use a
  -- simp (config := {zeta := false}) only [a]
  -- fails with: invalid 'simp', proposition expected ℕ
  -- rw [a]
  -- fails with: tactic 'rewrite' failed, equality or iff proof expected ℕ
  unfold_let a -- works, but can't do rewriting like I want
  rfl

I know the new change should make the zeta := false unnecessary, but how are we supposed to do rewriting with a let bound variable? In Lean 3 it was just simp only [a].

[Scott Morrison]

Update coming soon. :-)

[Scott Morrison]

Can I summon some more assistance on #7847? There are quite a few things we still need to fix up here, but I think the payoff is great: we get lots of improvements to simp. (And, under the hood, much more configuration for DiscrTree.)

[Scott Morrison]

• Mathlib.LinearAlgebra.QuadraticForm.Complex has a messy proof which has gone off the rails. @Eric Wieser or @Anne Baanen?

[Scott Morrison]

• There are many failures due to a change in behaviour in norm_cast which I haven't looked at yet.
  • Mathlib.Combinatorics.SimpleGraph.Chunk
  • Mathlib.Analysis.MeanInequalities
  • Mathlib.Algebra.Order.CompleteField
  • Mathlib.NumberTheory.Padics.RingHoms
  • Mathlib.NumberTheory.PythagoreanTriples

(these should presumably be fixed not by changing the proofs!)

[Scott Morrison]

Scott Morrison said:

Update coming soon. :-)

@Jireh Loreaux @Bhavik Mehta, Leo has just pushed a change to lean4#2734 so both simp [a] and rw [a] should work. The toolchain is still coming!

[Anne Baanen]

Scott Morrison said:

• Mathlib.LinearAlgebra.QuadraticForm.Complex has a messy proof which has gone off the rails. Eric Wieser or Anne Baanen?

Sorry, not sure how to help here. I don't see any changes to that file in #7847 and there are build errors in its dependencies so I can't see what is going wrong.

[Scott Morrison]

Hi @Anne Baanen, Leo pushed another commit which further changed things, so some earlier stuff broke. I think it's now back to the point where QuadraticForm.Complex is failing again.

You may want to elan toolchain uninstall leanprover/lean4-pr-releases:pr-release-2734 to make sure you get the toolchain with Leo's latest changes.

[Anne Baanen]

Okay! I'll check it out right after lunch, in half an hour or so :)

[Anne Baanen]

Compilation (finally!) finished and indeed there seems to be a failure. One moment please...

[Anne Baanen]

Looks like the cause is essentially the following: we have a let w := if _ then _ else _ and split_ifs doesn't see through the let binding any more.

[Scott Morrison]

Okay. I propose we add a unfold_let, and -- After leanprover/lean4#2734, we need to do the zeta reduction before split_ifs

[Scott Morrison]

Hmm, maybe its not that simple. Not sure where the unfolding would have to happen.

[Scott Morrison]

Ah:

simp (config := {zeta := false}) only [one_mul, Units.val_mk0, smul_eq_mul]

does the trick?

[Scott Morrison]

(on line 57)

[Anne Baanen]

We need to do a zeta followed by beta. So my approach was to do a simp only [w] right before the split_ifs.

[Anne Baanen]

Scott Morrison said:

Ah:

simp (config := {zeta := false}) only [one_mul, Units.val_mk0, smul_eq_mul]

does the trick?

Interesting, so it's not so much that split_ifs doesn't do zeta reduction, it's that it disagrees with simp whether to do so.

[Scott Morrison]

Wooohoo! Builds.