Как вставить значения в неизвестных в доказательстве теоремы Изабель? - PullRequest
Новая
       61

Как вставить значения в неизвестных в доказательстве теоремы Изабель?

2 голосов
/ 09 марта 2020

У меня есть следующие подзадачи: 

proof (prove)
goal (2 subgoals):
 1. ⋀y. ∃x. P x ⟹ P (?x6 y)
 2. ⋀y. ∃x. P x ⟹ Q (?y8 y) ⟹ Q y

Я хочу завершить доказательство или продолжить пробовать вещи, но я не знаю, как ввести вещи в неизвестные (схемы c переменные), то есть переменные с ?.

Как это сделать?

Ответы [ 2 ]

2 голосов
/ 09 марта 2020

Во-первых, необходимо понять, как переменные схемы c появились в ваших подзадачах. Обычно, если вы не используете schematic_goal, переменные схемы c появляются в подзадачах после некоторой формы применения правила, неявного или явного.

  1. Если приложение правила было явным (например, apply (rule conjunct1)), то разумно стандартной методологией для решения проблемы, которую вы описали, является замена переменных, которые вы будете sh, на «попробовать» непосредственно в правило, например apply (rule conjunct1[of A]). В этом случае в ваших целях не будет переменных c схемы и, следовательно, проблема неявно исчезнет.
  2. Если применение правила было неявным (например, с помощью одного из инструментов классического мышления), то Ваши варианты зависят от того, были ли подцели созданы в сценарии apply или в теле доказательства Изара. Тем не менее, прежде чем я продолжу, я хотел бы упомянуть, что доказательства, где вы должны взаимодействовать с подцелями, сгенерированными после применения любых методов «черного ящика», не считаются очень хорошим стилем (по крайней мере, на мой взгляд) , В первом случае вам ничего не нужно делать, чтобы «попробовать что-то». Как только переменная, которую вы будете подставлять sh для замены (например, z), определена, вы можете использовать show "∃x. P x ⟹ P (z y)" в теле доказательства Изара. Аналогично, в сценарии apply вы можете разрешить с помощью предварительно подставленных переменных.

Я демонстрирую все эти методы в контексте упрощенного примера ниже: 

context
  fixes A B :: bool
  assumes AB: "A ∧ B"
begin

lemma A by (rule conjunct1[of _ B]) (rule AB)

lemma A 
  by (rule conjunct1) (rule AB)

lemma A 
proof(rule conjunct1)
  show "A ∧ B" by (rule AB)
qed

end
1 голос
/ 10 марта 2020

Важные части уже объяснены пользователем9716869. Я просто хотел добавить:

Ваша текущая подзадача, вероятно, не решаема, если у вас нет дополнительной информации. Если вам требуется x из ∃x. P x для создания экземпляра схемы c переменная ?x6, то вам нужно получить значение x до создания переменной c схемы.

Схемы c переменные создаются автоматически при сопоставлении. Это хорошо работает, если переменная schemati c не является функцией, поэтому вы можете просто продолжать писать свое доказательство, как если бы правильное значение уже было там. Если вы хотите зафиксировать значение в доказательстве применения стиля (другие случаи уже приведены в другом ответе), вы можете использовать subgoal_tac, за которым следует assumption: 

lemma "⋀y. ∃x. P x ⟹ ∃x::nat. P x"
  apply (rule exI)
 ― ‹⋀y. ∃x. P x ⟹ P (?x y)›
  apply (subgoal_tac "P 42", assumption)
 ― ‹⋀y. ∃x. P x ⟹ P 42›
  oops ― ‹Not possible to prove›

lemma "⋀y. ∃x. P x ⟹ ∃x::nat. P x"
  apply (erule exE)
 ― ‹⋀y x. P x ⟹ ∃x. P x›
  apply (rule exI)
 ― ‹⋀y x. P x ⟹ P (?x2 y x)›
  apply (subgoal_tac "P x", assumption)
 ― ‹⋀y x. P x ⟹ P x›
  by assumption
...