主页 / coding / 问题 / 79577886
Accepted
Joris KBos
Asked: 2025-04-17 02:30:49 +0800 CST

Lean 4：Agda 用户难以理解 Lean 的相等类型、类型不匹配、不减少

  • 772

我对 Agda 很熟悉。我决定尝试一下 Lean，但我发现命题相等性真的让我很困扰。有时候我发现 rfl 能正常工作，但有时候却不行，原因我完全不明白，这真让人沮丧。举个例子：

inductive Λ where
  | var : String → Λ
  | app : Λ → Λ → Λ
  | abs : String → Λ → Λ
  deriving Repr, BEq, DecidableEq

def FV : Λ → HashSet String
  | Λ.var x => HashSet.ofList [x]
  | Λ.app m n  => FV m ∪ FV n
  | Λ.abs x m => (FV m).erase x
  
#eval FV (Λ.var "x")  -- Std.HashSet.ofList ["x"]
example : FV (Λ.var "x") = HashSet.ofList ["x"] := rfl  -- fine
example : (2 == 1 + 1) = true := rfl -- fine
#eval FV (Λ.var "x") == HashSet.ofList ["x"]  -- true
example : (FV (Λ.var "x") == HashSet.ofList ["x"]) = true := rfl
--type mismatch
--  rfl
--has type
--  ?m.9390 = ?m.9390 : Prop
--but is expected to have type
--  (FV (Λ.var "x") == HashSet.ofList ["x"]) = true : Prop

表达式的计算结果与预期一致，但在前两个例子中， rfl 运行良好，但在最后一个例子中却莫名其妙地不行，似乎没有减少 = 两边的项。我可以想象两个具有相同值的 HashSet 并不总是相等，因为它们可能最终位于不同的 bucket 中，但我不确定这是否是问题所在，因为它的计算结果似乎很好。

functional-programming

1 个回答

  1. Best Answer

    这里的问题与其说是相等类型，不如说是它#eval与核约简不同。许多复杂的定义虽然具有良好的计算特性（就生成高效代码而言），但它们在核中无法很好地约简，甚至根本无法约简。造成这种情况的主要原因之一是，定义在某种程度上依赖于合理的递归，而递归通常被标记为不可约，因此会阻碍核计算。在这种情况下，我怀疑HashSet.ofList函数及其==上的函数HashSet是导致核计算失败的原因。

    • 1

相关问题