[Merged by Bors] - fix: more closely match mathlib3 behavior in tauto, improving performance by dwrensha · Pull Request #1507 · leanprover-community/mathlib4

dwrensha · 2023-01-12T17:36:18Z

The iterateAtMost 3 in distribNot currently is not acting as intended, because iterations after the first one still use the same LocalDecl, so they have a no-longer-relevant type. This PR fixes that by maintaining a list of fvars that still need to be worked on, updating it on each distribNot call, to account for possible renamings.
The casesMatching and constructorMatching calls in the main loop need to have recursive := true in order to match the behavior of their counterparts in mathlib3. See the some () argument here: https://github.com/leanprover-community/mathlib/blob/217daaf45adff6a74a82df0dab1506ed3d5e2eec/src/tactic/tauto.lean#L226.

After this change, I observe tactic execution on Preoder.toCircularPreorder to drop from 6.8 seconds to 5.5 seconds.
Moreover, on this more difficult example, the current code on master fails (times out) while after this PR is applied, it succeeds:

example {α : Type} [Preorder α] (a b c : α) (x₀ x₁ x₂ : Prop)
 (this1 : x₀ → x₁ → a ≤ c)
 (this2 : x₁ → x₂ → b ≤ a)
 (this3 : x₂ → x₀ → c ≤ b) :
    ((x₀ ∧ ¬b ≤ a) ∧ x₁ ∧ ¬c ≤ b ∨
         (x₁ ∧ ¬c ≤ b) ∧ x₂ ∧ ¬a ≤ c ∨ (x₂ ∧ ¬a ≤ c) ∧ x₀ ∧ ¬b ≤ a ↔
       (x₀ ∧ x₁ ∨ x₁ ∧ x₂ ∨ x₂ ∧ x₀) ∧
         ¬(c ≤ b ∧ b ≤ a ∨ b ≤ a ∧ a ≤ c ∨ a ≤ c ∧ c ≤ b)) :=
by tauto

(I did not add this to tests/Tauto.lean because it takes 8.5 seconds to execute, which seems maybe too expensive for a test.)

…ance

gebner · 2023-01-12T17:51:21Z

Mathlib/Tactic/Tauto.lean

-def distribNotAt (h : LocalDecl) (g : MVarId) : MetaM MVarId := do
+def distribNotAt (fvarUserName : Name) (g : MVarId) : MetaM MVarId := g.withContext do
+  let ctx ← getLCtx
+  let h ← match LocalContext.findFromUserName? ctx fvarUserName with


Using user names is flaky (we might have two hypotheses with the same user name, after all). This function should probably return the new fvar id (which you can get from the output of replace).

If I use FVarIds, then I don't see an easy way to keep track of the remaining hypotheses to work on (the for h in ← getLCtx in distribNot). We'll run distribNotAt on the first FVarId, and then by the time we get around to the second FVarId, it might no longer be present in the local context! I suppose that I can use the information in AssertAfterResult.subst to thread that information through?

Ok, done. Now we key hypothesis by their fvar ID, and we keep track of renamings by passing around the list of what remains to do. This makes things a bit more complex, but is probably worth it for the increased robustness.

JLimperg · 2023-01-12T18:03:34Z

When I try your example on this branch, I still get a large number of timeouts at isDefEq and then a failure. Same with maxHeartbeats 1000000.

JLimperg · 2023-01-12T18:31:20Z

Never mind, after a lake clean the example works. Sorry for the noise.

The main thing I want to fix here is that `tauto` on master currently never fails *quickly*. E.g. this takes many seconds to fail: ```lean example (p : Prop) : p := by tauto ``` The reason is that the final step of `tauto` repeats until it sees a failure, and `constructorMatching` never fails, so we end up going until a timeout is hit. https://github.com/leanprover-community/mathlib4/blob/e78a2694fd2c5b00c16b4139f4a45faa17d2718d/Mathlib/Tactic/Tauto.lean#L150-L153 When I originally wrote this code, I had expected that `constructorMatching` would fail when it finds no match, similar to how the mathlib3 tactic `constructor_matching` fails when it finds no match. To fix the problem, this PR adds a `throwOnNoMatch` optional parameter to the `casesMatching` and `constructorMatching` functions, with default value set to `!recursive`. This means that the `casesm` and `constructorm` tactics will fail on no match, but the `casesm*` and `constructorm*` tactics will succeed on no match. That corresponds exactly to how the analogous tactics work in mathlib3. According to some [zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/casesm.20.2F.20constructorm.20on.20no.20match.3A.20error.20or.20not.3F), other folks agree that the mathlib3 behavior was better. This PR also explicitly sets `(throwOnNoMatch := false)` on the other calls to `constructorMatching` and `casesMatching` in `tautoCore`, because in those cases we don't want a failure. Technically, to exactly match the mathlib3 behavior there, we should be setting `(recursive := true)`, as I do in #1507, but if I do that here without the other performance fixes in that PR, then the proof of `Preorder.toCircularPreorder` gets pushed over the default `maxHeartbeats` timeout.

gebner

bors d+

gebner · 2023-01-18T19:35:16Z

Mathlib/Tactic/Tauto.lean

+  let ctx ← getLCtx
+  let h ← match LocalContext.find? ctx fvarId with
+          | some h => pure h
+          | none => throwError "fvar {fvarId.name} not found"


Suggested change

let ctx ← getLCtx

let h ← match LocalContext.find? ctx fvarId with

| some h => pure h

| none => throwError "fvar {fvarId.name} not found"

let some h ← (← getLCtx).find? ctx fvarId | throwError "fvar {fvarId.name} not found"

Or even better:

Suggested change

let ctx ← getLCtx

let h ← match LocalContext.find? ctx fvarId with

| some h => pure h

| none => throwError "fvar {fvarId.name} not found"

let h ← fvarId.getDecl

bors · 2023-01-18T19:38:10Z

✌️ dwrensha can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

dwrensha · 2023-01-18T21:55:08Z

bors r+

…ance (#1507) - The `iterateAtMost 3` in `distribNot` currently is not acting as intended, because iterations after the first one still use the same `LocalDecl`, so they have a no-longer-relevant type. This PR fixes that by maintaining a list of fvars that still need to be worked on, updating it on each `distribNot` call, to account for possible renamings. - The `casesMatching` and `constructorMatching` calls in the main loop need to have `recursive := true` in order to match the behavior of their counterparts in mathlib3. See the `some ()` argument here: https://github.com/leanprover-community/mathlib/blob/217daaf45adff6a74a82df0dab1506ed3d5e2eec/src/tactic/tauto.lean#L226. After this change, I observe tactic execution on `Preoder.toCircularPreorder` to drop from 6.8 seconds to 5.5 seconds. Moreover, on this more difficult example, the current code on master fails (times out) while after this PR is applied, it succeeds: ```lean example {α : Type} [Preorder α] (a b c : α) (x₀ x₁ x₂ : Prop) (this1 : x₀ → x₁ → a ≤ c) (this2 : x₁ → x₂ → b ≤ a) (this3 : x₂ → x₀ → c ≤ b) : ((x₀ ∧ ¬b ≤ a) ∧ x₁ ∧ ¬c ≤ b ∨ (x₁ ∧ ¬c ≤ b) ∧ x₂ ∧ ¬a ≤ c ∨ (x₂ ∧ ¬a ≤ c) ∧ x₀ ∧ ¬b ≤ a ↔ (x₀ ∧ x₁ ∨ x₁ ∧ x₂ ∨ x₂ ∧ x₀) ∧ ¬(c ≤ b ∧ b ≤ a ∨ b ≤ a ∧ a ≤ c ∨ a ≤ c ∧ c ≤ b)) := by tauto ``` (I did not add this to tests/Tauto.lean because it takes 8.5 seconds to execute, which seems maybe too expensive for a test.)

bors · 2023-01-18T22:00:33Z

Pull request successfully merged into master.

Build succeeded:

Build
Lint style

The main thing I want to fix here is that `tauto` on master currently never fails *quickly*. E.g. this takes many seconds to fail: ```lean example (p : Prop) : p := by tauto ``` The reason is that the final step of `tauto` repeats until it sees a failure, and `constructorMatching` never fails, so we end up going until a timeout is hit. https://github.com/leanprover-community/mathlib4/blob/e78a2694fd2c5b00c16b4139f4a45faa17d2718d/Mathlib/Tactic/Tauto.lean#L150-L153 When I originally wrote this code, I had expected that `constructorMatching` would fail when it finds no match, similar to how the mathlib3 tactic `constructor_matching` fails when it finds no match. To fix the problem, this PR adds a `throwOnNoMatch` optional parameter to the `casesMatching` and `constructorMatching` functions, with default value set to `!recursive`. This means that the `casesm` and `constructorm` tactics will fail on no match, but the `casesm*` and `constructorm*` tactics will succeed on no match. That corresponds exactly to how the analogous tactics work in mathlib3. According to some [zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/casesm.20.2F.20constructorm.20on.20no.20match.3A.20error.20or.20not.3F), other folks agree that the mathlib3 behavior was better. This PR also explicitly sets `(throwOnNoMatch := false)` on the other calls to `constructorMatching` and `casesMatching` in `tautoCore`, because in those cases we don't want a failure. Technically, to exactly match the mathlib3 behavior there, we should be setting `(recursive := true)`, as I do in #1507, but if I do that here without the other performance fixes in that PR, then the proof of `Preorder.toCircularPreorder` gets pushed over the default `maxHeartbeats` timeout.

…ance (#1507) - The `iterateAtMost 3` in `distribNot` currently is not acting as intended, because iterations after the first one still use the same `LocalDecl`, so they have a no-longer-relevant type. This PR fixes that by maintaining a list of fvars that still need to be worked on, updating it on each `distribNot` call, to account for possible renamings. - The `casesMatching` and `constructorMatching` calls in the main loop need to have `recursive := true` in order to match the behavior of their counterparts in mathlib3. See the `some ()` argument here: https://github.com/leanprover-community/mathlib/blob/217daaf45adff6a74a82df0dab1506ed3d5e2eec/src/tactic/tauto.lean#L226. After this change, I observe tactic execution on `Preoder.toCircularPreorder` to drop from 6.8 seconds to 5.5 seconds. Moreover, on this more difficult example, the current code on master fails (times out) while after this PR is applied, it succeeds: ```lean example {α : Type} [Preorder α] (a b c : α) (x₀ x₁ x₂ : Prop) (this1 : x₀ → x₁ → a ≤ c) (this2 : x₁ → x₂ → b ≤ a) (this3 : x₂ → x₀ → c ≤ b) : ((x₀ ∧ ¬b ≤ a) ∧ x₁ ∧ ¬c ≤ b ∨ (x₁ ∧ ¬c ≤ b) ∧ x₂ ∧ ¬a ≤ c ∨ (x₂ ∧ ¬a ≤ c) ∧ x₀ ∧ ¬b ≤ a ↔ (x₀ ∧ x₁ ∨ x₁ ∧ x₂ ∨ x₂ ∧ x₀) ∧ ¬(c ≤ b ∧ b ≤ a ∨ b ≤ a ∧ a ≤ c ∨ a ≤ c ∧ c ≤ b)) := by tauto ``` (I did not add this to tests/Tauto.lean because it takes 8.5 seconds to execute, which seems maybe too expensive for a test.)

fix: more closely match mathlib3 behavior in tauto, improving perform…

07872da

…ance

dwrensha added t-meta Tactics, attributes or user commands awaiting-review labels Jan 12, 2023

gebner reviewed Jan 12, 2023

View reviewed changes

gebner added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jan 12, 2023

dwrensha added 2 commits January 12, 2023 15:00

operate on fvarId rather than userName

564a326

use result.fvarId

5c8dc49

dwrensha added WIP Work in progress awaiting-review and removed WIP Work in progress awaiting-author A reviewer has asked the author a question or requested changes. labels Jan 12, 2023

Merge branch 'master' into debug-tauto-2

ccfd3b9

dwrensha mentioned this pull request Jan 13, 2023

[Merged by Bors] - fix: make casesm and constructorm fail if no matches are found #1552

Closed

kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 17, 2023

gebner reviewed Jan 18, 2023

View reviewed changes

dwrensha added 2 commits January 18, 2023 15:59

Merge branch 'master' into debug-tauto-2

8c06282

better way to go from FVarId to LDecl

dbdb599

kim-em removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 18, 2023

dwrensha added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jan 18, 2023

bors bot changed the title ~~fix: more closely match mathlib3 behavior in tauto, improving performance~~ [Merged by Bors] - fix: more closely match mathlib3 behavior in tauto, improving performance Jan 18, 2023

bors bot closed this Jan 18, 2023

bors bot deleted the debug-tauto-2 branch January 18, 2023 22:00

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - fix: more closely match mathlib3 behavior in tauto, improving performance#1507

[Merged by Bors] - fix: more closely match mathlib3 behavior in tauto, improving performance#1507
dwrensha wants to merge 6 commits intomasterfrom
debug-tauto-2

dwrensha commented Jan 12, 2023 •

edited

Loading

Uh oh!

gebner Jan 12, 2023

Uh oh!

dwrensha Jan 12, 2023 •

edited

Loading

Uh oh!

dwrensha Jan 12, 2023

Uh oh!

JLimperg commented Jan 12, 2023

Uh oh!

JLimperg commented Jan 12, 2023

Uh oh!

gebner left a comment

Uh oh!

gebner Jan 18, 2023

Uh oh!

gebner Jan 18, 2023

Uh oh!

bors bot commented Jan 18, 2023

Uh oh!

dwrensha commented Jan 18, 2023

Uh oh!

bors bot commented Jan 18, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

dwrensha commented Jan 12, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

gebner Jan 12, 2023

Choose a reason for hiding this comment

Uh oh!

dwrensha Jan 12, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

dwrensha Jan 12, 2023

Choose a reason for hiding this comment

Uh oh!

JLimperg commented Jan 12, 2023

Uh oh!

JLimperg commented Jan 12, 2023

Uh oh!

gebner left a comment

Choose a reason for hiding this comment

Uh oh!

gebner Jan 18, 2023

Choose a reason for hiding this comment

Uh oh!

gebner Jan 18, 2023

Choose a reason for hiding this comment

Uh oh!

bors bot commented Jan 18, 2023

Uh oh!

dwrensha commented Jan 18, 2023

Uh oh!

bors bot commented Jan 18, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

dwrensha commented Jan 12, 2023 •

edited

Loading

dwrensha Jan 12, 2023 •

edited

Loading