How can I use a dummy variable to prove a lemma in Lean3?

Question

I have the following definition for the operator D:

noncomputable def D: (ℝ → ℝ) → (ℝ → ℝ) := λ f, deriv f

I want to prove that D is linear in the vector space of differentiable functions, so basically this:

noncomputable variable x : ℝ
lemma D_lin (h g : ℝ → ℝ)(a : ℝ): D (a • h + g) = a • D h + D g :=

The strategy I have in mind is to evaluate both sides with respect to a dummy real variable x. This is what I've tried:

begin
  rw D,
  simp,
  intro x,
end

But I receive the following error:

intro tactic failed, Pi/let expression expected
state:
h g : ℝ → ℝ,
a : ℝ
⊢ deriv (a • h + g) = a • deriv h + deriv g

I don't have any idea what this means. Is there a way to apply the proposition to a dummy variable without having it as a parameter of the lemma?

Answer 1

Others have already explained why intro does not apply here.

One thing you should watch out for here is that you're missing the hypotheses that the functions h and g are differentiable. Here's a quickly-written proof of the corrected theorem, which I give here because with the way deriv_add and deriv_const_smul are formulated it's a bit of a fight with Lean to finish it up:

import analysis.calculus.deriv

noncomputable def D : (ℝ → ℝ) → (ℝ → ℝ) := λ f, deriv f

lemma D_lin (h g : ℝ → ℝ) (hd : differentiable ℝ h) (gd : differentiable ℝ g)
  (a : ℝ) : D (a • h + g) = a • D h + D g :=
begin
  unfold D,
  ext x,
  transitivity deriv (a • h) x + deriv g x,
  { apply deriv_add,
    exact differentiable_at.const_mul (hd x) _,
    exact gd x, },
  { rw [pi.add_apply, add_left_inj],
    exact deriv_const_smul _ (hd x), },
end

Design-wise, this is not the "right" linearity lemma to prove since it's not very easy to apply. Instead, consider having two lemmas so that you can apply it to any expression involving addition and scalar multiplication:

lemma D_add (h g : ℝ → ℝ) (hd : differentiable ℝ h) (gd : differentiable ℝ g) :
  D (h + g) = D h + D g :=
begin
  ext x,
  exact deriv_add (hd x) (gd x),
end

lemma D_smul (h : ℝ → ℝ) (hd : differentiable ℝ h) (a : ℝ) :
  D (a • h) = a • D h :=
begin
  ext x,
  exact deriv_const_smul _ (hd x),
end

With these, one proof of D_lin is then rw [D_add, D_smul], assumption, apply differentiable.const_mul, assumption, assumption. (It'd be nice if there were some automation for these differentiability side-goals!)

As a bonus, here's that D is a derivation:

lemma D_mul (h g : ℝ → ℝ) (hd : differentiable ℝ h) (gd : differentiable ℝ g) :
  D (h * g) = D h * g + h * D g :=
begin
  ext x,
  exact deriv_mul (hd x) (gd x),
end

Answer 2

The intro tactic only works if your goal is of the form P -> Q or \forall x, blah. Your goal is not, so you get an error telling you this (in an admittedly obscure way : these types I've just mentioned are called Pi types). I think what you want is ext x. ext, the extensionality tactic, will prove that two functions are equal if they give the same output for every input.

Answer 3

An answer from a more type-theoretic perspective (if you only want to do mathematics in Lean then safely ignore this).

In Martin-Löf type theories (Lean being a variant with impredicativity), it is impossible to prove the following theorem without additional axioms:

Theorem (Function Extensionality). Two functions $f,g : A\to B$ are equal if and only if $\forall x, f(x) = g(x)$.

Therefore it is necessary to introduce this as an axiom. Alternatively, some other axiom may imply this. In Lean, the axioms about quotients imply this theorem. You can use these axioms with the tactic ext.

In other type theories, this may become a theorem. For instance, in a type theory where the equality type is represented as an interval, then the proof is trivial:

funext p i x = p x i

More generally, the existence of an interval already implies function extensionality.