Commit 2023-01-18 21:55 de661cd1
View on Github →fix: more closely match mathlib3 behavior in tauto, improving performance (#1507)
- The
iterateAtMost 3
indistribNot
currently is not acting as intended, because iterations after the first one still use the sameLocalDecl
, 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 eachdistribNot
call, to account for possible renamings. - The
casesMatching
andconstructorMatching
calls in the main loop need to haverecursive := true
in order to match the behavior of their counterparts in mathlib3. See thesome ()
argument here: https://github.com/leanprover-community/mathlib/blob/217daaf45adff6a74a82df0dab1506ed3d5e2eec/src/tactic/tauto.lean#L226. After this change, I observe tactic execution onPreoder.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.)