Sledgehammer дает достаточных доказательств Tactic

Question

У меня есть

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)) 

я получил звонок от Metis кувалдой где

structural_even.intros (1) = 0 structural_even

Я получаю

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., несмотря на то, система говорит «Успешная попытка решить задачу путем экспортируемого правила».

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

Answer 1

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

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

show "computational_even 0 ⟹ structural_even 0" 

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

presume "computational_even 0" 
show "structural_even 0" 

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

BTW, предположение для этого случая вообще не требуется, поскольку 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)), Isabelle будет жаловаться, что соответствующий show оператор не может уточнить любые отложенные цели, и вы не сможете продолжать.