Как вы используете индукцию с тактикой / Изара в Изабель /HOL?

Question

Я пытаюсь понять, почему каждый из приведенных ниже примеров работает или не работает, и более абстрактно, как индукция взаимодействует с тактикой против Изара. Я работаю над 4.3 в Программировании и проверке в Isabelle/HOL (декабрь 2016) для Windows 10 с последней версией Isabelle/HOL (2016-1)

Существует 8 случаев: лемма либо длинная (включает явное имя), либо короткая, структурированная (с использованием assumes а также shows) или неструктурированные (используя стрелки), и доказательство является либо структурированным (Изар), либо неструктурированным (тактическое).

theory Confusing_Induction
  imports Main
begin

(* 4.3 *)
inductive ev :: " nat ⇒ bool " where
  ev0: " ev 0 " |
  evSS: " ev n ⟹ ev (n + 2) "

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

1. Структурированная краткая лемма и структурированное доказательство

(* Hangs/gets stuck/loops on the following *)
(*
lemma assumes a: " ev (Suc(Suc m)) " shows" ev m "
proof(induction  "Suc (Suc m)" arbitrary: " m " rule: ev.induct)
*)

2. Неструктурированная краткая лемма и структурированное доказательство

(* And this one ends up having issues with
   "Illegal application of proof command in state mode" *)
(*
lemma " ev (Suc (Suc m)) ⟹ ev m " 
proof(induction " Suc (Suc m) " arbitrary: " m " rule: ev.induct)
  case ev0
  then show ?case sorry
next
  case (evSS n)
  then show ?case sorry
qed
*)

3. Структурированная длинная лемма и структурированное доказательство

(* And neither of these can apply the induction *)
(*
lemma assumes a1: " ev n " and a2: " n = (Suc (Suc m)) " shows " ev m "
proof (induction " n " arbitrary: " m " rule: ev.induct)

lemma assumes a1: " n = (Suc (Suc m)) " and a2: "ev n " shows " ev m "
proof (induction " n " arbitrary: " m " rule: ev.induct)
*)

(* But this one can ?! *)
(*
lemma assumes a1: " ev n " and a2: " n = (Suc (Suc m)) " shows " ev m "
proof -
  from a1 and a2 show " ev m "
  proof (induction " n " arbitrary: " m " rule: ev.induct)
    case ev0
    then show ?case by simp
  next
    case (evSS n) thus ?case by simp
  qed
qed
*)

4. Неструктурированная длинная лемма и структурированное доказательство

(* And this is the manually expanded form of the Advanced Rule Induciton from 4.4.6 *)
lemma tmp: " ev n ⟹  n = (Suc (Suc m)) ⟹ ev m "
proof (induction " n " arbitrary: " m " rule: ev.induct)
  case ev0 thus ?case by simp
next
  case (evSS n) thus ?case by simp
qed

lemma " ev (Suc (Suc m)) ⟹ ev m "
  using tmp by blast

**5. Структурированная краткая лемма и неструктурированное доказательство *

(* Also gets stuck/hangs *)
(*
lemma assumes a: " ev (Suc (Suc m)) " shows " ev m "
  apply(induction  "Suc (Suc m)" arbitrary: " m " rule: ev.induct)
*)

6. Неструктурированная краткая лемма и неструктурированное доказательство

(* This goes through no problem (``arbitrary: " m "`` seems to be optional, why?)  *)
lemma " ev (Suc(Suc m)) ⟹ ev m "
  apply(induction  "Suc (Suc m)" arbitrary: " m " rule: ev.induct)
  apply(auto)
  done

7. Структурированная длинная лемма и неструктурированное доказательство

(* But both of these "fail to apply the proof method" *)
(*
lemma assumes a1: " n = (Suc (Suc m)) " and a2: " ev n" shows " ev m "
  apply(induction " n " arbitrary: " m " rule: ev.induct)

lemma assumes a1: " ev n "  and a2: " n = (Suc (Suc m)) " shows " ev m "
  apply(induction " n " arbitrary: " m " rule: ev.induct)
*)

8. Неструктурированная длинная лемма и неструктурированное доказательство

lemma " ev n ⟹  n = (Suc (Suc m)) ⟹ ev m "
  apply(induction  " n " arbitrary: " m " rule: ev.induct)
  apply(auto)
  done

end

Answer 1

Я разместил это на [e-mail] и получил следующий ответ от Ларри Полсона. Я воспроизвел это ниже.

---

Спасибо за ваш запрос. Некоторые из ваших проблем связаны с правильной подачей помещения в индукцию, но здесь есть как минимум две большие проблемы.

(* 1. Structured short lemma & structured proof *)
(* Hangs/gets stuck/loops on the following *)

lemma assumes a: "ev (Suc(Suc m))” shows "ev m"
proof(induction  "Suc (Suc m)"  rule: ev.induct)

Делая это таким образом, ваше предположение не видно, цель просто "ev m", поэтому индукция не применима. Но совершенно плохо, что эта ошибка приводит к цикличности индукционного метода.

(* 2. Unstructured short lemma & structured proof *)
(* And this one ends up having issues with
   "Illegal application of proof command in state mode" *)
lemma "ev (Suc (Suc m)) ⟹ ev m" 
proof(induction "Suc (Suc m)"  rule: ev.induct)
  case ev0
  then show ?case
    sorry
next
  case (evSS n)
  then show ?case sorry
qed

Здесь вы получаете ошибку "Не удалось уточнить любую ожидающую цель", которая нарушает остальную часть доказательства. Причина, по которой вы получаете это сообщение об ошибке, заключается в том, что по какой-то причине существует несоответствие между вашими целями и целями, которые Индукционные методы думают, что у вас есть. На самом деле это доказательство может быть написано прямо, но его форма довольно неожиданна. Это тоже очень плохо.

lemma "ev (Suc (Suc m)) ⟹ ev m" 
proof(induction "Suc (Suc m)"  rule: ev.induct)
  show "⋀n. ev n ⟹
         (n = Suc (Suc m) ⟹ ev m) ⟹
         n + 2 = Suc (Suc m) ⟹ ev m"
    by simp
qed

Ваша (3,7,8) такая же проблема, как ваша (1), за исключением того, что метод индукции (правильно) не работает. Ясно, что аргумент "Suc (Suc m)" заставляет индукционный метод зацикливаться по какой-то причине, как в вашем (5).

(* 6. Unstructured short lemma & unstructured proof *)
(* This goes through no problem (``arbitrary: " m "`` seems to be optional, why?)  *)

Это просто, что только некоторые доказательства нуждаются в "произвольном", а именно, когда гипотеза индукции включает переменные, которые должны быть обобщены.

Ваш (7) может быть написано так:

lemma assumes "ev n" and " n = (Suc (Suc m)) " shows " ev m "
  using assms
proof(induction " n " arbitrary: " m " rule: ev.induct)
  case ev0
  then show ?case
    sorry
next
  case (evSS n)
  then show ?case
    sorry
qed

То есть вы можете предоставить предположения для доказательства, как показано ("использование"). Мы даже получаем правильные случаи, делающие это таким образом.

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

Ларри Полсон