[Merged by Bors] - feat: Port positivity extensions for `Nat.ceil`, `Int.ceil`, `Int.floor` #7089

dwrensha · 2023-09-10T23:07:14Z

Mathlib/Algebra/Order/Floor.lean

semorrison · 2023-09-14T10:27:01Z

Mathlib/Algebra/Order/Floor.lean

+  let (.app (.app (.app (.app _ (α' : Q(Type))) _) _) a) ← whnfR e
+    | throwError "failed to match on Int.floor application"


Hard to tell what this is matching for!

And is it really meant to be constrained to Type?

Can we use a Qq match here?

Hard to tell what this is matching for!

I added some comments and included the .const head. Hopefully that makes things clearer.

And is it really meant to be constrained to Type?

Ah, good point. This should be Type u. Fixed.

Can we use a Qq match here?

Maybe! But I was unable to figure out how. Even if we do figure it out, I suspect the result will be more complicated that what I have here. (For one thing, I think it would require adding more synthInstanceQ.)

…atched on

Mathlib/Algebra/Order/Floor.lean

eric-wieser · 2023-09-14T14:54:58Z

Mathlib/Algebra/Order/Floor.lean

+  -- match on `@Int.floor α' _ _ a`
+  let (.app (.app (.app (.app (.const ``Int.floor _) (α' : Q(Type $u))) _) _) a) ← whnfR e
+    | throwError "failed to match on Int.floor application"


The Qq syntax is something like

have e : Q(ℤ) := ← whnfR e let ~q(@Int.floor $α' $inst1 $inst2 $a) := e | throwError "failed to match on Int.floor application"

thought I seem to be having trouble making the rest work

Mathlib/Algebra/Order/Floor.lean

eric-wieser · 2023-09-14T15:09:14Z

Mathlib/Algebra/Order/Floor.lean

+/-- Extension for the `positivity` tactic: `Int.floor` is nonnegative if its input is. -/
+@[positivity ⌊ _ ⌋]
+def evalFloor : PositivityExt where eval {u _α} _zα _pα e := do
+  -- match on `@Int.floor α' _ _ a`
+  let (.app (.app (.app (.app (.const ``Int.floor _) (α' : Q(Type $u))) _) _) a) ← whnfR e
+    | throwError "failed to match on Int.floor application"
+  let zα' : Q(Zero $α') ← synthInstanceQ q(Zero $α')
+  let pα' : Q(PartialOrder $α') ← synthInstanceQ q(PartialOrder $α')
+  match ← core zα' pα' a with
+  | .positive pa => pure (.nonnegative (← mkAppM ``int_floor_nonneg_of_pos #[pa]))
+  | .nonnegative pa => pure (.nonnegative (← mkAppM ``int_floor_nonneg #[pa]))
+  | _ => pure .none


Here's a full Qq version:

Suggested change

/-- Extension for the `positivity` tactic: `Int.floor` is nonnegative if its input is. -/

@[positivity ⌊ _ ⌋]

def evalFloor : PositivityExt where eval {u _α} _zα _pα e := do

-- match on `@Int.floor α' _ _ a`

let (.app (.app (.app (.app (.const ``Int.floor _) (α' : Q(Type $u))) _) _) a) ← whnfR e

| throwError "failed to match on Int.floor application"

let zα' : Q(Zero $α') ← synthInstanceQ q(Zero $α')

let pα' : Q(PartialOrder $α') ← synthInstanceQ q(PartialOrder $α')

match ← core zα' pα' a with

| .positive pa => pure (.nonnegative (← mkAppM ``int_floor_nonneg_of_pos #[pa]))

| .nonnegative pa => pure (.nonnegative (← mkAppM ``int_floor_nonneg #[pa]))

| _ => pure .none

/-- Extension for the `positivity` tactic: `Int.floor` is nonnegative if its input is. -/

@[positivity ⌊ _ ⌋]

def evalFloor : PositivityExt where eval {_u _α} _zα _pα (e : Q(ℤ)) := do

let ~q(@Int.floor $α' $i $j $a) := e | throwError "failed to match on Int.floor application"

let zα' : Q(Zero $α') ← synthInstanceQ (u := u_1.succ) _

let pα' : Q(PartialOrder $α') ← synthInstanceQ (u := u_1.succ) _

assertInstancesCommute

match ← core zα' pα' a with

| .positive pa =>

letI ret : Q(0 ≤ $e) := q(int_floor_nonneg_of_pos (α := $α') $pa)

pure (.nonnegative ret)

| .nonnegative pa =>

letI ret : Q(0 ≤ $e) := q(int_floor_nonneg (α := $α') $pa)

pure (.nonnegative ret)

| _ => pure .none

Thanks!
I actually prefer what I have, as it's shorter and easier (for me at least) to understand.

I guess that u_1 gets inserted into the context from the ~q() match? Is there a way to make that binding explicit?

Yes, the u_1 is being inserted unhygienically and I can't work out how to name it.

The advantage of my spelling is that it's much less fragile to argument changes to Int.floor.

The advantage of my spelling is that it's much less fragile to argument changes to Int.floor.

How so? It seems to me that your matching on ~q(@Int.floor $α' $i $j $a) is essentially the same as my matching on (.app (.app (.app (.app (.const ``Int.floor [u']) (α' : Q(Type $u'))) _) _) a)

Here's a shorter version, that does the instance search at compile time:

Suggested change

/-- Extension for the `positivity` tactic: `Int.floor` is nonnegative if its input is. -/

@[positivity ⌊ _ ⌋]

def evalFloor : PositivityExt where eval {u _α} _zα _pα e := do

-- match on `@Int.floor α' _ _ a`

let (.app (.app (.app (.app (.const ``Int.floor _) (α' : Q(Type $u))) _) _) a) ← whnfR e

| throwError "failed to match on Int.floor application"

let zα' : Q(Zero $α') ← synthInstanceQ q(Zero $α')

let pα' : Q(PartialOrder $α') ← synthInstanceQ q(PartialOrder $α')

match ← core zα' pα' a with

| .positive pa => pure (.nonnegative (← mkAppM ``int_floor_nonneg_of_pos #[pa]))

| .nonnegative pa => pure (.nonnegative (← mkAppM ``int_floor_nonneg #[pa]))

| _ => pure .none

/-- Extension for the `positivity` tactic: `Int.floor` is nonnegative if its input is. -/

@[positivity ⌊ _ ⌋]

def evalFloor : PositivityExt where eval {_u _α} _zα _pα (e : Q(ℤ)) := do

let ~q(@Int.floor $α' $i $j $a) := e | throwError "failed to match on Int.floor application"

match ← core q(inferInstance) q(inferInstance) a with

| .positive pa =>

letI ret : Q(0 ≤ $e) := q(int_floor_nonneg_of_pos (α := $α') $pa)

pure (.nonnegative <| ret)

| .nonnegative pa =>

letI ret : Q(0 ≤ $e) := q(int_floor_nonneg (α := $α') $pa)

pure (.nonnegative ret)

| _ => pure .none

ah, that's starting to look more reasonable. I'll try that.

How so? It seems to me that your matching on ~q(@Int.floor $α' $i $j $a) is essentially the same as my matching on (.app (.app (.app (.app (.const ``Int.floor [u']) (α' : Q(Type $u'))) _) _) a)

If the syntax changes, my code will become a Qq error at compile time. Yours will become a match failure at tactic use.

dwrensha · 2023-09-14T16:16:23Z

I have not been able to get the Nat.ceil case to fully work with Qq. Here's what I have:

/-- Extension for the `positivity` tactic: `Nat.ceil` is positive if its input is. -/
@[positivity ⌈ _ ⌉₊]
def evalNatCeil : PositivityExt where eval {_u _α} _zα _pα (e : Q(ℕ)) := do
  let ~q(@Nat.ceil $α' $i $j $a) := e | throwError "failed to match on Nat.ceil application"
  match ← core q(inferInstance) q(inferInstance) a with
  | .positive pa =>
      let _los : Q(LinearOrderedSemiring $α') ← synthInstanceQ q(LinearOrderedSemiring $α')
      letI ret : Q(0 < $e) := q(nat_ceil_pos (α := $α') $pa)
      pure (.positive ret)
  | _ => pure .none

and I get the error:

application type mismatch
  Mathlib.Meta.Positivity.nat_ceil_pos «$pa»
argument
  «$pa»
has type
  @OfNat.ofNat «$α'» 0 (@Zero.toOfNat0 «$α'» inferInstance) < «$a» : Prop
but is expected to have type
  @OfNat.ofNat «$α'» 0 (@Zero.toOfNat0 «$α'» MonoidWithZero.toZero) < ?m.346824 : Prop

dwrensha · 2023-09-14T17:09:20Z

I pushed a version that uses Qq for the matching part of Nat.ceil. I still have not figured out how to make it work for the proof construction part, but I'm not too worried about that, as the matching part is where the main concerns were in our discussion above.

eric-wieser · 2023-09-14T17:12:05Z

Mathlib/Algebra/Order/Floor.lean

+private theorem int_floor_nonneg [LinearOrderedRing α] [FloorRing α] {a : α} (ha : 0 ≤ a) :
+    0 ≤ ⌊a⌋ :=
+  Int.floor_nonneg.2 ha
+
+private theorem int_floor_nonneg_of_pos [LinearOrderedRing α] [FloorRing α] {a : α}
+    (ha : 0 < a) :
+    0 ≤ ⌊a⌋ :=
+  int_floor_nonneg ha.le


I'm curious if there's now any benefit to these; presumably you could inline them in the q()s below. Maybe there's a performance benefit with having them separated? cc @semorrison, @gebner.

I'm curious too! I kept them like this (as they were in mathlib3) for the sake of making the port as direct as possible.

Maybe the point is that in mathlib3, inlining was more painful because there was no q()?

(hm... but these are all just a single application, so constructing them without q() is not very cumbersome at all. So... I'm at a loss)

I wrote the original extensions. It was very hard to make mk_app work reliably and I resorted to never use it more than once per term construction. A typical problem is that it would eagerly try to insert the a = 0 argument when I wanted to construct a term of type a ≠ 0.

eric-wieser · 2023-09-14T17:23:22Z

I still have not figured out how to make it work for the proof construction part

I pushed a change to do this

YaelDillies

Analytic number theory really needs those extensions back.

maintainer merge

github-actions · 2023-09-25T13:58:51Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

fpvandoorn · 2023-09-26T17:20:27Z

bors merge

…or` (#7089) Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

bors · 2023-09-26T18:32:19Z

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

feat: port positivity extensions for Int.floor, Nat.ceil, and Int.ceil

5920378

dwrensha added the awaiting-review The author would like community review of the PR label Sep 10, 2023

improve error messages

f814d95

semorrison reviewed Sep 14, 2023

View reviewed changes

Mathlib/Algebra/Order/Floor.lean Outdated Show resolved Hide resolved

semorrison reviewed Sep 14, 2023

View reviewed changes

Mathlib/Algebra/Order/Floor.lean Outdated Show resolved Hide resolved

semorrison reviewed Sep 14, 2023

View reviewed changes

dwrensha added 2 commits September 14, 2023 07:32

fix style

c8e7f3a

add universe variable to matches, and make it clearer what is being m…

8bd7e4b

…atched on

eric-wieser reviewed Sep 14, 2023

View reviewed changes

Mathlib/Algebra/Order/Floor.lean Outdated Show resolved Hide resolved

fix types: Zero -> PartialOrder

0364b81

eric-wieser reviewed Sep 14, 2023

View reviewed changes

Mathlib/Algebra/Order/Floor.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Sep 14, 2023

View reviewed changes

dwrensha added 3 commits September 14, 2023 11:12

a better universe

c93b5fe

use eric-wieser's fancier Qq-based code for the Int.floor case

0e01b9a

use fancier Qq-based implementation for Int.ceil

e813eac

use Qq for the match, at least

b2d35ae

eric-wieser reviewed Sep 14, 2023

View reviewed changes

eric-wieser approved these changes Sep 14, 2023

View reviewed changes

remove mkAppM

2326f9f

Merge branch 'master' into positivity-floor

5d62133

YaelDillies approved these changes Sep 25, 2023

View reviewed changes

YaelDillies added the t-meta Tactics, attributes or user commands label Sep 25, 2023

YaelDillies changed the title ~~feat: port positivity extensions for Int.floor, Nat.ceil, and Int.ceil~~ feat: Port positivity extensions for Nat.ceil, Int.ceil, Int.floor Sep 25, 2023

github-actions bot added the ready-to-merge This PR has been sent to bors. label Sep 26, 2023

github-actions bot removed the awaiting-review The author would like community review of the PR label Sep 26, 2023

bors bot pushed a commit that referenced this pull request Sep 26, 2023

feat: Port positivity extensions for Nat.ceil, Int.ceil, `Int.flo…

26b2588

…or` (#7089) Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

bors bot changed the title ~~feat: Port positivity extensions for Nat.ceil, Int.ceil, Int.floor~~ [Merged by Bors] - feat: Port positivity extensions for Nat.ceil, Int.ceil, Int.floor Sep 26, 2023

bors bot closed this Sep 26, 2023

bors bot deleted the positivity-floor branch September 26, 2023 18:32

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: Port positivity extensions for `Nat.ceil`, `Int.ceil`, `Int.floor` #7089

[Merged by Bors] - feat: Port positivity extensions for `Nat.ceil`, `Int.ceil`, `Int.floor` #7089

dwrensha commented Sep 10, 2023

semorrison Sep 14, 2023

eric-wieser Sep 14, 2023

dwrensha Sep 14, 2023

dwrensha Sep 14, 2023 •

edited

Loading

eric-wieser Sep 14, 2023

eric-wieser Sep 14, 2023 •

edited

Loading

dwrensha Sep 14, 2023

eric-wieser Sep 14, 2023

dwrensha Sep 14, 2023

eric-wieser Sep 14, 2023 •

edited

Loading

dwrensha Sep 14, 2023

eric-wieser Sep 14, 2023 •

edited

Loading

dwrensha commented Sep 14, 2023

dwrensha commented Sep 14, 2023

eric-wieser Sep 14, 2023 •

edited

Loading

dwrensha Sep 14, 2023

dwrensha Sep 14, 2023 •

edited

Loading

YaelDillies Sep 25, 2023

eric-wieser commented Sep 14, 2023

YaelDillies left a comment

github-actions bot commented Sep 25, 2023

fpvandoorn commented Sep 26, 2023

bors bot commented Sep 26, 2023

		let (.app (.app (.app (.app _ (α' : Q(Type))) _) _) a) ← whnfR e
		\| throwError "failed to match on Int.floor application"

[Merged by Bors] - feat: Port positivity extensions for Nat.ceil, Int.ceil, Int.floor #7089

[Merged by Bors] - feat: Port positivity extensions for Nat.ceil, Int.ceil, Int.floor #7089

Conversation

dwrensha commented Sep 10, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

dwrensha Sep 14, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eric-wieser Sep 14, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eric-wieser Sep 14, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eric-wieser Sep 14, 2023 • edited Loading

Choose a reason for hiding this comment

dwrensha commented Sep 14, 2023

dwrensha commented Sep 14, 2023

eric-wieser Sep 14, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

dwrensha Sep 14, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eric-wieser commented Sep 14, 2023

YaelDillies left a comment

Choose a reason for hiding this comment

github-actions bot commented Sep 25, 2023

fpvandoorn commented Sep 26, 2023

bors bot commented Sep 26, 2023

[Merged by Bors] - feat: Port positivity extensions for `Nat.ceil`, `Int.ceil`, `Int.floor` #7089

[Merged by Bors] - feat: Port positivity extensions for `Nat.ceil`, `Int.ceil`, `Int.floor` #7089

dwrensha Sep 14, 2023 •

edited

Loading

eric-wieser Sep 14, 2023 •

edited

Loading

eric-wieser Sep 14, 2023 •

edited

Loading

eric-wieser Sep 14, 2023 •

edited

Loading

eric-wieser Sep 14, 2023 •

edited

Loading

dwrensha Sep 14, 2023 •

edited

Loading