Укрощение мета-смысла в доказательствах Изара

Question

Доказывая простую теорему, я наткнулся на последствия мета-уровня в доказательстве. Можно ли их иметь или их можно избежать? Если я должен справиться с ними, это правильный способ сделать это?

theory Sandbox
imports Main
begin

lemma "(x::nat) > 0 ∨ x = 0"
proof (cases x)
  assume "x = 0"
  show "0 < x ∨ x = 0" by (auto)
next
  have "x = Suc n ⟹ 0 < x" by (simp only: Nat.zero_less_Suc)
  then have "x = Suc n ⟹ 0 < x ∨ x = 0" by (auto)
  then show "⋀nat. x = Suc nat ⟹ 0 < x ∨ x = 0" by (auto)
qed

end

Я думаю, это легче доказать, но я хотел получить структурированное доказательство.

Answer 1

В принципе мета-подтекст ==> нечего избегать (на самом деле это "родной" способ выражения правил вывода в Изабель). Существует канонический способ, который часто позволяет нам избежать мета-смысла при написании доказательств Изара. Например, для общей цели

"!!x. A ==> B"

мы можем написать на Изаре

fix x
assume "A"
...
show "B"

Для вашего конкретного примера, глядя на него в Изабель /jEdit, вы можете заметить, что n второго случая подсвечивается. Причина в том, что это свободная переменная. Хотя это само по себе не является проблемой, более канонично исправлять такие переменные локально (как типичное утверждение "для произвольного, но фиксированного..." в учебниках). Например,

next
  fix n
  assume "x = Suc n"
  then have "0 < x" by (simp only: Nat.zero_less_Suc)
  then show "0 < x ∨ x = 0" ..
qed

Здесь снова можно увидеть, как fix/assume/show в Изаре соответствует актуальной цели, т. е.

1. ⋀nat. x = Suc nat ⟹ 0 < x ∨ x = 0

Answer 2

При написании структурированных доказательств лучше всего избегать мета-следствия (и количественного определения) для самой внешней структуры подцели. Т.е. вместо того, чтобы говорить о

⋀x. P x ⟹ Q x ⟹ R x

ты должен использовать

fix x
assume "P x" "Q x"
...
show "R x"

Если P x а также Q x иметь некоторую структуру, хорошо использовать мета-импликацию и -quantification для них.

Есть ряд причин, чтобы предпочесть fix/assumes над мета-операторами в структурированных доказательствах.

• Несколько тривиально, вам не нужно указывать их снова в каждом заявлении "имейте и покажите".

• Более важно, когда вы используете fix для количественной оценки переменной она остается неизменной во всем доказательстве. Если вы используете ⋀, это свежо определено в каждом have заявление (и не существует снаружи). Это делает невозможным непосредственное обращение к этой переменной и часто усложняет область поиска для автоматизированных инструментов. Подобные вещи имеют место для assume против ⟹,

• Более сложным моментом является поведение show в присутствии мета-значений. Рассмотрим следующую попытку доказательства:

  lemma "P ⟷ Q"
  proof
    show "P ⟹ Q" sorry
  next
    show "Q ⟹ P" sorry
  qed
  

  После proof Команда, есть две подзадачи: P ⟹ Q а также Q ⟹ P, Тем не менее, финал qed выходит из строя. Как это случилось?

  Первый show применяет правило P ⟹ Q к первой применимой подцели, а именно P ⟹ Q, Используя обычный механизм разрешения правил Изабель, это дает P ⟹ P (assume Pпоказать Q` удалил бы подцель).

  Второй show применяет правило Q ⟹ P к первой применимой подцели: это сейчас P ⟹ P (как Q ⟹ P является второй подцелью), уступая P ⟹ Q снова.

  В результате у нас еще есть две подзадачи P ⟹ Q а также Q ⟹ P а также qed не может закрыть цель.

  Во многих случаях мы не замечаем такого поведения show, как тривиальные подцели вроде P ⟹ P может быть решена qed,

Несколько слов о поведении show: Как мы видели выше, мета-смысл в show не соответствует assume, Вместо этого это соответствует assumeменее известный брат, presume, presume позволяет вводить новые допущения, но требует от них последующего применения. В качестве примера сравните

lemma "P 2 ⟹ P 0"
proof -
  presume "P 1" then show "P 0" sorry
next
  assume "P 2" then show "P 1" sorry
qed

а также

lemma "P 2 ⟹ P 0"
proof -
  show "P 1 ⟹ P 0" sorry
next
  assume "P 2" then show "P 1" sorry
qed