exact is unexpectedly slower than simp_all

Stream: new members

[SaNoy SaKnoi]

While minimizing this proof to reduce load times, I tried to close the goal using exact instead of simp_all. However, simp_all seems to close the goal much faster than exact (which is the same on live.lean-lang.org), which seems counterintuitive to me as exact should be a less powerful tactic. Is this intended behaviour?

import Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

noncomputable def f (x: {x | Real.cos x ≠ 0}) : ℝ := Real.tan x

-- set_option pp.all true
noncomputable def g (x: {x | Real.cos (x * Real.pi / 2) ≠ 0}) : ℝ := by
  obtain ⟨val, prop⟩ := x
  apply f
  constructor
  case val => exact val * Real.pi / 2
  dsimp at prop ⊢
  -- sorry
  simp_all
  -- exact prop

[Sebastian Ullrich]

It's not exact itself that is slow but the kernel checking afterwards. Using show_term simp_all you can see that they do produce different proof terms but it's hard to say why one is instantaneous to check and one is slow.

[Daniel Weber]

Note that this is solved by using a docs#Subtype directly instead of using a set, which I believe is also the recommended way to do this.

[Markus Schmaus]

Uncommenting the refine in the code below makes exact fast, even though it doesn't change the goal in any obvious way.

import Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

noncomputable def f (x: {x | Real.cos x ≠ 0}) : ℝ := Real.tan x

-- set_option pp.all true
noncomputable def g (x: {x | Real.cos (x * Real.pi / 2) ≠ 0}) : ℝ := by
  obtain ⟨val, prop⟩ := x
  apply f
  constructor
  case val => exact val * Real.pi / 2
  dsimp at prop ⊢
  -- refine of_eq_true (Eq.trans (congrArg Not (eq_false ?_)) not_false_eq_true)
  exact prop

[Daniel Weber]

Here's a tacticless example (tactics are generally not recommended for providing data, but that doesn't seem to be the problem here):

import Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

noncomputable def f (x: {x | Real.cos x ≠ 0}) : ℝ := Real.tan x

-- fast
noncomputable def g (x: {x | Real.cos (x * Real.pi / 2) ≠ 0}) : ℝ :=
  f ⟨x.val * Real.pi / 2, of_eq_true (Eq.trans (congrArg Not (eq_false x.prop)) not_false_eq_true)⟩

-- fast
noncomputable def g2 (x: {x // Real.cos (x * Real.pi / 2) ≠ 0}) : ℝ :=
  f ⟨x.val * Real.pi / 2, x.prop⟩

-- fast
noncomputable def g3 (x: {x | Real.cos (x * Real.pi / 2) ≠ 0}) : ℝ :=
  f ⟨x.val * Real.pi / 2, x.prop.out⟩

-- slow
noncomputable def g4 (x: {x | Real.cos (x * Real.pi / 2) ≠ 0}) : ℝ :=
  f ⟨x.val * Real.pi / 2, x.prop⟩

[Daniel Weber]

The problem seems to be that it's trying to reduce Real.cos:
This works fine

import Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

noncomputable opaque rcos (x : ℝ) : ℝ := Real.cos x

-- fast
noncomputable def g (val : ℝ) (prop : val ∈ {x | rcos (x * 1) ≠ 0}) : val * 1 ∈ {x | rcos x ≠ 0} := prop

but this is slow

import Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

noncomputable def rcos (x : ℝ) : ℝ := Real.cos x
-- slow
noncomputable def g (val : ℝ) (prop : val ∈ {x | rcos (x * 1) ≠ 0}) : val * 1 ∈ {x | rcos x ≠ 0} := prop

[SaNoy SaKnoi]

just got back to this, thank you for the explanations by everyone!

[Notification Bot]

SaNoy SaKnoi has marked this topic as resolved.

[Notification Bot]

Mario Carneiro has marked this topic as unresolved.

[Mario Carneiro]

the bug minimization still seems to be ongoing...