Nano Hash - криптовалюты, майнинг, программирование

Решите уравнения, включающие «очевидные» операции над множеством

Я регулярно обнаруживаю, что «auto» не решит уравнение, которое мне кажется достаточно простым, по крайней мере, используя поиск по терминам, включающим ∪, ∩ и -.

Failed to finish proof⌂:
goal (1 subgoal):
 1. ArityAnalysis.Afix Aexp Γ⋅(Aexp e⋅n) f|` (fv Γ ∪ fv e - domA Γ) =
    ArityAnalysis.Afix Aexp Γ⋅(Aexp e⋅n) f|` ((fv Γ ∪ fv e - domA Γ) ∩ - domA Γ)

Я могу обойти это (например, by auto (metis Diff_eq Diff_idemp)), но мне интересно, есть ли какая-то автоматизация, которую мне не хватает. Может быть, какой-то специальный набор simp, например ac_simps, для операций с наборами?

set isabelle
10.07.2014

Ответы:


1

Рассуждения о множествах в Isabelle2013-2 в основном выполняются классическим рассуждением, использующим правила введения и исключения, которые пытаются найти точечное решение. Я не знаю ни одного способа рассуждать о булевых алгебрах путем переписывания на Изабель. (Примечание: запись Regular-Expressions в Архиве формальных доказательств предоставляет метод regexp для работы с такими равенствами, но он не интегрирован с другими автоматизированными методами, такими как auto.) К счастью, все теоремы, которые вам нужны, есть в библиотеке HOL , но по умолчанию их нет в наборе simpset, потому что иногда они работают против вас. В вашем примере достаточно добавить Diff_eq к simpset.

С более сложными выражениями множества может быть трудно найти набор нормализующих правил перезаписи. Поэтому я предпочитаю позволить классическому рассуждению с его настройкой работать над установленным равенством. Для этого необходимо, чтобы равенство было подцелью, то есть оно не должно быть скрыто под функциональными приложениями. То есть вы хотите доказать f x = f y, доказав x = y, что выражается правилом arg_cong. Добавление arg_cong в качестве [intro] к auto направляет его в этом направлении, но это может не всегда работать, потому что объединение HO может помешать. В этом случае обычно достаточно явно указать f, как в

by(auto intro: arg_cong[where f="%x. ArityAnalysis.Afix Aexp Γ⋅(Aexp e⋅n) f|` x"])
10.07.2014
  • Хех, это напомнило мне многие рассуждения по уравнениям в Агде. И было бы здорово, если бы был способ использовать arg_cong как intro! без совпадения с f = (λ x.x). 10.07.2014
    • Новые материалы
    Кластеризация: более глубокий взгляд
    Кластеризация — это метод обучения без учителя, в котором мы пытаемся найти группы в наборе данных на основе некоторых известных или неизвестных свойств, которые могут существовать. Независимо от..
    Как написать эффективное резюме
    Предложения по дизайну и макету, чтобы представить себя профессионально Вам не позвонили на собеседование после того, как вы несколько раз подали заявку на работу своей мечты? У вас может..
    Частный метод Python: улучшение инкапсуляции и безопасности
    Введение Python — универсальный и мощный язык программирования, известный своей простотой и удобством использования. Одной из ключевых особенностей, отличающих Python от других языков, является..
    Как я автоматизирую тестирование с помощью Jest
    Шутка для победы, когда дело касается автоматизации тестирования Одной очень важной частью разработки программного обеспечения является автоматизация тестирования, поскольку она создает..
    Работа с векторными символическими архитектурами, часть 4 (искусственный интеллект)
    Hyperseed: неконтролируемое обучение с векторными символическими архитектурами (arXiv) Автор: Евгений Осипов , Сачин Кахавала , Диланта Хапутантри , Тимал Кемпития , Дасвин Де Сильва ,..
    Понимание расстояния Вассерштейна: мощная метрика в машинном обучении
    В обширной области машинного обучения часто возникает необходимость сравнивать и измерять различия между распределениями вероятностей. Традиционные метрики расстояния, такие как евклидово..
    Обеспечение масштабируемости LLM: облачный анализ с помощью AWS Fargate и Copilot
    В динамичной области искусственного интеллекта все большее распространение получают модели больших языков (LLM). Они жизненно важны для различных приложений, таких как интеллектуальные..