Isabelle auto prover работает над леммой, зависает на специальном футляре

Question

Почему висит вторая «легальная» проверка леммы? Вторая лемма является частным случаем первого.

primrec ListSumTAux :: "nat list ⇒ nat ⇒ nat" where 
    "ListSumTAux []  n = n" | 
    "ListSumTAux (x#xs) n = ListSumTAux xs (n+x)" 

    lemma ListSumTAux_1 : " ∀a b. ListSumTAux xs (a+b) = a + ListSumTAux xs b" 
    apply (induct xs) 
    apply (auto)  (* Works fine *) 
    done 

    lemma ListSumTAux_2 : "∀ a. ListSumTAux xs a = a + ListSumTAux xs 0 " 
    apply (induct xs) 
    apply (auto)  (* Hangs on this *) 
    oops 

Answer 1

Прежде всего: это неудобно государственные цели с квантором HOL ∀. Свободные переменные в целях неявно универсально оцениваются в любом случае, поэтому вы можете просто оставить ∀. Вы, однако, сказать команду induction универсально количественной оценки этих переменных в шаг индукции с помощью arbitrary:

lemma ListSumTAux_1 : "ListSumTAux xs (a+b) = a + ListSumTAux xs b" 
    apply (induct xs arbitrary: a b) 
    apply (auto) 
done 

Теперь, чтобы ответить на ваш вопрос: auto застревает, потому что ваша гипотеза индукции имеет вид

⋀a. ListSumTAux xs a = a + ListSumTAux xs 0 

auto использует упрощение Isabelle, которое принимает это как правило перезаписи. Тем не менее, вы заметите, что левая сторона этого правила соответствует правой Hande стороны этого цикла, что приводит к бесконечной последовательности переписывания

ListSumTAux xs a → a + ListSumTAux xs 0 → a + (0 + ListSumTAux xs 0) → 
    a + (0 + (0 + ListSumTAux xs 0)) 

Когда происходят такие ситуации, есть несколько вещей, которые вы можете сделать :

1. вы можете сделать структурированную Изар доказательства и делать вещи вручную
2. вы можете попробовать перевернуть уравнение в вопросе, то есть записать цель как a + ListSumTAux xs 0 = ListSumTAux xs a. Тогда левая сторона больше не соответствует правой части.
3. Вы можете ввести дополнительное помещение, такое как a ≠ 0, к уравнению, которое предотвращает цикл прокрутки.

В любом случае, вы не сможете доказать свою цель таким образом, потому что это слишком специфичны: если вы утверждаете вашу цель как ListSumTAux xs a = a + ListSumTAux xs 0, то вы будете иметь в индукции в 0 как хорошо, но конечно, ваш аккумулятор не всегда будет 0.

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