CODEWITHSUNDEEP
isabelle
Ferd
Ferd

Reputation: 147

Free type variables in proof by induction

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?

Upvotes: 3

Views: 472

Answers (2)

Johannes
Johannes

Reputation: 161

This is an inherent limitation how induction works in HOL. Induction is a rule in HOL, so it is not possible to generalize any types in the induction hypothesis.

A specialized solution for your problem is to first prove

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

and then prove add_k_cps.

A general approach is: prove instances for fixed types first, for which the induction works. In the example case is is an induction by nat. And then derive a proof generalized in the type itself.

Upvotes: 4

Andreas Lochbihler
Andreas Lochbihler

Reputation: 5108

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.

Upvotes: 4

Related Questions