Search code examples
isabelle

Using an inverse value of an injective function

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?

Solution

  • 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.