sin = cos timeout

Stream: general

[Kevin Buzzard]

At the cool #Is there code for X? stream which most people aren't subscribed to, Patrick found the following time-out:

import analysis.complex.exponential

open complex

set_option trace.type_context.is_def_eq true
set_option trace.type_context.is_def_eq_detail true
example (x : ℂ)  : differentiable_at ℂ sin x :=
differentiable_cos x

Note that we're trying to prove that sin is differentiable by telling Lean that cos is differentiable.

The set_option commands are just so you can see the unifier failing. The first 262144 bytes of the trace output are here at this gist. Searching for sin x' =?= cos x' shows a bunch of unfun stuff. It's a bit complex -- the numbers go up from [8] to [19] but then right near the end of the trace drop back to [9].

[Kevin Buzzard]

Johan suggested marking sin and cos irreducible, but this doesn't seem to solve the problem.

[Kevin Buzzard]

[type_context.is_def_eq_detail] [9]: sin x' + -sin x =?= cos x' + -cos ?m_1
[type_context.is_def_eq_detail] [10]: sin x' =?= cos x'
...
[type_context.is_def_eq_detail] [10]: add_semigroup.add (sin x') (-sin x) =?= add_semigroup.add (cos x') (-cos ?m_1)
[type_context.is_def_eq_detail] [11]: sin x' =?= cos x'
...
[type_context.is_def_eq_detail] [11]: add_monoid.add (sin x') (-sin x) =?= add_monoid.add (cos x') (-cos ?m_1)
[type_context.is_def_eq_detail] [12]: sin x' =?= cos x'
...
[type_context.is_def_eq_detail] [12]: add_group.add (sin x') (-sin x) =?= add_group.add (cos x') (-cos ?m_1)
[type_context.is_def_eq_detail] [13]: sin x' =?= cos x'
...
[type_context.is_def_eq_detail] [13]: add_comm_group.add (sin x') (-sin x) =?= add_comm_group.add (cos x') (-cos ?m_1)
[type_context.is_def_eq_detail] [14]: sin x' =?= cos x'
...
[type_context.is_def_eq_detail] [14]: ring.add (sin x') (-sin x) =?= ring.add (cos x') (-cos ?m_1)
[type_context.is_def_eq_detail] [15]: sin x' =?= cos x'
...
[type_context.is_def_eq_detail] [15]: field.add (sin x') (-sin x) =?= field.add (cos x') (-cos ?m_1)
[type_context.is_def_eq_detail] [16]: sin x' =?= cos x'
...
[type_context.is_def_eq_detail] [16]: field.add (sin x') (-sin x) =?= field.add (cos x') (-cos ?m_1)
[type_context.is_def_eq_detail] [17]: sin x' =?= cos x'
...
[type_context.is_def_eq_detail] [17]: comm_ring.add (sin x') (-sin x) =?= comm_ring.add (cos x') (-cos ?m_1)
[type_context.is_def_eq_detail] [18]: sin x' =?= cos x'
...

A nice little tour through the algebra heirarchy there...

[Kevin Buzzard]

With

attribute [irreducible] sin cos

beforehand, the gist is completely different.

sin =?= cos fails immediately, so it's easier to see what the actual problem is.

[Reid Barton]

I think this shows one should not try to use instance search as a theorem prover

[Kevin Buzzard]

:-)

[Reid Barton]

Maybe in Lean 4 it would be more sensible

[Reid Barton]

Is that what's going on here?

[Reid Barton]

You've given the is_def_eq trace but not the instances trace and I have to sort of guess at the latter.

[Reid Barton]

Oh maybe it isn't.

[Reid Barton]

I guess it is just the definition of has_fderiv_at that is so complicated if you fully unfold it.

[Kevin Buzzard]

Very early on, Lean asks

has_fderiv_at sin f' x =?= has_fderiv_at cos f' ?m_8

Because sin isn't cos, it then tries

[type_context.is_def_eq_detail] unfold left&right: has_fderiv_at

and asks

has_fderiv_at_filter sin f' x (nhds x) =?= has_fderiv_at_filter cos f' ?m_8 (nhds ?m_8)

Again this fails quickly because sin isn't cos. It then unfolds again and asks another question:

[type_context.is_def_eq_detail] unfold left&right: has_fderiv_at_filter
[type_context.is_def_eq_detail] [5]: asymptotics.is_o (λ (x' : ?m_1), sin x' - sin x - ⇑f' (x' - x)) (λ (x' : ?m_1), x' - x) (nhds x) =?= asymptotics.is_o (λ (x' : ℂ), cos x' - cos ?m_8 - ⇑f' (x' - ?m_8)) (λ (x' : ℂ), x' - ?m_8) (nhds ?m_8)

This is where the trouble starts, because there are two subtractions on each side. It asks

sin x' - sin x =?= cos x' - cos ?m_1

and because sub is add neg we now go through a tour of the heirarchy starting at add_semigroup.add and going up to comm_ring.add. Then it unfolds the second subtraction a bit more:

[type_context.is_def_eq_detail] [10]: add_monoid.add (sin x' - sin x) (-⇑f' (x' - x)) =?= add_monoid.add (cos x' - cos ?m_1) (-⇑f' (x' - ?m_1))

and again tries to unify sin x' - sin x with cos x' - cos x (which takes a long time to fail because it goes up the heirarchy again). This (heirarchy)^2 loop takes 2000 lines of output to fail, and then tries

[type_context.is_def_eq_detail] unfold left&right: asymptotics.is_o

giving us the exciting new problem

[type_context.is_def_eq_detail] [6]: asymptotics.is_O_with c (λ (x' : ?m_1), sin x' - sin x - ⇑f' (x' - x)) (λ (x' : ?m_1), x' - x) (nhds x) =?= asymptotics.is_O_with c (λ (x' : ℂ), cos x' - cos ?m_8 - ⇑f' (x' - ?m_8)) (λ (x' : ℂ), x' - ?m_8) (nhds ?m_8)

which again involves a double traversal of the entire heirarchy, and even though the story does not end there, the trace does because we get to 262144 characters.

[Reid Barton]

The issue seems to be that there are lots of these + and - subexpressions which could each independently be unfolded to various amounts, perhaps resulting in new + and - subexpressions (if you unfold the definitions for the complex numbers in terms of the reals for example), and the result is an exponentially large search problem

[Kevin Buzzard]

Yes as well as going up the algebra heirarchy we often consider real and imaginary parts of things. Is this some indication that more things need to be made irreducible? Should asymptotics.is_o be irreducible? Should has_fderiv_at_filter be? I have no idea.

[Kevin Buzzard]

Marking asymptotics.is_o as irreducible as well, fixes the problem (it takes a few seconds to fail, but it fails).

type mismatch, term
  differentiable_cos x
has type
  differentiable_at ℂ cos x
but is expected to have type
  differentiable_at ℂ sin x

[Rob Lewis]

I've said it before, a lot more definitions in mathlib should be marked irreducible.

[Yury G. Kudryashov]

I often write proofs applying is_o to some h : 0 < c.

[Yury G. Kudryashov]

Though we can add something like is_o.def

[Yury G. Kudryashov]

Or we can make has_deriv_at irreducible outside of the files that set up the theory.

[Johan Commelin]

attribute [irreducible] sin cos has_deriv_at

set_option trace.type_context.is_def_eq true
set_option trace.type_context.is_def_eq_detail true

example (x : ℂ) : differentiable_at ℂ sin x :=
differentiable_cos x

still takes a long time to fail

[Reid Barton]

I guess another alternative to irreducible is to make it a structure

[Yury G. Kudryashov]

I'd prefer to still have the current defeq while setting up the theory.

[Johan Commelin]

But why is it still timing out after making sin, cos, and has_deriv irreducible?

[Reid Barton]

Because differentiable_at uses has_fderiv_at which is unrelated to has_deriv