Неравенство рассуждения в Isabelle

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 

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

Успешная попытка решить задачу по экспортируемой правилу: п * п < * б

Но тогда:

Не удалось применить первоначальное доказательство method⌂: с помощью этого: п < п < б цель (1 подцель): 1. п * п < а * б

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

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, заключается в том, что, как вы можете видеть, они часто бывают длинными, медленными и не очень освещающими. На стороне обслуживания вещей они также несколько хрупкие w.r.t. изменения в теории фона. Тем не менее, это хорошее место для начала, и вы можете часто читать соответствующие факты для вашего доказательства из доказательств кувалды (например, здесь).

Другим способом найти соответствующие факты является команда 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 но сообщение об ошибке является следствием нелинейного характера интерактивного Isabelle: Когда вы пишете by, попытка доказательства разветвляется на задний план и обработка подтверждающего документа впоследствии продолжается так, как будто доказательство преуспело. Это делается для того, чтобы разрешить параллелизацию и позволить пользователям продолжать работу с документами, даже если некоторые доказательства нарушены.

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