feat: add left/right actions to term tree coercion elaborator and make `^` a right action #2778

kmill · 2023-10-27T23:31:00Z

Implements RFC #2854 and fixes #2220

Adds leftact% and rightact% syntax to the expression tree elaborator. These are like binop%, but instead of being for homogeneous binary operations, these are for actions, which are binary operations where one operand "acts" on the other. Left action tend to have the type α → β → β and right actions tend to have the type α → β → α.

The difference in elaboration is that leftact% notations only propagate types through the right-hand argument and rightact% notations only propagate types through the left-hand argument.
Changes the ^ notation to use rightact% because exponentiation is an action of the exponent upon the base. This is supported by the Pow class already having the type of a right action -- often there isn't a completely homogeneous exponentiation operation.
Adds NatPow and HomogeneousPow classes with default Pow instances. These are here to allow. types to subscribe to a particular defaulting behavior. Types that prefer the exponent to be a Nat can implement NatPow, and types that prefer a completely homogeneous operation can implement HomogeneousPow. For example, Float implements HomogeneousPow. The NatPow behavior is widely expected in Mathlib, and it can later be used for its Pow instance for monoids. Without HomogeneousPow, sensible expressions like (2.2 ^ 2.2 : Float) would not elaborate.

kmill · 2023-10-28T00:31:47Z

(I've based this on 4.2.0-rc4 for now to make it easier to fix mathlib. Once I've made the fixes, I'll put it back on master, since that seems like what I'm supposed to be doing.)

kmill · 2023-10-29T22:09:49Z

@leodemoura I found a way to prevent a couple of regressions. Now if x : Nat then x ^ 2 elaborates with 2 : Nat (and in ∃ k, n = 2 ^ k then k elaborates as a Nat). We also have (2 ^ 64 : Float) elaborating with 64 : Float.

The trick is to create two typeclasses that provide default instances for Pow. The first, NatPow, is for the case where a type wants the exponent to be a Nat, and the second, RPow, is for the case where the type wants Pow to be completely homogeneous. We seem to need separate typeclasses like this so that the default_instance mechanism doesn't overzealously specialize types (for example, a Pow Float Float default instance would cause #check 2 ^ 2 to yield 2 ^ 2 : Float).

Without RPow, I'd experimented with giving Float a NatPow instance, but an unfortunate regression was that x ^ 2.2 would lead to a "failed to synthesize instance OfScientific Nat" error. I felt that needing to write x ^ (2.2 : Float) would be unacceptable to anyone using Lean for numerical computations.

I chose the name RPow just for sake of having a name -- it means "reflexive pow" -- and I'm happy to change it.

Does this seem like a sensible design?

Edit: RPow is now known as HomogeneousPow. This is all described in the RFC.

PatrickMassot · 2023-10-31T13:39:09Z

Note that Mathlib uses rpow to mean "real power", so the proposed name "reflexive power" would create some confusion.

ericrbg · 2023-11-01T11:48:13Z

Will this cause similar issues with trying to find Neg Nat if we want to write (z : C) ^ (-1)?

kmill · 2023-11-01T17:17:37Z

@ericrbg Yes, unfortunately. You have to write (z : C) ^ (-1 : Int) to get that to elaborate. It seems like it's not possible with this design to be able to elaborate (z : C) ^ (-1) with an Int power while simultaneously elaborating (z : C) ^ 2 with a Nat power -- and I spent some time trying to think of how to get it to work before settling on this one. If you use the default instance mechanism to get the first to work, then the second will come out with an Int power.

ericrbg · 2023-11-01T17:29:49Z

Is it not possible to have different "priority" default instances, e.g. it can try the Nat one first and then if that fails the Int one?

kmill · 2023-11-01T17:46:20Z

@ericrbg Yes, but no.

class F (α : Type) where
  f : α → Bool

@[default_instance high]
instance : F Nat where
  f _ := true

@[default_instance low]
instance : F Int where
  f _ := false

#eval F.f 2
-- true
#eval F.f (-2)
/-
failed to synthesize instance
  Neg Nat
-/
#eval F.f (-2 : Int)
-- false

kim-em · 2023-11-05T23:48:15Z

@kmill, when you want to do Mathlib testing, could you:

rebase this PR onto origin/nightly-testing
make the Mathlib fixes on the lean-pr-testing-2778 branch of Mathlib?

leanprover-community-mathlib4-bot · 2023-11-09T03:48:57Z

💥 Mathlib branch lean-pr-testing-2778 build failed against this PR. (2023-11-09 03:48:56) View Log
❌ Mathlib branch lean-pr-testing-2778 built against this PR, but testing failed. (2023-11-09 06:27:31) View Log
🟡 Mathlib branch lean-pr-testing-2778 build this PR didn't complete normally. (2023-11-09 12:31:50) View Log
❌ Mathlib branch lean-pr-testing-2778 built against this PR, but testing failed. (2023-11-09 13:25:10) View Log
❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-11-09 22:02:20)
💥 Mathlib branch lean-pr-testing-2778 build failed against this PR. (2023-11-09 22:55:06) View Log
✅ Mathlib branch lean-pr-testing-2778 has successfully built against this PR. (2023-11-10 00:14:47) View Log
❌ Mathlib branch lean-pr-testing-2778 built against this PR, but testing failed. (2023-11-10 00:27:09) View Log
✅ Mathlib branch lean-pr-testing-2778 has successfully built against this PR. (2023-11-11 06:54:28) View Log

src/Init/Prelude.lean

kim-em · 2023-11-12T04:31:03Z

src/Lean/Elab/Extra.lean

-  we still want to be able to write `(5 > 2) == (2 > 1)`.
+  - `binrel% R x y` elaborates `R x y` using the `binop%/...` expression trees in both `x` and `y`.
+    It is similar to how `binop% R x y` elaborates but with a significant difference:
+    it does not use the expected type when computing the types of the operads.


Suggested change

it does not use the expected type when computing the types of the operads.

it does not use the expected type when computing the types of the operands.

# PR contents This is the supremum of - #8284 - #8056 - #8023 - #8332 - #8226 (already approved) - #7834 (already approved) along with some minor fixes from failures on nightly-testing as Mathlib `master` is merged into it. Note that some PRs for changes that are already compatible with the current toolchain and will be necessary have already been split out: #8380. I am hopeful that in future we will be able to progressively merge adaptation PRs into a `bump/v4.X.0` branch, so we never end up with a "big merge" like this. However one of these adaptation PRs (#8056) predates my new scheme for combined CI, and it wasn't possible to keep that PR viable in the meantime. # Lean PRs involved in this bump In particular this includes adjustments for the Lean PRs * leanprover/lean4#2778 * leanprover/lean4#2790 * leanprover/lean4#2783 * leanprover/lean4#2825 * leanprover/lean4#2722 ## leanprover/lean4#2778 We can get rid of all the ``` local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 ``` macros across Mathlib (and in any projects that want to write natural number powers of reals). ## leanprover/lean4#2722 Changes the default behaviour of `simp` to `(config := {decide := false})`. This makes `simp` (and consequentially `norm_num`) less powerful, but also more consistent, and less likely to blow up in long failures. This requires a variety of changes: changing some previously by `simp` or `norm_num` to `decide` or `rfl`, or adding `(config := {decide := true})`. ## leanprover/lean4#2783 This changed the behaviour of `simp` so that `simp [f]` will only unfold "fully applied" occurrences of `f`. The old behaviour can be recovered with `simp (config := { unfoldPartialApp := true })`. We may in future add a syntax for this, e.g. `simp [!f]`; please provide feedback! In the meantime, we have made the following changes: * switching to using explicit lemmas that have the intended level of application * `(config := { unfoldPartialApp := true })` in some places, to recover the old behaviour * Using `@[eqns]` to manually adjust the equation lemmas for a particular definition, recovering the old behaviour just for that definition. See #8371, where we do this for `Function.comp` and `Function.flip`. This change in Lean may require further changes down the line (e.g. adding the `!f` syntax, and/or upstreaming the special treatment for `Function.comp` and `Function.flip`, and/or removing this special treatment). Please keep an open and skeptical mind about these changes! Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Mauricio Collares <[email protected]>

This is the supremum of - #8284 - #8056 - #8023 - #8332 - #8226 (already approved) - #7834 (already approved) along with some minor fixes from failures on nightly-testing as Mathlib `master` is merged into it. Note that some PRs for changes that are already compatible with the current toolchain and will be necessary have already been split out: #8380. I am hopeful that in future we will be able to progressively merge adaptation PRs into a `bump/v4.X.0` branch, so we never end up with a "big merge" like this. However one of these adaptation PRs (#8056) predates my new scheme for combined CI, and it wasn't possible to keep that PR viable in the meantime. In particular this includes adjustments for the Lean PRs * leanprover/lean4#2778 * leanprover/lean4#2790 * leanprover/lean4#2783 * leanprover/lean4#2825 * leanprover/lean4#2722 We can get rid of all the ``` local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 ``` macros across Mathlib (and in any projects that want to write natural number powers of reals). Changes the default behaviour of `simp` to `(config := {decide := false})`. This makes `simp` (and consequentially `norm_num`) less powerful, but also more consistent, and less likely to blow up in long failures. This requires a variety of changes: changing some previously by `simp` or `norm_num` to `decide` or `rfl`, or adding `(config := {decide := true})`. This changed the behaviour of `simp` so that `simp [f]` will only unfold "fully applied" occurrences of `f`. The old behaviour can be recovered with `simp (config := { unfoldPartialApp := true })`. We may in future add a syntax for this, e.g. `simp [!f]`; please provide feedback! In the meantime, we have made the following changes: * switching to using explicit lemmas that have the intended level of application * `(config := { unfoldPartialApp := true })` in some places, to recover the old behaviour * Using `@[eqns]` to manually adjust the equation lemmas for a particular definition, recovering the old behaviour just for that definition. See #8371, where we do this for `Function.comp` and `Function.flip`. This change in Lean may require further changes down the line (e.g. adding the `!f` syntax, and/or upstreaming the special treatment for `Function.comp` and `Function.flip`, and/or removing this special treatment). Please keep an open and skeptical mind about these changes! Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Mauricio Collares <[email protected]>

# PR contents This is the supremum of - #8284 - #8056 - #8023 - #8332 - #8226 (already approved) - #7834 (already approved) along with some minor fixes from failures on nightly-testing as Mathlib `master` is merged into it. Note that some PRs for changes that are already compatible with the current toolchain and will be necessary have already been split out: #8380. I am hopeful that in future we will be able to progressively merge adaptation PRs into a `bump/v4.X.0` branch, so we never end up with a "big merge" like this. However one of these adaptation PRs (#8056) predates my new scheme for combined CI, and it wasn't possible to keep that PR viable in the meantime. # Lean PRs involved in this bump In particular this includes adjustments for the Lean PRs * leanprover/lean4#2778 * leanprover/lean4#2790 * leanprover/lean4#2783 * leanprover/lean4#2825 * leanprover/lean4#2722 ## leanprover/lean4#2778 We can get rid of all the ``` local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220 ``` macros across Mathlib (and in any projects that want to write natural number powers of reals). ## leanprover/lean4#2722 Changes the default behaviour of `simp` to `(config := {decide := false})`. This makes `simp` (and consequentially `norm_num`) less powerful, but also more consistent, and less likely to blow up in long failures. This requires a variety of changes: changing some previously by `simp` or `norm_num` to `decide` or `rfl`, or adding `(config := {decide := true})`. ## leanprover/lean4#2783 This changed the behaviour of `simp` so that `simp [f]` will only unfold "fully applied" occurrences of `f`. The old behaviour can be recovered with `simp (config := { unfoldPartialApp := true })`. We may in future add a syntax for this, e.g. `simp [!f]`; please provide feedback! In the meantime, we have made the following changes: * switching to using explicit lemmas that have the intended level of application * `(config := { unfoldPartialApp := true })` in some places, to recover the old behaviour * Using `@[eqns]` to manually adjust the equation lemmas for a particular definition, recovering the old behaviour just for that definition. See #8371, where we do this for `Function.comp` and `Function.flip`. This change in Lean may require further changes down the line (e.g. adding the `!f` syntax, and/or upstreaming the special treatment for `Function.comp` and `Function.flip`, and/or removing this special treatment). Please keep an open and skeptical mind about these changes! Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Mauricio Collares <[email protected]>

kmill mentioned this pull request Oct 27, 2023

Add left/right actions to term tree coercion and make ^ a right action #2667

Closed

kmill force-pushed the pow-rightact branch from 97e163d to 5c8f5de Compare October 28, 2023 00:21

kmill force-pushed the pow-rightact branch from a1f0216 to 6a0746f Compare October 29, 2023 21:07

kmill changed the title ~~Add left/right actions to term tree coercion and make ^ a right action~~ feat: add left/right actions to term tree coercion elaborator and make ^ a right action Oct 29, 2023

Kha and others added 4 commits November 8, 2023 17:37

feat: add leftact%/rightact% syntax

01ea305

chore: update stage0

cb0340e

feat: leftact%/rightact% binop variants

a999a44

chore: update stage0

4b3f3c8

kmill force-pushed the pow-rightact branch from 6a0746f to 41d5fd4 Compare November 9, 2023 02:01

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Nov 9, 2023

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 9, 2023

Update lean-toolchain for testing leanprover/lean4#2778

5519030

leanprover-community-mathlib4-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Nov 9, 2023

kim-em mentioned this pull request Nov 9, 2023

chore: adaptations for leanprover/lean4#2778 leanprover-community/mathlib4#8284

Closed

Kha added 2 commits November 9, 2023 12:37

fix: make ^ a right action, add NatPow and HomogeneousPow

1e0b5b5

fix: look through binop% variants in elabCDotFunctionAlias?

1771118

kmill force-pushed the pow-rightact branch from 41d5fd4 to 1771118 Compare November 9, 2023 20:58

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 9, 2023

Trigger CI for leanprover/lean4#2778

0891f3b

leanprover-community-mathlib4-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Nov 10, 2023

kmill added the awaiting-review Waiting for someone to review the PR label Nov 10, 2023

kim-em reviewed Nov 12, 2023

View reviewed changes

src/Init/Prelude.lean Show resolved Hide resolved

kim-em reviewed Nov 12, 2023

View reviewed changes

kim-em merged commit 8cfcf7c into leanprover:master Nov 12, 2023
17 checks passed

kim-em mentioned this pull request Nov 14, 2023

[Merged by Bors] - chore: bump to v4.3.0-rc2 leanprover-community/mathlib4#8366

Closed

This was referenced Jan 4, 2024

chore: fix nightly testing to work with 2024-01-03 leanprover-community/mathlib4#9438

Merged

[Merged by Bors] - chore: CI: improve comment created on lean PRs leanprover-community/mathlib4#9585

Closed

alexkireeff mentioned this pull request Jul 8, 2024

Pow type coercion broken #4696

Open

3 tasks

kmill mentioned this pull request Aug 4, 2024

perf: use NatPow Int instead of HPow Int Nat Int #4903

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: add left/right actions to term tree coercion elaborator and make `^` a right action #2778

feat: add left/right actions to term tree coercion elaborator and make `^` a right action #2778

kmill commented Oct 27, 2023 •

edited

Loading

kmill commented Oct 28, 2023

kmill commented Oct 29, 2023 •

edited

Loading

PatrickMassot commented Oct 31, 2023

ericrbg commented Nov 1, 2023

kmill commented Nov 1, 2023

ericrbg commented Nov 1, 2023

kmill commented Nov 1, 2023 •

edited

Loading

kim-em commented Nov 5, 2023

leanprover-community-mathlib4-bot commented Nov 9, 2023 •

edited

Loading

kim-em Nov 12, 2023

	it does not use the expected type when computing the types of the operads.
	it does not use the expected type when computing the types of the operands.

feat: add left/right actions to term tree coercion elaborator and make ^ a right action #2778

feat: add left/right actions to term tree coercion elaborator and make ^ a right action #2778

Conversation

kmill commented Oct 27, 2023 • edited Loading

kmill commented Oct 28, 2023

kmill commented Oct 29, 2023 • edited Loading

PatrickMassot commented Oct 31, 2023

ericrbg commented Nov 1, 2023

kmill commented Nov 1, 2023

ericrbg commented Nov 1, 2023

kmill commented Nov 1, 2023 • edited Loading

kim-em commented Nov 5, 2023

leanprover-community-mathlib4-bot commented Nov 9, 2023 • edited Loading

kim-em Nov 12, 2023

Choose a reason for hiding this comment

feat: add left/right actions to term tree coercion elaborator and make `^` a right action #2778

feat: add left/right actions to term tree coercion elaborator and make `^` a right action #2778

kmill commented Oct 27, 2023 •

edited

Loading

kmill commented Oct 29, 2023 •

edited

Loading

kmill commented Nov 1, 2023 •

edited

Loading

leanprover-community-mathlib4-bot commented Nov 9, 2023 •

edited

Loading