CODEWITHSUNDEEP
functional-programmingisabelletheorem-proving
Ankit Gupta
Ankit Gupta

Reputation: 121

How to extract the instantiated variable in Isabelle?

I am trying to prove the following in Isabelle:

theorem map_fold: "∃h b. (map f xs)  = foldr h xs b"
apply (induction xs)
apply auto
done

How can I get the instantiated value of h and b?

Upvotes: 2

Views: 480

Answers (2)

Manuel Eberl
Manuel Eberl

Reputation: 8248

One way is to use SOME:

h := SOME h. ∃b. map f xs = foldr h xs b
b := SOME b. map f xs = foldr h xs b

Using your map_fold theorem and some fiddling around with someI_ex, you could prove that with these definitions, map f xs = foldr h xs b does indeed hold.

However, while this logically gives you values of h and b, I expect you will not be very satisfied with them, because you don't actualls see what h and b are; and there is no way (logically) to do that either.

In some cases, you can also formulate a theorem stating “There are f, xs such that no h, b exist with map f xs = foldr h xs b” and get nitpick to find a counterexample for that statement, but this case is too complicated for nitpick, as it would have to find a function on an infinite domain that depends on another function on an infinite domain.

I do not think there is a way for you to actually get the existential witnesses h and b out of the theorem you proved as concrete values. You will just have to find them yourself by inspection of the induction cases and find that they are h = λx xs. f x # xs and b = [].

This is by far the easiest solution.

Update: Proof extraction

Upon re-reading this thread today, I actually remembered that proof extraction does exist in Isabelle. It requires explicit proof terms to be computed for all theorems, so you need to start Isabelle with isabelle jedit -l HOL-Proofs. Then you can do this:

theorem map_fold: "∃h b. (map f xs)  = foldr h xs b"
  by (induction xs) auto

extract map_fold

This defines you a constant map_fold of type ('a ⇒ 'b) ⇒ 'a list ⇒ ('a ⇒ 'b list ⇒ 'b list) × 'b list, i.e. given a mapping function and a list, it gives you the function and the initial state you have to put into the foldr in order to get the same result. You can look at the definition using thm map_fold_def. Simplifying it a bit, it looks like this:

map_fold f xs = 
    rec_list (λx xa. default, []) (λx xa H. (λa b. f a # map f xa, default)) xs

This is a bit difficult to read, but you can see the [] and the f a # map f xa.

Unfortunately, proof terms get pretty big, so I doubt this will be of much use for anything more than toy examples.

Upvotes: 2

Brian Huffman
Brian Huffman

Reputation: 981

An approach that sometimes works for this purpose is to state a schematic lemma:

schematic_lemma "map f xs = foldr ?h xs ?b"
apply (induct xs)
apply simp
...

Methods like simp or rule can instantiate schematic variables during the proof (a result of unification). If you are able to complete the proof, then you can just look at the resulting lemma to see what the final instantiations were.

Beware that schematic variables can be a bit tricky: sometimes simp will instantiate a schematic variable in a way that makes the current goal trivially provable, but simultaneously makes other subgoals unsolvable.

In this specific case, Isabelle is able to instantiate ?b with no problem, but it can't determine ?h by unification. In general, schematic variables with function types are much trickier to handle.

In the end, I did something like what Manuel suggested: First, state a lemma with ordinary variables (lemma "map f xs = foldr h xs b"). Then see where the proof by induction gets stuck, and incrementally refine the statement until it is provable.

Upvotes: 3

Related Questions