Построение полезных лемм - PullRequest
Новая
       6

Построение полезных лемм

0 голосов
/ 10 октября 2018

В учебном пособии Программирование и проверка в Изабель / HOL есть пошаговое объяснение доказательства обратного изменения списка в два раза, что дает исходный список (2.2.4 Процесс проверки).

theorem rev_rev [simp]: "rev(rev xs) = xs"
apply(induction xs)
apply(auto)

После автоматического шага остается одна подцель: 

1. V x1 xs.
     rev (rev xs) = xs =⇒
     rev (app (rev xs) (Cons x1 Nil)) = Cons x1 xs

Затем автор говорит: «Чтобы еще больше упростить эту подцель, лемма напрашивается сама собой». И представляет rev_app.приведенная ниже лемма: 

lemma rev_app [simp]: "rev(app xs ys) = app (rev ys) (rev xs)"

Является ли это просто интуицией и практикой, как в случае ручных и бумажных доказательств, которые позволяют увидеть, как подзадача 1. может быть упрощена, и придумать лемму, подобную rev_app?Я просто не могу понять, как эта лемма предлагает себя.

1 Ответ

0 голосов
/ 10 октября 2018

Это действительно сложно для людей, незнакомых с формальными доказательствами.Со временем, вы узнаете много эвристических подходов, чтобы придумать потенциальные леммы.

В этом случае (чисто эквалайзерное рассуждение) эвристика обычно работает, рассматривая вовлеченные константы подцелей.

Например, основная лемма описывает свойство rev / rev.Однако подцели нужно что-то около rev / app.Это то, что говорит вам, что вам нужна лемма об этих двух.

Остальное, к сожалению, можно описать только как «человеческую изобретательность»: увидеть, что rev(app xs ys) = app (rev ys) (rev xs) является разумным свойством для rev/app.

Существуют различные исследования по автоматическому обнаружению таких свойств, например IsaHipster .

...