Estou bastante confortável com o Agda. Decidi experimentar o Lean, mas acho que a igualdade proposicional está realmente me atrapalhando. Às vezes, acho que o RFL simplesmente funciona, mas outras vezes não, por razões que me escapam completamente, o que é bastante frustrante. Para dar um exemplo:
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
As expressões são avaliadas conforme o esperado, mas nos dois primeiros exemplos, rfl funciona perfeitamente, mas no último, misteriosamente, não funciona, aparentemente sem reduzir os termos em ambos os lados de = . Eu poderia imaginar dois HashSets com os mesmos valores nem sempre sendo iguais, pois poderiam ter acabado em grupos diferentes, mas não tenho certeza se esse é o problema, porque parece ser avaliado perfeitamente.
O problema aqui não é tanto o tipo de igualdade, mas o fato de que
#evalnão é o mesmo que redução de kernel, e muitas definições complexas são feitas de tal forma que, embora tenham boas propriedades computacionais (no sentido de produzir código eficiente), não reduzem bem no kernel ou não reduzem de forma alguma. Uma das principais causas para isso é que a definição depende de alguma forma de uma recursão bem fundamentada, que geralmente é marcada como irredutível e, portanto, bloqueará a computação do kernel. Nesse caso, eu suspeitaria que aHashSet.ofListfunção e a==função onHashSetseriam a razão para a falha na computação no kernel.