Спойлер: можно использовать стандартный список индукции и auto, чтобы доказать теорему, т.е. что-то похожее на by (induct xs ...) (auto simp: ...).Я сознательно пропустил разделы в доказательстве, чтобы вы могли заполнить их самостоятельно.Вам нужно будет подумать, нужно ли указывать какие-либо переменные (например, m или x) как arbitrary, а также понять, какая информация может понадобиться упрощающему (ищите подсказки в спецификации min_list в теорииList).
Что касается вашего вопроса о сложности проблемы, я полагаю, что сложность является функцией опыта.Скорее всего, когда я начал изучать Изабель, мне было трудно формализовать доказательства, подобные тому, что был в вашем вопросе.После некоторого времени, потраченного на кодирование в Isabelle (к моменту ответа на этот вопрос, я должен был накопить эквивалент 4-5 месяцев полного кодирования в Isabelle), такие проблемы больше не представляются значительнымивызов для меня.Конечно, есть и другие факторы, которые необходимо учитывать, например, предыдущее обучение математике или логике и предыдущий опыт программирования.
Общие советы от того, кто изучает Изабель самостоятельно(совет может не соответствовать подходу, который обычно рекомендуют профессиональные инструкторы)
Я считаю, что при доказательстве аналогичных результатов важно понимать, что Изабель, прежде всего, инструмент для формализации«ручку и бумагу» доказательства.Поэтому важно иметь под рукой «ручку и бумагу», прежде чем пытаться ее формализовать.Я бы предложил следующий общий подход при решении подобных проблем:
- Напишите доказательство на бумаге.
- Формализируйте доказательство, используя
Isar, предоставляя как можно больше деталей и не заботясьслишком много о длине доказательства.Кроме того, постарайтесь не полагаться на инструменты для автоматического рассуждения (например, auto, blast, meson, metis, fastforce) и использовать прямые методы, такие как rule и intro, так как выcan. - После того, как ваше
Isar доказательство выполнено, примените инструменты для автоматического рассуждения (например, auto, blast) к вашему доказательству Isar, чтобы максимально упростить ваше доказательство.
Конечно, со временем, когда вы добьетесь прогресса в изучении Изабель, будет все легче опускать 1 и 2.
Я могу предоставить более подробную информацию, например, полное краткое доказательство идлинная Isar версия доказательства.
ОБНОВЛЕНИЕ
Согласно вашему запросу в комментариях, я предоставляю неофициальное доказательство.
Лемма .m = min_list (x # xs) ⟹ m ∈ set (x # xs).
Замечания .Для полноты изложения я также даю определение min_list и некоторые комментарии о const set.Определение min_list можно найти в теории List:
fun min_list :: "'a::ord list ⇒ 'a" where
"min_list (x # xs) = (case xs of [] ⇒ x | _ ⇒ min x (min_list xs))"
const set определен неявно и является частью инфраструктуры datatype для list (см.документ «Определение (Co) типов данных и примитивно (Co) рекурсивных функций в Изабель / HOL» в стандартной документации, если Изабель).В частности, это называется «функция установки» типа данных.Многие основные свойства const set могут быть найдены при проверке / поиске, например, find_theorems list.set.Я полагаю, что теорема thm list.set представляет основные свойства const set (я позволил себе переименовать схематические переменные в теореме):
set [] = {}
set (?x # ?xs) = insert ?x (set ?xs)
Доказательство .Доказательством служит структурная индукция в списке xs.Принцип индукции сформулирован как безымянная лемма в начале теории List.Для полноты излагаю принцип индукции ниже:
"P [] ⟹ (⋀a list. P list ⟹ P (a # list)) ⟹ P list"
Базовый случай : предположим, xs = [], показать m = min_list (x # xs) ⟹ m ∈ set (x # xs) для всех x.Из определения min_list легко понять, что min_list (x # []) = x.Точно так же set (x # []) = {x} может быть показано непосредственно из свойств const set.Подставляя в предикат выше, осталось показать, что m = x ⟹ m ∈ {x} для всех x.Это следует из базовой теории множеств.
Индуктивный шаг : предположим, ⋀x. m = min_list (x # xs) ⟹ m ∈ set (x # xs), показать m = min_list (a # x # xs) ⟹ m ∈ set (a # x # xs) для всех a, x и xs. Исправьте a, x и xs. Предположим, m = min_list (a # x # xs). Тогда осталось показать, что m ∈ set (a # x # xs). Учитывая m = min_list (a # x # xs), из определения min_list, легко сделать вывод, что либо m = a, либо m = min_list (x # xs). Рассмотрим эти случаи в явном виде:
- Случай I:
m = a. a ∈ set (a # x # xs) следует из определений. Затем m ∈ set (a # x # xs) путем подстановки.
- Случай II:
m = min_list (x # xs). Тогда из предположения ⋀x. m = min_list (x # xs) ⟹ m ∈ set (x # xs) следует, что m ∈ set (x # xs). Таким образом, m ∈ set (a # x # xs) следует из свойств set.
Во всех возможных случаях m ∈ set (a # x # xs), что и требовалось доказать.
Итак, доказательство завершено.
Заключительные мысли . Попробуйте преобразовать это неофициальное доказательство в Isar доказательство. Кроме того, обратите внимание, что доказательство может быть не идеальным - я могу внести изменения в доказательство позже.