Idiomatic calculus proofs in Isabelle

Question

I'm trying to learn Isabelle using some simple real analysis problems. Below is my attempt at a proof. It checks up until the last hence.

theory l2
  imports 
    "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
    "~~/src/HOL/Multivariate_Analysis/Derivative"
    "~~/src/HOL/Multivariate_Analysis/Integration"
    "~~/src/HOL/Complex_Main"
    "~~/src/HOL/Library/Inner_Product"
    "~~/src/HOL/Real_Vector_Spaces"
  begin

  thm linear.scaleR

  lemma line_fundamental_theorem_calculus:
    fixes x y :: "'a :: real_inner"
    and   s :: "real"
    and   f :: "'a ⇒ real"
    assumes "∀v. (f has_derivative (f' v)) (at v) "
    shows "((λt. f(x+t*⇩R(y-x))) has_derivative (λt. t *⇩R ((f'(x + s*⇩R(y-x))) (y-x)))) (at s)"
  proof -
   let ?z = "(λt. x + t*⇩R(y-x)) :: real ⇒ 'a"
   let ?dzdt = " (λt. t*⇩R(y-x))"
   have c1: "f ∘ ?z = (λt. f(x+t*⇩R(y-x)))" by auto
   have c2: "(f'(x + s*⇩R(y-x))) ∘ (λt. t*⇩R(y-x)) = (λt. (f'(x + s*⇩R(y-x))) (t*⇩R(y-x)))" by auto
   have a1: "(f has_derivative (f' (x + s*⇩R(y-x)))) (at (x + s*⇩R(y-x))) " using assms by auto
   have c3: "linear (f'(x + s*⇩R(y-x)))" using assms has_derivative_linear by auto
   have c5: "(f'(x + s*⇩R(y-x))) (t*⇩R(y-x)) = t *⇩R ((f'(x + s*⇩R(y-x))) (y-x))"  using c3 linear.scaleR by blast

   have h1: "(?z has_derivative ?dzdt) (at s)" by (fastforce intro: derivative_eq_intros)
   hence "((f ∘ ?z) has_derivative ((f'(x + s*⇩R(y-x))) ∘ ?dzdt)) (at s) " using assms a1 c1 by (fastforce intro: derivative_eq_intros)
   hence "((f ∘ ?z) has_derivative ((f'(x + s*⇩R(y-x))) ∘ (λt. t*⇩R(y-x)))) (at s) " by auto
   hence "((f ∘ ?z) has_derivative (λt. (f'(x + s*⇩R(y-x))) (t*⇩R(y-x)))) (at s) " by (auto simp: c2)

   hence "((f ∘ ?z) has_derivative (λt. t *⇩R ((f'(x + s*⇩R(y-x))) (y-x)))) (at s) " 
   then show ?thesis 
  qed                                               

  end

I have a few questions:

How do I finish the proof? It looks to me that I can just apply c5 to prove the last hence, but the various combinations of auto, simp etc. that I've tried don't seem to do it.
What would be a more isabelle-idomatic version of this proof? I expect that it would be simpler with has_vector_derivative instead of has_derivative, but I'm more interested in keeping it with has_derivative, but restructuring. The examples given in the Isabelle documentation seem to make larger steps between the hence statements, is there a way to do that here?
I've found that I need to use derivative_eq_intros here. Is there an alternative to the fastforce intro: derivative_eq_intros line that would be quicker? It takes a few seconds at the moment.
In general, for this kind of proof involving vectors and calculus, is there other rule sets like derivative_eq_intros that I should know about? What is it using by default on real_inner quantities with simp? Can I apply the algebra method here?
Sledgehammer was pretty useless in this proof, do I need to pass in some parameters or sets of theorems so that it has a chance of proving some of the steps here?

Manuel Eberl Manuel Eberl · Accepted Answer · 2016-11-02T07:51:24

You still need to pull out the t from under the linear operator of the derivative. You can do that linear_cmult[OF c3]. Then unfold the function composition with o_def and you're done.
There are a few unnecessary steps in there. The simplifier can do most of the reasoning you did by itself. Also, your assumption about the derivative of f is much too strong; it is enough for f to have a derivative (let's call it D) at the point x + s(y - x). I put a proof of that at the end of my answer.
You can add an exclamation mark to the "intro". That tells fastforce to apply the rules eagerly and without backtracking. This should be used with care (especially with intro rules that are not equivalences) as it can easily lead to non-termination, but the rules for derivatives are usually safe. This speeds up the process a lot here.
There is tendsto_intros and tendsto_eq_intros for limits, but they tend to work a lot less reliably than their equivalents for derivatives, since there are often several matching rules for limits. I haven't used vector spaces much in Isabelle so I cannot comment on that. As for algebra, I think that works with Gröbner bases on rings, so I would be surprised if it were applictable to inner products. A quick test seems to indicate that it is, indeed, not. Some of the rules are in the simp set, so the simplifier will use them automatically. For the rest, you'll have to use find_theorems or look into the respective theories to say what properties have been proven for it.
Not really. You can chain in additional facts with using or from, but sledgehammer is usually pretty good at finding relevant facts itself. I don't know enough about it to speculate on why it wasn't very helpful here; in my experience, sometimes it works and sometimes it doesn't.

Now here's the proof:

lemma line_fundamental_theorem_calculus:
  assumes "(f has_derivative D) (at (x + s*⇩R(y-x))) "
  shows "((λt. f(x+t*⇩R(y-x))) has_derivative (λt. t *⇩R (D (y-x)))) (at s)"
proof -
  let ?z = "(λt. x + t*⇩R(y-x))" and ?dzdt = "λt. t *⇩R (y-x)"
  have lin: "linear D" using assms has_derivative_linear by auto
  have "((f ∘ ?z) has_derivative (D ∘ ?dzdt)) (at s) " 
    using assms by (fastforce intro!: derivative_eq_intros)
  thus ?thesis by (simp add: o_def linear_cmul[OF lin])
qed

Idiomatic calculus proofs in Isabelle

2 Answers