Принудительно отчетливость типов данных

Question

я определил следующий тип данных в Isabelle

datatype bc_t = B | C 

и не видят, как доказать следующую основную лемму

lemma "∀ x::bc_t . (x=B ⟶ x≠C)" 

В предположении B≠C доказательство проходит через:

lemma "⟦B≠C; x=B⟧ ⟹ x≠C" 
by metis 

Есть ли способ доказать лемму без явного предположения ион, что B и C различны?

Обновление: Как Мануэль Eberl предложил в комментарии к ответу, проблема была вызвана ошибочным правилом упрощения (лемма с атрибутом [simp], опущенным здесь), который сделал петлю упрощения процесса и, таким образом, игнорируемым автоматически генерируются правила упрощения B≠C, C≠B (найдено в bs_t.simps, как указал Крис в его ответе). Как и в ответе gc44, simp достаточно, чтобы доказать лемму в нормальной ситуации.

Answer 1

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

datatype bc_t = B | C 

lemma "∀ x::bc_t . (x = B ⟶ x ~= C)" 
try0 
using[[simp_trace]] 
using [[simp_trace_depth_limit=100]] 
apply(simp) 
done 

lemma "∀ x::bc_t . (x = B ⟶ x ~= C)" 
sledgehammer 
by (metis bc_t.distinct(1)) 

Я использовал try0, потому что я был в "Plugin Options/Isabelle/General" непроверенную Auto Methods. Много раз в вариантах у меня есть все флажки с автоматическими инструментами, отличные от Sledgehammer.

Вы можете использовать sledgehammer, как я покажу там, или вы можете использовать его в панели Sledgehammer PIDE. С simp_trace, когда вы наводите курсор на строку apply(simp), вы можете узнать, как это доказал метод simp, который будет основан на правилах замены.

Update 140108_1305

В авто инструменты важны для помогают нам работать быстро, но это также важно, чтобы иногда понять основную логику доказательства. Здесь можно использовать simp_trace и другие атрибуты метода simp. Прочтите tutorial.pdf, prog-prove.pdf и isar-ref.pdf для получения дополнительной информации и уроков по использованию simp.

Три таких атрибута для управления методом simp: add, del и only.

В вашем примере я хочу использовать simp_trace, а также only, чтобы четко указать, какие правила используются, чтобы помочь мне понять логику.

metis Удостоверение от Sledgehammer заставляет предположить, что simp может использовать только некоторые правила. Я смотрю на трассировку simp, и пусть simp использует только правила, которые я могу вырезать и вставить с панели управления. Я считаю 4 названных правила, и на самом деле это не то, что стоит делать, хотя мне пришлось это выяснить.

[Update 140101_0745: Попытка не более чем анализировать ситуацию, я в конечном итоге с помощью del, потому что моя Грандиозная схема использования only не вырабатывал. С simp only вместо simp del метод apply с ошибкой, что означает, что он не может упростить цель только с этими четырьмя правилами. Это не относится к auto simp only вместо simp only. Метод auto не ограничен в пути simp есть, и это может сделать много вещей, он не будет рассказывать вам о, например, вызывая blast.]

lemma "∀ x::bc_t . (x = B ⟶ x ~= C)"  
using[[simp_trace]] 
using [[simp_trace_depth_limit=100]] 
apply(simp del: 
    bc_t.distinct(1) 
    simp_thms(8) 
    simp_thms(17) 
    simp_thms(35) 
    ) 
oops 

Ну, теперь, когда я смотрю на новейшем simp след, есть еще более simp правил. У упрощения есть более 1 камня, чтобы убить птицу, поэтому я сдаюсь.

Следует помнить, что вы можете использовать simp с методами, такими как auto и fastforce, например apply(auto simp add: stufferThm). С auto, в частности, если правил simp недостаточно, чтобы доказать теорему, может потребоваться использовать blast, который не будет отображаться на трассе simp. Это важно знать при использовании only, поэтому вы не находитесь под впечатлениями, что правила simp - это все, что необходимо для доказательства, которое найдено по auto.

Здесь я комментирую ваш комментарий ниже.

Если simp остается фиолетовым очень долго, ему приходится делать огромное количество упрощений, или он находится в замкнутом цикле, как упоминает Эберль. Или плохо. Я не считаю, что 40 секунд simp подтверждают хорошее доказательство.

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

Использование try0, и когда никаких доказательств не найдено, это даст вам список автоматических методов доказательства экспериментировать с, как force, fastforce, auto и т.д. Если simp зацикливается с auto, вы можете попробовать его с fastforce , Экспериментальные подсчеты для многих.

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

Обновление 140109_0750: Предоставление обобщений всегда сопряжено с риском. Развертывание определения будет много раз мешать Кувалдеру найти доказательство. Кувалда хорошо работает, сопоставляя теоремы высокого уровня, поэтому безнадежно расширенная формула будет много раз обрекать ее на неудачу. Даже чрезвычайно расширенная формула может привести к тому, что другие автоматические методы не смогут найти доказательства. Однако для вещей вычислительного характера, основанных на уравнениях, расширяющиеся определения могут позволить simp полностью уменьшить огромное сложное выражение. Вы должны знать, когда их удерживать, и когда их разворачивать. Самое замечательное в том, что легко пробовать много вещей достаточно быстро.]

definition stuffTrue :: "bool" where 
    "stuffTrue = True" 

theorem "stuffTrue" 
    apply(unfold stuffTrue_def) 
    by(simp) 

Вопрос не в том, что это тривиально. Простые вещи не всегда легко доказать. Что тривиально - это типизация, которая требуется, когда вы узнаете, как использовать автоматические инструменты.

Answer 2

При создании datatype куча правил упрощения будет выведена автоматически (под именем <datatype-name>.simps) и добавлена ​​в упрощение. В вашем примере это будет

datatype bc_t = B | C 
thm bc_t.simps 

B ≠ C 
C ≠ B 
(case B of B ⇒ ?f1.0 | C ⇒ ?f2.0) = ?f1.0 
(case C of B ⇒ ?f1.0 | C ⇒ ?f2.0) = ?f2.0 
bc_t_rec ?f1.0 ?f2.0 B = ?f1.0 
bc_t_rec ?f1.0 ?f2.0 C = ?f2. 

, который включает в себя тот факт, B и C различны. (Подмножество этих фактов, только говорящих об отличимости, доступно через имя bc_t.distinct.)

С помощью этих правил упрощения можно решить вашу лемм by simp.