Email Gateway (Jul 20 2025 at 16:45): Email Gateway (Jul 20 2025 at 16:45):From: Elliot Bobrow <ebobrow@g.hmc.edu>
Hello Isabelle developers,
I've noticed that Isabelle's logic for case statements and fun
definitions automatically defaults to returning undefined for unspecified
inputs:
fun f :: "'a option \<Rightarrow> nat" where "f x = (case x of Some _
\<Rightarrow> 1)"
lemma "f None = undefined" by simp
fun f' :: "'a option \<Rightarrow> nat" where "f' (Some _) = 1"
lemma "f' None = undefined" by (meson f'.elims option.distinct(1))
However, the same does not hold for primrec definitions:
primrec (nonexhaustive) f'' :: "'a option \<Rightarrow> nat" where "f''
(Some _) = 0"
lemma "f'' None = undefined" oops
Is there a reason for this? It seems it would be good to be consistent
here, and the functions would still be primitive recursive. Having
undefined as a default case seems like a good idea for the sake of
clarity and explicitness.
This has come up in a research project (collaborators CC'd) which involves
proving a number of functions primitive recursive according to a
user-defined predicate. We are doing this by constructing equivalent
functions out of known primitive recursive functions and proving them
equivalent on all inputs. However, it is impossible to do this for e.g.
nth because an equivalent function must always return [] ! n for
out-of-bounds inputs. This is a function of n and we do not know it to be
primitive recursive, so we're stuck. If instead we had that [] ! n
evaluates to undefined, the problem becomes trivial by returning the
constant undefined on out-of-bounds inputs, which we know to be primitive
recursive because it is a constant. This might not be the only instance
where the current behavior makes it more difficult/impossible to reason
about equality.
Elliot
Email Gateway (Aug 11 2025 at 15:23):From: Dmitriy Traytel via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
Hi Elliot,
For your simplified example the property actually holds:
primrec (nonexhaustive) f'' :: "'a option \<Rightarrow> nat" where "f'' (Some _) = 0"
lemma "f'' None = undefined"
unfolding f''_def by simp
This is not exported to the user on purpose, but still available.
With nth it is more subtle because of the extra argument. Primrec choses to let the unspecified value depend on the additional parameter (therefore "[] ! 42 = [] ! 43” will not be provable as “[] ! 42 = undefined 42” and “[] ! 43 = undefined 43” unless the element type is a singleton).
lemma "nth [] n = undefined n"
unfolding nth_def by simp
The “fun” command indeed makes a different choice (which would make "[] ! 42 = [] ! 43” and "[] ! 42 = undefined" true, if nth was defined using fun).
I think it depends on the application which choice is good or bad (the latter gives you “accidental" equalities such as "[] ! 42 = [] ! 43” or “hd [] = [] ! 43” which may raise some questions about your model but might eliminate some side conditions from lemmas). If you don’t like a particular choice you can always wrap the function in question to correct it.
Best wishes,
Dmitriy
On 20 Jul 2025, at 18.45, Elliot Bobrow <ebobrow@g.hmc.edu> wrote:
Hello Isabelle developers,
I've noticed that Isabelle's logic for case statements and fun definitions automatically defaults to returning undefined for unspecified inputs:
fun f :: "'a option \<Rightarrow> nat" where "f x = (case x of Some _ \<Rightarrow> 1)"
lemma "f None = undefined" by simp
fun f' :: "'a option \<Rightarrow> nat" where "f' (Some _) = 1"
lemma "f' None = undefined" by (meson f'.elims option.distinct(1))
However, the same does not hold for primrec definitions:
primrec (nonexhaustive) f'' :: "'a option \<Rightarrow> nat" where "f'' (Some _) = 0"
lemma "f'' None = undefined" oops
Is there a reason for this? It seems it would be good to be consistent here, and the functions would still be primitive recursive. Having undefined as a default case seems like a good idea for the sake of clarity and explicitness.
This has come up in a research project (collaborators CC'd) which involves proving a number of functions primitive recursive according to a user-defined predicate. We are doing this by constructing equivalent functions out of known primitive recursive functions and proving them equivalent on all inputs. However, it is impossible to do this for e.g. nth because an equivalent function must always return [] ! n for out-of-bounds inputs. This is a function of n and we do not know it to be primitive recursive, so we're stuck. If instead we had that [] ! n evaluates to undefined, the problem becomes trivial by returning the constant undefined on out-of-bounds inputs, which we know to be primitive recursive because it is a constant. This might not be the only instance where the current behavior makes it more difficult/impossible to reason about equality.
Elliot
Last updated: Aug 31 2025 at 20:21 UTC