Преобразование свободных переменных связанных переменных

Question

Я хочу, чтобы доказать следующую лемму

lemma assumes "f (w+n) - f w/n ≤ g (w+n)" 
shows "∀n. (f (w+n) - f w)/n ≤ g (w+n)" 

Я предположил, что это было бы очень просто, однако это оказывается сложнее, чем я думал, что первый. Из моих мыслей неравенство в предположении справедливо для всех w и n, поэтому результат, который я пытаюсь доказать, также должен быть справедливым.

Я искал документацию и работал кувалдой, однако я не был успешным.

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

Answer 1

Как уже было сказано ранее, ваше предложение не выполняется. Классы типов, однако, не имеют к этому никакого отношения; это очень фундаментальная логическая проблема.

Прежде всего, следует отметить, что ваше предположение было, вероятно, должно быть

(f (w+n) - f w)/n ≤ g (w+n) 

, как вы написали, то это означает

f (w+n) - (f w/n) ≤ g (w+n) 

Но даже если вы исправить это, это все еще не выполняется, и причина этого заключается в том, что означают свободные переменные. Конвенция в Изабель заключается в том, что свободные переменные (которые не связаны нигде в контексте) в лемме неявно универсально квалифицированы. Это обычно конвенция в математике; мы пишем a + b = b + a, а не ∀a b. a + b = b + a.

поэтому Ваша лемма означает, что это Isabelle:

∀f g w n. (f (w+n) - f w)/n ≤ g (w+n) ⟹ ∀n. (f (w+n) - f w)/n ≤ g (w+n) 

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

lemma "(f (w+n) - f w)/n ≤ g (w+n)" 

то, что уже означает, что это имеет место для всех n (по той же конвенции). Но когда вы просто берете это и проецируете его в предположение о другой лемме, то одно и то же соглашение приводит к противоположному значению: «для любого n, если предположение верно, тогда ...».

Если вы действительно хотите высказать предположение таким образом, что оно имеет место для всеn, вы должны написать

lemma assumes "⋀n. (f (w+n) - f w)/n ≤ g (w+n)" 
     shows "∀n. (f (w+n) - f w)/n ≤ g (w+n)" 

Тогда доказательство только одно применение правила allI и может быть делается автоматически с blast или auto. Заметим, что ⋀ является универсальным классификатором Изабеллы в мета логике. Его значение аналогично тому, когда в математике вы говорите «Исправьте некоторый n». или «Пусть n - фиксированное, но произвольное число».

Answer 2

(Формулы HOL для этого другого ответа на лимиты неверны. У меня нет доступа к этой учетной записи пользователя. Я отправил отредактированный ответ, но я не знаю, будет ли он отображаться. y x вместо x y. Я не исправить, потому что я не знаю, как это сделать. Я просто сделал несколько дополнительных замечаний в верхней части.)

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

Когда я подключаю вашу лемм, Нитчик говорит мне об этом d a встречный пример:

Auto Nitpick found a counterexample for 
card "'a∷{inverse,minus,plus,ord}" = 2: 

Это потому, что у меня включен режим «Авто Nitpick». Перейдите на страницу параметров, затем настройки «Изабель/Общие». Обычно я включил «Auto Nitpick», «Auto Quickcheck» и «Auto Solve Direct».

Я только что заметил, что у меня нет «Авто-методов». По какой-то причине, по-видимому, он слишком сильно всасывал слишком много CPU, но, как правило, это тоже полезно.

Если ваш процессор работает с полным отверстием, и вы не думаете, что это должно быть, тогда вы отключите «Авто методы», чтобы узнать, есть ли проблема. Я не использую «Auto Sledgehammer». Это довольно требовательно к процессору, и я запускаю его напрямую.

Auto Nitpick спасает меня от многих неприятностей. Он просто появляется, когда я этого не ожидаю. По какой-то причине я никогда не задумывался о том, чтобы запустить его прямо. Вы делаете это с nitpick. Подробнее см. В PDF-файле.

Что касается того, почему ваша лемма терпит неудачу, я не знаю. Может быть, кто-то еще узнает.

То, что я сейчас ищу, - это сортировка для ваших переменных. В конце концов, вам нужно получить представление о типах и типах классов. Существуют различные способы получения дополнительной информации. Я использую declare, где иногда я получаю слишком много информации:

declare[[show_sorts=true, show_consts=true]] 

В панели вывода, я вижу, что он показал в контрпример. Рода вашего типа заключается в следующем:

'a :: {inverse,minus,plus,ord} 

Ваши переменные, например w, являются w :: 'a :: {inverse,minus,plus,ord}. Эти 4 вида описывают алгебраические свойства, которые имеют ваши переменные. Вам нужно понять, какие ограничения влечет за собой использование ваших функций. Вам могут понадобиться дополнительные сорта, чтобы получить то, что вы хотите.