potential simp_procs

Stream: mathlib4

[Johan Commelin]

Inspired by #Is there code for X? > Matrix.cons_val_five I propose that we collect lemmas that should probably be simp-procified. Here is a start.

-- Mathlib/Data/Matrix/Notation.lean -- around L400-450
theorem one_fin_three : (1 : Matrix (Fin 3) (Fin 3) α) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] := by
  ext i j
--
theorem natCast_fin_three (n : ℕ) :
    (n : Matrix (Fin 3) (Fin 3) α) = !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] := by
--
theorem ofNat_fin_three (n : ℕ) [n.AtLeastTwo] :
    (ofNat(n) : Matrix (Fin 3) (Fin 3) α) =
--
theorem eta_fin_three (A : Matrix (Fin 3) (Fin 3) α) :
    A = !![A 0 0, A 0 1, A 0 2;
--
theorem mul_fin_three [AddCommMonoid α] [Mul α]
    (a₁₁ a₁₂ a₁₃ a₂₁ a₂₂ a₂₃ a₃₁ a₃₂ a₃₃ b₁₁ b₁₂ b₁₃ b₂₁ b₂₂ b₂₃ b₃₁ b₃₂ b₃₃ : α) :

[Johan Commelin]

-- Mathlib/Data/Set/Card.lean
theorem encard_eq_three {α : Type u_1} {s : Set α} :
    encard s = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z} := by
--
theorem ncard_eq_three : s.ncard = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z} := by
  rw [← encard_eq_three, ncard_def, ← Nat.cast_inj (R := ℕ∞), Nat.cast_ofNat]

[Johan Commelin]

-- Mathlib/Data/Nat/Cast/Defs.lean -- L174
theorem cast_three [AddMonoidWithOne R] : ((3 : ℕ) : R) = (3 : R) := rfl

[Johan Commelin]

-- Mathlib/NumberTheory/Divisors.lean -- L605
theorem divisorsAntidiagonal_three :
    Int.divisorsAntidiag 3 = {(1, 3), (3, 1), (-1, -3), (-3, -1)} :=

[Johan Commelin]

-- Mathlib/LinearAlgebra/Matrix/Trace.lean -- L214
theorem trace_fin_three (A : Matrix (Fin 3) (Fin 3) R) : trace A = A 0 0 + A 1 1 + A 2 2 := by

[Johan Commelin]

One simp-proc to rule them all:

-- Mathlib/Algebra/BigOperators/Fin.lean -- L114
theorem prod_univ_three [CommMonoid β] (f : Fin 3 → β) : ∏ i, f i = f 0 * f 1 * f 2 := by

[Johan Commelin]

-- Mathlib/Algebra/FreeMonoid/Basic.lean -- L145
theorem length_eq_three {v : FreeMonoid α} : v.length = 3 ↔ ∃ (a b c : α), v = of a * of b * of c :=

[Johan Commelin]

-- Mathlib/Algebra/Order/Antidiag/Nat.lean -- L246
theorem finMulAntidiag_three {n : ℕ} (a) (ha : a ∈ finMulAntidiag 3 n) : a 0 * a 1 * a 2 = n := by

[Johan Commelin]

I found these by scanning through the output of rg "theorem.*_three"

[Kevin Buzzard]

Nice trick! Now we maybe need to write a simpproc tutorial or blog post explaining how these things work. @Yaël Dillies ?

[Eric Wieser]

I made a start on those matrix simprocs back in Lean 3!

[Yaël Dillies]

I think it wouldn't be so hard to turn my metaprogramming study group session into a blogpost tutorial. It would be a lot harder to write a fully fledged explanation of what simprocs are and do

[Kevin Buzzard]

Yes I pinged you precisely because of your study group talk (we are having a metaprogramming study group at Imperial)

[Henrik Böving]

Is the issue here "how to meta program" or "I already know basics of meta programming but idk what a simproc is"? Because if you know how to play with Expr in Lean then simprocs are pretty trivial to explain.

[Kevin Buzzard]

For me it was "I know the very basics of metaprogramming but have no idea what the word "simproc" even means", before I saw Yael's talk

[Kevin Buzzard]

And what I realised after Johan's post was that searching for lemmas with three in the name might be a good way of giving some really natural examples (the first example Yael gave in the talk looked a little contrived to me but these look great)

[Yaël Dillies]

Yeah I knew about many of these potential simprocs which you mention in your first message (although it didn't occur to me to search for _three!), but I thought they all had a similar flavour, so I only mentioned one of them (and then mentioned others of a different flavour)

[Yaël Dillies]

Btw @Paul Lezeau and I are working on the Nat.divisorsAntidiag and Int.divisorsAntidiag ones in #21915

[Paul Lezeau]

I also plan on writing a simproc to compute Nat.nth Nat.Prime.

[Kevin Buzzard]

Maybe more people will write them if someone knocks off a blog post written with computer scientists in mind (ie assume some metaprogramming experience) saying "this is what a simproc is, this is the problem they solve, here are some of the ones we need"

[Kevin Buzzard]

Right now there seems to be 0 resources other than the favoured-by-computer-scientists "find an example in the source code and read it and understand it yourself"

[Paul Lezeau]

@Yaël Dillies and I would be happy to have a go at writing such a blog post:)

[Vlad Tsyrklevich]

Perhaps it should just be a section of Metaprogramming in Lean?

[Paul Lezeau]

I think having both could be useful as these would be complementary: a relatively brief blog post introducing these in the way Kevin suggested, and a more detailed explanation in the book

[Adam Topaz]

Henrik Böving said:

Is the issue here "how to meta program" or "I already know basics of meta programming but idk what a simproc is"? Because if you know how to play with Expr in Lean then simprocs are pretty trivial to explain.

@Henrik Böving . What is the trivial explanation? I haven't seriously looked into simprocs yet, but would like to understand :)

[Henrik Böving]

To give a simple example from bv_decide, say we want to detect situations where we multiply a BitVec with a BitVec constant that is a power of two and turn it into a left shift instead to get rid of the multiplication:

simproc [bv_normalize] bv_mul_twoPow ((_ : BitVec _) * (BitVec.ofNat _ _)) := fun e => do
  let_expr HMul.hMul _ _ _ _ lhs rhsExpr := e | return .continue
  let some ⟨w, rhs⟩ ← getBitVecValue? rhsExpr | return .continue
  let some pow := isTwoPow rhs | return .continue
  let expr ← mkAppM ``HShiftLeft.hShiftLeft #[lhs, toExpr pow]
  let proof := mkApp3 (mkConst ``BitVec.mul_twoPow_eq_shiftLeft) (toExpr w) lhs (toExpr pow)
  return .visit { expr := expr, proof? := some proof }

[bv_normalize] adds thsi simproc to the [bv_normalize] simpset, if you are using the default simp set you can leave that out of course, then we have the name bv_mul_twoPow followed by the pattern we want to trigger on: ((_ : BitVec _) * (BitVec.ofNat _ _)) a multiplication of some BitVec with some BitVec constant. If simp spots this pattern it is going to call the function we provide below with the expression it detected the pattern on and then we can return one of three things:

• .continue to indicate that we are not responsible for this pattern after all
• .visit or .done to say "we produced this new expression, keep working on it" (see the docstring for the precise semantics with respect to the traversal behavior of simp)

If we decide to go for the latter both visit and done take two arguments, for one the new expression we simplified to and secondly a proof that the two are equal (or none if they are defeq).

And that's it more or less^^

[Adam Topaz]

simple indeed!

[Matthew Ballard]

Now @Adam Topaz can write a bunch of simpprocs for CategoryTheory :)

[Eric Wieser]

I'll follow up with a more powerful Qq version of the above later :)

[Chris Henson]

As the target audience of having done some metaprogramming but not worked with simprocs, I think @Henrik Böving's example makes sense. Would it be mostly accurate to put it succinctly as "adding a metaprogram that transforms Exprs to a simpset"?

[Eric Wieser]

Here's the Qq version, and an example that fails with the non-qq version:

import Mathlib


theorem BitVec.twoPow_eq_ofNat {w} (i) : BitVec.twoPow w i = BitVec.ofNat w (2 ^ i) := by
  sorry

open Qq
simproc [bv_normalize] bv_mul_twoPow' ((_ : BitVec _) * (BitVec.ofNat _ _)) := .ofQ fun u α e => do
  match u, α, e with
  | 1, ~q(BitVec $w), ~q($lhs * BitVec.ofNat _ (OfNat.ofNat $rhs)) => do
    let rhs_v := rhs.natLit!
    unless 2 ^ (Nat.log 2 rhs_v) = rhs_v do return .continue
    have pow : Q(ℕ) := Lean.mkRawNatLit (Nat.log 2 rhs_v)
    let _i : OfNat.ofNat $rhs =Q 2 ^ OfNat.ofNat $pow := ⟨⟩
    return .visit <| .mk _ <|
      some q((congrArg ($lhs * ·) (BitVec.twoPow_eq_ofNat _).symm).trans <| BitVec.mul_twoPow_eq_shiftLeft $lhs $pow)
  | _, _, _ => return .continue

example {w} (x : BitVec w) : x * BitVec.ofNat w 64 = x <<< 6 := by
  simp [bv_mul_twoPow']

[Eric Wieser]

(assuming the lemma is true, of course!)

[Adam Topaz]

I guess the other (slightly more technical) question I would have about simproc development is about the additional stuff SimpM gives us over MetaM.

[Eric Wieser]

Henrik Böving said:

secondly a proof that the two are equal

One thing that always gets me is remembering which way around this proof goes: the Qq version makes it a compile error if you get this wrong :)

[Henrik Böving]

Chris Henson said:

As the target audience of having done some metaprogramming but not worked with simprocs, I think Henrik Böving's example makes sense. Would it be mostly accurate to put it succinctly as "adding a metaprogram that transforms Exprs to a simpset"?

Yes

Eric Wieser said:

Here's the Qq version, and an example that fails with the non-qq version:

import Mathlib


theorem BitVec.twoPow_eq_ofNat {w} (i) : BitVec.twoPow w i = BitVec.ofNat w (2 ^ i) := by
  sorry

open Qq
simproc [bv_normalize] bv_mul_twoPow' ((_ : BitVec _) * (BitVec.ofNat _ _)) := .ofQ fun u α e => do
  match u, α, e with
  | 1, ~q(BitVec $w), ~q($lhs * BitVec.ofNat _ (OfNat.ofNat $rhs)) => do
    let rhs_v := rhs.natLit!
    unless 2 ^ (Nat.log 2 rhs_v) = rhs_v do return .continue
    have pow : Q(ℕ) := Lean.mkRawNatLit (Nat.log 2 rhs_v)
    let _i : OfNat.ofNat $rhs =Q 2 ^ OfNat.ofNat $pow := ⟨⟩
    return .visit <| .mk _ <|
      some q((congrArg ($lhs * ·) (BitVec.twoPow_eq_ofNat _).symm).trans <| BitVec.mul_twoPow_eq_shiftLeft $lhs $pow)
  | _, _, _ => return .continue

example {w} (x : BitVec w) : x * BitVec.ofNat w 64 = x <<< 6 := by
  simp [bv_mul_twoPow']

This improvement isn't really bound to Qq though, it could be added perfectly normally with core means as well. The reason that the above simproc works like it does is because it is meant for the specific situatuon of bv_decide where the shown situation is not in scope.

Adam Topaz said:

I guess the other (slightly more technical) question I would have about simproc development is about the additional stuff SimpM gives us over MetaM.

One nice thing you can do is call simp (like, as a meta function) on subterms and work with it. A notable example for why this might be useful is docs#reduceIte. For this its a bit important to understand the way that simp applies lemmas (and simprocs): the default way is to apply them after all sub terms have already been simplified. However if you have an if then else you might want to check "hey, maybe the condition simps to true or false and I don't need to take a look at one of the match arms after all". In this case you want to mark your simproc as "pre" (that's what the downward arrow does). reduceIte then runs simp on the condition and checks if its true or false and depending on the result drops one of the arms before you waste time running simp on it.

[Henrik Böving]

Eric Wieser said:

Henrik Böving said:

secondly a proof that the two are equal

One thing that always gets me is remembering which way around this proof goes: the Qq version makes it a compile error if you get this wrong :)

Given that it goes from input to output, left to right like everything else in simp and usual rewriting theory, that's always been pretty intuitive for me.

[Eric Wieser]

I guess it's moot now that lean4#3319 is merged, which adds a clear docstring :)

[Yaël Dillies]

Lemmarocs when? docs#dist_triangle8 :melt:

[Mario Carneiro]

we usually call them "commands"

[Mario Carneiro]

you can also use macros for that kind of thing

[Yaël Dillies]

Of course, this was a joke. But the sentiment is that lemmas which are not eligible for a simproc (eg because they don't prove an equality) should not be forgotten

[Mario Carneiro]

oh, I thought the issue was with writing the lemma, not using it

[Mario Carneiro]

I don't know why that lemma you linked exists

[Eric Wieser]

It's used in docs#dist_integral_mulExpNegMulSq_comp_le

[Mario Carneiro]

it's a bit weird of a setup, it looks like a calc block but all of the work is outside the block and there is only one line

[Mario Carneiro]

I think it should just be proving those additions one at a time

[Bhavik Mehta]

Another natural one is the dual of existsAndEq, namely forallImpEq, which would eg prove this equivalence:

 (∀ a b c, p b → a = x → q c → r a b c) ↔ (∀ b c, p b → q c → r x b c)

That is, if some prop-valued pi-type contains an equality, that binder can be resolved

[Bhavik Mehta]

Yaël Dillies said:

Btw Paul Lezeau and I are working on the Nat.divisorsAntidiag and Int.divisorsAntidiag ones in #21915

you should add the Nat.divisors one I made too :)

[Eric Wieser]

Isn't that just simp +contextual?

[Eric Wieser]

I guess that only works for one direction of equality

[Bhavik Mehta]

Right, it also keeps the forall around, unlike existsAndEq which gets rid of the exists

[Paul Lezeau]

Bhavik Mehta said:

you should add the Nat.divisors one I made too :)

#23026 if anyone is interested:)

[Yaël Dillies]

Eric Wieser said:

I guess that only works for one direction of equality

and only when the ∀ a is next to the a = x. My recent best kept secrete technique is doing forall_swap (β := pattern_that_matches_a_and_nothing_else) to get the a = x binder to move leftwards until it collides with the ∀ a.

[Bhavik Mehta]

Does that commute it with implications as well? In any case, I'm glad to hear you have the same frustration I do :)

[Yaël Dillies]

Yes it does! They are non-dependent foralls after all

[Eric Wieser]

I think that such a simproc would have a discr_tree_key of _

[Mario Carneiro]

Bhavik Mehta said:

Another natural one is the dual of existsAndEq, namely forallImpEq, which would eg prove this equivalence:

 (∀ a b c, p b → a = x → q c → r a b c) ↔ (∀ b c, p b → q c → r x b c)

That is, if some prop-valued pi-type contains an equality, that binder can be resolved

Oh, I thought this went without saying. Yes, this also needs a simproc for exactly the same reasons

[Bhavik Mehta]

Oh, here's an example I expected a simproc to solve but it doesn't:

example {α β : Type} (f : β → α) {p q : β → Prop} :
    (∃ a b, p b ∧ f b = a ∧ q b) ↔ ∃ b, p b ∧ q b := by
  simp

I thought this was within the realm of existsAndEq, but maybe not. @Vasilii Nesterov, do you have ideas? Edit: Ah, I see it doesn't handle nested exists. In that case, that's another submission for this thread!

[Tristan Figueroa-Reid]

(this message was edited - it originally had the specific example from #23125) which was generalized above by Bhavik Mehta

[Bhavik Mehta]

To save people the reading, my example came from that PR

[Edward van de Meent]

should there be a simproc for reducing Nat.find or something? i'm guessing that this is likely a bad idea to be "on" by default, but having it might be useful nonetheless

[Vasilii Nesterov]

Bhavik Mehta said:

Oh, here's an example I expected a simproc to solve but it doesn't:

example {α β : Type} (f : β → α) {p q : β → Prop} :
    (∃ a b, p b ∧ f b = a ∧ q b) ↔ ∃ b, p b ∧ q b := by
  simp

I thought this was within the realm of existsAndEq, but maybe not. Vasilii Nesterov, do you have ideas? Edit: Ah, I see it doesn't handle nested exists. In that case, that's another submission for this thread!

I've finally done it: #23365. I think it was the hardest metaprogramming I've ever done :smiling_face_with_tear:

[Vasilii Nesterov]

Paul Lezeau said:

I also plan on writing a simproc to compute Nat.nth Nat.Prime.

Maybe generalize it to Nat.nth P with DecidablePred P?

[Paul Lezeau]

Vasilii Nesterov said:

Maybe generalize it to Nat.nth P with DecidablePred P?

I think both would be worth having: one general simproc for the decidable pred case, and a specialised (and faster) one for Nat.Prime!

[Paul Lezeau]

If anyone's interested, @Yaël Dillies and I have a draft version of the blog post here. This is very much work in progress, but feedback and corrections on the content would be very much appreciated :grinning:

[Bolton Bailey]

Along the lines of Damiano's work on compute_degree, it would be nice to have a simproc that could evaluate the coefficients of polynomials expressed using C and X and analogues thereof, the sort of thing that would allow this question to be solved by simp.

[Eric Wieser]

That looks like a missing simp lemma to me, no proc needed

[Bolton Bailey]

What simp lemma do you think is missing there?

[Eric Wieser]

dpcs#Polynomial.coeff_ofNat

[Bolton Bailey]

I think there may be two orthogonal issues with that question. One is the ofNat thing, but another is that docs#Polynomial.coeff_C is (rightly) not a simp lemma, but there could be a simproc that detects when the second argument is known precisely and computes the coefficient (perhaps only if the coefficient we are asking for is greater than or equal to the degree of the polynomial).

[Eric Wieser]

My potentially hot take here is that we should rename Polynomial.toFinsupp to Polynomial.coeff, and there should be a simp lemma that says (C a).coeff = AddMonoidAlgebra.of a

[Eric Wieser]

Even with the current spelling, I think we should have a lemma that says (C a).coeff = Pi.single 0 a

[Kevin Buzzard]

docs#Polynomial.coeff

[Kevin Buzzard]

I was going to say "you'll lose that it's an R-module hom" but apparently it never was!

[Kevin Buzzard]

(Pi.single a 0 I should think)

[Kim Morrison]

Paul Lezeau said:

I also plan on writing a simproc to compute Nat.nth Nat.Prime.

Could we also just replace the norm_num extension for Prime 37 with a simproc? (And generally, replace norm_num extensions where possible with simprocs.)

[Eric Wieser]

And generally, replace norm_num extensions where possible with simprocs

I think we need a proof of concept for passing metadata between simprocs for that to not be a (likely significant) performance hit

[Eric Wieser]

(the cost is paid by parsing and then reserializing the numerals at the boundary between simprocs, unlike in norm_num where an intermediate represenation is passed all the way through)

[Kim Morrison]

Really? Parsing and reserializing numerals should be super fast?

[Eric Wieser]

Each parse also involves resythesizing (division) ring structures too

[Kim Morrison]

Oh, I thought we were talking about Prime 37.

[Eric Wieser]

I was referring to your "and generally" comment

[Kim Morrison]

Got it. Let's start with the low-hanging fruit. The fact that the norm_num architecture is not extensible has been a big problem, and we need to address it eventually.

[Mario Carneiro]

you must mean something else by not extensible, norm_num is clearly an extensible tactic

[Kim Morrison]

Sorry, I agree that was unclear.

Oh, I meant that we've never grown beyond deriveNat, deriveInt, deriveRat, deriveBool.

[Mario Carneiro]

I don't see it as a problem. It is designed specifically for normalizing numerical expressions, it's right in the name. Supporting other normal forms would just turn it into simp, and would lose out on the optimizations it employs for those types. Just use simprocs if you want to norm-not-nums.

[Mario Carneiro]

simp does not support rewriting with relations that are not equalities

[Yakov Pechersky]

Kevin Buzzard said:

I was going to say "you'll lose that it's an R-module hom" but apparently it never was!

But the PowerSeries one is a hom, which means it's difficult to access coeffs over things that aren't Semiring

[Mario Carneiro]

Mario Carneiro said:

I don't see it as a problem. It is designed specifically for normalizing numerical expressions, it's right in the name. Supporting other normal forms would just turn it into simp, and would lose out on the optimizations it employs for those types. Just use simprocs if you want to norm-not-nums.

Also, another consideration: since norm_num uses simp, if you write a non-numerical normalization routine as a simproc, norm_num will still be able to use it in conjunction with the things it does for numerals. So if you have something that e.g. mixes calculating the sum of a list and normalizing the elements of the list, that would work if the list manipulation is in a simproc