Свободные переменные типа в доказательстве по индукции

Question

При попытке доказать леммы о функциях в стиле продолжения прохождения по индукции я столкнулся с проблемой со свободными переменными типа. В моей гипотезе индукции продолжение представляет собой переменную типа , но ее тип включает тип. В результате Isabelle не может унифицировать переменную типа с конкретным типом, когда я пытаюсь применить i.h. Я приготовил этот минимальный пример:

fun add_k :: "nat ⇒ nat ⇒ (nat ⇒ 'a) ⇒ 'a" where 
"add_k 0 m k = k m" | 
"add_k (Suc n) m k = add_k n m (λn'. k (Suc n'))" 

lemma add_k_cps: "∀k. add_k n m k = k (add_k n m id)" 
proof(rule, induction n) 
    case 0 show ?case by simp 
next 
    case (Suc n) 
    have "add_k (Suc n) m k = add_k n m (λn'. k (Suc n'))" by simp 
    also have "… = k (Suc (add_k n m id))" 
     using Suc[where k="(λn'. k (Suc n'))"] by metis 
    also have "… = k (add_k n m (λn'. Suc n'))" 
     using Suc[where k="(λn'. Suc n')"] sorry (* Type unification failed *) 
    also have "… = k (add_k (Suc n) m id)" by simp 
    finally show ?case . 
qed 

В «жалком шаге», явная конкретизация схематических переменной ?k завершается с

Type unification failed 

Failed to meet type constraint: 

Term: Suc :: nat ⇒ nat 
Type: nat ⇒ 'a 

так 'a свободно и не схематичные. Без создания экземпляра упрощение в любом случае не срабатывает, и я не мог найти другие методы, которые могли бы работать.

Поскольку я не могу количественно описать типы, я не вижу никакого способа, как сделать код 'a внутри доказательства. Когда переменная члена становится схематически локально внутри доказательства, почему это не так с переменными в его типе? После того как лемма доказана, они все равно становятся схематическими на уровне теории. Это кажется весьма ограниченным. Может ли вариант сделать это в будущем или существует какое-то присущее ограничение? Альтернативно, существует ли подход, чтобы избежать этой проблемы и все еще сохраняя продолжение схематически полиморфным в доказанной лемме?

Answer 1

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

К счастью, есть способ доказать вашу лемму в стиле CPS без количественного определения типа. Проблема в том, что ваше утверждение недостаточно общее, потому что оно содержит id. Если обобщить, то доказательство работы:

lemma add_k_cps: "add_k n m (k ∘ f) = k (add_k n m f)" 
proof(induction n arbitrary: f) 
    case 0 show ?case by simp 
next 
    case (Suc n) 
    have "add_k (Suc n) m (k ∘ f) = add_k n m (k ∘ (λn'. f (Suc n')))" by(simp add: o_def) 
    also have "… = k (add_k n m (λn'. f (Suc n')))" 
    using Suc.IH[where f="(λn'. f (Suc n'))"] by metis 
    also have "… = k (add_k (Suc n) m f)" by simp 
    finally show ?case . 
qed 

Вы получаете оригинальную теорему назад, если вы выбираете f = id.

Answer 2

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

Специализированное решение для вашей проблемы является первым доказать

lemma add_k_cps_nat: "add_k n m k = k (n + m)" 
    by (induction n arbitrary: m k) auto 

, а затем доказать add_k_cps.

Общий подход: сначала указать экземпляры для фиксированных типов, для которых работает индукция. В примере пример - индукция по nat. А затем выведите доказательство, обобщенное в самом типе.