How to prove code correctness lemmas with the "undefined" constant

Question

Given I have a very simple definition for code generation. It is only defined for certain cases and throws a runtime exception otherwise.

definition "blubb a = (if P a then True else undefined)"

Now I want to show blubb correct. The case in which the exception is thrown should be ignored (from my point of view, not the mathematical point of view). However, I end up with a subgoal that assumes that some arbitrary value X is undefined. The following lemma is more or less equivalent to the subgoal. I want to show False as I want to ignore the case in which the exception is thrown (i.e., undefined is returned).

lemma "X = undefined ⟹ False"

This is not provable.

  try

Nitpick found a counterexample for card 'a = 1:
 Free variable:
  X = a1

What is the best way to show correctness of functions that might throw exceptions or deal with undefined? This relates to this question.

What exactly do you mean by showing blubb correct? For me that would just be P a ==> blubb, which is trivial with the given definition. — chris
blubb is just an example. For example, blubb a could be an efficient algorithm to calculate distinct a faster than the default implementation, but is just defined for sorted lists (bad example) .... — corny

davidg davidg · Accepted Answer · 2013-03-20T01:27:18

undefined is a constant in Isabelle which you don't know anything about. In particular, you can not in general prove that X ≠ undefined.

If you want to write functions that are only valid for certain inputs, you might consider using the 'a option type, as follows:

definition "blubb a ≡ (if P a then Some True else None)"

and then in your proofs assume that blubb a is defined as follows:

lemma "∃x. blubb a = Some x ⟹ Q (blubb a)"
  ...

or simply:

lemma "a ∈ dom blubb ⟹ Q (blubb a)"
  ...

The value of blubb a can then be extracted using the (blubb a).

How to prove code correctness lemmas with the "undefined" constant

1 Answers