关于元组的Isabelle/HOL问题

Question

关于伊莎贝尔/霍尔，我有一个初学者的问题：

我要证明以下引理：

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的变量，其中第二个x 影影为第一个。

实际上，{(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 ‹...›显式地引入空闲变量。