Как мне доказать лемму из упражнения 4.6 в «Программирование и доказательство в Isabelle / HOL»?

Я пытаюсь выполнить упражнение 4.6 из раздела «Программирование и доказательство в Isabelle / HOL». Он просит определить функцию elems :: "'a list ⇒ 'a set", которая преобразует список в набор, и доказать лемму "x ∈ elems xs ⟹ ∃ ys zs . xs = ys @ x # zs ∧ x ∉ elems ys". До сих пор я зашел так далеко:

fun elems :: "'a list ⇒ 'a set" where
  "elems [] = {}" |
  "elems (x # xs) = {x} ∪ elems xs"

lemma first_occ: "x ∈ elems xs ⟹ ∃ ys zs . xs = ys @ x # zs ∧ x ∉ elems ys"
proof (induction xs)
  case Nil
  thus ?case by simp
next
  case (Cons u us)
  show ?case
  proof cases
    assume "x = u"
    thus ?case
    proof
    ⟨…⟩

На этом этапе я получаю сообщение об ошибке «Не удалось применить метод первоначальной проверки». Это странно, поскольку цель ?case - это суждение ∃ ys zs . u # us = ys @ x # zs ∧ x ∉ elems ys, и должна быть возможность доказать экзистенциальные суждения, показав суждение под ∃ для конкретного свидетеля.


quantifiers isabelle isar
person Wolfgang Jeltsch    schedule 24.11.2017    source источник

Ответы (1)


arrow_upward
0
arrow_downward

проблема с вашей строкой proof в том, что она proof предназначена для применения некоторого правила по умолчанию. В приведенном выше доказательстве Изабель не может понять, что вы хотите выполнить экзистенциальное введение. Итак, вы, вероятно, захотите явно указать системе сделать это, например, продолжив что-то вроде proof (intro exI).

Надеюсь, это поможет, Рене

person René Thiemann    schedule 24.11.2017
comment
Почему Изабель не может этого понять? Если целью является предложение формы ∃ x . P; поэтому Изабель должна автоматически выбирать экзистенциальное введение. Он работал в других ситуациях (например, в примере кода в моем вопросе «Как я могу эффективно доказать экзистенциальные предложения с несколькими переменными в Isabelle / Isar? ”; почему не здесь? - person Wolfgang Jeltsch; 24.11.2017
comment
Потому что вы также приковали факт к thus. Методы доказательства, такие как rule, будут работать только в том случае, если все связанные факты могут быть объединены с предположениями правила для применения в правильном порядке. Если вы не укажете метод явно, Изабель будет использовать standard, который аналогичен rule с некоторым набором правил по умолчанию. TL; DR вы редко хотите объединять факты в proof. Используйте здесь show вместо thus. - person Manuel Eberl; 28.11.2017