(Update: я начинаю на них, а потом кто-то дает ответ после того, как я работал совсем немного, так что я иду вперед и поставить то, что я сделал
. То, что я хотел бы знать, пришел в другой ответ, который является использование term ?thesis в доказательстве, чтобы помочь совпасть сообщение об ошибке с тем, где проблема.
Может быть, мой ответ здесь добавляет немного контекста для другого ответа.)
Ниже я использую !! для мета-логики all, вместо \<And>.
Вы вошли в таинственную мета-логику-vs-object-logic-zone. Небольшое понимание делает вещи намного менее загадочными.
Внизу, я даю вам способ показать использование скрытой функции Trueprop, которая отнимает некоторые тайны.
- объяснить немного о 3 чистых мета-логических операторов, а также их отношения OTO в HOL объектно-логики,
- дают 3 различные формы вашего
lemma, начиная с вашей,
- где
show ?thesis из третья форма, наконец, приемлема для двигателя доказательства.
Я не совсем разбираюсь здесь. Для меня много раз неважно, что я полностью понимаю все, но важно, чтобы я не был полностью в темноте о типах используемых в мета-логике и объектно-логических функциях, которые находятся в основе из всего этого.
HOL BOOL, чисто проп и Trueprop :: (BOOL => проп), чтобы связать Hol в Pure
Обозначение для функции Trueprop обычно скрыты. Вы можете определить нотацию, чтобы увидеть, где она применяется на панели вывода.Я определяю notation здесь с некоторыми заявляет:
notation (output) Trueprop ("_:@T" [1000] 999)
declare[[show_brackets=false, show_types, show_sorts=false, show_consts]]
Вот тип Trueprop:
term "Trueprop :: bool => prop"
В вашем lemma ниже, потому что вы используете --> вместо ==>, вывод показывает, что ряд последствия имеют тип bool, и его принуждают к prop по Trueprop, как показано на рисунке :@T.
HOL логические соединители имеют тип bool. Например,
term "op --> :: (bool => bool => bool)"
term "A --> B :: bool"
3 основные операторы Pure: эк (==), имп (==>), и все (!!)
Здесь я подтверждаю, их типы. CNTL-клик на них, чтобы доставить вас к ним. Небольшое осознание вовлеченных типов может сделать сообщения об ошибках менее загадочными.
term "Pure.eq :: 'a => 'a => prop"
term "Pure.imp :: prop => prop => prop"
term "Pure.all :: ('a => prop) => prop"
Слишком много, чтобы попробовать и сказать обо всем этом. Кому-то нужно написать учебник для логических новичков, как и я, объясняя логику Изабель/HOL, начиная с Pure.
проп против BOOL
Свободные переменные неявно, повсеместно количественно, так что я могу избавиться от использования !!. В результате тип члена изменяется от prop до bool. Включение информации о типе может помочь понять сообщения об ошибках типа.
term "(!! d k l :: int. 0 < d --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1
--> -(2 * l) < 2 * k - 1 --> k ≤ l
--> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)) :: prop"
term "(0 < (d::int) --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1
--> -(2 * l) < 2 * k - 1 --> k ≤ l
--> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)) :: bool"
Ваш оригинальный
Вы начинаете с ?thesis :: INT => Int => Int => bool`.
declare[[show_types=false]]
lemma "!! d k l :: int. 0 < d --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1
--> -(2 * l) < 2 * k - 1 --> k ≤ l
--> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)" (*
1. !!d k l. (0 < d --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1 -->
- (2 * l) < 2 * k - 1 --> k ≤ l -->
d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)):@T *)
proof -
fix d k l ::int
assume " ¬ 2 * k + 1 ≤ 2 * l" "k ≤ l"
then have "k = l" by simp
then have "d * (4 * l - 1) = d * (4 * k - 1) " by auto
moreover have "d * (2 * l - 2) + d * (2 * l) + d = d * (4 * l - 1)" by algebra
ultimately have "d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)" by auto
from this
term "?thesis" (*
"λd k l. 0 < d --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1
--> - (2 * l) < 2 * k - 1
--> k ≤ l --> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)"
:: "int => int => int => bool" *)
show ?thesis (*
Type unification failed: Clash of types "_ => _" and "bool"
Type error in application: incompatible operand type
Operator: Trueprop :: bool => prop
Operand: ?thesis∷int => int => int => bool ::
int => int => int => bool
Coercion Inference:
Local coercion insertion on the operand failed:
No coercion known for type constructors: "fun" and "bool" *)
oops
Избавление от явного использования !!
я избавиться от !!, и теперь я получаю ?thesis :: bool и меняет сообщение об ошибке в очень общем, разочарование ошибки, «не в состоянии уточнить любые неисполненные Цель". Это как-то означает, что я не согласен с тем, что я собираюсь сделать с show, с тем, что движок проверки зрения видит в качестве цели (я думаю).
lemma "0 < (d::int)
--> ¬ 2 * k + 1 ≤ 2 * l
--> 2 * l ≠ 1
--> - (2 * l) < 2 * k - 1 --> k ≤ l
--> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)"
proof -
fix d k l ::int
assume " ¬ 2 * k + 1 ≤ 2 * l" "k ≤ l"
then have "k=l" by simp
then have "d * (4 * l - 1) = d * (4 * k - 1) " by auto
moreover have "d * (2 * l - 2) + d * (2 * l) + d = d * (4 * l - 1)" by algebra
ultimately have "d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)" by auto
from this
term "?thesis" (*
"0 < d --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1 --> - (2 * l) < 2 * k - 1
--> k ≤ l --> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)"
:: "bool"
*)
show ?thesis (*
Failed to refine any pending goal
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
((¬ 2 * ?ka2 + 1 ≤ 2 * ?la2):@T) ==>
((?ka2 ≤ ?la2):@T) ==>
(0 < d --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1 --> - (2 * l) < 2 * k - 1
--> k ≤ l --> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)):@T *)
oops
Теперь ==> вместо -> и show ?thesis, который получает принял
И теперь я заменяю --> с ==>. Тип ?thesis по-прежнему bool, и теперь он принимает show ?thesis.
lemma "0 < (d::int)
==> ¬ 2 * k + 1 ≤ 2 * l
==> 2 * l ≠ 1
==> - (2 * l) < 2 * k - 1 ==> k ≤ l
==> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)"
proof -
fix d k l ::int
assume " ¬ 2 * k + 1 ≤ 2 * l" "k ≤ l"
then have "k=l" by simp
then have "d * (4 * l - 1) = d * (4 * k - 1) " by auto
moreover have "d * (2 * l - 2) + d * (2 * l) + d = d * (4 * l - 1)" by algebra
ultimately have "d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)" by auto
from this
term "?thesis" (*
"d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)" :: "bool"*)
show ?thesis (*
goal (1 subgoal):
1. (d * ((2::int) * k - (2::int)) + d * ((2::int) * l) + d =
d * ((4::int) * k - (1::int))):@T *)
oops
Не нужно больше напрягать мой мозг сегодня. Есть тонкости в том, что мы должны делать, чтобы дать доказательство двигателю фактов, которые он хочет, в том виде, в котором они им нужны. Я могу посмотреть на другой ответ и разобраться в деталях.