Free type variables in proof by induction

Question

While trying to prove lemmas about functions in continuation-passing style by induction I have come across a problem with free type variables. In my induction hypothesis, the continuation is a schematic variable but its type involves a free type variable. As a result Isabelle is not able to unify the type variable with a concrete type when I try to apply the i.h. I have cooked up this minimal example:

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

In the "sorry step", the explicit instantiation of the schematic variable ?k fails with

Type unification failed

Failed to meet type constraint:

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

since 'a is free and not schematic. Without the instantiation the simplifier fails anyway and I couldn't find other methods that would work.

Since I cannot quantify over types, I don't see any way how to make 'a schematic inside the proof. When a term variable becomes schematic locally inside a proof, why isn't this the case with variables in its type too? After the lemma has been proved, they become schematic at the theory level anyway. This seems quite limiting. Could an option to do this be implemented in the future or is there some inherent limitation? Alternatively, is there an approach to avoid this problem and still keeping the continuation schematically polymorphic in the proven lemma?

Andreas Lochbihler Andreas Lochbihler · Accepted Answer · 2016-12-07T05:04:50

Free type variables become schematic in a theorem when the theorem is exported from the block in which the type variables have been fixed. In particular, you cannot quantify over type variables in a block and then instantiate the type variable within the block, as you are trying to do in your induction. Arbitrary quantification over types leads to inconsistencies in HOL, so there is little hope that this could be changed.

Fortunately, there is a way to prove your lemma in CPS style without type quantification. The problem is that your statement is not general enough, because it contains id. If you generalise it, then the proof works:

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

You get your original theorem back, if you choose f = id.

Free type variables in proof by induction

2 Answers