Почему simp не может применить метод начального доказательства, когда взрыв успешно работает с теми же фактами?

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

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

by (blast intro: DH_bdiam2_f Fbox2_R l2)

Это работает отлично и денди, однако, если я попытаюсь использовать простое добавление тех же правил, например:

by (simp only: DH_bdiam2_f Fbox2_R l2)

Я получаю сообщение об ошибке, что ни одно из правил не применимо

Failed to apply initial proof method⌂:

Что именно происходит? Я ожидал, что simp либо завершится, либо истечет время ожидания, но, конечно, не это. Что мне не хватает?


theorem-proving isabelle
person Naurgul    schedule 09.09.2016    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Это сообщение об ошибке, которое вы получаете, когда тактика не дает шага доказательства. Для simp это тот случай, когда ни одно правило не соответствует (т.е. перезапись ни с DH_bdiam2_f ... невозможна). Глядя на ваш код, эти правила исходят из индуктивного предиката. Обычно они не подходят для переписывания (= упрощения) правил. В разделе Programming and Proving in Isabelle/HOL разбросаны подсказки о подходящих правилах упрощения и введения, а также пояснения о подходящей тактике.

person larsrh    schedule 09.09.2016
comment
Спасибо за Ваш ответ. Как вы думаете, можно ли отредактировать мою теорию, чтобы упростить работу с симпами, или мне следует отказаться от симпов и сосредоточиться на других тактиках? Причина, по которой я так забочусь о simp, в первую очередь заключается в том, что он единственный, который обеспечивает удобочитаемую трассировку доказательства. - person Naurgul; 10.09.2016
comment
Я думаю, вы должны использовать другие инструменты. Чтобы получить удобочитаемые доказательства, я предлагаю использовать (структурированные) доказательства Isar. - person larsrh; 11.09.2016
comment
Я попытался использовать экспериментальный режим проверки isar от sledgehammer, и он дал интересные результаты. Любые дальнейшие советы приветствуются. - person Naurgul; 12.09.2016
comment
Вы можете написать доказательства Изара вручную. Если вы хотите что-то понятное для человека, вы не можете использовать автоматизированные инструменты для его создания. - person larsrh; 13.09.2016
comment
Спасибо за вашу помощь, это ценится. - person Naurgul; 14.09.2016