Understanding pattern matching on functions?

Stream: new members

[Mr Proof]

I am trying to understand the Lean syntax so I would like to define a formal derivative.
From what I see there's two ways to do this. Either an operator D which acts on functions R->R or an operator D which actions on some expression object f(x) with the second parameter being the independent variable x.

Let's suppose I have D acting on a function D(fun (x:Real)=>f(x)+g(x)) I want to pattern match this and output is D(fun (x:Real)=>f(x)) + D(fun (x:Real)=>g(x)) but I'm not really sure how to pattern match on functions.

A second thing is D( (x:Real)=>c) where c is not dependent on x, then this must become 0. But how can I tell that c does not depend on x? (It may depend on other variables like y and z).

Any tips?

[Henrik Böving]

Pattern matching on functions is impossible. They are not an inductive type but an entirely different construct instead

[Kyle Miller]

To do formal derivatives, you need to make a type of formal functions (expressions). This type would have a function to give an interpretation as actual Real -> Real functions.

[Mr Proof]

I see. Is there already a way to make formal expressions in Lean? Prop types already seem expression-like.

In the HEPlean project they were defining the partial derivative as:

/-- partial derivative -/
noncomputable
abbrev pderiv (i : Fin n) (u : EuclideanSpace ℝ (Fin n) → U) (x : EuclideanSpace ℝ (Fin n)) :=
  deriv (fun (h' : ℝ) => u (x + h' • basisFun (Fin n) ℝ i)) 0

I'm not sure if this is "formal" or not but seems to act on functions rather than formal expressions. I'm wondering how that is possible.

[Kyle Miller]

The answer to your first question is inductive types, but Type-valued, not Prop-valued.

For the second, it's not formal. The deriv function does not "see" the definition of the function passed to it.