proof of derivative related property

Stream: new members

[Guangzhi Xiong]

Hi everyone,

I defined two functions 'theta(t)' and 'phi(t)' and would like to have the following proof (some condition related to the proof of geodesic curves on 2D sphere).

import analysis.special_functions.trigonometric.basic
import analysis.calculus.deriv
import analysis.calculus.iterated_deriv

def theta (t : ℝ) : ℝ := t
def phi (t : ℝ) : ℝ := 0

theorem prop_1 : ∀ t : ℝ, iterated_deriv 2 theta t = 2 * (real.sin(phi t) / real.cos(phi t)) * deriv theta t * deriv phi t :=
begin
  sorry,
end

I'm not familiar with the proof related to derivative functions. They seem to be more complicated than functions like "sin" and "cos". Should I first prove that "deriv theta t = 1" and "deriv phi t = 0" before taking further steps? Thanks!

[Eric Wieser]

Does simp [theta, phi] make progress?

[Guangzhi Xiong]

Oh, that helps! The derivatives of functions have been automatically computed. Thank you so much!

But now the goal becomes ∀ (t : ℝ), iterated_deriv 2 theta t = 0. The 2-nd order derivative cannot be computed automatically. Is there any way to convert it to a target with only deriv instead of iterated_deriv?

[Alex J. Best]

Does rewriting docs#iterated_deriv_succ' help?

[Guangzhi Xiong]

Thanks for the suggestion. I use rw iterated_deriv_succ' twice and the target now becomes
∀ (t : ℝ), iterated_deriv 0 (deriv (deriv theta)) t = 0
It seems that if I define the theorem as

∀ t : ℝ,  deriv (deriv theta) t = 2 * (real.sin(phi t) / real.cos(phi t)) * deriv theta t * deriv phi t

the target would also be ∀ (t : ℝ), deriv (deriv theta) t = 0 after applying simp [theta, phi].

[Kevin Sullivan]

Guangzhi Xiong said:

Thanks for the suggestion. I use rw iterated_deriv_succ' twice and the target now becomes
∀ (t : ℝ), iterated_deriv 0 (deriv (deriv theta)) t = 0
It seems that if I define the theorem as

∀ t : ℝ,  deriv (deriv theta) t = 2 * (real.sin(phi t) / real.cos(phi t)) * deriv theta t * deriv phi t

the target would also be ∀ (t : ℝ), deriv (deriv theta) t = 0 after applying simp [theta, phi].

I see in the documentation for deriv that it knows how to compute the derivative of the identity function. Maybe express theta as the identity function first?

[Guangzhi Xiong]

Thanks for pointing that out! I also noticed that there are theorems called deriv_id' and deriv_id'', which look very helpful on this problem. I tried rw but it doesn't work in the current situation. Is there any other tactic that can be used to express the theta function as an identity function? Or should I try to use id when defining theta?

[Kevin Sullivan]

Guangzhi Xiong said:

Thanks for pointing that out! I also noticed that there are theorems called deriv_id' and deriv_id'', which look very helpful on this problem. I tried rw but it doesn't work in the current situation. Is there any other tactic that can be used to express the theta function as an identity function? Or should I try to use id when defining theta?

The theorem works for id, so maybe express theta as id? Maybe then the theorem will unify with your remaining goal? (Or prove that theta = id then rewrite theta to id?)

[Guangzhi Xiong]

Yes, by defining the theta function as
def theta : ℝ → ℝ := id
the theorem can be proved directly using simp. I will also try if I can prove theta=id without redefining the theta function. Many thanks to all of you for your help!

[Eric Wieser]

delta theta should unfold theta in your goal

[Kevin Sullivan]

Guangzhi Xiong said:

Yes, by defining the theta function as
def theta : ℝ → ℝ := id
the theorem can be proved directly using simp. I will also try if I can prove theta=id without redefining the theta function. Many thanks to all of you for your help!

Consider using funext, which says that to show f = g it suffices to show \all x, f x = g x.

[Eric Wieser]

theta = id is true by rfl

[Guangzhi Xiong]

Thank you all guys. I just tried delta theta, which unfolds theta to λ (t : ℝ), t). Then it would be clear enough for Lean to prove the theorem by simp.

[Eric Wieser]

The general rule here is that if you introduce your own defs, Lean will know nothing about them until you tell it otherwise

[Eric Wieser]

You need to do one of:

• Write an API (collection of basic lemmas) for them
• Make them @[reducible]
• Unfold them in your proofs using delta/rw/simp

[Guangzhi Xiong]

Oh yes, I've learned that today. Thank you so much for your advice!