Algebra.BigOperators.Finprod mathlib4#1766

Stream: mathlib4

[Lukas Miaskiwskyi]

Link to PR: mathlib4#1766

Running into strange issues right at the start of the file:

noncomputable irreducible_def finsum {M α} [AddCommMonoid M] (f : α → M) : M :=
  if h : (support (f ∘ PLift.down)).Finite then ∑ i in h.toFinset, f i.down else 0
#align finsum finsum

Throws the error failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Classical.propDecidable', and it does not have executable code. What I find the weirdest is that the error throws the red squiggles onto the docstring of the function.

Replacing irreducible_def with def and adding an @[irreducible] attribute seems to work, but irreducible_def seems to do more than the attribute, so that's probably not an ideal fix.

[Reid Barton]

irreducible_def is just a command someone wrote (I think Gabriel), it probably doesn't interact with noncomputable properly yet.

[Lukas Miaskiwskyi]

Also a notational question: The statements of many theorems in this file contain expressions like ∏ᶠ i ∈ s, f i and (∏ᶠ (i) (_h : i = a), f i) which I would like to port to lean4 notation syntax. The product in the BigOperators.Basic does not allow for such expressions currently, so I don't have that to guide me, and we probably don't want to refactor all the theorem statements at this point.

How would we like the lean4 syntax to be set up for this? For the first one, the macro_rules case

macro_rules (kind := bigfinprod)
(∏ᶠ $x:ident ∈ $s:ident, $p) => `(finprod fun $x => (finprod (α := $x ∈ $s) (fun _ => $p)))

seems to reproduce the lean3 behavior, but I don't know if that's good design.

The second one I'm trying to match with

syntax (name := bigfinprod_condition) "∏ᶠ (" extBinder ") (" extBinder "), " term:67 : term
macro_rules (kind := bigfinprod_condition)
  | `(∏ᶠ ($x:ident) ($u:ident), $p) => `(finprod fun $x => (finprod (α := $u) (fun _ => $p)))

But that throws a strange expected ')' error at (α := $u) . Could be that I do not yet fully understand the syntax here.

[Lukas Miaskiwskyi]

cc @Johan Commelin since he mentioned porting the notation to how BigOperators.Basic does it

[Eric Wieser]

You should be able to build the notation in the same way as the supᵢ notation

[Ruben Van de Velde]

I thought we shouldn't have supr anymore

[Eric Wieser]

Whoops, I removed the stray r

[Lukas Miaskiwskyi]

Thanks for the suggestion, Eric, that sent me on a painful journey of understanding the syntax. What seems to reproduce all the lean3-style notation in this file is:

syntax (name := bigfinprod) "∏ᶠ " extBinders ", " term:67 : term
macro_rules (kind := bigfinprod)
  | `(∏ᶠ $x:ident, $p) => `(finprod (fun $x:ident ↦ $p))
  | `(∏ᶠ $x:ident : $t, $p) => `(finprod (fun $x:ident : $t ↦ $p))
  | `(∏ᶠ $x:ident $b:binderPred, $p) =>
    `(finprod fun $x => (finprod (α := satisfies_binder_pred% $x $b) (fun _ => $p)))

  | `(∏ᶠ ($x:ident) ($h:ident : $t), $p) =>
      `(finprod fun ($x) => finprod (α := $t) (fun $h => $p))
  | `(∏ᶠ ($x:ident : $_) ($h:ident : $t), $p) =>
      `(finprod fun ($x) => finprod (α := $t) (fun $h => $p))

  | `(∏ᶠ ($x:ident) ($y:ident), $p) =>
      `(finprod fun $x => (finprod fun $y => $p))
  | `(∏ᶠ ($x:ident) ($y:ident) ($h:ident : $t), $p) =>
      `(finprod fun $x => (finprod fun $y => (finprod (α := $t) fun $h => $p)))

  | `(∏ᶠ ($x:ident) ($y:ident) ($z:ident), $p) =>
      `(finprod fun $x => (finprod fun $y => (finprod fun $z => $p)))
  | `(∏ᶠ ($x:ident) ($y:ident) ($z:ident) ($h:ident : $t), $p) =>
      `(finprod fun $x => (finprod fun $y => (finprod fun $z => (finprod (α := $t) fun $h => $p))))

And similar for finsum. But that's of course extremely fickle, since now the notation breaks if the user gives a typehint at an unconsidered place. And of course it would be nice to allow arbitrarily many arguments to take the product over, rather than just three. Any easy fixes?

[Eric Wieser]

What did we do here for docs4#supᵢ?

[Eric Wieser]

Why do we need anything different to what we had here?

notation3 "∏ᶠ "(...)", "r:(scoped f => finprod f) => r

[Lukas Miaskiwskyi]

In the PR, Johan mentioned that using the macro_rules approach allows you to set operator precedence properly, which I suppose notation3doesn't. But other than that, the file works fine without it. And the macro_rules approach in supᵢ does not include iterated applications. Chris & Johan agreed to fix the notation at a later time, so it is now merged anyway.

[Rob Lewis]

A question here, since I'll (hopefullly) be using finsum in class soon: right now it seems that the pretty printer doesn't use finsum/prod notation at all. For example,

import Mathlib.Algebra.BigOperators.Finprod

example : ∀ n : ℕ, (∑ᶠ k ≤ n, k) = n*(n+1)/2 := by
  -- ⊢ ∀ (n : ℕ), (finsum fun k => finsum fun h => k) = n * (n + 1) / 2

Is there any way I can coax this to display like the input, or is it impossible for now? Unfortunately I can't show students something like finsum fun k => finsum fun h => k :sad:

[Patrick Massot]

Hi Rob! It's nice to see you here. You need a unexpander for finsum.

[Patrick Massot]

I'll try to see if I can write that by imitating other examples.

[Rob Lewis]

Good to be here :smile: Every week I tell myself the chaos of the semester will die down and I'll have more time to spend here, next week...

[Rob Lewis]

Thanks! (And I can try myself if you could point me to other examples?)

[David Renshaw]

Here's one example: https://github.com/leanprover-community/mathlib4/blob/88c789ef511f8bf32a7d30ae403e29857748c079/Mathlib/Init/Set.lean#L78-L82

[David Renshaw]

Another thing that's possible is using delab: https://github.com/dwrensha/lean4-maze/blob/b7b36525dbf48989d09cd89c79703b55343af124/Maze.lean#L160

I don't have a good understanding of when Unexpander or delab is more appropriate.

[Rob Lewis]

Awesome, thanks David. Unsurprisingly a little tricker than I was hoping! I'm struggling to even parse what pattern I need to unexpand...

[Rob Lewis]

I need to give in and admit I'm stumped here -- this is about as far as I got, going off an existsi example, which isn't right.

import Mathlib.Algebra.BigOperators.Finprod

@[app_unexpander finsum] def unexpandFinsum : Lean.PrettyPrinter.Unexpander
  | `($(_) fun $_:ident ↦ finsum fun $h:ident ↦ $p) => `(∑ᶠ $h:ident, $p)
  | _                                               => throw ()

example : (∑ᶠ x ≤ 2, x)= 4 := by
  sorry

Maybe this does need a delab? Somehow we need to access the type of h? But I'm copying things without really understanding here.

[Alexander Bentkamp]

Yes, I think a delab is necessary since the unexpander can only access the information that is already present in the syntax, and the type of h is not in the syntax. Here is what I came up with so far for Finset.sum:

import Mathlib.Algebra.BigOperators.Basic

open Lean PrettyPrinter Delaborator SubExpr

namespace BigOperators

example :  ∑ i : Fin n, ((i : ℕ) + 1) = 4 := by
  sorry

@[local delab app.Finset.sum]
def delabFinsetSum : Delab := do
  guard $ (← getExpr).getAppNumArgs == 5
  guard $ ((← getExpr).getArg! 3).isAppOf' ``Finset.univ
  guard $ ((← getExpr).getArg! 4).isLambda
  withNaryArg 4 do
    let α ← withBindingDomain delab
    withBindingBodyUnusedName fun n => do
      let n : TSyntax `ident := ⟨n⟩
      let b ← delab
      `(∑ $n:ident : $α, $b)

example : ∑ i : Fin n, ((i : ℕ) + 1) = 4 := by
  sorry