Isabelle / HOL关于元组的问题

Question

我有一个关于Isabelle / HOL的初学者问题：

我想证明以下引理：

lemma 
  shows "{(x,y) . x ∈ {0..<n} ∧ y ∈ {0..<n} ∧ x = y} = {(x,x). x < n}"

但是证明状态是：

proof (prove)
goal (1 subgoal):
 1. {(x, y). x ∈ {0..<n} ∧ y ∈ {0..<n} ∧ x = y} = {(xa, x). x < n}

为什么xa出现，我如何以正确（简洁）的方式定义集合？

Answer 1

设定值(x,y)中的{(x,y). ....}为绑定变量名称。在编写{(x,x). x < n}时，您绑定了名为x的two变量，其中第二个x shadows第一个。

实际上，

{(x,x). x < n}只是lambda术语的一种很好的语法。在内部，它转换为Collect (case_prod (λx. λx. x < n))。以这种方式查看术语，阴影更明显。

要解决您的问题，您必须明确表示第一个和第二个绑定变量要相同的信息，即：{(x1,x2). x1 = x2 ∧ x1 < n}。

作为旁注：您试图展示的引理不是正确的。 （例如，n可能是int。）如果希望n成为nat，则必须明确指出这一点，例如，在目标中输入类似{(x,y). x ∈ {0..<(n::nat)} ∧ y ∈ {0..<n} ∧ x = y} = {(x1,x2). x1 = x2 ∧ x1 < n}的类型。

特别是，如果您是初学者，我强烈建议您使用语法lemma Name: fixes n :: ‹nat› assumes ‹...› shows ‹...›在引理头中明确引入自由变量。