Using an inverse value of an injective function

Question

I'm trying to prove this lemma:

lemma 
  assumes "x = inv f y" and "inj f" and "x ≠ undefined"
  shows "y ∈ range f"
  using assms try

But Nitpick tells me this statement is not true:

Trying "solve_direct", "quickcheck", "try0", "sledgehammer", and "nitpick"... 
Nitpick found a counterexample for card 'b = 3
and card 'a = 2:

  Free variables:
    f = (λx. _)(a1 := b1, a2 := b2)
    x = a2
    y = b3

Nitpick's counterexample assumes that y = b3 is not in the range of f. But in that case, how can there be an x = inv f b3 which is not undefined?

user_303637 · Answer

The value undefined is an arbitrary unknown value. You cannot use it do check that the result of a function is not defined. All functions in Isabelle are total.

If y is not in the range of f, then inv f y could be any value.

You could work around this by defining your own inverse function that uses an option type.

user_9716869 · Answer

peq has already provided a good answer. However, I would like to make several side remarks that you may find helpful (i.e. this is not an answer, but an addendum to peq's answer).

Generally, I am aware of two in-built convenience facilities in Isabelle/HOL for mimicking (technically, f::'a=>'b will always be a total function with the domain UNIV::'a set) functions with a restricted domain/codomain:

Tools in the theory Map that are accessible from the theory Main. These tools could supplement peq's suggestion for working with the type constructor option.
Tools in HOL-Library.FuncSet. These tools were developed around the idea of using undefined to "restrict" the domain/range of a function.

Following the second suggestion of using HOL-Library.FuncSet, for example, you could "restrict" inv to the range of the function. In this case, the theorem that you have stated can be proven under the restricted inverse:

theory Scratch
  imports 
    Main
    "HOL-Library.FuncSet"
begin

abbreviation inv' where "inv' f ≡ restrict (inv f) (range f)"

lemma 
  assumes "x = inv' f y" and "inj f" and "x ≠ undefined"
  shows "y ∈ range f"
  using assms unfolding restrict_def by meson

end

Note, however, that the theorem above is still not very useful as it implicitly omits the possibility that undefined = inv' f y when y is in the range of f.

Having tried both sets of tools that I mentioned above quite extensively, my personal opinion (not that you should assume that it carries any weight) is that often the simplest and the most natural solution is not to use them and merely provide additional assumptions that specify that the set (or particular values) upon which the function or its inverse must act are in the (desired) domain/range of the function.

Using an inverse value of an injective function

2 Answers