Блог

Рассмотрим следующую лемму, которая должна быть легко доказуемой:

 lemma
  fixes n m::nat
  defines "m ≡ n - 1"
  shows "m ≤ n"
proof(induction n)
  case 0
  then show ?case unfolding m_def 
      (* Why does «n» appear here? *)
next
  case (Suc n)
  then show ?case sorry
qed
 

Однако после развертывания m цель становится n - 1 ≤ 0 вместо 0 - 1 ≤ 0 того , чтобы сделать цель недоказуемой, поскольку n = 2 это контрпример.

Это ошибка в Изабель? Как я могу правильно развернуть определение?

Я думаю , что полезным объяснением могло бы быть следующее: Вспомните определение nat.induct , а именно

 ?P 0 ⟹ (⋀n. ?P n ⟹ ?P (Suc n)) ⟹ ?P ?n
 

и обратите внимание, что это ?n означает, что n это неявно универсально количественно определено, то есть предыдущее определение эквивалентно

 ⋀n. ?P 0 ⟹ (⋀n. ?P n ⟹ ?P (Suc n)) ⟹ ?P n
 

Теперь, применяясь nat.induct к вашему примеру, ясно , что первой подцелью, которую нужно доказать, является ?P 0 , т. е. m ≤ 0 Однако в этом контексте n все еще является произвольным, но фиксированным nat , в частности , это не так n = 0 , и именно по этой причине после развертывания определения m вы получаете n - 1 ≤ 0 в качестве новой подцели. Что касается вашего конкретного вопроса, проблема в том, что вы не можете доказать свой результат с помощью индукции n (но вы можете легко доказать это с помощью unfolding m_def by simp ).

Как отметил Хавьер, n определение в заголовке леммы отличается от n созданного induction . Другими словами, любые факты «извне», на которые ссылается эта ссылка n , не могут быть непосредственно использованы в окружающей proof (induction n) среде.

Тем не менее, Изабель предлагает способ «внедрить» такие факты, передав их в induction :

 lemma
  fixes n m::nat
  defines "m ≡ n - 1"
  shows "m ≤ n"
  using m_def (* this allows induction to use this fact *)
proof(induction n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case by simp
qed
 

using assms будет работать так же хорошо и в этом случае.

Обратите внимание, что прямая ссылка m_def больше не требуется, так как для каждого из них включена его версия case (в 0.hyps и Suc.hyps ; используйте print_cases внутри доказательства для получения дополнительной информации).