如何证明具有偏函数的引理？

Question

您能建议如何证明这个简单的引理吗？

datatype val = BVal bool | IVal int

lemma the_unif:
"the (x :: val option) = the (y :: val option) ⟹ x = y"
  apply (induct x; induct y)
  apply simp

我试图通过归纳来证明这一点，但我坚持使用案例 ⋀option. the None = the (Some option) ⟹ None = Some option。

option 可以等于BVal x 或IVal x。它永远不会等于the None。所以在这种情况下，假设总是有错误的价值。

更新：

我可以证明以下引理：

lemma the_none_ne_the_some:
  "x ≠ the None ⟹ the None ≠ the (Some x)"
  by simp

所以我想，第一个引理也可以被证明。

一般引理无法证明，因为它确实不成立：

lemma the_unif:
  "the x = the y ⟹ x = y"

反例：

x = None
y = Some (the None)

但在第一个引理中，x 和 y 都不能等于 Some (the None)。所以我找不到第一个引理的反例。

哦，我知道了，我可以证明以下引理：

lemma the_unif:
  "x ≠ Some (the None) ⟹ y ≠ Some (the None) ⟹ the x = the y ⟹ x = y"
  by (induct x; induct y; simp)

但是如何证明x :: val option 隐含x ≠ Some (the None)？

更新 2：

似乎无法证明：

lemma val_not_the_none:
  "x = BVal b ∨ x = IVal i ⟹ x ≠ the None"

但如果引理不成立，那么它们一定有反例吗？你能提供一个吗？

Answer 1

你试图证明的东西根本不成立。 the None 未指定 - 从本质上讲，没有什么不重要的事情可以证明。因此，说“它永远不会等于the None”是空洞的，因为你不知道the None 是什么。