Dsimp and deriv

Stream: mathlib4

[Daniel Rehsmann]

I have following code:

def U (P1 P2 q : ℝ → ℝ) (r : ℝ) : ℝ := deriv q r * P1 r - (1 - q r) * deriv P1 r
lemma U_deriv_pos (h : Assumptions P1 P2 q): ∀ r > 0, 0 < deriv (U P1 P2 q) r := by
  unfold

which gives following goal state:

⊢ 0 < deriv (fun r ↦ deriv q r * P1 r - (1 - q r) * deriv P1 r) r

How can I remove the lambda definition here, i.e., changing the goal state to:

⊢ 0 < deriv (deriv q r * P1 r - (1 - q r) * deriv P1 r) r

1.) dsimp makes no progress
2.)change 0 < deriv (deriv q * P1 - (1 - q) * deriv P1) r works, but seems to be a very unhandy way of solving such issues.

Do you have any ideas to do this more economically?

[Ilmārs Cīrulis]

In the definition of U variable P2 is unused.

[Etienne Marion]

Can you provide a #mwe please?

[Ilmārs Cīrulis]

Do you mean def U (P1 P2 q : ℝ → ℝ) (r : ℝ) : ℝ := deriv q r * P1 r - (1 - q r) * deriv P2 r? Or smth like that

[Daniel Rehsmann]

Here a mwe

import Mathlib
open Set
open Real
noncomputable section
variable (q : ℝ → ℝ)
def f (q : ℝ → ℝ) (r c : ℝ) : ℝ := c * deriv q r
lemma f_deriv_pos : ∀ r > 0, 0 < deriv (f q) r := by
  unfold f
  dsimp

Here dsimp makes no progress, and remains at goal state

0 < deriv (fun r c ↦ c * deriv q r) r

How can I get rid of the lambda definitions inside deriv ( ) r

[Aaron Liu]

Daniel Rehsmann said:

How can I remove the lambda definition here, i.e., changing the goal state to:

⊢ 0 < deriv (deriv q r * P1 r - (1 - q r) * deriv P1 r) r

Does that typecheck?

[Daniel Rehsmann]

(deleted)

[Daniel Rehsmann]

Aaron Liu said:

Daniel Rehsmann said:

How can I remove the lambda definition here, i.e., changing the goal state to:

⊢ 0 < deriv (deriv q r * P1 r - (1 - q r) * deriv P1 r) r

Does that typecheck?

Yes. To simplify discussions, i added a mwe.

[Etienne Marion]

What change do you want to do? The first argument of deriv has to be a function.

[Aaron Liu]

Can confirm it does not in fact typecheck

[Daniel Rehsmann]

Etienne Marion said:

What change do you want to do? The first argument of deriv has to be a function.

I would like to have a goal state:0 < deriv (c * deriv q r) r

[Daniel Rehsmann]

Aaron Liu said:

Can confirm it does not in fact typecheck

In my environment, it does. Thats why I added a mwe

[Etienne Marion]

There is no c in the environment, this can't work

[Daniel Rehsmann]

Etienne Marion said:

There is no c in the environment, this can't work

Well, I worked a little bit on the mwe:

open Set
open Real
noncomputable section
variable (q p : ℝ → ℝ)
def f (q p: ℝ → ℝ) (r:ℝ) : ℝ := deriv q r + deriv p r
lemma f_deriv_pos (q p: ℝ → ℝ) (r: ℝ) : ∀ r > 0, 0 < deriv (f q p) r := by
  rintro r rpos
  unfold f

has the same problem. The problem is unrelated to c.

[Aaron Liu]

import Mathlib
open Set
open Real
noncomputable section
variable (q p : ℝ → ℝ)
def f (q p: ℝ → ℝ) (r:ℝ) : ℝ := deriv q r + deriv p r
lemma f_deriv_pos (q p: ℝ → ℝ) (r: ℝ) : ∀ r > 0, 0 < deriv (f q p) r := by
  rintro r rpos
  unfold f
  -- error
  #check deriv (deriv q r + deriv p r) r

[Etienne Marion]

I am guessing you want this:

import Mathlib

open Set
open Real
noncomputable section
variable (q p : ℝ → ℝ)
def f (q p: ℝ → ℝ) (r:ℝ) : ℝ := deriv q r + deriv p r
lemma f_deriv_pos (q p: ℝ → ℝ) (r: ℝ) : ∀ r > 0, 0 < deriv (f q p) r := by
  rintro r rpos
  unfold f
  rw [← Pi.add_def]

The simplifier will not remove the fun r => _ because it is considered to be the most unfolded form. Either use change as you did, or find the relevant lemma (as I did with Pi.add_def), but what we usually do is just keep the fun r => _ form and apply lemmas to it directly.

[Daniel Rehsmann]

Ok thank you. I am quite new to lean, so the typical way to work on such nested functions is to keep expressions fun r => _ in the goal state as they are and directly apply lemmas, correct?

[Etienne Marion]

Indeed. Both forms are definitionally equal, which means that any lemma which applies to one will apply to the other. However, you can have trouble when you use rw to rewrite a term, because rw does not see through definitional equality. That is why some lemmas in the library exist in both versions, one for f and one for fun x => f x.

[Daniel Rehsmann]

I see. But pushing dsimp inside a function argument is not possible? I prefer the later notation.

[Etienne Marion]

I'm not sure I understand the question. If you just have f + g then dsimp won't rewrite it to fun x => f x + g x, and if you have fun x => f x + g x it won't rewrite it to f + g. However, if you have (f + g) x or (fun y => f y + g y) x then in both cases it will rewrite to f x + g x.

[Daniel Rehsmann]

Here again the minimal example

open Set
open Real
noncomputable section
variable (q: ℝ → ℝ)
def f3 (q: ℝ → ℝ) (r:ℝ) : ℝ := deriv q r
lemma f3_deriv_pos (q: ℝ → ℝ) (r: ℝ) : ∀ r > 0, 0 < deriv (f3 q) r := by
  rintro r rpos
  unfold f3

I simply want to push dsimp (or any simp tactic that gets rid of the lambda expression) on the _ section of of the function
deriv (_) r

[Etienne Marion]

You can just change your definition of f3.

import Mathlib

noncomputable def f3 (q : ℝ → ℝ) : ℝ → ℝ := deriv q

lemma f3_deriv_pos (q : ℝ → ℝ) : ∀ r > 0, 0 < deriv (f3 q) r := by
  intro r rpos
  unfold f3

[Daniel Rehsmann]

Perfect! Thank you!