Локальные допущения в режиме состояния

Часто, доказывая утверждение в режиме доказательства, я обнаруживаю, что мне нужны некоторые промежуточные утверждения, которые еще не сформулированы и не доказаны. Чтобы указать их, я обычно использую команду subgoal, за которой следует proof-, чтобы перейти в режим состояния. Однако в процессе все локальные допущения удаляются. Типичный пример может выглядеть так

lemma "0 < n ⟷ ((2::nat)^n < 3^n)"
  apply(auto)
  subgoal
  proof-
    have "0<n" sorry (* here I would like to refer to the assumption from the subgoal *)
    then show ?thesis sorry
  qed
  subgoal sorry
  done

Я знаю, что могу явно сформулировать предположения, используя assume. Однако это быстро становится довольно утомительным, если задействовано несколько предположений. Есть ли более простой способ просто сослаться на все предположения? В качестве альтернативы, есть ли хороший способ реализовать утверждения с короткими доказательствами непосредственно в режиме доказательства?


isabelle isar
person Benedikt    schedule 06.01.2021    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Существует синтаксис subgoal premises prems для привязки предпосылки подцели к имени prems (или любому другому имени, но prems является разумным значением по умолчанию):

lemma "0 < n ⟷ ((2::nat)^n < 3^n)"
  apply(auto)
  subgoal premises prems
  proof -
    thm prems

Также существует метод goal_cases, который автоматически дает имена всем текущим подцелям - я считаю его очень полезным. Если subgoal premises не существует, вы можете сделать это:

lemma "0 < n ⟷ ((2::nat)^n < 3^n)"
  apply(auto)
  subgoal
  proof goal_cases
    case 1

Между прочим, глядя на ваш пример, считается плохой идеей делать что-либо после auto, что зависит от точной формы состояния доказательства, например metis вызовов или доказательств Isar. auto довольно жесток и может вести себя иначе в следующем выпуске Isabelle, так что такие доказательства ломаются. Я рекомендую сделать здесь красивое структурированное доказательство Isar.

Также обратите внимание, что ваша теорема является прямым следствием power_strict_mono и power_less_imp_less_base и может быть доказана в одной строке:

lemma "0 < n ⟷ ((2::nat)^n < 3^n)"
  by (auto intro: Nat.gr0I power_strict_mono)`
person Manuel Eberl    schedule 06.01.2021
comment
О применении автоматического доказательства -: proofcraft.org/blog/isabelle-style.html - хороший справочник по хорошему стилю доказательств. - person Mathias Fleury; 07.01.2021