Isabelle 中的惯用微积分证明

Question

我正在尝试使用一些简单的真实分析问题来学习 Isabelle。以下是我的证明尝试。它会检查到最后一个。

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

我有几个问题：

如何完成证明？在我看来，我可以只应用 c5 来证明最后一个 hence，但是我尝试过的 auto、simp 等的各种组合似乎并没有这样做。
这个证明的更 isabelle-idomatic 版本是什么？我希望使用 has_vector_derivative 而不是 has_derivative 会更简单，但我更感兴趣的是将其保留为 has_derivative，但要进行重组。 Isabelle 文档中给出的示例似乎在 theence 语句之间做了更大的步长，这里有办法做到这一点吗？
我发现我需要在这里使用 derivative_eq_intros。是否有 fastforce intro: derivative_eq_intros 行的替代方法会更快？目前需要几秒钟。
一般来说，对于这种涉及向量和微积分的证明，我是否应该了解其他规则集，如derivative_eq_intros？默认情况下，它在 real_inner 数量上使用 simp 是什么？我可以在这里应用代数方法吗？
Sledgehammer 在这个证明中毫无用处，我是否需要传递一些参数或定理集以便它有机会证明这里的一些步骤？

Answer 1

你还需要把导数线性算子下面的t拉出来。你可以做到 linear_cmult[OF c3]。然后用o_def展开函数组合就大功告成了
里面有一些不必要的步骤。简化器可以完成您自己完成的大部分推理。另外，您对 f 的导数的假设太强了； f 在 x + s(y - x) 点有一个导数（我们称它为 D）就足够了。我在回答的最后给出了证明。
您可以在"intro"后加感叹号。这告诉 fastforce 急切地应用规则而不回溯。这应该小心使用（尤其是对于不是等价的介绍规则），因为它很容易导致不终止，但衍生规则通常是安全的。这大大加快了这里的过程。
限制有 tendsto_intros 和 tendsto_eq_intros，但它们的工作可靠性往往比衍生物的等价物低得多，因为限制通常有多个匹配规则.我在 Isabelle 中没有太多使用向量空间，所以我不能对此发表评论。至于 algebra，我认为它适用于基于环的 Gröbner，所以如果它适用于内积，我会感到惊讶。快速测试似乎表明它确实不是。一些规则在简化集中，所以简化器会自动使用它们。对于其余部分，您将不得不使用 find_theorems 或研究相应的理论来说明已经证明了它的哪些属性。
不是真的。您可以使用 using 或 from 链接其他事实，但 sledgehammer 通常非常擅长查找相关事实本身。我对它的了解还不够，无法推测为什么它在这里不是很有用；根据我的经验，有时有效，有时无效。

证明如下：

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

Answer 2

对你的导入做一个简短的评论：只导入 “~~/src/HOL/Multivariate_Analysis”（将只是“~~/src/HOL/Analysis”）。当您从 isabelle/jEdit 开始使用 -lHOL-Multivariate_Analysis.

时，您会得到最好的结果

您的第一行导入会导入所有其他内容，其他行是不必要的。如果他们不小心修改了一些自动化数据库（例如简单规则、intro/dest/elim 规则等），它们可能会成为问题

Isabelle 中的惯用微积分证明

Idiomatic calculus proofs in Isabelle

isabelle