Рассуждения о неравенстве в Изабель

Question

У меня есть следующее простое доказательство:

lemma
    fixes a b n :: nat
    assumes a: "a > n" "b > n"
    shows "a*b > n*n"
proof -
    from assms show "a*b > n*n" by(simp_all add: field_simps)  ERROR
qed

В состоянии доказательства Изабель говорит:

Успешная попытка решить цель с помощью экспортированного правила: n * n

Но потом:

Не удалось применить метод начального доказательства⌂: с помощью этого: n

В чем проблема?. На самом деле я заинтересован в отдельных шагах, чтобы сделать профф, так что я подумал, что Изабель может показать мне путь.

Answer 1

field_simps это хорошо для перестановки терминов, но не очень хорошо для такого рода рассуждений. Когда вы хотите доказать что-то подобное, вам обычно нужно хорошее правило для этого; в этом случае что-то о (строгих) неравенствах и умножении.

Если у вас есть что-то, что выглядит тривиально, но вы не знаете, как это доказать, и / или вы не знаете, как называются соответствующие факты в Изабель, sledgehammer часто полезно:

from assms show "a*b > n*n"
  sledgehammer

  > Sledgehammering... 
  > Proof found... 
  > "cvc4": Try this:
  >   by (metis (no_types, lifting) dual_order.strict_trans gr_implies_not_zero 
  >         linorder_neqE_nat mult.commute nat_0_less_mult_iff 
  >         nat_mult_less_cancel1) (796 ms)

Проблема с доказательствами найдена sledgehammer в том, что, как вы видите, они часто длинные, медленные и не очень освещающие. С точки зрения обслуживания, они также являются несколько хрупкими по отношению к изменениям в теории фона. Тем не менее, это хорошее место для начала, и вы часто можете прочитать соответствующие факты для вашего доказательства из доказательств кувалдой (например, nat_mult_less_cancel1 Вот).

Еще один способ найти соответствующие факты find_theorems команда или, что эквивалентно, панель запросов в IDE Isabelle / jEdit. Если вы делаете

find_theorems "_ * _ > _ * _"

или, что эквивалентно, введите _ * _ > _ * _ на панели запросов вы получаете много выходных данных для чтения, но некоторые важные факты скрываются в конце этого вывода, например mult_strict_mono':

thm mult_strict_mono'
> ?a < ?b ⟹ ?c < ?d ⟹ 0 ≤ ?a ⟹ 0 ≤ ?c ⟹ ?a * ?c < ?b * ?d

Ваше доказательство выглядит так:

from assms show "a*b > n*n"
  by (rule mult_strict_mono') simp_all

simp_all просто выполняет оставшиеся обязательства по доказательству n ≥ 0,

Да, и кстати: тот факт, что вы получаете Successful attempt to solve goal но тогда сообщение об ошибке является следствием нелинейной природы интерактивной Изабель: когда вы пишете byпопытка доказательства отодвигается на задний план, и обработка документа подтверждения затем продолжается, как если бы доказательство прошло успешно. Это сделано для того, чтобы позволить распараллеливание и позволить пользователям продолжать работать с документами, даже если некоторые доказательства будут сломаны.

Successful attempt сообщение исходит от части Изабель, которая вызывается после showи эта часть видит успешное (но все еще ожидающее) доказательство a*b > n*n, Тем не менее, вы сразу же получите сообщение об ошибке от by (simp_all …) говоря, что метод доказательства не удался. В режиме пакетной обработки такие сбои являются более существенными (и более очевидными).