Кувалда дает тактику недостаточного доказательства

У меня есть

theory Even
imports Main

begin

inductive
  structural_even :: "nat ⇒ bool"
where
  "structural_even 0"
| "structural_even n ⟹ structural_even (Suc(Suc n))"

fun
  computational_even :: "nat ⇒ bool"
where
  "computational_even 0 = True"
| "computational_even (Suc 0) = False"
| "computational_even (Suc(Suc n)) = computational_even n"


lemma "computational_even n ⟹ structural_even n"
proof (induct n rule: computational_even.induct)
 show "computational_even 0 ⟹ structural_even 0"
 by (metis structural_even.intros(1))
next

После доказательства я получаю

goal (3 subgoals):
 1. computational_even 0 ⟹ structural_even 0
 2. computational_even (Suc 0) ⟹ structural_even (Suc 0)
 3. ⋀n. (computational_even n ⟹ structural_even n) ⟹ computational_even (Suc (Suc n)) ⟹ structural_even (Suc (Suc n))

Я получил вызов метиса от кувалды, где

Structure_even.intros(1) = Structure_even 0

я получил

show computational_even 0 ⟹ structural_even 0 
Successful attempt to solve goal by exported rule:
 computational_even 0 ⟹ structural_even 0 
proof (state): depth 0

потом. Однако после следующего я получаю

goal (3 subgoals):
 1. computational_even 0 ⟹ computational_even 0
 2. computational_even (Suc 0) ⟹ structural_even (Suc 0)
 3. ⋀n. (computational_even n ⟹ structural_even n) ⟹ computational_even (Suc (Suc n)) ⟹ structural_even (Suc (Suc n))

Таким образом, есть тривиальная остаточная подцель в 1., несмотря на то, что система сказала «Успешная попытка решить цель по экспортированному правилу».

Почему это происходит, и как я могу это исправить?


isabelle isar
person Gergely    schedule 02.02.2016    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Sledgehammer нашел правильное доказательство (хотя вместо этого вы можете использовать simp). На самом деле вы можете продолжить со второй и третьей подцелями (которые будут сведены к таким же новым подцелям, как и для № 1, после того, как вы их докажете) и, наконец, завершить доказательство с помощью qed.

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

show "computational_even 0 ⟹ structural_even 0"

заменяется эквивалентным

presume "computational_even 0"
show "structural_even 0"

Ваше доказательство показывает, что structural_even 0 истинно, как только computational_even 0 истинно, но Изабель «не имеет ни малейшего представления», почему последнее истинно. Поэтому у вас остается новая подцель, состоящая в том, что предположение, сформулированное в доказательстве, может быть выведено из предположения, сформулированного в подцели. Эта подцель будет обрабатываться qed, которая завершает доказательство с учетом предположений.

Кстати, предположение для этого случая вообще не требуется, потому что structural_even 0 истинно по своему определению. Так что предположение можно смело удалить, оставив только

show "structural_even 0"

Более того, с помощью presume можно указывать произвольные предположения, но доказывать их придется позже. Например, вы можете доказать цель

presume "computational_even (Suc 0)"
show "structural_even 0"

но тогда вам придется доказать (ложную) цель computational_even 0 ⟹ computational_even (Suc 0).

Чтобы объединить предположение с предпосылкой цели, вместо этого используется assume:

assume "computational_even 0"
show "structural_even 0"

В этом случае нет необходимости доказывать предположение о подцели (это уже делается на шаге объединения с assume). В результате после завершения доказательства подцели останется только 2 подцели, как вы и ожидали.

В качестве бесплатного бонуса, когда assume используется с неправильным предположением (например, как в более раннем ошибочном случае, computational_even (Suc 0)), Изабель будет жаловаться, что соответствующее утверждение show не может уточнить какую-либо ожидающую цель, и вы не сможете продолжить.

person Alexander Kogtenkov    schedule 02.02.2016