使用单射函数的反值

Question

我试图证明这个引理：

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

但是 Nitpick 告诉我这个说法是不正确的：

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 的反例假设 y = b3 不在 f 的范围内。但是那样的话，怎么会有一个不是undefined的x = inv f b3呢？

Answer 1

值 undefined 是任意未知值。您不能使用它来检查函数的结果是否未定义。 Isabelle 中的所有功能都是完整的。

如果y不在f的范围内，那么inv f y可以是任意值。

您可以通过定义自己的使用选项类型的反函数来解决这个问题。

Answer 2

peq已经给出了很好的答案。但是，我想发表一些您可能会觉得有用的旁白（即这不是答案，而是 peq 答案的附录）。

一般来说，我知道 Isabelle/HOL 中有两个内置的便利工具用于模仿（从技术上讲，f::'a=>'b 将始终是域 UNIV::'a set 的总函数）函数受限制的 domain/codomain:

可从理论 Main 访问的理论 Map 中的工具。这些工具可以补充 peq 关于使用类型构造函数 option.
HOL-Library.FuncSet 中的工具。这些工具是围绕使用 undefined 到 "restrict" 函数的 domain/range 的想法开发的。

按照第二个建议使用HOL-Library.FuncSet，例如，您可以"restrict" inv到函数的范围。在这种情况下，你所说的定理可以在受限逆条件下得到证明：

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

但是请注意，上面的定理仍然不是很有用，因为它隐含地忽略了当 y 在 f 范围内时 undefined = inv' f y 的可能性。

在广泛尝试了我上面提到的两套工具之后，我个人的意见（并不是说你应该假设它们有任何重量）通常是最简单和最自然的解决方案是不使用它们，而只是提供额外的假设，指定函数或其反函数必须作用的集合（或特定值）在函数的（期望）domain/range 中。

使用单射函数的反值

Using an inverse value of an injective function

isabelle