Алгебраические упрощения в Изабель

Question

Я играл с основными примерами доказательств в Изабель.

Рассмотрим следующее простое доказательство:

lemma
    fixes n::nat
    shows "n*(n+1) = n^2 + n"
    by simp

Мне кажется, что такой мощный помощник по доказательствам, как Изабель, должен бытьв состоянии доказать эту лемму без особых указаний.Тем не менее, я был удивлен, обнаружив, что Изабель на самом деле не может применить правило simp здесь (я также пробовал другие "общие" правила, такие как simp_all , auto , force , blast но результат тот же).

Если я заменю последнюю строку на следующую, то получится:

by (simp add: power2_eq_square)

Меня беспокоит то, что мне не нужно было рассказывать системе о конкретном правиле power2_eq_square , чтобы завершить это доказательство.

Играя с похожими тривиальными примерами, яобнаружил, что simp может доказать

n*(n+2)=n*n+n*2

, но не с

n*(n+3)=n*n+n*3

Последний пример доказан

by (simp add: distrib_left)

Этодля меня полная загадка, почему мне нужно указать distrib_left во втором примере, а не в первом (почему?).

Я привел эти примеры не ради себя, но в основном, чтобы проиллюстрировать мой главный вопрос:

Есть ли способ автоматизации Vочищение рутинных алгебраических тождеств, таких как приведенные выше в Изабель?Если нет, то почему бы и нет?Какие технические препятствия?

Answer 1

Ежедневная доказательная работа действительно часто натыкается на «рутинные алгебраические тождества»;но после некоторого практического опыта обычно развивается интуиция, как эффективно решать такие проблемы.Образец, который я разработал за эти годы, например:

context semidom
begin

lemma "a * (b ^ 2 + c) + 2 = a * b * b + c * a + 2"

Типичное доказательственное доказательство начинается с

  apply auto

Тогда ассоциативность и коммутативность также считаются

  apply (auto simp add: ac_simps)

Затем применяются более алгебраические нормализующие правила

  apply (auto simp add: algebra_simps)

Затем последний пробел легко заполняется кувалдой

  apply (simp add: power2_eq_square)

После этого доказательство может быть компактифицировано

  by (simp add: algebra_simps power2_eq_square)

Answer 2

Лемма

lemma power2_eq_square: "a^2 = a * a"

не является хорошим правилом переписывания в целом, так как оно легко взорвет размер терминов.Таким образом, ожидается, что автоматизация, основанная на переписывании терминов, такая как simp, не применит это без вашего ведома.

То, что вы хотите, - это своего рода поисковый запрос , и Изабель обеспечивает это: После написания своей леммы вы можете вызвать инструмент sledgehammer, и он быстро и быстро найдет для вас подтверждение:

Sledgehammering... 
Proof found... 
"z3": Try this: by (simp add: power2_eq_square) (1 ms) 
"cvc4": Try this: by (simp add: power2_eq_square) (5 ms)