Commit 2023-01-18 21:55 de661cd1

fix: more closely match mathlib3 behavior in tauto, improving performance (#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:

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.)