Идиоматические исчисления в Isabelle

Question

Я пытаюсь изучить Изабель, используя некоторые простые проблемы с реальным анализом. Ниже приведена моя попытка доказательства. Он проверяет до последнего.

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 

У меня есть несколько вопросов:

1. Как закончить доказательство? Мне кажется, что я могу просто применить c5 для доказательства последнего, но различные комбинации auto, simp и т. Д., Которые я пробовал, похоже, не делают этого.
2. Что было бы более изобелой идоматической версией этого доказательства? Я ожидаю, что было бы проще с has_vector_derivative вместо has_derivative, но я больше заинтересован в том, чтобы сохранить его has_derivative, но реструктурировать. Примеры, приведенные в документации Isabelle, как представляется, делают более значительные шаги между заявлениями отсюда, есть ли способ сделать это здесь?
3. Я обнаружил, что здесь мне нужно использовать производные_ик_интроны. Есть ли альтернатива быстрой инициативе fastforce: производная_eq_intros, которая будет быстрее? На данный момент это занимает несколько секунд.
4. В целом, для такого рода доказательств, связанных с векторами и исчислением, существуют ли другие наборы правил, такие как производные_ик_интросы, о которых я должен знать? Что он использует по умолчанию для значений real_inner с simp? Могу ли я применить метод алгебры здесь?
5. Кувалда была довольно бесполезной в этом доказательстве, мне нужно передать некоторые параметры или множества теорем, чтобы иметь возможность доказать некоторые из этих шагов здесь?

Answer 1

1. Вам все еще нужно, чтобы вытащить из-под t линейного оператора производной. Вы можете сделать это linear_cmult[OF c3]. Затем разверните функциональную композицию с o_def, и все готово.

2. Есть несколько ненужных шагов. Упрощение может сделать большинство рассуждений, которые вы сделали сами по себе. Кроме того, ваше предположение о производной от f очень сильное; для f достаточно иметь производную (назовем ее D) в точке x + s(y - x). Я подтвердил это в конце своего ответа.

3. Вы можете добавить восклицательный знак к «intro». Это говорит fastforce, чтобы применять правила с нетерпением и без обратного отслеживания. Это следует использовать с осторожностью (особенно с правилами ввода, которые не являются эквивалентами), поскольку это может легко привести к прерыванию, но правила для производных обычно безопасны. Это ускоряет процесс здесь.

4. Для лимитов существует tendsto_intros и tendsto_eq_intros, но они имеют тенденцию работать намного менее надежно, чем их эквиваленты для производных, поскольку часто существует несколько правил соответствия для лимитов. Я не использовал векторные пространства много в Изабель, поэтому я не могу прокомментировать это. Что касается algebra, я думаю, что работает с основами Грёбнера на кольцах, поэтому я был бы удивлен, если бы он был подстрекатель к внутренним продуктам. Быстрая проверка, похоже, указывает на то, что это действительно не так. Некоторые из правил находятся в наборе simp, поэтому упроститель будет использовать их автоматически. В остальном вам нужно будет использовать find_theorems или заглянуть в соответствующие теории, чтобы сказать, какие свойства были доказаны для него.

5. Не совсем. Вы можете связать дополнительные факты с using или from, но кувалдой обычно очень хорошо удается найти актуальные факты.Я не знаю достаточно об этом, чтобы размышлять о том, почему здесь это не очень полезно; по моему опыту, иногда это работает, а иногда и нет.

Теперь вот доказательство:

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/Анализ "). Вы получаете лучший результат при запуске isabelle/jEdit с -lHOL-Multivariate_Analysis.

Ваша первая строка импорта импортирует все остальное, другие строки не нужны. Они могут стать проблемой, если они случайно изменят некоторые базы данных автоматизации (например, правила simp, правила ввода/удаления/исключения и т. Д.)