Hammers, SMT

Stream: general

[Bas Spitters]

What is the status of hammers (like sledgehammer) in lean? Development in Coq seems to be somewhat stalled, but there are some interesting datasets:
https://coq.discourse.group/t/coqhammer-1-1-1-for-coq-8-9/327/12
https://coq.discourse.group/t/machine-learning-and-hammers-for-coq/303

Chantal Keller is doing nice work with on safely importing SMT proofs into Coq, and she is defining her own intermediate format. Could the same be used for lean?
https://github.com/smtcoq/smtcoq

[Gabriel Ebner]

I've been working on a sledgehammer-like tool. Here are the slides from FoMM in January: https://gebner.org/pdfs/2020-01-08_fomm20_leanhammer.pdf

[Gabriel Ebner]

However due to performance issues, I don't think this will ever make it into Lean3/mathlib. Any future work will happen in Lean 4.

[Bas Spitters]

Nice! How much of this can be modularized? You don't seem to be using any parts of sledgehammer, coqhammer, deephol, ...
BTW did you look at easycrypt? It uses why3 as an intermediate, and is quite pleasant to use.

[Gabriel Ebner]

No, everything I've had for FoMM is homegrown. Since then, I've hooked up the relevance filter from CoqHammer (because it's pretty generic and written in C++, which is nice since Lean is also C++). But in my tests it didn't perform any better than the dumb filters I was using before.

[Gabriel Ebner]

I don't think it makes sense to reuse translations at all. It's pretty short and straightforward code, but it depends very much on the logic of the proof assistant.

[Gabriel Ebner]

I didn't know about easycrypt. I'll take a look but it seems extremely specific ("reasoning about relational properties of probabilistic computations with adversarial code").

[Bas Spitters]

What are the relevant differences between classical Coq, isabelle and lean?

[Bas Spitters]

Easycrypt has an ambient logic: Classical HOL. There tactic language is ssr with an smt tactic. The libraries are fairly close copies of math-comp.

[Bas Spitters]

They have more rewriting build in than Coq.

[Gabriel Ebner]

Isabelle is very much different from the other two: the logic is simply-typed lambda calculus, which is much weaker than the type theories of Lean and Coq, and also much closer to what external provers expect. Additionally, type classes in Isabelle are much more restricted than in Lean: they are coherent, which means that there is a unique instance per type. Hence you just need predicates for type classes that say which type has a type class, and you can e.g. write add(a,b) for addition (in a sound translation). In Lean and Coq, you can have multiple implementations of addition for a type so you might need to carry around an additional argument that says which type class instance you use.

[Gabriel Ebner]

The differences between Lean and Coq are smaller. Coq has more syntactic features that you need to encode: in a addition to lambdas, they also have fixpoints and match expressions. On the other hand, Lean makes an auxiliary definitions if you write a match, and also adds equational lemmas that hide the actual implementation as recursors. You typically don't want to definitionally unfold the auxiliary definition, and only use the equational lemmas.

[Bas Spitters]

Thanks. I understood you translated lean to HOL (as in your slides). From that point on, one could imagine that similar tools could be used as for isabelle and easycrypt.
F* of course is another data point. However, I understand that the translation they are doing to smt solvers is not really well understood.