熟用Agda的Lean用户困惑：等式类型rfl失效的类型不匹配问题

你熟Agda，转Lean碰到的rfl时灵时不灵，本质是定义相等和命题相等的差异——Agda里refl能覆盖的场景，Lean里rfl只认最严格的定义相等。

你的HashSet例子为啥rfl用不了？ #

FV (Λ.var "x") == HashSet.ofList ["x"]求值返回true，是因为HashSet的==是外延相等：只要两个集合的元素完全一样，就判定相等。但rfl要求的是定义相等——两个表达式经过Lean的归约规则（β/ι/δ）后，底层结构完全一致。

Lean的HashSet是哈希表实现的，ofList ["x"]生成的集合，和FV (Λ.var "x")输出的集合，哪怕元素相同，底层的哈希桶分布、存储结构可能不一样，所以它们不是定义相等，rfl自然证不了。

该怎么证明这种相等？ #

别死磕rfl，用Lean给集合相等准备的工具：

• 用HashSet.ext引理：它的逻辑是“两个HashSet相等，当且仅当任意元素属于左边的同时也属于右边”
• 举个具体写法：

  theorem fv_var_x : FV (Λ.var "x") = HashSet.ofList ["x"] :=
  HashSet.ext (fun s => by
    simp [FV, Λ.var] -- 展开FV和var的定义，让Lean自动判断元素归属的等价性
  )
  

• 如果FV的定义就是直接生成包含变量的集合，甚至直接用simp就能把两边归约到可证明的状态，不用手动写太多。

最后补个Lean和Agda的相等差异 #

Agda的refl能通过rewrite、同余规则处理不少非定义相等的情况，但Lean的rfl是纯定义相等的判定工具，命题相等（=）大多需要靠引理、simp、rewrite这些手段来证明。

内容的提问来源于stack exchange，提问作者Joris KBos